AlgHom.comp_apply
theorem AlgHom.comp_apply :
∀ {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [inst : CommSemiring R] [inst_1 : Semiring A]
[inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
(φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B) (p : A), (φ₁.comp φ₂) p = φ₁ (φ₂ p)
The theorem `AlgHom.comp_apply` states that for any commutative semiring `R` and semirings `A`, `B`, and `C` with `R`-algebra structures, given two algebra homomorphisms `φ₁` from `B` to `C` and `φ₂` from `A` to `B`, and an element `p` of `A`, the result of applying the composition of `φ₁` and `φ₂` to `p` is the same as applying `φ₁` to the result of applying `φ₂` to `p`. This expresses the property that the composition of algebra homomorphisms is associative, aligning with the intuition from function composition in general.
More concisely: For commutative semirings `R`, `A`, `B`, `C` with `R`-algebra structures, and algebra homomorphisms `φ₁: B → C` and `φ₂: A → B`, `φ₁ ∘ φ₂ (p) = φ₁ (φ₂ (p))` for all `p` in `A`.
|
AlgHom.id_comp
theorem AlgHom.id_comp :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B), (AlgHom.id R B).comp φ = φ
The theorem `AlgHom.id_comp` states that for any commutative semiring `R`, semirings `A` and `B`, and algebra structures over `R` on `A` and `B`, the composition of the identity algebra homomorphism on `B` and any algebra homomorphism `φ` from `A` to `B` is equivalent to `φ` itself. In other words, when an algebra homomorphism is followed by the identity operation, it doesn't change the original algebra homomorphism, which mirrors the mathematical concept that applying identity function to any function leaves the function unchanged.
More concisely: For any commutative semirings R, semirings A and B, and algebra structures over R on A and B, the composition of the identity algebra homomorphism on B and any algebra homomorphism from A to B is equal to the algebra homomorphism itself.
|
AlgHom.ext
theorem AlgHom.ext :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] {φ₁ φ₂ : A →ₐ[R] B}, (∀ (x : A), φ₁ x = φ₂ x) → φ₁ = φ₂
This theorem states that for any commutative semiring `R`, for any semirings `A` and `B`, and given that `A` and `B` are `R`-algebras, if we have two algebra homomorphisms `φ₁` and `φ₂` from `A` to `B`, and for all elements `x` in `A`, `φ₁ x` equals `φ₂ x`, then the two homomorphisms `φ₁` and `φ₂` are identical. In other words, two algebra homomorphisms between the same pair of `R`-algebras are equal if they map every element of the domain to the same element in the codomain.
More concisely: If `R` is a commutative semiring, `A` and `B` are `R`-algebras, and `φ₁` and `φ₂` are homomorphisms from `A` to `B` such that `φ₁ x = φ₂ x` for all `x` in `A`, then `φ₁ = φ₂`.
|
AlgHom.map_sub
theorem AlgHom.map_sub :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Ring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B) (x y : A), φ (x - y) = φ x - φ y
This theorem, `AlgHom.map_sub`, asserts that for all types `R`, `A`, and `B` where `R` is a commutative semiring, `A` and `B` are rings, and `A` and `B` are both `R`-algebras, if you have an algebra homomorphism `φ` from `A` to `B` and any two elements `x` and `y` of `A`, then applying `φ` to the difference `x - y` is the same as the difference of `φ(x)` and `φ(y)`. In mathematical terms, it states that algebra homomorphisms preserve subtraction.
More concisely: For commutative semirings R, and R-algebras A and B that are rings, any algebra homomorphism φ from A to B satisfies φ(x - y) = φ(x) - φ(y) for all x, y in A.
|
AlgHom.comp_id
theorem AlgHom.comp_id :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B), φ.comp (AlgHom.id R A) = φ
The theorem `AlgHom.comp_id` states that for any commutative semiring `R`, any semirings `A` and `B`, and any algebra structure over `A` and `B` with respect to `R`, if we have an algebra homomorphism `φ` from `A` to `B`, then the composition of `φ` with the identity map on `A` (using the function `AlgHom.comp`) is equal to `φ` itself. In other words, this expresses the mathematical idea that composing any map with the identity map leaves the map unchanged, in the context of algebra homomorphisms.
More concisely: For any commutative semiring `R`, any algebra homomorphisms `φ: A → B` over `R` from semirings `A` and `B`, `AlgHom.comp φ id_A = φ`.
|
AlgHom.map_sum
theorem AlgHom.map_sum :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B) {ι : Type u_1} (f : ι → A) (s : Finset ι),
φ (s.sum fun x => f x) = s.sum fun x => φ (f x)
The theorem `AlgHom.map_sum` states that for any commutative semiring `R`, semirings `A` and `B`, and algebras `A` and `B` over `R`, given an algebra homomorphism `φ` from `A` to `B`, a function `f` mapping elements of some type `ι` to `A`, and a finite set `s` of type `ι`, the homomorphism of the sum of the function `f` applied to each element in `s` is equal to the sum of the homomorphism of the function `f` applied to each element in `s`. In other words, the algebra homomorphism distributes over the sum of a finite set in `A`. This can be written in LaTeX as follows: for all φ, f and s, φ(∑_{x ∈ s} f(x)) = ∑_{x ∈ s} φ(f(x)).
More concisely: For any commutative semiring R, algebras A and B over R, algebra homomorphism φ from A to B, function f from some type ι to A, and finite set s of type ι, φ(∑x∈s f(x)) = ∑x∈s φ(f(x)).
|
AlgHom.comp_algebraMap
theorem AlgHom.comp_algebraMap :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B), (↑φ).comp (algebraMap R A) = algebraMap R B
This theorem states that for any commutative semiring `R`, semirings `A` and `B`, and any algebra structures over `R` on `A` and `B`, the composition of the ring homomorphism corresponding to an algebra homomorphism `φ` from `A` to `B` and the ring homomorphism embedding of `R` into `A` (given by the algebra structure) is equal to the ring homomorphism embedding of `R` into `B`. In other words, an algebra homomorphism preserves the structure of the ring homomorphism that maps the base ring into the algebra, showing the compatibility of the algebra homomorphism with the underlying ring structure.
More concisely: For any commutative semirings `R`, semirings `A` and `B`, and algebra structures over `R` on `A` and `B`, the algebra homomorphism `φ` from `A` to `B` preserves the ring homomorphism property, i.e., the composition of `φ` with the embedding of `R` into `A` is equal to the embedding of `R` into `B`.
|
AlgHom.map_smul
theorem AlgHom.map_smul :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B) (r : R) (x : A), φ (r • x) = r • φ x
This theorem states that for any commutative semiring `R`, semirings `A` and `B`, along with the algebra structures of `R` over `A` and `B`, a given algebra homomorphism `φ` from `A` to `B` preserves the action of scalars. Specifically, for any element `r` from `R` and `x` from `A`, applying the homomorphism `φ` to the scalar multiplication of `r` and `x` (`r • x`) is the same as first applying the homomorphism `φ` to `x` and then scaling by `r` (`r • φ x`). In other words, the algebra homomorphism `φ` commutes with the scalar multiplication operation.
More concisely: Given commutative semirings `R`, semirings `A` and `B`, algebra structures over `R` on `A` and `B`, and an algebra homomorphism `φ` from `A` to `B`, the scalar multiplication of `r` in `R` with `x` in `A` equals the scalar multiplication of `r` with `φ(x)` in `B`, for all `r` in `R` and `x` in `A`.
|
AlgHom.map_one
theorem AlgHom.map_one :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B), φ 1 = 1
This theorem states that for any commutative semiring `R`, and any semirings `A` and `B`, where `A` and `B` are `R`-algebras, any algebra homomorphism `φ` from `A` to `B` maps the multiplicative identity element `1` in `A` to the multiplicative identity element `1` in `B`. In simpler terms, it means that under an algebra homomorphism, the number `1` in the original algebra `A` will always be mapped to the number `1` in the target algebra `B`.
More concisely: For any commutative semirings `R`, and `R-algebra homomorphisms `φ` from `A` to `B` between `R-algebras` `A` and `B`, `φ(1_A) = 1_B`.
|
AlgHom.map_pow
theorem AlgHom.map_pow :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B) (x : A) (n : ℕ), φ (x ^ n) = φ x ^ n
This theorem states that for any commutative semiring `R`, semirings `A` and `B`, with `A` and `B` as algebras over `R`, and any algebra homomorphism `φ` from `A` to `B`, the image of the power of an element `x` from `A` under `φ`, is equal to the power of the image of `x` under `φ`. In other words, raising to the power `n` commutes with the algebra homomorphism `φ`. This is expressed as `φ (x ^ n) = φ x ^ n`.
More concisely: Given commutative semirings `R`, semirings `A` and `B`, with `A` and `B` as `R`-algebras and a homomorphism `φ` from `A` to `B`, the image of `φ` of `x^n` is equal to `(φ(x))^n` for any `x in A` and natural number `n`.
|
AlgHom.toLinearMap_injective
theorem AlgHom.toLinearMap_injective :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B], Function.Injective AlgHom.toLinearMap
The theorem `AlgHom.toLinearMap_injective` states that for any commutative semiring `R` and any two semirings `A` and `B` over `R`, the function `AlgHom.toLinearMap`, which converts an algebra homomorphism from `A` to `B` over `R` to a linear map, is injective. In other words, if two different algebra homomorphisms are mapped to the same linear map by `AlgHom.toLinearMap`, then those algebra homomorphisms were actually the same to begin with.
More concisely: If two algebra homomorphisms from commutative semirings over a common base ring map to the same linear map under `AlgHom.toLinearMap`, then they are equal as homomorphisms.
|
AlgHom.commutes
theorem AlgHom.commutes :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B) (r : R),
φ ((algebraMap R A) r) = (algebraMap R B) r
The theorem `AlgHom.commutes` states that for all commutative semirings `R` and semirings `A` and `B`, equipped with an algebra structure over `R`, and for every algebra homomorphism `φ` from `A` to `B`, the application of `φ` after mapping an element `r` from `R` to `A` via the `algebraMap` is the same as directly mapping the element `r` to `B` via the `algebraMap`. In other words, given any element in the base ring, the algebra homomorphism from `A` to `B` commutes with the algebra maps from `R` to `A` and `R` to `B`. This can be written in mathematical notation as `φ(algebraMap(R,A)(r)) = algebraMap(R,B)(r)` for all `r` in `R`.
More concisely: For every commutative semiring homomorphism φ between algebra structures over a commutative semiring R, and for all elements r in R, φ(α(r)) = α'(r), where α and α' denote the algebra maps from R to the respective algebra structures.
|
AlgHom.map_add
theorem AlgHom.map_add :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B) (r s : A), φ (r + s) = φ r + φ s
This theorem states that for any commutative semiring `R`, semiring `A`, and semiring `B`, given that `A` and `B` are `R`-algebras, an algebra homomorphism `φ` from `A` to `B` preserves addition. In other words, for any elements `r` and `s` in `A`, the image of the sum (`r + s`) under `φ` is the sum of the images (`φ r + φ s`). This is a property of algebra homomorphisms, which must preserve both the algebraic structure (operation-preserving) and the scalar multiplication.
More concisely: Given commutative semirings `R`, semirings `A` and `B`, and an `R`-algebra homomorphism `φ` from `A` to `B`, for all elements `r` and `s` in `A`, we have `φ(r + s) = φ(r) + φ(s)`.
|
AlgHom.map_zero
theorem AlgHom.map_zero :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B), φ 0 = 0
This theorem states that for any commutative semiring `R`, semirings `A` and `B`, with `A` and `B` as `R`-algebras, and any algebra homomorphism `φ` from `A` to `B`, the image of the zero element of `A` under `φ` is the zero element of `B`. In other words, an algebra homomorphism always maps the zero element to the zero element.
More concisely: Given commutative semirings `R`, `A`, and `B` with `A` and `B` as `R`-algebras, and an algebra homomorphism `φ` from `A` to `B`, the image of the additive identity of `A` under `φ` is the additive identity of `B`.
|
AlgHom.map_mul
theorem AlgHom.map_mul :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B) (x y : A), φ (x * y) = φ x * φ y
This theorem states that for any commutative semiring `R` and any two semirings `A` and `B`, given an algebra structure over `R` on `A` and `B`, for any algebra homomorphism `φ` from `A` to `B` over `R`, the image of the product of two elements `x` and `y` in `A` under `φ` is equal to the product of the images of `x` and `y` under `φ`. This is a statement about the homomorphism preserving multiplication.
More concisely: For any commutative semiring `R`, algebra structures over `R` on semirings `A` and `B`, and algebra homomorphism `φ` from `A` to `B` over `R`, the image of the product of elements `x` and `y` in `A` under `φ` equals the product of the images of `x` and `y` in `B`.
|
AlgHom.coe_ringHom_injective
theorem AlgHom.coe_ringHom_injective :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B], Function.Injective RingHomClass.toRingHom
The theorem `AlgHom.coe_ringHom_injective` states that for any commutative semiring `R`, semirings `A` and `B`, and algebraic structures over `R` on `A` and `B`, the function `RingHomClass.toRingHom` is injective. This injectiveness means that if two elements of the type `F` satisfying `RingHomClass F α β` are mapped to the same ring homomorphism by `RingHomClass.toRingHom`, then those two elements were the same to begin with.
More concisely: The `RingHomClass.toRingHom` function maps distinct ring homomorphisms from a commutative semiring `R` to algebraic structures over `R` in `A` and `B` to distinct homomorphisms.
|
AlgHom.map_neg
theorem AlgHom.map_neg :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Ring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B) (x : A), φ (-x) = -φ x
This theorem states that for any types `R`, `A`, `B`, where `R` is a Commutative Semiring, `A` and `B` are Rings, and both `A` and `B` are `R`-algebras, any algebra homomorphism `φ` from `A` to `B` preserves the negation operation. That is, applying `φ` to the negative of an element `x` in `A` gives the same result as first applying `φ` to `x` and then taking the negative of the result. In mathematical terms, for any `x` in `A`, `φ(-x) = -φ(x)`.
More concisely: For any commutative semiring `R`, and `R`-algebras `A` and `B` that are rings, any algebra homomorphism `φ` from `A` to `B` satisfies `φ(-x) = -φ(x)` for all `x` in `A`.
|
AlgHom.ext_iff
theorem AlgHom.ext_iff :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] {φ₁ φ₂ : A →ₐ[R] B}, φ₁ = φ₂ ↔ ∀ (x : A), φ₁ x = φ₂ x
This theorem states that for any commutative semiring `R`, semirings `A` and `B`, with `A` and `B` being `R`-algebras, two algebra homomorphisms `φ₁` and `φ₂` from `A` to `B` are equal if and only if they map every element of `A` to the same element in `B`. In other words, two algebra homomorphisms are identical if they behave identically for every element in their domain.
More concisely: Two `R`-algebra homomorphisms from a commutative semiring `A` to a commutative semiring `B` are equal if and only if they map every element of `A` to the same element in `B`.
|
Algebra.ext_id
theorem Algebra.ext_id :
∀ {R : Type u} (A : Type v) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (f g : R →ₐ[R] A),
f = g
This theorem, `Algebra.ext_id`, states that for any given type `R` and `A`, where `R` is a commutative semiring and `A` is a semiring that also forms an algebra over `R`, for any two algebra homomorphisms `f` and `g` from `R` to `A`, `f` is equal to `g`. In other words, it asserts the uniqueness of algebra homomorphisms between two specific algebraic structures.
More concisely: If `R` is a commutative semiring and `A` is an `R`-algebra, any two algebra homomorphisms from `R` to `A` are equal.
|
AlgHom.congr_fun
theorem AlgHom.congr_fun :
∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
[inst_3 : Algebra R A] [inst_4 : Algebra R B] {φ₁ φ₂ : A →ₐ[R] B}, φ₁ = φ₂ → ∀ (x : A), φ₁ x = φ₂ x
This theorem states that for any two algebra homomorphisms `φ₁` and `φ₂` from a semiring `A` to another semiring `B` over a common commutative semiring `R`, if `φ₁` and `φ₂` are equal, then they map each element `x` in `A` to the same element in `B`. Essentially, if two algebra homomorphisms are the same, they behave the same way on every element in their domain.
More concisely: Given two algebra homomorphisms φ₁ and φ₂ from a semiring A to another semiring B over a common commutative semiring R, if φ₁ = φ₂, then ∀x ∈ A, φ₁(x) = φ₂(x).
|