Documentation

Mathlib.Algebra.Module.Submodule.Ker

Kernel of a linear map #

This file defines the kernel of a linear map.

Main definitions #

Notation #

Tags #

linear algebra, vector space, module

Properties of linear maps #

source
def LinearMap.ker {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) :
Submodule R M

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
    source
    @[simp]
    theorem LinearMap.mem_ker {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} {y : M} :
    y ∈ f.ker ↔ f y = 0
    source
    @[simp]
    theorem LinearMap.ker_id {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
    id.ker = ⊥
    source
    @[simp]
    theorem LinearMap.map_coe_ker {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (x : ↥f.ker) :
    f ↑x = 0
    source
    theorem LinearMap.ker_toAddSubmonoid {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) :
    f.ker.toAddSubmonoid = AddMonoidHom.mker f
    source
    theorem LinearMap.le_ker_iff_comp_subtype_eq_zero {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {N : Submodule R M} {f : M →ₛₗ[τ₁₂] M₂} :
    N ≤ f.ker ↔ f ∘ₛₗ N.subtype = 0
    source
    theorem LinearMap.comp_ker_subtype {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) :
    f ∘ₛₗ f.ker.subtype = 0
    source
    theorem LinearMap.ker_comp {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} [Semiring R] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
    (g ∘ₛₗ f).ker = Submodule.comap f g.ker
    source
    theorem LinearMap.ker_le_ker_comp {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} [Semiring R] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
    f.ker ≤ (g ∘ₛₗ f).ker
    source
    theorem LinearMap.ker_sup_ker_le_ker_comp_of_commute {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {f g : M →ₗ[R] M} (h : Commute f g) :
    f.ker ⊔ g.ker ≤ (f ∘ₗ g).ker
    source
    @[simp]
    theorem LinearMap.ker_le_comap {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {p : Submodule R₂ M₂} (f : M →ₛₗ[τ₁₂] M₂) :
    f.ker ≤ Submodule.comap f p
    source
    theorem LinearMap.disjoint_ker {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M} :
    Disjoint p f.ker ↔ ∀ x ∈ p, f x = 0 → x = 0
    source
    theorem LinearMap.ker_eq_bot' {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} :
    f.ker = ⊥ ↔ ∀ (m : M), f m = 0 → m = 0
    source
    theorem LinearMap.ker_eq_bot_of_inverse {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₁] M} (h : g ∘ₛₗ f = id) :
    f.ker = ⊥
    source
    theorem LinearMap.le_ker_iff_map {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M} :
    p ≤ f.ker ↔ Submodule.map f p = ⊥
    source
    @[simp]
    theorem LinearMap.ker_codRestrict {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (p : Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (hf : ∀ (c : M), f c ∈ p) :
    (codRestrict p f hf).ker = f.ker
    source
    theorem LinearMap.ker_domRestrict {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (p : Submodule R M) (f : M →ₛₗ[τ₁₂] M₂) :
    (f.domRestrict p).ker = Submodule.comap p.subtype f.ker
    source
    theorem LinearMap.ker_restrict {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {p : Submodule R M} {q : Submodule R₂ M₂} {f : M →ₛₗ[τ₁₂] M₂} (hf : ∀ x ∈ p, f x ∈ q) :
    (f.restrict hf).ker = Submodule.comap p.subtype f.ker
    source
    @[simp]
    theorem LinearMap.ker_zero {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} :
    ker 0 = ⊤
    source
    @[simp]
    theorem LinearMap.ker_eq_top {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} :
    f.ker = ⊤ ↔ f = 0
    source
    @[simp]
    theorem LinearMap.domRestrict_ker_self {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) :
    f.domRestrict f.ker = 0
    source
    theorem LinearMap.exists_ne_zero_of_sSup_eq_top {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} (h : f ≠ 0) (s : Set (Submodule R M)) (hs : sSup s = ⊤) :
    ∃ m ∈ s, f ∘ₛₗ m.subtype ≠ 0
    source
    @[simp]
    theorem AddMonoidHom.coe_toIntLinearMap_ker {M : Type u_10} {M₂ : Type u_11} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) :
    f.toIntLinearMap.ker = AddSubgroup.toIntSubmodule f.ker
    source
    theorem LinearMap.ker_eq_bot_of_injective {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} (hf : Function.Injective ⇑f) :
    f.ker = ⊥
    source
    def LinearMap.iterateKer {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M) :
    ℕ →o Submodule R M

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

    Equations
    Instances For
      source
      @[simp]
      theorem LinearMap.iterateKer_coe {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M) (n : ℕ) :
      f.iterateKer n = (f ^ n).ker
      source
      theorem LinearMap.ker_submoduleMap {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] (f : M →ₛₗ[τ₁₂] M₂) (p : Submodule R M) :
      (f.submoduleMap p).ker = Submodule.comap p.subtype f.ker
      source
      @[simp]
      theorem LinearMap.ker_neg {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Ring R] [Ring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) :
      (-f).ker = f.ker
      source
      theorem LinearMap.ker_toAddSubgroup {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Ring R] [Ring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) :
      f.ker.toAddSubgroup = f.toAddMonoidHom.ker
      source
      theorem LinearMap.sub_mem_ker_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Ring R] [Ring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} {x y : M} :
      x - y ∈ f.ker ↔ f x = f y
      source
      theorem LinearMap.disjoint_ker_iff_injOn {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Ring R] [Ring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M} :
      Disjoint p f.ker ↔ Set.InjOn ⇑f ↑p
      source
      theorem LinearMap.injOn_of_disjoint_ker {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Ring R] [Ring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M} {s : Set M} (h : s ⊆ ↑p) (hd : Disjoint p f.ker) :
      Set.InjOn (⇑f) s
      source
      theorem LinearMap.ker_eq_bot {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Ring R] [Ring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} :
      f.ker = ⊥ ↔ Function.Injective ⇑f
      source
      @[simp]
      theorem LinearMap.injective_domRestrict_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Ring R] [Ring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} :
      Function.Injective ⇑(f.domRestrict S) ↔ Disjoint S f.ker
      source
      @[simp]
      theorem LinearMap.injective_restrict_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Ring R] [Ring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {p : Submodule R M} {q : Submodule R₂ M₂} {f : M →ₛₗ[τ₁₂] M₂} (hf : ∀ x ∈ p, f x ∈ q) :
      Function.Injective ⇑(f.restrict hf) ↔ Disjoint p f.ker
      source
      @[deprecated LinearMap.injective_restrict_iff (since := "2026-07-01")]
      theorem LinearMap.injective_restrict_iff_disjoint {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Ring R] [Ring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {p : Submodule R M} {q : Submodule R₂ M₂} {f : M →ₛₗ[τ₁₂] M₂} (hf : ∀ x ∈ p, f x ∈ q) :
      Function.Injective ⇑(f.restrict hf) ↔ Disjoint p f.ker

      Alias of LinearMap.injective_restrict_iff.

      source
      @[simp]
      theorem LinearMap.injective_codRestrict_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Ring R] [Ring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {q : Submodule R₂ M₂} {f : M →ₛₗ[τ₁₂] M₂} (hf : ∀ (x : M), f x ∈ q) :
      Function.Injective ⇑(codRestrict q f hf) ↔ Function.Injective ⇑f
      source
      theorem LinearMap.ker_le_ker_smul {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [CommSemiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (c : R₂) :
      f.ker ≤ (c • f).ker
      source
      theorem LinearMap.ker_smul {K : Type u_4} {V : Type u_8} {V₂ : Type u_9} [Semifield K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] (f : V →ₗ[K] V₂) (a : K) (h : a ≠ 0) :
      (a • f).ker = f.ker
      source
      theorem LinearMap.ker_smul' {K : Type u_4} {V : Type u_8} {V₂ : Type u_9} [Semifield K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] (f : V →ₗ[K] V₂) (a : K) :
      (a • f).ker = ⨅ (_ : a ≠ 0), f.ker
      source
      @[simp]
      theorem Submodule.comap_bot {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) :
      comap f ⊥ = f.ker
      source
      @[simp]
      theorem Submodule.ker_subtype {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
      p.subtype.ker = ⊥
      source
      @[simp]
      theorem Submodule.ker_inclusion {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p p' : Submodule R M) (h : p ≤ p') :
      (inclusion h).ker = ⊥
      source
      theorem LinearMap.ker_comp_of_ker_eq_bot {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} [Semiring R] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) {g : M₂ →ₛₗ[τ₂₃] M₃} (hg : g.ker = ⊥) :
      (g ∘ₛₗ f).ker = f.ker
      source
      @[simp]
      theorem LinearMap.ker_restrictScalars (R : Type u_10) {S : Type u_11} {M : Type u_12} {N : Type u_13} [Semiring R] [Semiring S] [SMul R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [AddCommMonoid N] [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[S] N) :
      (↑R f).ker = Submodule.restrictScalars R f.ker

      Linear equivalences #

      source
      @[simp]
      theorem LinearEquiv.ker {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) :
      (↑e).ker = ⊥
      source
      @[simp]
      theorem LinearEquiv.ker_comp {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} [Semiring R] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] {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₂) :
      (↑e'' ∘ₛₗ l).ker = l.ker