# Kernel of a linear map #

This file defines the kernel of a linear map.

## Main definitions #

• LinearMap.ker: the kernel of a linear map as a submodule of the domain

## Notations #

• We continue to use the notations M →ₛₗ[σ] M₂ and M →ₗ[R] M₂ for the type of semilinear (resp. linear) maps from M to M₂ over the ring homomorphism σ (resp. over the ring R).

## Tags #

linear algebra, vector space, module

### Properties of linear maps #

def LinearMap.ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_12} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] (f : F) :

The kernel of a linear map f : M → M₂ is defined to be comap f ⊥. This is equivalent to the set of x : M such that f x = 0. The kernel is a submodule of M.

Equations
Instances For
@[simp]
theorem LinearMap.mem_ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_12} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} {y : M} :
f y = 0
@[simp]
theorem LinearMap.ker_id {R : Type u_1} {M : Type u_6} [] [] [Module R M] :
LinearMap.ker LinearMap.id =
@[simp]
theorem LinearMap.map_coe_ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_12} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] (f : F) (x : { x : M // }) :
f x = 0
theorem LinearMap.ker_toAddSubmonoid {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) :
theorem LinearMap.comp_ker_subtype {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) :
f.comp .subtype = 0
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} [] [Semiring R₂] [Semiring R₃] [] [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
LinearMap.ker (g.comp f) =
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} [] [Semiring R₂] [Semiring R₃] [] [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
LinearMap.ker (g.comp f)
theorem LinearMap.ker_sup_ker_le_ker_comp_of_commute {R : Type u_1} {M : Type u_6} [] [] [Module R M] {f : M →ₗ[R] M} {g : M →ₗ[R] M} (h : Commute f g) :
LinearMap.ker (f ∘ₗ g)
@[simp]
theorem LinearMap.ker_le_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {p : Submodule R₂ M₂} (f : M →ₛₗ[τ₁₂] M₂) :
theorem LinearMap.disjoint_ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_12} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} {p : } :
xp, f x = 0x = 0
theorem LinearMap.ker_eq_bot' {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_12} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} :
∀ (m : M), f m = 0m = 0
theorem LinearMap.ker_eq_bot_of_inverse {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₁] M} (h : g.comp f = LinearMap.id) :
theorem LinearMap.le_ker_iff_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_12} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] {f : F} {p : } :
theorem LinearMap.ker_codRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₂₁ : R₂ →+* R} (p : ) (f : M₂ →ₛₗ[τ₂₁] M) (hf : ∀ (c : M₂), f c p) :
theorem LinearMap.ker_restrict {R : Type u_1} {M : Type u_6} {M₁ : Type u_7} [] [] [Module R M] [] [Module R M₁] {p : } {q : Submodule R M₁} {f : M →ₗ[R] M₁} (hf : xp, f x q) :
LinearMap.ker (f.restrict hf) = LinearMap.ker (f.domRestrict p)
@[simp]
theorem LinearMap.ker_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} :
theorem LinearMap.ker_eq_top {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} :
f = 0
@[simp]
theorem AddMonoidHom.coe_toIntLinearMap_ker {M : Type u_13} {M₂ : Type u_14} [] [] (f : M →+ M₂) :
theorem LinearMap.ker_eq_bot_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_12} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : ) :
@[simp]
theorem LinearMap.iterateKer_coe {R : Type u_1} {M : Type u_6} [] [] [Module R M] (f : M →ₗ[R] M) (n : ) :
f.iterateKer n = LinearMap.ker (f ^ n)
def LinearMap.iterateKer {R : Type u_1} {M : Type u_6} [] [] [Module R M] (f : M →ₗ[R] M) :

The increasing sequence of submodules consisting of the kernels of the iterates of a linear map.

Equations
Instances For
theorem LinearMap.ker_toAddSubgroup {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [Ring R] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) :
theorem LinearMap.sub_mem_ker_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [Ring R] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_12} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} {x : M} {y : M} :
x - y f x = f y
theorem LinearMap.disjoint_ker' {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [Ring R] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_12} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} {p : } :
xp, yp, f x = f yx = y
theorem LinearMap.injOn_of_disjoint_ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [Ring R] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_12} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} {p : } {s : Set M} (h : s p) (hd : ) :
Set.InjOn (⇑f) s
theorem LinearMapClass.ker_eq_bot {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [Ring R] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (F : Type u_12) [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} :
theorem LinearMap.ker_eq_bot {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [Ring R] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} :
@[simp]
theorem LinearMap.injective_domRestrict_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [Ring R] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} {S : } :
Function.Injective (f.domRestrict S) =
@[simp]
theorem LinearMap.injective_restrict_iff_disjoint {R : Type u_1} {M : Type u_6} [Ring R] [] [Module R M] {p : } {f : M →ₗ[R] M} (hf : xp, f x p) :
Function.Injective (f.restrict hf)
theorem LinearMap.ker_smul {K : Type u_5} {V : Type u_10} {V₂ : Type u_11} [] [] [Module K V] [] [Module K V₂] (f : V →ₗ[K] V₂) (a : K) (h : a 0) :
theorem LinearMap.ker_smul' {K : Type u_5} {V : Type u_10} {V₂ : Type u_11} [] [] [Module K V] [] [Module K V₂] (f : V →ₗ[K] V₂) (a : K) :
LinearMap.ker (a f) = ⨅ (_ : a 0),
@[simp]
theorem Submodule.comap_bot {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_12} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] (f : F) :
@[simp]
theorem Submodule.ker_subtype {R : Type u_1} {M : Type u_6} [] [] [Module R M] (p : ) :
LinearMap.ker p.subtype =
@[simp]
theorem Submodule.ker_inclusion {R : Type u_1} {M : Type u_6} [] [] [Module R M] (p : ) (p' : ) (h : p p') :
theorem LinearMap.ker_comp_of_ker_eq_bot {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_6} {M₂ : Type u_8} {M₃ : Type u_9} [] [Semiring R₂] [Semiring R₃] [] [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) {g : M₂ →ₛₗ[τ₂₃] M₃} (hg : ) :
LinearMap.ker (g.comp f) =

### Linear equivalences #

@[simp]
theorem LinearEquiv.ker {R : Type u_1} {R₂ : Type u_3} {M : Type u_6} {M₂ : Type u_8} [] [Semiring R₂] [] [] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) :
@[simp]
theorem LinearEquiv.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} [] [Semiring R₂] [Semiring R₃] [] [] [] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {σ₃₂ : R₃ →+* R₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} (e'' : M₂ ≃ₛₗ[σ₂₃] M₃) (l : M →ₛₗ[σ₁₂] M₂) :
LinearMap.ker ((↑e'').comp l) =