IsLinearMap.isLinearMap_add
theorem IsLinearMap.isLinearMap_add :
∀ {R : Type u_1} {M : Type u_9} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
IsLinearMap R fun x => x.1 + x.2
This theorem states that, for any semiring `R` and any additive commutative monoid `M` that also has the structure of an `R`-module, the function that takes a pair of elements `(x, y)` in `M` and adds them together is a linear map. In mathematical terms, given any scalar `r` and any two elements `m1`, `m2` of `M`, the function respects scalar multiplication (`f(r * m) = r * f(m)`) and addition (`f(m1 + m2) = f(m1) + f(m2)`).
More concisely: For any semiring `R`, additive commutative monoid `M` being an `R`-module implies the addition function on `M` is a linear map with respect to scalars and vectors.
|
LinearMap.funLeft_comp
theorem LinearMap.funLeft_comp :
∀ (R : Type u_1) (M : Type u_9) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {m : Type u_20}
{n : Type u_21} {p : Type u_22} (f₁ : n → p) (f₂ : m → n),
LinearMap.funLeft R M (f₁ ∘ f₂) = LinearMap.funLeft R M f₂ ∘ₗ LinearMap.funLeft R M f₁
This theorem states that for any semiring `R`, additively commutative monoid `M`, `R`-module structure on `M`, and arbitrary types `m`, `n`, and `p`, if we have two functions `f₁ : n → p` and `f₂ : m → n`, then constructing a linear map from `n → M` to `m → M` using the composition of `f₁` and `f₂` (`f₁ ∘ f₂`) is the same as composing the linear map constructed using `f₂` with the linear map constructed using `f₁`. In other words, the construction of these linear maps commutes with function composition.
More concisely: For any semiring `R`, additively commutative monoid `M` with an `R`-module structure, and types `m`, `n`, `p`, if `f₁ : n → p` and `f₂ : m → n` are functions, then the linear maps from `n → M` to `m → M` constructed using `f₁ ∘ f₂` and `f₂ ∘ f₁` are equal.
|
Mathlib.LinearAlgebra.Basic._auxLemma.1
theorem Mathlib.LinearAlgebra.Basic._auxLemma.1 :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_12} [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 : Type u_20} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F τ₁₂ M M₂] {x : M}
{f g : F}, (x ∈ LinearMap.eqLocus f g) = (f x = g x)
The theorem `Mathlib.LinearAlgebra.Basic._auxLemma.1` states that for all types `R`, `R₂`, `M`, and `M₂` such that `R` and `R₂` are semirings, `M` and `M₂` are additively commutative monoids, and `M` and `M₂` are modules over `R` and `R₂` respectively; for any type `F` which has a function-like relationship between `M` and `M₂`, and any semilinear map from `R` to `R₂` denoted by `τ₁₂` that has a surjective ring homomorphism, and any function `f` of type `F` and any `x` from `M₂`, the theorem asserts that `x` is in the range of the linear map `f` if and only if there exists a `y` such that `f(y) = x`.
More concisely: Given semirings R and R₂, additively commutative monoids and R-modules M and M₂, a semilinear map τ₁₂ from R to R₂ that is a surjective ring homomorphism, and a function F from M₂ to M with the property that for all x in M₂, there exists y such that f(y) = x if and only if x is in the image of f under τ₁₂, then for all x in M₂, x is in the range of f if and only if there exists a y in M such that f(y) = x.
|
LinearMap.funLeft_id
theorem LinearMap.funLeft_id :
∀ (R : Type u_1) (M : Type u_9) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : Type u_21}
(g : n → M), (LinearMap.funLeft R M id) g = g
This theorem states that for any semiring `R`, an additive commutative monoid `M`, and a module `M` over `R`, given a function `g` from an arbitrary type `n` to `M`, applying the function `LinearMap.funLeft R M id` to `g` results in `g` itself. In other words, the function `LinearMap.funLeft R M id` acts as an identity for any function from `n` to `M`.
More concisely: For any semiring R, additive commutative monoid M, and R-module M, the function `LinearMap.funLeft R M id` is the identity for any function from an arbitrary type to M.
|
LinearEquiv.range
theorem LinearEquiv.range :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {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₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
(e : M ≃ₛₗ[σ₁₂] M₂), LinearMap.range ↑e = ⊤
The theorem `LinearEquiv.range` states that for any linear equivalence `e` between two modules `M` and `M₂` over semirings `R` and `R₂` respectively, the range of the corresponding linear map is the whole target module `M₂`. In other words, every element of `M₂` is reachable by applying the linear map to some element of `M`. This aligns with the intuition that a linear equivalence, being a bijective linear map, should "cover" the entire target module.
More concisely: For any linear equivalence between modules, the image of the module under the corresponding linear map is the entire target module.
|