LinearEquiv.toLinearMap_injective
theorem LinearEquiv.toLinearMap_injective :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module S M₂] {σ : R →+* S}
{σ' : S →+* R} [inst_6 : RingHomInvPair σ σ'] [inst_7 : RingHomInvPair σ' σ],
Function.Injective LinearEquiv.toLinearMap
The theorem `LinearEquiv.toLinearMap_injective` states that for all semirings `R` and `S`, all additive commutative monoids `M` and `M₂`, and all modules over `R` and `S`, the function `LinearEquiv.toLinearMap` is injective. This implies that if two linear equivalences have the same corresponding linear map, then those two linear equivalences are the same. The injective property ensures uniqueness: it guarantees that we won't have two different linear equivalences that give rise to the same linear map. This works under the conditions that `σ : R →+* S` and `σ' : S →+* R` form a pair of inverse ring homomorphisms.
More concisely: For every semiring homomorphism `σ : R →+* S` and modules `M` over `R` and `N` over `S`, the induced linear map from a linear equivalence `φ : M ≅ N` is unique.
|
LinearEquiv.map_smul
theorem LinearEquiv.map_smul :
∀ {R₁ : Type u_2} {N₁ : Type u_11} {N₂ : Type u_12} [inst : Semiring R₁] [inst_1 : AddCommMonoid N₁]
[inst_2 : AddCommMonoid N₂] {module_N₁ : Module R₁ N₁} {module_N₂ : Module R₁ N₂} (e : N₁ ≃ₗ[R₁] N₂) (c : R₁)
(x : N₁), e (c • x) = c • e x
This theorem asserts that for any semiring `R₁`, and additive commutative monoids `N₁` and `N₂`, where `N₁` and `N₂` are `R₁`-modules, a linear equivalence `e` between `N₁` and `N₂` will preserve scalar multiplication. Specifically, for any scalar `c` in `R₁` and vector `x` in `N₁`, applying `e` to the result of scaling `x` by `c` (`e (c • x)`) is the same as scaling the result of applying `e` to `x` by `c` (`c • e x`). This property is a key characteristic of linear transformations.
More concisely: Given any semiring `R₁`, additive commutative monoids `N₁` and `N₂` as `R₁`-modules, and a linear equivalence `e` between `N₁` and `N₂`, for all `c in R₁` and `x in N₁`, we have `e (c • x) = c • e x`.
|
LinearEquiv.apply_symm_apply
theorem LinearEquiv.apply_symm_apply :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
{σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (c : M₂),
e (e.symm c) = c
This theorem, `LinearEquiv.apply_symm_apply`, states that for any semiring `R` and `S`, commutative additive monoid `M` and `M₂`, a module `M` over `R`, a module `M₂` over `S`, and two ring homomorphisms `σ: R →+* S` and `σ': S →+* R` that are inverses to each other, given a linear equivalence `e: M ≃ₛₗ[σ] M₂` and any element `c` from `M₂`, applying `e` on the result of applying the inverse of `e` on `c` will return `c`. This can be intuitively understood as reversing the transformation applied by `e` via its inverse and applying `e` again which will result in the original element `c`. Essentially, it is a way to express the property that the inverse of a linear equivalence undoes the mapping of the original linear equivalence.
More concisely: For any semirings R and S, commutative additive monoids M and M₂, modules M over R and M₂ over S, ring homomorphisms σ : R →+* S and σ' : S →+* R that are inverses, and a linear equivalence e : M ≃ₛₗ[σ] M₂, e (σ' (e (x))) = x for all x in M₂.
|
LinearEquiv.toAddMonoidHom_commutes
theorem LinearEquiv.toAddMonoidHom_commutes :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
{σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
e.toAddMonoidHom = e.toAddEquiv.toAddMonoidHom
This theorem states that for any linear equivalence `e` between two additive commutative monoids `M` and `M₂` (which are also modules over semirings `R` and `S` respectively), the two different ways of obtaining an `AddMonoidHom` from `e` yield the same result. More specifically, you can obtain an `AddMonoidHom` directly from `e` or first convert `e` to an `AddEquiv` and then to an `AddMonoidHom`, and these two methods are equivalent.
More concisely: For any linear equivalence between additive commutative monoids that are modules over semirings, the two ways of obtaining an additive monoid homomorphism yield the same result.
|
LinearEquiv.map_add
theorem LinearEquiv.map_add :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
{σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (a b : M),
e (a + b) = e a + e b
This theorem states that for any two elements `a` and `b` from a module `M` over a semiring `R`, the image of their sum under a linear equivalence `e` (a linear mapping that is bijective and thus invertible) to a module `M₂` over another semiring `S` is equal to the sum of the images of `a` and `b` under `e`. In other words, this theorem guarantees that a linear equivalence preserves the operation of addition from `M` to `M₂`.
More concisely: For any linear equivalence `e` between modules `M` and `M₂` over semirings `R` and `S` respectively, and for any elements `a` and `b` in `M`, we have `e(a + b) = e(a) + e(b)`.
|
LinearEquiv.map_zero
theorem LinearEquiv.map_zero :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
{σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂), e 0 = 0
This theorem states that for any linear equivalence `e` between two modules `M` and `M₂` over rings `R` and `S` respectively, the image of the zero element of `M` under `e` is the zero element of `M₂`. Here, the linear equivalence is defined with respect to two ring homomorphisms `σ` and `σ'` that form inverse pairs, i.e., the composition in each direction is the identity function on the respective ring.
More concisely: Given linear equivalences `e : M ≃ M₂` between modules `M` over ring `R` and `M₂` over ring `S`, and ring homomorphisms `σ : R → S` and `σ' : S → R` forming inverse pairs, the image of the zero element of `M` under `e` is the zero element of `M₂`.
|
LinearEquiv.symm_apply_eq
theorem LinearEquiv.symm_apply_eq :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
{σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) {x : M₂}
{y : M}, e.symm x = y ↔ x = e y
The theorem 'LinearEquiv.symm_apply_eq' states that for any two types 'M' and 'M₂' that are modules over the semirings 'R' and 'S' respectively, and given a linear equivalence 'e' from 'M' to 'M₂' with associated ring homomorphisms 'σ' and 'σ', for any elements 'x' of 'M₂' and 'y' of 'M', the inverse of 'e' applied to 'x' equals 'y' if and only if 'x' equals 'e' applied to 'y'.
More concisely: For linear equivalences $e : M \cong M'_s$ between $R$-modules $M$ and $S$-modules $M'_s$ with associated ring homomorphisms $\sigma : R \to S$ and $\sigma'_s : S \to R$, if $x \in M'_s$ and $y \in M$ satisfy $e(y) = x$, then $x = e(y)$.
|
LinearEquiv.toEquiv_injective
theorem LinearEquiv.toEquiv_injective :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module S M₂] {σ : R →+* S}
{σ' : S →+* R} [inst_6 : RingHomInvPair σ σ'] [inst_7 : RingHomInvPair σ' σ],
Function.Injective LinearEquiv.toEquiv
The theorem `LinearEquiv.toEquiv_injective` states that for any types `R`, `S`, `M`, and `M₂`, where `R` and `S` are semirings, `M` and `M₂` are additive commutative monoids, `M` is a module over `R`, `M₂` is a module over `S`, and there are two ring homomorphisms `σ: R →+* S` and `σ': S →+* R` that form a pair of inverse ring homomorphisms, the function `LinearEquiv.toEquiv` is injective. In other words, if two linear equivalences have the same underlying function equivalence, then they must be the same linear equivalence.
More concisely: If `σ: R →+* S` and `σ': S →+* R` are a pair of inverse ring homomorphisms between semirings `R` and `S`, and `LinearEquiv.toEquiv` maps two linear equivalences between modules `M` over `R` and `M₂` over `S` with the same underlying function equivalence, then these linear equivalences are equal.
|
LinearEquiv.symm_apply_apply
theorem LinearEquiv.symm_apply_apply :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
{σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (b : M),
e.symm (e b) = b
This theorem states that for any types `R`, `S`, `M`, and `M₂`, given that `R` and `S` are semirings, `M` and `M₂` are additive commutative monoids, `M` is a module over `R`, and `M₂` is a module over `S`, and given two ring homomorphisms `σ : R →+* S` and `σ' : S →+* R` that form a ring homomorphism inverse pair (both ways), for any linear equivalence `e : M ≃ₛₗ[σ] M₂` and any element `b` of type `M`, applying `e` to `b` and then applying the inverse of `e` to the result yields `b` again. In other words, a linear equivalence and its inverse form a 'round trip': applying one after the other gives you back where you started.
More concisely: Given two ring homomorphisms forming an inverse pair between semirings `R` and `S`, and modules `M` over `R`, `M₂` over `S`, any linear equivalence between `M` and `M₂` (as `R`-modules) satisfies applying the inverse of the equivalence to the equivalence of elements gives the original element.
|
LinearEquiv.bijective
theorem LinearEquiv.bijective :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
{σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
Function.Bijective ⇑e
The theorem `LinearEquiv.bijective` states that for any types `R`, `S`, `M`, and `M₂`, where `R` and `S` are semirings, `M` and `M₂` are additive commutative monoids, `M` is a module over `R`, `M₂` is a module over `S`, and `σ` and `σ'` form a pair of ring homomorphisms that are inverse to each other, any linear equivalence `e` between `M` and `M₂` (under the homomorphism `σ`) is a bijective function. In other words, every linear equivalence is an injective (one-to-one) and surjective (onto) function.
More concisely: Given semirings R and S, additive commutative monoids M and M₂, a module M over R, a module M₂ over S, ring homomorphisms σ : R -> S and σ' : S -> R that are inverses of each other, and a linear equivalence e between M and M₂ under σ, then e is a bijective function.
|
LinearEquiv.injective
theorem LinearEquiv.injective :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
{σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
Function.Injective ⇑e
The theorem `LinearEquiv.injective` states that for any semirings `R` and `S`, additive commutative monoids `M` and `M₂`, and provided `M` and `M₂` are modules over `R` and `S` respectively, if there exists a pair of ring homomorphisms `σ : R →+* S` and `σ' : S →+* R` that are inverses of each other, then any linear equivalence `e : M ≃ₛₗ[σ] M₂` is an injective function. In other words, if two elements from `M` are mapped to the same element in `M₂` by this linear equivalence, then the two original elements from `M` were actually the same.
More concisely: If `R` and `S` are semirings, `M` and `M₂` are additive commutative `R`-modules and `S`-modules respectively, and there exist invertive ring homomorphisms `σ : R → S` and `σ' : S → R`, then any linear equivalence `e : M ≈[σ] M₂` is an injective function.
|
LinearEquiv.left_inv
theorem LinearEquiv.left_inv :
∀ {R : Type u_16} {S : Type u_17} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {σ' : S →+* R}
[inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] {M : Type u_18} {M₂ : Type u_19}
[inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid M₂] [inst_6 : Module R M] [inst_7 : Module S M₂]
(self : M ≃ₛₗ[σ] M₂), Function.LeftInverse self.invFun self.toFun
This theorem states that for any semirings `R` and `S` with `σ` as a ring homomorphism from `R` to `S` and `σ'` as a ring homomorphism from `S` to `R` which form pairs of inverse ring homomorphisms, and any additive commutative monoids `M` and `M₂` which are also `R` and `S` modules respectively, for any linear equivalence `self` from `M` to `M₂` over `σ`, the inverse function `self.invFun` of the linear equivalence is a left inverse to the underlying function `self.toFun` of the linear equivalence. That is, applying `self.invFun` after applying `self.toFun` to any element in `M` returns the original element.
More concisely: For any ring homomorphisms σ: R -> S and σ': S -> R with inverse homomorphisms, and any additive commutative monoids M and M₂ that are R-modules and S-modules, respectively, any linear equivalence self from M to M₂ over σ satisfies self.invFun . self.toFun = id\_M.
|
SemilinearEquivClass.map_smulₛₗ
theorem SemilinearEquivClass.map_smulₛₗ :
∀ {F : Type u_16} {R : outParam (Type u_17)} {S : outParam (Type u_18)} [inst : Semiring R] [inst_1 : Semiring S]
{σ : outParam (R →+* S)} {σ' : outParam (S →+* R)} [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ]
{M : outParam (Type u_19)} {M₂ : outParam (Type u_20)} [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid M₂]
[inst_6 : Module R M] [inst_7 : Module S M₂] [inst_8 : EquivLike F M M₂] [self : SemilinearEquivClass F σ M M₂]
(f : F) (r : R) (x : M), f (r • x) = σ r • f x
This theorem states that for a semilinear equivalence `f` over a ring homomorphism `σ`, when `f` is applied to a scalar multiplication `r • x` (where `r` is a scalar and `x` is a vector), it is equal to the scalar multiplication `σ r • f x`. Here, `σ r` is the image of the scalar `r` under the ring homomorphism `σ`, `f` is the semilinear equivalence, and `x` is the vector. This result holds in the context of semirings `R` and `S`, and modules `M` and `M₂` over these semirings.
More concisely: For a semilinear equivalence $f$ over a ring homomorphism $\sigma$: $f(r \cdot x) = \sigma(r) \cdot f(x)$ for all scalars $r$ and vectors $x$, in the context of semirings $R$ and $S$, and modules $M$ and $M\_2$ over these semirings.
|
LinearEquiv.symm_symm
theorem LinearEquiv.symm_symm :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
{σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
e.symm.symm = e
This theorem states that for any two types `M` and `M₂` with associated semirings `R` and `S`, if they are equipped with addition-commutative monoid structures and module structures, and `σ` and `σ'` form a pair of inverse ring homomorphisms between `R` and `S`, then for any linear equivalence `e` between `M` and `M₂` under the ring homomorphism `σ`, the double application of the symmetry operation on `e` (i.e., applying symmetry twice in succession) will yield the original equivalence `e`. This means that the symmetry operation is its own inverse.
More concisely: Given types `M` and `M₂` with semirings `R` and `S`, equipped with addition-commutative monoid and module structures, and having ring homomorphisms `σ: R → S` and `σ': S → R` that form an inverse pair, any linear equivalence `e: M ≃ₐσ M₂` satisfies `e ∘ symmetry(e) = id`.
|
LinearEquiv.ext
theorem LinearEquiv.ext :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
{σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} {e e' : M ≃ₛₗ[σ] M₂},
(∀ (x : M), e x = e' x) → e = e'
This theorem, `LinearEquiv.ext`, states that for any two semirings `R` and `S`, two additive commutative monoids `M` and `M₂`, given `M` is a module over `R` and `M₂` is a module over `S`, two ring homomorphisms `σ` and `σ'` that form a pair of inverse ring homomorphisms `re₁` and `re₂`, and any two linear equivalences `e` and `e'` from `M` to `M₂` over the ring homomorphism `σ`, if for every element `x` in `M`, `e` of `x` equals `e'` of `x`, then `e` is identical to `e'`. In other words, two linear equivalences are considered the same if they map every element of `M` to the same element in `M₂` under the given ring homomorphism.
More concisely: Given two additive commutative semigroups `M` and `M₂`, two semigroup homomorphisms `σ: R → S` and `σ': S → R` forming a ring isomorphism, and two linear equivalences `e: M ≅ M₂` and `e': M ≅ M₂` over `σ`, if `e(x) = e'(x)` for all `x` in `M`, then `e = e'`.
|
LinearEquiv.map_smulₛₗ
theorem LinearEquiv.map_smulₛₗ :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
{σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) (c : R)
(x : M), e (c • x) = σ c • e x
This theorem states that for any semirings `R` and `S`, additive commutative monoids `M` and `M₂`, a module `M` over `R`, a module `M₂` over `S`, ring homomorphisms `σ : R →+* S` and `σ' : S →+* R` that form a ring homomorphism inverse pair, and a linear equivalence `e : M ≃ₛₗ[σ] M₂`, if we scale `x` in `M` by `c` in `R` and then apply the linear equivalence `e`, it's the same as applying the ring homomorphism `σ` to `c` and scaling `e(x)` by the result. In mathematical terms, it asserts that `e (c • x) = σ c • e x` for any `c` in `R` and `x` in `M`.
More concisely: For any semirings R and S, additive commutative monoids M and M₂, a module M over R, a module M₂ over S, ring homomorphisms σ : R →+* S and σ' : S →+* R forming a ring homomorphism inverse pair, and a linear equivalence e : M ≃ₛₗ[σ] M₂, we have e (cx) = σ(c) * e(x) for all c in R and x in M.
|
LinearEquiv.map_eq_zero_iff
theorem LinearEquiv.map_eq_zero_iff :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
{σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂) {x : M},
e x = 0 ↔ x = 0
This theorem states that for any semirings `R` and `S`, additive commutative monoids `M` and `M₂`, modules `M` over `R`, `M₂` over `S`, ring homomorphisms `σ` from `R` to `S` and `σ'` from `S` to `R` that form a pair of inverse ring homomorphisms `re₁` and `re₂`, and a linear equivalence `e` from `M` to `M₂` that respects these structures, an element `x` in `M` is mapped to the zero of `M₂` by `e` if and only if `x` is the zero of `M`. This implies that the linear equivalence `e` preserves the zero of the module.
More concisely: For any semirings R and S, additive commutative monoids M and M₂, modules M over R and M₂ over S, ring homomorphisms σ:R -> S and σ':S -> R that form a pair of inverse ring homomorphisms, and a linear equivalence e:M -> M₂ respecting these structures, e(x) = 0 in M₂ if and only if x = 0 in M.
|
LinearEquiv.surjective
theorem LinearEquiv.surjective :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
{σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂),
Function.Surjective ⇑e
The theorem `LinearEquiv.surjective` states that, for any semirings `R` and `S`, additive commutative monoids `M` and `M₂`, and any modules `M` over `R` and `M₂` over `S`, given any two ring homomorphisms `σ : R →+* S` and `σ' : S →+* R` such that `σ` and `σ'` form a ring homomorphism inverse pair both ways, and given a linear equivalence `e : M ≃ₛₗ[σ] M₂`, the function `e` is surjective. That is, for every element in `M₂`, there exists an element in `M` such that applying the linear equivalence to this element results in the element in `M₂`.
More concisely: Given any ring homomorphism inverse pair σ : R →+* S and σ' : S →+* R between semirings R and S, and a linear equivalence e : M ≃ₛₗ[σ] M₂ between additive commutative monoids M over R and M₂ over S, e is a surjection.
|
LinearEquiv.right_inv
theorem LinearEquiv.right_inv :
∀ {R : Type u_16} {S : Type u_17} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {σ' : S →+* R}
[inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] {M : Type u_18} {M₂ : Type u_19}
[inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid M₂] [inst_6 : Module R M] [inst_7 : Module S M₂]
(self : M ≃ₛₗ[σ] M₂), Function.RightInverse self.invFun self.toFun
The theorem `LinearEquiv.right_inv` states that for any semirings `R` and `S`, any ring homomorphisms `σ : R →+* S` and `σ' : S →+* R` that form an inverse pair, and any `R`-module `M` and `S`-module `M₂`, the inverse function of a linear equivalence from `M` to `M₂` (denoted by `self.invFun`) is a right inverse to the underlying function of the linear equivalence (denoted by `self.toFun`). In other words, applying `self.toFun` after `self.invFun` gives you the identity function on `M₂`. This is expressed formally as `Function.RightInverse self.invFun self.toFun`.
More concisely: Given any pair of inverse ring homomorphisms σ : R → S and σ' : S → R between semirings R and S, and any linear equivalences f : M ≃ M₂ between R-module M and S-module M₂, the inverse function g of f is a right inverse to f, i.e., f ∘ g = idM₂.
|