LinearMap.map_sub
theorem LinearMap.map_sub :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] {module_M : Module R M} {module_M₂ : Module S M₂}
{σ : R →+* S} (f : M →ₛₗ[σ] M₂) (x y : M), f (x - y) = f x - f y
The theorem `LinearMap.map_sub` states that for any two elements `x` and `y` of a module `M` over a semiring `R`, and a linear map `f` from `M` to another module `M₂` over a semiring `S`, the image of the difference `x - y` under `f` is equal to the difference of the images of `x` and `y`. In other words, the linear map `f` preserves subtraction. This holds under the condition that there exists a ring homomorphism from `R` to `S`.
More concisely: For any linear map $f$ between modules $M$ and $M\_2$ over semirings $R$ and $S$, respectively, with a ring homomorphism $h : R \rightarrow S$, we have $f(x - y) = f(x) - f(y)$ for all $x, y \in M$.
|
LinearMap.ext_iff
theorem LinearMap.ext_iff :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [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}
{f g : M →ₛₗ[σ] M₃}, f = g ↔ ∀ (x : M), f x = g x
This theorem states that for all semirings `R` and `S`, additive commutative monoids `M` and `M₃`, with `M` and `M₃` being modules over `R` and `S` respectively, and a ring homomorphism `σ` from `R` to `S`, two linear maps `f` and `g` from `M` to `M₃` are equal if and only if they produce the same output for all inputs `x` in `M`. In other words, two linear maps are identical if they behave the same way on all elements of the module `M`.
More concisely: For all semirings R and S, additive commutative monoids M and M₃, and ring homomorphisms σ from R to S, two linear maps f and g from M to M₃ are equal if and only if they agree on all elements of M.
|
LinearMap.CompatibleSMul.map_smul
theorem LinearMap.CompatibleSMul.map_smul :
∀ {M : Type u_9} {M₂ : Type u_11} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂] {R : Type u_17}
{S : Type u_18} [inst_2 : Semiring S] [inst_3 : SMul R M] [inst_4 : Module S M] [inst_5 : SMul R M₂]
[inst_6 : Module S M₂] [self : LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (c : R) (x : M),
fₗ (c • x) = c • fₗ x
This theorem states that for any two types `M` and `M₂` that are both additive commutative monoids, and for any two types `R` and `S` where `S` is a semiring and `R` and `S` each have scalar multiplication defined on `M` and `M₂`, if a linear map `fₗ` exists from `M` to `M₂` under the semiring `S`, then scalar multiplication by `R` can be moved through this linear map. In other words, for any scalar `c` of type `R` and any element `x` of type `M`, applying the linear map to the result of scaling `x` by `c` is equivalent to scaling the result of applying the linear map to `x` by `c`. This is expressed with the equation `fₗ (c • x) = c • fₗ x`.
More concisely: For any additive commutative monoids `M` and `M₂`, semiring `S` with scalar multiplication on `M` and `M₂`, and linear map `fₗ` from `M` to `M₂` under `S`, we have `fₗ (c • x) = c • fₗ x` for all scalars `c` in `R` and elements `x` in `M`.
|
LinearMap.ext_ring
theorem LinearMap.ext_ring :
∀ {R : Type u_1} {S : Type u_6} {M₃ : Type u_12} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M₃] [inst_3 : Module S M₃] {σ : R →+* S} {f g : R →ₛₗ[σ] M₃}, f 1 = g 1 → f = g
This theorem states that for any semirings `R` and `S`, a commutative additive monoid `M₃`, and a module `S` over `M₃`, if two `σ`-linear maps `f` and `g` from `R` to `M₃` are equal when applied to the multiplicative identity (1) of `R`, then those two `σ`-linear maps are identical. Essentially, this theorem is about the uniqueness of `σ`-linear maps when they share the same value at the multiplicative identity.
More concisely: If two `σ`-linear maps from a semiring to a commutative additive monoid, when applied to the multiplicative identity, yield the same result, then those maps are equal.
|
LinearMap.map_smul'
theorem LinearMap.map_smul' :
∀ {R : Type u_17} {S : Type u_18} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {M : Type u_19}
{M₂ : Type u_20} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M]
[inst_5 : Module S M₂] (self : M →ₛₗ[σ] M₂) (m : R) (x : M), self.toFun (m • x) = σ m • self.toFun x
This theorem states that for every semiring `R` and `S`, with a ring homomorphism `σ` from `R` to `S`, and every module `M` over `R` and `M₂` over `S`, any linear map from `M` to `M₂` is compatible with scalar multiplication. This means, in particular, that the linear map, when applied to the scalar multiplication of a scalar `m` from `R` and an element `x` from `M`, equals the scalar multiplication of the image of `m` under `σ` and the image of `x` under the linear map. Essentially, this theorem ensures the commutativity of the diagram involving scalar multiplication and the linear map.
More concisely: Given a semiring homomorphism σ from semiring R to semiring S, any linear map from an R-module M to an S-module M₂ commutes with scalar multiplication, that is, for all m in R and x in M, (σ(m) * M₂(x)) = M₂(m * x).
|
LinearMap.comp_apply
theorem LinearMap.comp_apply :
∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12}
[inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁]
[inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂}
{module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃}
[inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) (x : M₁),
(f.comp g) x = f (g x)
This theorem, `LinearMap.comp_apply`, states that for all semirings `R₁`, `R₂`, `R₃`, additive commutative monoids `M₁`, `M₂`, `M₃`, where `M₁` is a module over `R₁`, `M₂` is a module over `R₂`, and `M₃` is a module over `R₃`, along with ring homomorphisms `σ₁₂` from `R₁` to `R₂`, `σ₂₃` from `R₂` to `R₃`, and `σ₁₃` from `R₁` to `R₃` that satisfy the ring homomorphism composition triple condition, given two linear maps `f` from `M₂` to `M₃` and `g` from `M₁` to `M₂`, and an element `x` of `M₁`, the application of the composition of `f` and `g` to `x` is the same as first applying `g` to `x` and then applying `f` to the result. This corresponds to the standard mathematical concept of function composition in the context of linear maps and modules.
More concisely: For linear maps `f : M₂ → M₃` and `g : M₁ → M₂` between modules over semirings `R₁`, `R₂`, `R₃`, and ring homomorphisms `σ₁₂`, `σ₂₃`, `σ₁₃` satisfying the ring homomorphism composition condition, `f (g x) = g (σ₁₃ x) ∘ f` for all `x` in `M₁`.
|
LinearMap.comp_add
theorem LinearMap.comp_add :
∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_11} {M₃ : Type u_12}
[inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M]
[inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] [inst_6 : Module R₁ M] [inst_7 : Module R₂ M₂]
[inst_8 : Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃}
[inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f g : M →ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃),
h.comp (f + g) = h.comp f + h.comp g
This theorem, `LinearMap.comp_add`, states that for any three semirings R₁, R₂, and R₃ and any three additive commutative monoids M, M₂, and M₃ that are also R₁, R₂, and R₃-modules respectively, and for any three ring homomorphisms σ₁₂ from R₁ to R₂, σ₂₃ from R₂ to R₃, and σ₁₃ from R₁ to R₃ (which form a composition triple), the composition of a linear map h from M₂ to M₃ with the sum of two linear maps f and g from M to M₂ is the same as the sum of the composition of h with f and the composition of h with g. In simpler terms, this theorem asserts the distributivity of function composition over addition for linear maps, which is a fundamental property in linear algebra.
More concisely: For any semirings R₁, R₂, and R₃, and additive commutative monoids M, M₂, and M₃ that are R₁, R₂, and R₃-modules respectively, and for any ring homomorphisms σ₁₂, σ₂₃, and σ₁₃ between them forming a composition triple, the composition of a linear map h from M₂ to M₃ with the sum of two linear maps f and g from M to M₂ is equal to the sum of the compositions of h with f and h with g.
|
LinearMap.map_smulₛₗ
theorem LinearMap.map_smulₛₗ :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [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}
(f : M →ₛₗ[σ] M₃) (c : R) (x : M), f (c • x) = σ c • f x
This theorem states that for any semirings `R` and `S`, additive commutative monoids `M` and `M₃`, `R`-module `M`, `S`-module `M₃`, ring homomorphism `σ` from `R` to `S`, linear map `f` from `M` to `M₃`, scalar `c` from `R`, and element `x` from `M`, the result of applying `f` to the scalar multiplication of `c` and `x` (i.e., `f (c • x)`) is equal to the scalar multiplication of `σ c` and `f x` (i.e., `σ c • f x`). In other words, it's demonstrating that a linear map distributes over scalar multiplication, under the provided conditions.
More concisely: For any semirings R and S, additive commutative monoids M and M₃, R-module M, S-module M₃, ring homomorphism σ from R to S, and linear map f from M to M₃, the law f (c • x) = σ (c) • f (x) holds for all scalars c in R and elements x in M.
|
LinearMap.id_comp
theorem LinearMap.id_comp :
∀ {R₂ : Type u_3} {R₃ : Type u_4} {M₂ : Type u_11} {M₃ : Type u_12} [inst : Semiring R₂] [inst_1 : Semiring R₃]
[inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
{σ₂₃ : R₂ →+* R₃} (f : M₂ →ₛₗ[σ₂₃] M₃), LinearMap.id.comp f = f
The theorem `LinearMap.id_comp` states that for any semirings `R₂` and `R₃`, any additive commutative monoids `M₂` and `M₃`, any modules `M₂` and `M₃` over `R₂` and `R₃` respectively, and any ring homomorphism from `R₂` to `R₃` denoted by `σ₂₃`, if we have a linear map `f` from `M₂` to `M₃`, then the composition of the linear identity map and `f` (i.e., `LinearMap.comp LinearMap.id f`) is equal to `f` itself. In essence, this theorem asserts that the identity map composed with any linear map leaves the linear map unchanged, which is a fundamental property of identity maps in the context of linear algebra.
More concisely: For any ring homomorphism σ₂₃ between semirings R₂ and R₃, and any linear map f from an additive commutative monoid/module M₂ to M₃ over R₂/R₃, the composition of the identity linear map and f equals f itself.
|
LinearMap.ext
theorem LinearMap.ext :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [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}
{f g : M →ₛₗ[σ] M₃}, (∀ (x : M), f x = g x) → f = g
This theorem, `LinearMap.ext`, states that for any two linear maps `f` and `g` from a module `M` over a semiring `R` to a module `M₃` over a semiring `S` (with a ring homomorphism `σ` from `R` to `S`), if for every element `x` in `M` the mappings `f x` and `g x` are equal, then the two linear maps `f` and `g` are themselves equal. This is a statement about the uniqueness of linear maps in mathematical structure.
More concisely: If two linear maps from one module over a semiring to another module over a semiring, with a given ring homomorphism between the semirings, map every element to the same image, then the linear maps are equal.
|
LinearMap.map_smul
theorem LinearMap.map_smul :
∀ {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] (fₗ : M →ₗ[R] M₂) (c : R) (x : M),
fₗ (c • x) = c • fₗ x
This theorem, `LinearMap.map_smul`, states that for any semiring `R`, any add-commutative monoids `M` and `M₂`, and any modules over `R` for `M` and `M₂`, if `fₗ` is a linear map from `M` to `M₂`, then scaling an element `x` of `M` by a scalar `c` from `R` before applying `fₗ` is the same as applying `fₗ` to `x` first and then scaling the result by `c`. This property is a key characteristic of linear maps, and it can be written in mathematical notation as `fₗ(c • x) = c • fₗ(x)`.
More concisely: For any linear map `f` between modules over a semiring, `f(cx) = c(fx)`.
|
LinearMap.map_smul_of_tower
theorem LinearMap.map_smul_of_tower :
∀ {M : Type u_9} {M₂ : Type u_11} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂] {R : Type u_17}
{S : Type u_18} [inst_2 : Semiring S] [inst_3 : SMul R M] [inst_4 : Module S M] [inst_5 : SMul R M₂]
[inst_6 : Module S M₂] [inst_7 : LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (c : R) (x : M),
fₗ (c • x) = c • fₗ x
This theorem, `LinearMap.map_smul_of_tower`, states that given certain conditions, linear transformation respects the scalar multiplication on two modules. More specifically, it says that for any additively commutative monoids `M` and `M₂`, a semiring `S`, and a scalar multiplication operation `SMul` on `R`, if `M` and `M₂` are also modules over `S` and `SMul` behaves compatibly with certain linear maps from `M` to `M₂`, then for any linear map `fₗ` from `M` to `M₂` over semiring `S`, any scalar `c` of type `R`, and any element `x` of `M`, the image of the scaled element `c • x` under `fₗ` is the same as the scaled image of `x` under `fₗ`, i.e., `fₗ (c • x) = c • fₗ x`. This theorem essentially establishes the compatibility of the linear map with scalar multiplication.
More concisely: Given additively commutative monoids `M` and `M₂`, a semiring `S`, and a scalar multiplication `SMul` on `R`, if `M`, `M₂`, and `SMul` satisfy certain conditions, then for any linear map `fₗ` from `M` to `M₂` over semiring `S`, `fₗ (c • x) = c • fₗ x` for all scalars `c` of type `R` and elements `x` of `M`.
|
LinearMap.add_apply
theorem LinearMap.add_apply :
∀ {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [inst : Semiring R₁] [inst_1 : Semiring R₂]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R₁ M] [inst_5 : Module R₂ M₂]
{σ₁₂ : R₁ →+* R₂} (f g : M →ₛₗ[σ₁₂] M₂) (x : M), (f + g) x = f x + g x
The theorem `LinearMap.add_apply` states that for any two linear maps `f` and `g` from a module `M` over a semiring `R₁` to a module `M₂` over a semiring `R₂`, and any element `x` of `M`, the result of applying the sum of the two linear maps (i.e., `(f + g) x`) is the same as the sum of the results of applying each linear map separately to `x` (i.e., `f x + g x`). This is essentially saying that the sum of two linear maps behaves as expected with respect to map application.
More concisely: For any linear maps `f` and `g` from module `M` over semiring `R₁` to module `M₂` over semiring `R₂`, and any `x` in `M`, `(f + g) x = f x + g x`.
|
LinearMap.restrictScalars_injective
theorem LinearMap.restrictScalars_injective :
∀ (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R M₂]
[inst_6 : Module S M] [inst_7 : Module S M₂] [inst_8 : LinearMap.CompatibleSMul M M₂ R S],
Function.Injective ↑R
The theorem `LinearMap.restrictScalars_injective` states that for any type `R`, and given types `S`, `M`, and `M₂`, along with a host of conditions on these types (such as `R` and `S` being semirings, `M` and `M₂` being additive commutative monoids, `M` and `M₂` being `R`-modules and `S`-modules, and the compatibility of scalar multiplication on these modules), the function that maps an element from `R` to its corresponding element in the larger type space is injective. In other words, no two different elements in `R` would map to the same element in the larger type space, given these conditions.
More concisely: Given semirings R and S, additive commutative monoids and R-modules M and M₂, and S-modules M and M₂ with compatible scalar multiplications, the restriction of scalars map from R to M and from R to M₂ are injective.
|
LinearMap.isLinear
theorem LinearMap.isLinear :
∀ {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] (fₗ : M →ₗ[R] M₂), IsLinearMap R ⇑fₗ
This theorem states that for any semiring `R` and any two additive commutative monoids `M` and `M₂` over `R`, every linear map `fₗ` from `M` to `M₂` is a linear map in the sense of the `IsLinearMap` predicate. In more detail, if `M` and `M₂` are modules over `R`, and `fₗ` is a linear map from `M` to `M₂`, then `fₗ` satisfies the properties of additivity and scalar multiplication required to be a linear map according to the definition of `IsLinearMap`.
More concisely: For any semiring `R`, any additive commutative monoids `M` and `M₂` over `R`, and any linear map `f` from `M` to `M₂`, `f` is a linear map (satisfying additivity and scalar multiplication properties).
|
LinearMap.comp_id
theorem LinearMap.comp_id :
∀ {R₂ : Type u_3} {R₃ : Type u_4} {M₂ : Type u_11} {M₃ : Type u_12} [inst : Semiring R₂] [inst_1 : Semiring R₃]
[inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
{σ₂₃ : R₂ →+* R₃} (f : M₂ →ₛₗ[σ₂₃] M₃), f.comp LinearMap.id = f
The theorem `LinearMap.comp_id` states that for any semirings `R₂` and `R₃`, additive commutative monoids `M₂` and `M₃`, if `M₂` and `M₃` are modules over `R₂` and `R₃` respectively, and if `σ₂₃` is a ring homomorphism from `R₂` to `R₃`, then for any linear map `f` from `M₂` to `M₃` over `σ₂₃`, the composition of `f` with the identity map is equal to `f` itself. In other words, applying an identity transformation in the context of linear maps doesn't change the original linear map.
More concisely: For any ring homomorphism σ₂₃ from semiring R₂ to semiring R₃, and linear maps f : M₂ → M₃ over σ₂₃ from additive commutative monoids M₂ and M₃, the composition of f with the identity map is equal to f itself.
|
IsLinearMap.map_smul
theorem IsLinearMap.map_smul :
∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
[inst_3 : Module R M] [inst_4 : Module R M₂] {f : M → M₂},
IsLinearMap R f → ∀ (c : R) (x : M), f (c • x) = c • f x
The theorem `IsLinearMap.map_smul` states that for any semiring `R` and additively commutative monoids `M` and `M₂` that are also `R`-modules, for any linear map `f` from `M` to `M₂`, and for any scalar `c` in `R` and vector `x` in `M`, the result of applying `f` to the scalar multiplication of `c` and `x` is equal to the scalar multiplication of `c` and the result of applying `f` to `x`. In other words, a linear map preserves scalar multiplication: `f (c • x) = c • f x`.
More concisely: For any linear map $f$ between $R$-modules $M$ and $M\_2$ over a semiring $R$, and for any scalar $c$ in $R$ and vector $x$ in $M$, we have $f(c\cdot x) = c\cdot f(x)$.
|
Function.Surjective.injective_linearMapComp_right
theorem Function.Surjective.injective_linearMapComp_right :
∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12}
[inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁]
[inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂}
{module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃}
[inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {g : M₁ →ₛₗ[σ₁₂] M₂},
Function.Surjective ⇑g → Function.Injective fun f => f.comp g
The theorem `Function.Surjective.injective_linearMapComp_right` states that for given semirings `R₁`, `R₂`, and `R₃`, as well as additive commutative monoids `M₁`, `M₂`, and `M₃` over which `R₁`, `R₂`, and `R₃` act as scalars respectively, and the ring homomorphisms `σ₁₂` from `R₁` to `R₂`, `σ₂₃` from `R₂` to `R₃`, and `σ₁₃` from `R₁` to `R₃` that satisfy the ring homomorphism triple condition, if a linear map `g` from `M₁` to `M₂` (over `σ₁₂`) is surjective (every element in `M₂` is the image of some element in `M₁` under `g`), then the function that takes a linear map `f` and returns the composition of `f` and `g` is injective (different linear maps yield different composed maps), i.e., if `f₁.comp g = f₂.comp g`, then `f₁ = f₂`.
More concisely: If `g` is a surjective linear map from the additive commutative monoid `M₁` to `M₂` over semirings `R₁` and `R₂`, and `σ₁₂`, `σ₂₃`, and `σ₁₃` are ring homomorphisms satisfying the ring homomorphism triple condition, then the function that maps a linear map `f` from `M₁` to `M₃` to `f.comp g` is injective.
|
LinearMap.id_apply
theorem LinearMap.id_apply :
∀ {R : Type u_1} {M : Type u_9} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M),
LinearMap.id x = x
This theorem, `LinearMap.id_apply`, states that for any semiring `R` and additive commutative monoid `M` that is also a module over `R`, the identity linear map, when applied to any element `x` of `M`, simply returns `x`. In other words, the action of the identity linear map leaves every element of the module unchanged.
More concisely: For any semiring R and additive commutative monoid M that is an R-module, the identity linear map is the identity function on M.
|
IsLinearMap.map_add
theorem IsLinearMap.map_add :
∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
[inst_3 : Module R M] [inst_4 : Module R M₂] {f : M → M₂}, IsLinearMap R f → ∀ (x y : M), f (x + y) = f x + f y
This theorem states that linear maps preserve addition. Specifically, for any semiring `R`, additive commutative monoids `M` and `M₂`, if `M` and `M₂` are also `R`-modules and `f` is a linear map from `M` to `M₂`, then for any elements `x` and `y` in `M`, applying the map `f` to the sum of `x` and `y` is the same as summing the result of applying `f` to `x` and `f` to `y` separately. In mathematical terms, if `f` is a linear map, then `f( x + y) = f(x) + f(y)`.
More concisely: For any linear map `f` between additive commutative monoids `M` and `M₂` that are `R`-modules, `f(x + y) = f(x) + f(y)` for all `x, y` in `M`.
|
IsLinearMap.isLinearMap_neg
theorem IsLinearMap.isLinearMap_neg :
∀ {R : Type u_1} {M : Type u_9} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
IsLinearMap R fun z => -z
This theorem states that for any semiring `R` and any additive commutative group `M` that is also a `R`-module, the function that maps every element `z` of `M` to its negation is a linear map. In mathematical terms, if `M` is a module over the semiring `R`, then the function `f: M -> M` defined by `f(z) = -z` for all `z` in `M` is a linear map.
More concisely: The negation function on an additive commutative group `M` that is an `R`-module over a semiring `R` is a linear map.
|
LinearMap.zero_apply
theorem LinearMap.zero_apply :
∀ {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [inst : Semiring R₁] [inst_1 : Semiring R₂]
[inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R₁ M] [inst_5 : Module R₂ M₂]
{σ₁₂ : R₁ →+* R₂} (x : M), 0 x = 0
The theorem `LinearMap.zero_apply` states that for any types `R₁`, `R₂`, `M`, and `M₂` along with their respective semiring, module, and addition commutative monoid structures, and any ring homomorphism `σ₁₂` from `R₁` to `R₂`, applying the zero linear map to any element `x` from `M` yields zero. In mathematical terms, if we have a zero linear map from one module to another, then the image of any element under this map is the zero element of the second module.
More concisely: For any ring homomorphism σ₁₂ between semirings R₁ and R₂, and any zero linear map f : M → M₂ between modules M and M₂ over R₁ and R₂ respectively, we have f(x) = 0 for all x ∈ M.
|
LinearMap.map_add
theorem LinearMap.map_add :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [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}
(f : M →ₛₗ[σ] M₃) (x y : M), f (x + y) = f x + f y
This theorem states that for any two elements `x` and `y` of a certain module `M`, the linear map `f` preserves the addition operation. More formally, if `R` and `S` are semirings, `M` and `M₃` are additive commutative monoids, `M` is an `R`-module, `M₃` is an `S`-module, and `σ` is a ring homomorphism from `R` to `S`, then for any linear map `f` from `M` to `M₃` (with respect to `σ`), the image of the sum of `x` and `y` under `f` equals the sum of the images of `x` and `y` under `f`. This theorem is essentially the statement of one of the key properties of linear maps: they preserve the algebraic structure of their domain.
More concisely: For any linear map $f$ from an additive commutative monoid $M$ (over semirings $R$ and $S$, with a ring homomorphism $\sigma$ from $R$ to $S$) between an $R$-module $M$ and an $S$-module $M\_3$, the image of the sum of any two elements $x, y \in M$ under $f$ equals the sum of the images of $x$ and $y$ under $f$.
|
LinearMap.map_zero
theorem LinearMap.map_zero :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [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}
(f : M →ₛₗ[σ] M₃), f 0 = 0
This theorem states that for all semirings R and S, with additive commutative monoids M and M₃, and modules M over R and M₃ over S, and for a ring homomorphism σ from R to S, a linear map f from M to M₃ (preserving the structure of the module under the ring homomorphism σ) sends the zero vector of M to the zero vector of M₃. In other words, every linear map maps the zero vector from its domain to the zero vector in its codomain.
More concisely: For any semirings R and S, ring homomorphism σ from R to S, and linear maps f from an additive commutative M-module M to an S-module M₃, if f preserves the module structure under σ, then f maps the zero vector of M to the zero vector of M₃.
|
LinearMap.smul_apply
theorem LinearMap.smul_apply :
∀ {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [inst : Semiring R]
[inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M]
[inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst_6 : Monoid S] [inst_7 : DistribMulAction S M₂]
[inst_8 : SMulCommClass R₂ S M₂] (a : S) (f : M →ₛₗ[σ₁₂] M₂) (x : M), (a • f) x = a • f x
This theorem states that for any semirings `R` and `R₂`, an additive commutative monoid `M`, another additive commutative monoid `M₂`, a module `M` over `R`, a module `M₂` over `R₂`, a ring homomorphism `σ₁₂` from `R` to `R₂`, a monoid `S`, a distributive multiplication action of `S` on `M₂`, and a commutative multiplication action of `R₂` and `S` on `M₂`, given an element `a` from `S`, a linear map `f` from `M` to `M₂`, and an element `x` from `M`, the application of the scaled linear map `(a • f)` to `x` is equal to the scaled result of the linear map `f` applied to `x`. In mathematical terms, this can be written as `(a • f)(x) = a • f(x)`.
More concisely: For any semirings R and R₂, additive commutative monoids M and M₂, module M over R, module M₂ over R₂, ring homomorphism σ₁₂ from R to R₂, monoid S acting distributively on M₂, commutative action of R₂ and S on M₂, element a from S, linear map f from M to M₂, and element x from M, the scaled linear map (a • f) equals the scaled result of applying f to x, that is, (a • f)(x) = a • f(x).
|
LinearMap.map_neg
theorem LinearMap.map_neg :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
[inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] {module_M : Module R M} {module_M₂ : Module S M₂}
{σ : R →+* S} (f : M →ₛₗ[σ] M₂) (x : M), f (-x) = -f x
This theorem states that for any semirings `R` and `S`, any additive commutative groups `M` and `M₂`, any modules `M` over `R` and `M₂` over `S`, any ring homomorphism `σ` from `R` to `S`, any linear map `f` from `M` to `M₂` under the homomorphism `σ`, and any element `x` in `M`, the image of the negation of `x` under `f` is the negation of the image of `x` under `f`. This is a property of linear maps that connects them to the operation of negation in the underlying groups and modules.
More concisely: For any semirings R and S, additive commutative groups M and M₂, modules M over R and M₂ over S, ring homomorphism σ from R to S, linear map f from M to M₂, and element x in M, we have ∣∣f(−x)∣∣ = ∣∣−f(x)∣∣.
|
LinearMap.congr_fun
theorem LinearMap.congr_fun :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [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}
{f g : M →ₛₗ[σ] M₃}, f = g → ∀ (x : M), f x = g x
This theorem states that if two linear maps, 'f' and 'g', over semirings 'R' and 'S' and additive commutative monoids 'M' and 'M₃' are equal, then for each point 'x' in 'M', the result of mapping 'x' through 'f' and 'g' will be the same. The theorem applies to the situation where 'M' is a module over 'R', 'M₃' is a module over 'S', and 'σ' is a ring homomorphism from 'R' to 'S'.
More concisely: If two linear maps over semirings with additive commutative monoid structures, where one is a ring homomorphism between the semirings, equal maps between modules over the semirings, then they map identical elements to identical images.
|
LinearMap.coe_injective
theorem LinearMap.coe_injective :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [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},
Function.Injective DFunLike.coe
This theorem states that for any types `R`, `S`, `M`, and `M₃`, given `R` and `S` are semirings, `M` and `M₃` are additively commutative monoids, `M` is an `R`-module, `M₃` is an `S`-module, and `σ` is a ring homomorphism from `R` to `S`, the function that maps each `F` in the type `DFunLike F α β` to the corresponding function from `α` to `β` is injective. In other words, if two different objects of the type `DFunLike F α β` map to the same function from `α` to `β`, then the two objects were actually the same to begin with. This theorem is often used to prove results about the uniqueness of certain mathematical constructions.
More concisely: Given `R`, `S` semirings, `M` an additively commutative monoid and `R`-module, `M₃` an additively commutative monoid and `S`-module, and `σ: R → S` a ring homomorphism, the function mapping `DFunLike F α β` to their corresponding functions from `α` to `β` is an injection.
|
Function.Injective.injective_linearMapComp_left
theorem Function.Injective.injective_linearMapComp_left :
∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12}
[inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁]
[inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂}
{module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃}
[inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃},
Function.Injective ⇑f → Function.Injective fun g => f.comp g
The theorem `Function.Injective.injective_linearMapComp_left` states that for any types `R₁`, `R₂`, `R₃`, `M₁`, `M₂`, `M₃`, if the semirings `R₁`, `R₂`, `R₃`, and additive commutative monoids `M₁`, `M₂`, `M₃` are given structure as modules over them, and if `σ₁₂`, `σ₂₃`, `σ₁₃` are ring homomorphisms forming a `RingHomCompTriple`, then for any linear map `f` from `M₂` to `M₃`, if `f` is injective, then the function which takes a linear map `g` (from `M₁` to `M₂`) as input and returns the composition of `f` and `g` is also injective. In other words, the injectiveness of a linear map is preserved under left composition.
More concisely: If `R₁`, `R₂`, `R₃` are semirings, and `M₁`, `M₂`, `M₃` are additive commutative monoids with module structures over `R₁`, `R₂`, `R₃`, respectively, and `σ₁₂`, `σ₂₃`, `σ₁₃` are ring homomorphisms forming a ring homomorphism composition triple, and `f: M₂ → M₃` is an injective linear map, then the function `g ↦ f ∘ g: M₁ → M₃` is also injective.
|
LinearMap.toFun_eq_coe
theorem LinearMap.toFun_eq_coe :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [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}
{f : M →ₛₗ[σ] M₃}, f.toFun = ⇑f
This theorem states that for any semirings `R` and `S`, additive commutative monoids `M` and `M₃`, modules `M` over `R` and `M₃` over `S`, and a ring homomorphism `σ` from `R` to `S`, the `toFun` function of a linear map `f` from `M` to `M₃` under `σ` is equal to `f` when considered as a function (i.e., `f.toFun = ⇑f`). Essentially, this reconfirms the identification of a linear map `f` with its underlying function.
More concisely: For any semirings R and S, additive commutative monoids M and M₃, modules M over R and M₃ over S, and a ring homomorphism σ from R to S, the toFun function of a linear map f from M to M₃ under σ equals f as functions.
|
LinearMap.toAddMonoidHom_injective
theorem LinearMap.toAddMonoidHom_injective :
∀ {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [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},
Function.Injective LinearMap.toAddMonoidHom
The theorem `LinearMap.toAddMonoidHom_injective` states that for any semirings `R` and `S`, additive commutative monoids `M` and `M₃`, `R`-module structure on `M`, `S`-module structure on `M₃`, and ring homomorphism `σ` from `R` to `S`, the function `LinearMap.toAddMonoidHom`, which converts a linear map to an additive map, is injective. In other words, if two linear maps become identical when viewed as additive maps, those two linear maps were originally identical.
More concisely: If two linear maps between modules over ring homomorphisms have the same additive map representation, then they are equal as linear maps.
|