LinearMap.ker_codRestrict
theorem LinearMap.ker_codRestrict :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [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} (p : Submodule R M) (f : M₂ →ₛₗ[τ₂₁] M) (hf : ∀ (c : M₂), f c ∈ p),
LinearMap.ker (LinearMap.codRestrict p f hf) = LinearMap.ker f
The theorem `LinearMap.ker_codRestrict` states that for any semirings `R` and `R₂`, any additive commutative monoids `M` and `M₂`, any `R`-module `M` and `R₂`-module `M₂`, a ring homomorphism `τ₂₁` from `R₂` to `R`, a submodule `p` of `M`, and a linear map `f` from `M₂` to `M` such that all values of `f` lie in `p`, the kernel (set of elements mapped to zero) of the linear map obtained by restricting the codomain of `f` to `p` is equal to the kernel of `f` itself. Therefore, binding the codomain does not change the elements that are mapped to zero by the linear map.
More concisely: The kernel of a linear map from one R-module to another, restricted to a submodule where all its values lie, is equal to the map's kernel itself.
|
LinearMap.ker_eq_bot'
theorem LinearMap.ker_eq_bot' :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [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_12} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F τ₁₂ M M₂] {f : F},
LinearMap.ker f = ⊥ ↔ ∀ (m : M), f m = 0 → m = 0
The theorem `LinearMap.ker_eq_bot'` states that for any types `R`, `R₂`, `M`, `M₂`, and `F`, given two semirings `R` and `R₂`, two additively commutative monoids `M` and `M₂`, modules `M` over `R` and `M₂` over `R₂`, a ring homomorphism `τ₁₂` from `R` to `R₂`, a type `F` which is a function-like from `M` to `M₂` and a semilinear map `f` from `M` to `M₂`, the kernel of the linear map `f` is the zero submodule if and only if for every element `m` of `M`, the implication is true that if `f m` equals zero then `m` equals zero. This theorem essentially describes the condition for a linear map to be injective or, equivalently, for its kernel to only contain the zero element.
More concisely: The kernel of a semilinear map between modules over commutative rings is the zero submodule if and only if it maps every non-zero element to a non-zero image.
|
LinearEquiv.ker
theorem LinearEquiv.ker :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [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.ker ↑e = ⊥
This theorem states that for any linear equivalence `e` between two modules `M` and `M₂` over semirings `R` and `R₂`, respectively, the kernel of the linear map corresponding to `e` is trivial, i.e., it contains only the zero vector. This is true under the conditions that `R` and `R₂` are semirings, `M` and `M₂` are additive commutative monoids, `M` and `M₂` have module structures over `R` and `R₂`, respectively, and there are ring homomorphisms `σ₁₂` : `R` → `R₂` and `σ₂₁` : `R₂` → `R` that are inverses to each other.
More concisely: Given semirings `R` and `R₂`, additive commutative monoids `M` and `M₂` with module structures over `R` and `R₂`, and ring homomorphisms `σ₁₂ : R → R₂` and `σ₂₁ : R₂ → R` that are inverses, any linear equivalence between `M` and `M₂` over `R` and `R₂` implies that their corresponding kernel is the zero module.
|
LinearMap.mem_ker
theorem LinearMap.mem_ker :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [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_12} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F τ₁₂ M M₂] {f : F}
{y : M}, y ∈ LinearMap.ker f ↔ f y = 0
The theorem `LinearMap.mem_ker` states that for any semirings `R` and `R₂`, additively commutative monoids `M` and `M₂`, `R`-module `M`, `R₂`-module `M₂`, a ring homomorphism `τ₁₂` from `R` to `R₂`, a function `f` from `M` to `M₂` that is also a semilinear map, and any element `y` of `M`, `y` is in the kernel of `f` if and only if the result of applying `f` to `y` is the zero element in `M₂`. The kernel of a linear map is the set of all elements that map to zero. In other words, the theorem characterizes the kernel of a semilinear map in terms of the function's action on the elements.
More concisely: A semilinear map from an `R`-module to an `R₂`-module, induced by a ring homomorphism from `R` to `R₂`, maps an element to zero in the target module if and only if that element is in the kernel of the map.
|
LinearMap.ker_eq_top
theorem LinearMap.ker_eq_top :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [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 : M →ₛₗ[τ₁₂] M₂}, LinearMap.ker f = ⊤ ↔ f = 0
This theorem states that for any semirings `R` and `R₂`, additive commutative monoids `M` and `M₂`, modules `M` over `R` and `M₂` over `R₂`, a ring homomorphism `τ₁₂` from `R` to `R₂`, and a linear map `f` from `M` to `M₂`, the kernel of the linear map `f` is equal to the whole space `M` (denoted by `⊤`) if and only if the linear map `f` is the zero map. In other words, a linear map is the zero map exactly when its kernel is the whole domain.
More concisely: For semirings R and R₂, additive commutative monoids M and M₂, modules M over R and M₂ over R₂, a ring homomorphism τ₁₂ from R to R₂, and a linear map f : M -> M₂, if and only if f is the zero map, then ker(f) = {x : M | ∀ y : M, f(x + y) = f(x) + f(y)} = M.
|
LinearMap.ker_le_ker_comp
theorem LinearMap.ker_le_ker_comp :
∀ {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_6} {M₂ : Type u_8} {M₃ : Type u_9} [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 : M →ₛₗ[τ₁₂] M₂)
(g : M₂ →ₛₗ[τ₂₃] M₃), LinearMap.ker f ≤ LinearMap.ker (g.comp f)
This theorem states that for any three semirings R, R₂, R₃ and three additively commutative monoids M, M₂, M₃, with M, M₂, M₃ being modules over R, R₂, R₃ respectively, and given three ring homomorphisms τ₁₂, τ₂₃, τ₁₃ (with τ₁₃ being the composition of τ₁₂ and τ₂₃), and two linear maps f (from M to M₂) and g (from M₂ to M₃), the kernel of the linear map f is a subspace (or is contained in) the kernel of the composition of the linear maps g and f. In terms of category theory, it suggests that the kernel of a morphism is always a subset of the kernel of its composition with another morphism.
More concisely: For any three semirings R, R₂, R₃, three additively commutative monoids M, M₂, M₃ that are modules over R, R₂, R₃ respectively, and given ring homomorphisms τ₁₂, τ₂₃, τ₁₃, two linear maps f : M → M₂ and g : M₂ → M₃, the kernel of f is contained in the kernel of g ∘ f.
|
Mathlib.Algebra.Module.Submodule.Ker._auxLemma.4
theorem Mathlib.Algebra.Module.Submodule.Ker._auxLemma.4 :
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b = (a ⊓ b ≤ ⊥)
This theorem states that for any type `α` equipped with the structure of a semilattice having a least element (with `α` as the type, a semilattice structure, and a least element structure), and for any two elements `a` and `b` of this type, `a` and `b` are disjoint if and only if the infimum of `a` and `b` is less than or equal to the least element. Here, being 'disjoint' is defined by the `Disjoint` function, which means that for any element `x` which is less than or equal to both `a` and `b`, `x` is also less than or equal to the bottom element.
More concisely: For any semilattice `α` with least element, elements `a` and `b` are disjoint if and only if the infimum of `a` and `b` equals the least element.
|
LinearMap.ker_eq_bot_of_injective
theorem LinearMap.ker_eq_bot_of_injective :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [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_12} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F τ₁₂ M M₂] {f : F},
Function.Injective ⇑f → LinearMap.ker f = ⊥
The theorem `LinearMap.ker_eq_bot_of_injective` states that for all types `R`, `R₂`, `M`, `M₂`, and `F`, if `R` and `R₂` are semirings, `M` and `M₂` are additive commutative monoids, `M` and `M₂` are modules over `R` and `R₂` respectively, `τ₁₂` is a ring homomorphism from `R` to `R₂`, `F` is a type that behaves like a function from `M` to `M₂` and `f` satisfies the property of a semilinear map from `M` to `M₂`, then if the function `f` is injective (i.e., no two different inputs give the same output), the kernel of the linear map `f` (i.e., the set of all inputs that `f` maps to the zero element) is the trivial submodule (represented as `⊥`). In simpler terms, injective linear maps don't map any non-zero inputs to zero.
More concisely: If `F : M → M₂`, `f : M → M₂` is a semilinear map, `τ₁₂ : R → R₂` is a ring homomorphism, and `f` is injective, then the kernel of the linear map `F` is the trivial submodule.
|
Mathlib.Algebra.Module.Submodule.Ker._auxLemma.1
theorem Mathlib.Algebra.Module.Submodule.Ker._auxLemma.1 :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [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_12} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F τ₁₂ M M₂] {f : F}
{y : M}, (y ∈ LinearMap.ker f) = (f y = 0)
This theorem states that for any semirings `R` and `R₂`, additive commutative monoids `M` and `M₂`, and modules over these semirings, given a ring homomorphism `τ₁₂` from `R` to `R₂`, a type `F` that behaves like a function from `M` to `M₂`, and a semilinear map `f` of type `F`, a vector `y` from `M` is in the kernel of `f` if and only if `f` applied to `y` is equal to zero. Here, the kernel of a linear map `f` is defined as the set of all vectors from `M` that `f` maps to zero. This theorem allows us to check whether a vector is in the kernel of `f` by simply applying `f` to the vector and checking if the result is zero.
More concisely: For any ring homomorphism τ₁₂ from semirings R and R₂, additive commutative monoids M and M₂, and module homomorphism F : M →ₗ[τ₁₂] M₂ from a type behaving like a function, if y ∈ M then y ∈ ker(F(f)) if and only if F(f)(y) = 0.
|
LinearMap.ker_eq_bot
theorem LinearMap.ker_eq_bot :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [inst : Ring R] [inst_1 : Ring R₂]
[inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
{τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂}, LinearMap.ker f = ⊥ ↔ Function.Injective ⇑f
The theorem `LinearMap.ker_eq_bot` states that for any two types `R` and `R₂` which have the structure of rings, and for any two types `M` and `M₂` which form additive commutative groups and are also modules over `R` and `R₂` respectively, for any ring homomorphism `τ₁₂ : R →+* R₂` and any linear map `f : M →ₛₗ[τ₁₂] M₂`, the kernel of the linear map `f` is trivial (denoted as `⊥`) if and only if the function `f` is injective.
In mathematical terms, this theorem is stating that the kernel of a linear map is trivial if and only if the map is injective, which is a fundamental result in linear algebra.
More concisely: The kernel of a linear map between two module instances over commutative rings is the zero submodule if and only if the map is injective.
|
Submodule.ker_subtype
theorem Submodule.ker_subtype :
∀ {R : Type u_1} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(p : Submodule R M), LinearMap.ker p.subtype = ⊥
The theorem `Submodule.ker_subtype` states that for any ring `R`, additive commutative monoid `M`, and any submodule `p` of `M` over `R`, the kernel of the embedding of the submodule `p` into the ambient space `M` is the trivial module (denoted by `⊥`). In other words, no non-zero element of the submodule `p` gets mapped to the zero element under the embedding operation.
More concisely: The theorem asserts that the kernel of the embedding of a submodule in a commutative additive monoid is the trivial submodule, containing only the additive identity.
|
LinearMap.disjoint_ker
theorem LinearMap.disjoint_ker :
∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [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_12} [inst_6 : FunLike F M M₂] [inst_7 : SemilinearMapClass F τ₁₂ M M₂] {f : F}
{p : Submodule R M}, Disjoint p (LinearMap.ker f) ↔ ∀ x ∈ p, f x = 0 → x = 0
The theorem `LinearMap.disjoint_ker` states that for any semiring `R` and `R₂`, additive commutative monoids `M` and `M₂`, modules `M` over `R` and `M₂` over `R₂`, and a semilinear map `τ₁₂` from `R` to `R₂`. Also, given `F` is a type such that there is a function-like mapping from `M` to `M₂`, and `f` behaves as a semilinear map under `F` and `τ₁₂`, and `p` is a submodule of `R` and `M`. Then, `p` is disjoint from the kernel of `f` if and only if for every `x` in `p`, if `f(x)` equals zero then `x` must also be zero.
In more plain terms, the kernel of a linear map (the set of elements that map to zero) is disjoint from a submodule `p` precisely when every element of that submodule which maps to zero is itself zero. This is a property about the interaction between submodules and the kernels of linear maps.
More concisely: A submodule `p` of a module over a semiring is disjoint from the kernel of a semilinear map if and only if every element of `p` mapping to zero under the map is itself zero.
|
LinearMap.ker_comp
theorem LinearMap.ker_comp :
∀ {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_6} {M₂ : Type u_8} {M₃ : Type u_9} [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 : M →ₛₗ[τ₁₂] M₂)
(g : M₂ →ₛₗ[τ₂₃] M₃), LinearMap.ker (g.comp f) = Submodule.comap f (LinearMap.ker g)
This theorem states that for any three semirings R, R₂, R₃ and three modules M, M₂, M₃ over those rings, and two ring homomorphisms τ₁₂, τ₂₃ (with τ₁₃ being the composite of τ₁₂ and τ₂₃), if we have two linear maps: one from M to M₂ and another from M₂ to M₃, then the kernel of the composition of the two linear maps (g composed with f) is equal to the preimage of the kernel of the second map (g) under the first map (f). In other words, all elements in M that are mapped to zero by the composed map (g composed with f) are exactly those elements that are mapped by f into elements of M₂ that are then mapped to zero by g.
More concisely: The kernel of the composition of two linear maps f : M -> M₂ and g : M₂ -> M₃ between modules over rings is equal to the preimage of the kernel of g under f.
|