AlgEquiv.apply_symm_apply
theorem AlgEquiv.apply_symm_apply :
∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁]
[inst_2 : Semiring A₂] [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₂),
e (e.symm x) = x
The theorem `AlgEquiv.apply_symm_apply` states that for any commutative semiring `R` and any two algebras `A₁` and `A₂` over `R`, and for any algebra equivalence `e` from `A₁` to `A₂` and any element `x` in `A₂`, applying the equivalence `e` to the result of applying the inverse of `e` (given by `AlgEquiv.symm e`) to `x` yields `x` itself. In other words, it states that applying an algebra equivalence and its inverse to an element in succession is the same as doing nothing, which is a fundamental property of any kind of equivalence.
More concisely: For any commutative semiring `R`, algebra equivalences `e` between commutative `R`-algebras `A₁` and `A₂`, and elements `x` in `A₂`, we have `e (AlgEquiv.symm e x) = x`.
|
AlgEquiv.symm_apply_apply
theorem AlgEquiv.symm_apply_apply :
∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁]
[inst_2 : Semiring A₂] [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (x : A₁),
e.symm (e x) = x
The theorem `AlgEquiv.symm_apply_apply` states that for any commutative semiring `R`, and any two semirings `A₁` and `A₂` over `R`, if we have an algebra equivalence `e` from `A₁` to `A₂`, then for any element `x` in `A₁`, applying `e` to `x`, and then applying the inverse of `e` (obtained from `AlgEquiv.symm e`) to the result, we get back `x`. This essentially says that the inverse of an algebra equivalence is its right-inverse, i.e., applying the function and then its inverse gives you the original element.
More concisely: For any commutative semiring `R` and algebra equivalences `e: A₁ ≃₁ A₂` between commutative semirings `A₁` and `A₂` over `R`, we have `e (x) = e⁻¹ (e x)` for all `x` in `A₁`.
|
AlgEquiv.ext
theorem AlgEquiv.ext :
∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁]
[inst_2 : Semiring A₂] [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] {f g : A₁ ≃ₐ[R] A₂},
(∀ (a : A₁), f a = g a) → f = g
This theorem, `AlgEquiv.ext`, states that for any commutative semiring `R` and any two semirings `A₁` and `A₂`, along with the algebra structure over them, if two algebraic equivalences `f` and `g` from `A₁` to `A₂` over `R` are such that their effects on any element `a` from `A₁` are identical (i.e., `f a = g a` for all `a` in `A₁`), then `f` and `g` are the same algebraic equivalence. This theorem is a declaration of the extensionality principle for algebraic equivalences.
More concisely: If two algebraic equivalences over a commutative semiring from one semiring to another have identical effects on all elements, they are equal.
|
AlgEquivClass.commutes
theorem AlgEquivClass.commutes :
∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)}
[inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B]
[inst_5 : EquivLike F A B] [self : AlgEquivClass F R A B] (f : F) (r : R),
f ((algebraMap R A) r) = (algebraMap R B) r
The theorem `AlgEquivClass.commutes` states that for any types `F`, `R`, `A`, and `B`, given that `R` is a commutative semiring, `A` and `B` are semirings, and `A` and `B` are both `R`-algebras, and for any equivalence `F` between `A` and `B`, the action of scalars commutes with the equivalence. In other words, for any such equivalence `f` and any element `r` of the commutative semiring `R`, applying `f` to the result of mapping `r` into `A` through the algebra structure is the same as mapping `r` into `B` through its algebra structure. This affirms that the equivalence preserves the scalar multiplication operation of the algebra structure.
More concisely: For any commutative semiring `R`, `R-algebras` `A` and `B` with an equivalence `f` between them, the scalar multiplication commutes with `f`, i.e., for all `r ∈ R` and `a ∈ A`, `f(r * a) = r * f(a)`.
|
AlgEquiv.map_mul'
theorem AlgEquiv.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] (self : A ≃ₐ[R] B) (x y : A),
self.toFun (x * y) = self.toFun x * self.toFun y
This theorem states that for any commutative semiring `R`, and any two semirings `A` and `B`, if we have an algebra structure over `R` on both `A` and `B`, and if we have an algebra isomorphism (denoted by `A ≃ₐ[R] B`) `self` from `A` to `B`, then this isomorphism preserves multiplication. In other words, applying `self` to the product of `x` and `y` (both elements of `A`), where `x * y` denotes multiplication in `A`, is the same as the product of applying `self` to `x` and `y` separately, where `self.toFun x * self.toFun y` denotes multiplication in `B`.
More concisely: For any commutative semirings `R` and algebra structures over `R` on semirings `A` and `B` with an algebra isomorphism `A ≃ₐ[R] B`, the isomorphism preserves multiplication: `self (x * y) = self x * self y` for all `x, y` in `A`.
|
AlgEquiv.surjective
theorem AlgEquiv.surjective :
∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁]
[inst_2 : Semiring A₂] [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂),
Function.Surjective ⇑e
The theorem `AlgEquiv.surjective` states that for any commutative semiring `R` and any two semirings `A₁` and `A₂` with a structure of `R`-algebra, every algebraic equivalence `e` between `A₁` and `A₂` is a surjective function. In other words, for every element in the semiring `A₂`, there exists an element in the semiring `A₁` such that the application of the equivalence `e` on the element of `A₁` will yield the corresponding element in `A₂`.
More concisely: For every commutative semiring `R`, and `R`-algebras `A₁` and `A₂` with an algebraic equivalence `e` between them, `e` is a surjective function.
|
AlgEquiv.comp_symm
theorem AlgEquiv.comp_symm :
∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁]
[inst_2 : Semiring A₂] [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂),
(↑e).comp ↑e.symm = AlgHom.id R A₂
The theorem `AlgEquiv.comp_symm` states that for all commutative semirings `R` and semirings `A₁` and `A₂` that are also `R`-algebras, if there is an algebraic equivalence `e` between `A₁` and `A₂`, then the composition of `e` and its inverse (or symmetric) is equal to the identity function on `A₂`. In other words, applying an algebraic equivalence and its inverse in succession results in the original element in the algebra `A₂`, just as we would expect with any function and its inverse.
More concisely: Given a commutative semiring `R`, `R-algebras` `A₁` and `A₂`, and an algebraic equivalence `e` between them, `e` and `e⁻¹` are mutually inverse. Hence, `e ∘ e⁻¹ = id A₂`.
|
AlgEquiv.coe_ringHom_commutes
theorem AlgEquiv.coe_ringHom_commutes :
∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁]
[inst_2 : Semiring A₂] [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), ↑↑e = ↑↑e
The theorem `AlgEquiv.coe_ringHom_commutes` states that for any commutative semiring `R` and two semirings `A₁` and `A₂`, given that `A₁` and `A₂` are both algebras over `R`, the double coercion of any algebra isomorphism `e` from `A₁` to `A₂` (viewed as a ring homomorphism) is itself. In other words, the process of double coercion doesn't change the algebra isomorphism `e`.
More concisely: Given any commutative semiring `R` and algebra isomorphisms `e : A₁ ≅ A₂` between commutative `R`-algebras `A₁` and `A₂`, the double application of the coercion function commutes with `e`, that is, `coe (A₂ : Type*) (coe (A₁ : Type*) e) = e`.
|
AlgEquiv.injective
theorem AlgEquiv.injective :
∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁]
[inst_2 : Semiring A₂] [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), Function.Injective ⇑e
The theorem `AlgEquiv.injective` states that for any commutative semiring `R` and semirings `A₁` and `A₂` with `R`-algebra structures, any algebra homomorphism `e` between `A₁` and `A₂` is injective. In other words, if `e` is an algebra homomorphism and `e(x) = e(y)` for some elements `x` and `y` in `A₁`, then `x = y`.
More concisely: For any commutative semirings `R`, and `R`-algebra structures on semirings `A₁` and `A₂`, an `R`-algebra homomorphism `e` between `A₁` and `A₂` is injective.
|
AlgEquiv.commutes
theorem AlgEquiv.commutes :
∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁]
[inst_2 : Semiring A₂] [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (r : R),
e ((algebraMap R A₁) r) = (algebraMap R A₂) r
The theorem `AlgEquiv.commutes` asserts that for all commutative semirings `R`, semirings `A₁` and `A₂`, and algebra structures on `R` with `A₁` and `A₂`, an algebra isomorphism `e` from `A₁` to `A₂` over `R` commutes with the algebra maps from `R` to `A₁` and `A₂`. In other words, for any element `r` of `R`, applying `e` after the algebra map from `R` to `A₁` is the same as applying the algebra map from `R` to `A₂` directly. This property is also known as "the compatibility of algebra isomorphisms with scalar multiplication".
More concisely: For any commutative semirings R, algebra structures on R with semirings A₁ and A₂, and an algebra isomorphism e from A₁ to A₂, e commutes with the algebra maps from R to A₁ and A₂, i.e., for all r in R, e (r *\_A₁ x) = r *\_A₂ (e x), where *\_A₁ and *\_A₂ denote multiplication in the respective algebra structures.
|
AlgEquiv.symm_comp
theorem AlgEquiv.symm_comp :
∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁]
[inst_2 : Semiring A₂] [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂),
(↑e.symm).comp ↑e = AlgHom.id R A₁
This theorem states that for any commutative semiring `R` and semirings `A₁` and `A₂` over `R` that also possess algebra structures, and for any algebra equivalence `e` from `A₁` to `A₂`, if you compose the algebra homomorphism corresponding to the inverse of `e` with the algebra homomorphism corresponding to `e`, you will get the identity algebra homomorphism on `A₁`. This is the algebraic version of the fact that applying a function followed by its inverse gives you the original input back, or formally, for a function `f` and its inverse `f⁻¹`, `f⁻¹(f(x)) = x` for all `x` in the domain of `f`.
More concisely: For any commutative semirings `R` with algebra structures `A₁` and `A₂` over `R`, and an algebra equivalence `e` from `A₁` to `A₂`, the composition of `e.algebraMap.inv` and `e.algebraMap` is the identity algebra homomorphism on `A₁`.
|
AlgEquiv.symm_symm
theorem AlgEquiv.symm_symm :
∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁]
[inst_2 : Semiring A₂] [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), e.symm.symm = e
The theorem `AlgEquiv.symm_symm` states that for any types `R`, `A₁`, and `A₂` where `R` is a commutative semiring, `A₁` and `A₂` are semirings, and `A₁` and `A₂` are algebras over `R`, for any algebra equivalence `e` from `A₁` to `A₂`, the algebra equivalence that is the result of applying the function `AlgEquiv.symm` twice to `e` is equal to `e` itself. In simpler terms, taking the 'symmetric' or 'inverse' of an algebra equivalence twice gives you back the original equivalence.
More concisely: For any commutative semiring `R` and algebra equivalences `e`: (`AlgEquiv.symm `∘` `AlgEquiv.symm`) `e` = `e`, where `A₁`, `A₂` are semirings and algebras over `R`.
|
AlgEquiv.toLinearEquiv_apply
theorem AlgEquiv.toLinearEquiv_apply :
∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁]
[inst_2 : Semiring A₂] [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) (a : A₁),
e.toLinearEquiv a = e a
This theorem states that for any commutative semiring `R` and any two semirings `A₁` and `A₂` over `R`, if `e` is an algebra equivalence from `A₁` to `A₂`, then the application of the corresponding linear equivalence (obtained by forgetting the multiplicative structures in the algebra equivalence `e` through `AlgEquiv.toLinearEquiv`) to any element `a` of `A₁` is the same as the application of the algebra equivalence `e` to `a`. In other words, the algebra equivalence and the corresponding linear equivalence act identically on the elements of `A₁`.
More concisely: For any commutative semiring `R`, if `e` is an algebra equivalence from semirings `A₁` to `A₂` over `R`, then for all `a` in `A₁`, `e a = AlgEquiv.toLinearEquiv e a`.
|
AlgEquiv.map_add'
theorem AlgEquiv.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] (self : A ≃ₐ[R] B) (x y : A),
self.toFun (x + y) = self.toFun x + self.toFun y
This theorem states that for any given algebraic equivalence between two algebraic structures (A and B), with both structures being semirings over a common commutative semiring R, the function defined by this equivalence preserves the operation of addition. More specifically, for any two elements 'x' and 'y' in A, the image of the sum of 'x' and 'y' under this function is equal to the sum of the images of 'x' and 'y'. In other words, this function distributes over the addition operation.
More concisely: Given an algebraic equivalence between semirings A and B over a commutative semiring R, the function induced by the equivalence preserves addition: for all x, y in A, (f x + f y) = f (x + y), where f is the function induced by the equivalence.
|
AlgEquiv.commutes'
theorem AlgEquiv.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] (self : A ≃ₐ[R] B) (r : R),
self.toFun ((algebraMap R A) r) = (algebraMap R B) r
The theorem `AlgEquiv.commutes'` states that for any commutative semiring `R`, semirings `A` and `B`, an `R`-algebra structure on `A` and `B`, an `R`-algebra equivalence `self` from `A` to `B`, and any scalar `r` from `R`, the action of `r` on `A` (through the `algebraMap` from `R` to `A`) followed by the application of the algebra equivalence `self`, is the same as the direct action of `r` on `B` (through the `algebraMap` from `R` to `B`). In other words, scalar multiplication commutes with the algebra equivalence.
More concisely: For any commutative semirings R, semirings A and B, R-algebra structures on A and B, R-algebra equivalence self from A to B, and scalar r from R, we have algebraMap (r : R) ⊤ (self x) = self (algebraMap (r : R) x) for all x : A.
|