Mathlib.Algebra.Module.Submodule.Ker

LinearMap.ker definition

(f : F) : Submodule R M

Full source

/-- 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`. -/
def ker (f : F) : Submodule R M :=
  comap f ⊥

Kernel of a linear map

Informal description

The kernel of a linear map $ f : M \to M₂ $ is the submodule of $ M $ consisting of all elements $ x \in M $ such that $ f(x) = 0 $. It is defined as the pullback of the zero submodule along $ f $, denoted $ \text{ker } f = \{ x \in M \mid f(x) = 0 \} $.

LinearMap.mem_ker theorem

{f : F} {y} : y ∈ ker f ↔ f y = 0

Full source

@[simp]
theorem mem_ker {f : F} {y} : y ∈ ker fy ∈ ker f ↔ f y = 0 :=
  mem_bot R₂

Characterization of Kernel Membership: $y \in \ker f \iff f(y) = 0$

Informal description

For any linear map $f \colon M \to M_2$ and any element $y \in M$, we have $y \in \ker f$ if and only if $f(y) = 0$.

LinearMap.ker_id theorem

: ker (LinearMap.id : M →ₗ[R] M) = ⊥

Full source

@[simp]
theorem ker_id : ker (LinearMap.id : M →ₗ[R] M) = ⊥ :=
  rfl

Kernel of Identity Linear Map is Zero Submodule

Informal description

The kernel of the identity linear map $\text{id} : M \to M$ on a module $M$ over a semiring $R$ is equal to the zero submodule $\{0\}$ of $M$.

LinearMap.map_coe_ker theorem

(f : F) (x : ker f) : f x = 0

Full source

@[simp]
theorem map_coe_ker (f : F) (x : ker f) : f x = 0 :=
  mem_ker.1 x.2

Elements in Kernel are Mapped to Zero

Informal description

For any linear map $f \colon M \to M_2$ and any element $x$ in the kernel of $f$, we have $f(x) = 0$.

LinearMap.ker_toAddSubmonoid theorem

(f : M →ₛₗ[τ₁₂] M₂) : (ker f).toAddSubmonoid = (AddMonoidHom.mker f)

Full source

theorem ker_toAddSubmonoid (f : M →ₛₗ[τ₁₂] M₂) : (ker f).toAddSubmonoid = (AddMonoidHom.mker f) :=
  rfl

Kernel of a Linear Map as Additive Submonoid

Informal description

For any semilinear map $f \colon M \to M₂$ between modules over a semiring, the underlying additive submonoid of its kernel $\ker f$ is equal to the kernel of $f$ viewed as an additive monoid homomorphism, i.e., $$(\ker f)_{\text{add}} = \{x \in M \mid f(x) = 0\}.$$

LinearMap.le_ker_iff_comp_subtype_eq_zero theorem

{N : Submodule R M} {f : M →ₛₗ[τ₁₂] M₂} : N ≤ ker f ↔ f ∘ₛₗ N.subtype = 0

Full source

theorem le_ker_iff_comp_subtype_eq_zero {N : Submodule R M} {f : M →ₛₗ[τ₁₂] M₂} :
    N ≤ ker f ↔ f ∘ₛₗ N.subtype = 0 := by
  rw [SetLike.le_def, LinearMap.ext_iff, Subtype.forall]; rfl

Submodule containment in kernel is equivalent to zero composition with inclusion

Informal description

Let $N$ be a submodule of an $R$-module $M$, and let $f \colon M \to M_2$ be a semilinear map between $R$-modules. Then $N$ is contained in the kernel of $f$ if and only if the composition of $f$ with the inclusion map $N \hookrightarrow M$ is the zero map, i.e., $$ N \subseteq \ker f \leftrightarrow f \circ \iota_N = 0 $$ where $\iota_N \colon N \hookrightarrow M$ is the canonical inclusion.

LinearMap.comp_ker_subtype theorem

(f : M →ₛₗ[τ₁₂] M₂) : f.comp (ker f).subtype = 0

Full source

theorem comp_ker_subtype (f : M →ₛₗ[τ₁₂] M₂) : f.comp (ker f).subtype = 0 :=
  LinearMap.ext fun x => mem_ker.1 x.2

Composition with Kernel Inclusion Yields Zero Map

Informal description

For any semilinear map $f \colon M \to M_2$ between modules over a semiring, the composition of $f$ with the inclusion map of its kernel $\ker f$ into $M$ is the zero map, i.e., $$ f \circ \iota_{\ker f} = 0 $$ where $\iota_{\ker f} \colon \ker f \hookrightarrow M$ is the canonical inclusion.

LinearMap.ker_comp theorem

 (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) : ker (g.comp f : M →ₛₗ[τ₁₃] M₃) = comap f (ker g)

Full source

theorem ker_comp (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
    ker (g.comp f : M →ₛₗ[τ₁₃] M₃) = comap f (ker g) :=
  rfl

Kernel of Composition Equals Pullback of Kernel

Informal description

Let $f \colon M \to M₂$ and $g \colon M₂ \to M₃$ be semilinear maps between modules over semirings connected by ring homomorphisms. Then the kernel of the composition $g \circ f$ is equal to the pullback of the kernel of $g$ along $f$, i.e., \[ \ker(g \circ f) = f^{-1}(\ker g). \]

LinearMap.ker_le_ker_comp theorem

 (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) : ker f ≤ ker (g.comp f : M →ₛₗ[τ₁₃] M₃)

Full source

theorem ker_le_ker_comp (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
    ker f ≤ ker (g.comp f : M →ₛₗ[τ₁₃] M₃) := by rw [ker_comp]; exact comap_mono bot_le

Kernel Inclusion Under Composition of Linear Maps

Informal description

For any semilinear maps $f \colon M \to M_2$ and $g \colon M_2 \to M_3$ between modules over semirings connected by ring homomorphisms, the kernel of $f$ is contained in the kernel of the composition $g \circ f$. That is, \[ \ker f \subseteq \ker (g \circ f). \]

LinearMap.ker_sup_ker_le_ker_comp_of_commute theorem

{f g : M →ₗ[R] M} (h : Commute f g) : ker f ⊔ ker g ≤ ker (f ∘ₗ g)

Full source

theorem ker_sup_ker_le_ker_comp_of_commute {f g : M →ₗ[R] M} (h : Commute f g) :
    kerker f ⊔ ker g ≤ ker (f ∘ₗ g) := by
  refine sup_le_iff.mpr ⟨?_, ker_le_ker_comp g f⟩
  rw [← Module.End.mul_eq_comp, h.eq, Module.End.mul_eq_comp]
  exact ker_le_ker_comp f g

Kernel Supremum Bound for Commuting Linear Maps: $\ker f \sqcup \ker g \leq \ker(f \circ g)$

Informal description

Let $M$ be a module over a semiring $R$, and let $f, g \colon M \to M$ be commuting linear maps (i.e., $f \circ g = g \circ f$). Then the supremum of their kernels is contained in the kernel of their composition: \[ \ker f \sqcup \ker g \leq \ker (f \circ g). \]

LinearMap.ker_le_comap theorem

{p : Submodule R₂ M₂} (f : M →ₛₗ[τ₁₂] M₂) : ker f ≤ p.comap f

Full source

@[simp]
theorem ker_le_comap {p : Submodule R₂ M₂} (f : M →ₛₗ[τ₁₂] M₂) :
    ker f ≤ p.comap f :=
  fun x hx ↦ by simp [mem_ker.mp hx]

Kernel is Contained in Pullback of Any Submodule

Informal description

For any semilinear map $f \colon M \to M_2$ between modules over semirings $R$ and $R_2$ (connected by a ring homomorphism $\tau_{12} \colon R \to R_2$) and any submodule $p \subseteq M_2$, the kernel of $f$ is contained in the pullback of $p$ along $f$. That is, $\ker f \subseteq \{x \in M \mid f(x) \in p\}$.

LinearMap.disjoint_ker theorem

{f : F} {p : Submodule R M} : Disjoint p (ker f) ↔ ∀ x ∈ p, f x = 0 → x = 0

Full source

theorem disjoint_ker {f : F} {p : Submodule R M} :
    DisjointDisjoint p (ker f) ↔ ∀ x ∈ p, f x = 0 → x = 0 := by
  simp [disjoint_def]

Disjointness of Submodule and Kernel of Linear Map

Informal description

Let $R$ be a semiring, $M$ be an $R$-module, and $f : M \to M$ be a linear map. For any submodule $p$ of $M$, the submodules $p$ and $\ker f$ are disjoint if and only if for every $x \in p$, if $f(x) = 0$ then $x = 0$.

LinearMap.ker_eq_bot' theorem

{f : F} : ker f = ⊥ ↔ ∀ m, f m = 0 → m = 0

Full source

theorem ker_eq_bot' {f : F} : kerker f = ⊥ ↔ ∀ m, f m = 0 → m = 0 := by
  simpa [disjoint_iff_inf_le] using disjoint_ker (f := f) (p := ⊤)

Kernel Equals Zero Submodule if and only if Linear Map is Injective

Informal description

For a linear map $f \colon M \to M_2$ between modules over a semiring $R$, the kernel of $f$ is equal to the zero submodule if and only if $f$ is injective. That is, $\ker f = \{0\}$ if and only if for every $m \in M$, $f(m) = 0$ implies $m = 0$.

LinearMap.ker_eq_bot_of_inverse theorem

 {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₁] M} (h : (g.comp f : M →ₗ[R] M) = id) :
  ker f = ⊥

Full source

theorem ker_eq_bot_of_inverse {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] {f : M →ₛₗ[τ₁₂] M₂}
    {g : M₂ →ₛₗ[τ₂₁] M} (h : (g.comp f : M →ₗ[R] M) = id) : ker f = ⊥ :=
  ker_eq_bot'.2 fun m hm => by rw [← id_apply (R := R) m, ← h, comp_apply, hm, g.map_zero]

Trivial Kernel of Linear Map with Left Inverse

Informal description

Let $R$ and $R_2$ be semirings, $M$ be an $R$-module, $M_2$ be an $R_2$-module, and $\tau_{12} : R \to R_2$ and $\tau_{21} : R_2 \to R$ be ring homomorphisms that are inverse pairs. For any $\tau_{12}$-semilinear map $f : M \to M_2$ and $\tau_{21}$-semilinear map $g : M_2 \to M$ such that $g \circ f = \text{id}_M$, the kernel of $f$ is trivial, i.e., $\ker f = \{0\}$.

LinearMap.le_ker_iff_map theorem

[RingHomSurjective τ₁₂] {f : F} {p : Submodule R M} : p ≤ ker f ↔ map f p = ⊥

Full source

theorem le_ker_iff_map [RingHomSurjective τ₁₂] {f : F} {p : Submodule R M} :
    p ≤ ker f ↔ map f p = ⊥ := by rw [ker, eq_bot_iff, map_le_iff_le_comap]

Submodule Containment in Kernel is Equivalent to Zero Image

Informal description

Let $R$ and $R₂$ be semirings, $M$ be an $R$-module, $M₂$ be an $R₂$-module, and $f : M \to M₂$ be a linear map. For any submodule $p$ of $M$, the following are equivalent: 1. $p$ is contained in the kernel of $f$, i.e., $p \subseteq \ker f = \{x \in M \mid f(x) = 0\}$. 2. The image of $p$ under $f$ is the zero submodule, i.e., $f(p) = \{0\}$. In symbols: \[ p \subseteq \ker f \leftrightarrow f(p) = \{0\}. \]

LinearMap.ker_codRestrict theorem

{τ₂₁ : R₂ →+* R} (p : Submodule R M) (f : M₂ →ₛₗ[τ₂₁] M) (hf) : ker (codRestrict p f hf) = ker f

Full source

theorem ker_codRestrict {τ₂₁ : R₂ →+* R} (p : Submodule R M) (f : M₂ →ₛₗ[τ₂₁] M) (hf) :
    ker (codRestrict p f hf) = ker f := by rw [ker, comap_codRestrict, Submodule.map_bot]; rfl

Kernel Equality for Codomain-Restricted Linear Maps

Informal description

Let $R$ and $R₂$ be semirings, $M$ be an $R$-module, $M₂$ be an $R₂$-module, and $\tau₂₁: R₂ \to R$ be a ring homomorphism. Given a submodule $p \subseteq M$ and a $\tau₂₁$-semilinear map $f: M₂ \to M$ such that $f(x) \in p$ for all $x \in M₂$ (with proof $hf$), the kernel of the codomain-restricted map $\text{codRestrict } p \ f \ hf: M₂ \to p$ is equal to the kernel of $f$. In other words: $$ \ker(\text{codRestrict } p \ f \ hf) = \ker f $$

LinearMap.ker_domRestrict theorem

 [AddCommMonoid M₁] [Module R M₁] (p : Submodule R M) (f : M →ₗ[R] M₁) : ker (domRestrict f p) = (ker f).comap p.subtype

Full source

lemma ker_domRestrict [AddCommMonoid M₁] [Module R M₁] (p : Submodule R M) (f : M →ₗ[R] M₁) :
    ker (domRestrict f p) = (ker f).comap p.subtype := ker_comp ..

Kernel of Domain-Restricted Linear Map Equals Pullback of Kernel

Informal description

Let $M$ and $M₁$ be modules over a semiring $R$, with $M₁$ being an additive commutative monoid. Given a submodule $p$ of $M$ and a linear map $f : M \to M₁$, the kernel of the domain-restricted map $f|_p : p \to M₁$ is equal to the pullback of the kernel of $f$ along the inclusion map $p \hookrightarrow M$. That is, \[ \ker(f|_p) = \{x \in p \mid f(x) = 0\}. \]

LinearMap.ker_restrict theorem

 [AddCommMonoid M₁] [Module R M₁] {p : Submodule R M} {q : Submodule R M₁} {f : M →ₗ[R] M₁}
  (hf : ∀ x : M, x ∈ p → f x ∈ q) : ker (f.restrict hf) = (ker f).comap p.subtype

Full source

theorem ker_restrict [AddCommMonoid M₁] [Module R M₁] {p : Submodule R M} {q : Submodule R M₁}
    {f : M →ₗ[R] M₁} (hf : ∀ x : M, x ∈ p → f x ∈ q) :
    ker (f.restrict hf) = (ker f).comap p.subtype := by
  rw [restrict_eq_codRestrict_domRestrict, ker_codRestrict, ker_domRestrict]

Kernel of Restricted Linear Map Equals Pullback of Kernel

Informal description

Let $M$ and $M₁$ be modules over a semiring $R$, with $M₁$ being an additive commutative monoid. Given submodules $p \subseteq M$ and $q \subseteq M₁$, and a linear map $f \colon M \to M₁$ such that $f(x) \in q$ for all $x \in p$, the kernel of the restricted map $f|_{p,q} \colon p \to q$ is equal to the pullback of the kernel of $f$ along the inclusion map $p \hookrightarrow M$. That is, \[ \ker(f|_{p,q}) = \{x \in p \mid f(x) = 0\}. \]

LinearMap.ker_zero theorem

: ker (0 : M →ₛₗ[τ₁₂] M₂) = ⊤

Full source

@[simp]
theorem ker_zero : ker (0 : M →ₛₗ[τ₁₂] M₂) = ⊤ :=
  eq_top_iff'.2 fun x => by simp

Kernel of the Zero Linear Map is the Entire Module

Informal description

The kernel of the zero linear map $0 : M \to M₂$ is the entire module $M$, i.e., $\ker(0) = M$.

LinearMap.ker_eq_top theorem

{f : M →ₛₗ[τ₁₂] M₂} : ker f = ⊤ ↔ f = 0

Full source

@[simp]
theorem ker_eq_top {f : M →ₛₗ[τ₁₂] M₂} : kerker f = ⊤ ↔ f = 0 :=
  ⟨fun h => ext fun _ => mem_ker.1 <| h.symm ▸ trivial, fun h => h.symm ▸ ker_zero⟩

Kernel Equals Entire Module if and only if Map is Zero

Informal description

For a semilinear map $f \colon M \to M₂$, the kernel of $f$ is equal to the entire module $M$ if and only if $f$ is the zero map. In other words, $\ker f = M \iff f = 0$.

LinearMap.exists_ne_zero_of_sSup_eq_top theorem

 {f : M →ₛₗ[τ₁₂] M₂} (h : f ≠ 0) (s : Set (Submodule R M)) (hs : sSup s = ⊤) : ∃ m ∈ s, f ∘ₛₗ m.subtype ≠ 0

Full source

theorem exists_ne_zero_of_sSup_eq_top {f : M →ₛₗ[τ₁₂] M₂} (h : f ≠ 0) (s : Set (Submodule R M))
    (hs : sSup s = ⊤): ∃ m ∈ s, f ∘ₛₗ m.subtype ≠ 0 := by
  contrapose! h
  simp_rw [← ker_eq_top, eq_top_iff, ← hs, sSup_le_iff, le_ker_iff_comp_subtype_eq_zero]
  exact h

Existence of Nontrivial Restriction for Nonzero Linear Maps on Full Supremum Submodules

Informal description

Let $f \colon M \to M₂$ be a nonzero semilinear map between modules over a semiring $R$, and let $s$ be a set of submodules of $M$ whose supremum is the entire module $M$. Then there exists a submodule $m \in s$ such that the composition of $f$ with the inclusion map $m \hookrightarrow M$ is nonzero, i.e., $f \circ m.\text{subtype} \neq 0$.

AddMonoidHom.coe_toIntLinearMap_ker theorem

 {M M₂ : Type*} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) :
  LinearMap.ker f.toIntLinearMap = AddSubgroup.toIntSubmodule f.ker

Full source

@[simp]
theorem _root_.AddMonoidHom.coe_toIntLinearMap_ker {M M₂ : Type*} [AddCommGroup M] [AddCommGroup M₂]
    (f : M →+ M₂) : LinearMap.ker f.toIntLinearMap = AddSubgroup.toIntSubmodule f.ker := rfl

Kernel Correspondence for $\mathbb{Z}$-Linear Extension of Additive Group Homomorphism

Informal description

Let $M$ and $M_2$ be additive commutative groups, and let $f \colon M \to M_2$ be an additive group homomorphism. Then the kernel of the induced $\mathbb{Z}$-linear map $f_{\mathbb{Z}} \colon M \to M_2$ is equal to the $\mathbb{Z}$-submodule corresponding to the kernel of $f$ as an additive subgroup. In other words, \[ \ker f_{\mathbb{Z}} = (\ker f)_{\mathbb{Z}} \] where $f_{\mathbb{Z}}$ is the canonical $\mathbb{Z}$-linear extension of $f$, and $(\ker f)_{\mathbb{Z}}$ is the $\mathbb{Z}$-submodule structure on $\ker f$.

LinearMap.ker_eq_bot_of_injective theorem

{f : F} (hf : Injective f) : ker f = ⊥

Full source

theorem ker_eq_bot_of_injective {f : F} (hf : Injective f) : ker f = ⊥ := by
  rw [eq_bot_iff]
  intro x hx
  simpa only [mem_ker, mem_bot, ← map_zero f, hf.eq_iff] using hx

Kernel of an injective linear map is trivial

Informal description

Let $f \colon M \to M₂$ be an injective linear map between modules over a semiring $R$. Then the kernel of $f$ is the trivial submodule $\{0\}$.

LinearMap.iterateKer definition

(f : M →ₗ[R] M) : ℕ →o Submodule R M

Full source

/-- The increasing sequence of submodules consisting of the kernels of the iterates of a linear map.
-/
@[simps]
def iterateKer (f : M →ₗ[R] M) : ℕℕ →o Submodule R M where
  toFun n := ker (f ^ n)
  monotone' n m w x h := by
    obtain ⟨c, rfl⟩ := Nat.exists_eq_add_of_le w
    rw [LinearMap.mem_ker] at h
    rw [LinearMap.mem_ker, add_comm, pow_add, Module.End.mul_apply, h, LinearMap.map_zero]

Increasing sequence of kernels of iterates of a linear map

Informal description

For a linear map $ f : M \to M $ over a ring $ R $, the function $ \text{iterateKer} $ maps each natural number $ n $ to the kernel of the $ n $-th iterate $ f^n $, forming an increasing sequence of submodules of $ M $. Specifically, for any $ n \leq m $, we have $ \ker(f^n) \subseteq \ker(f^m) $.

LinearMap.ker_toAddSubgroup theorem

(f : M →ₛₗ[τ₁₂] M₂) : (ker f).toAddSubgroup = f.toAddMonoidHom.ker

Full source

theorem ker_toAddSubgroup (f : M →ₛₗ[τ₁₂] M₂) : (ker f).toAddSubgroup = f.toAddMonoidHom.ker :=
  rfl

Kernel of Linear Map as Additive Subgroup Equals Kernel of Additive Homomorphism

Informal description

For a semilinear map $f \colon M \to M_2$ over a ring homomorphism $\tau_{12}$, the additive subgroup associated with the kernel of $f$ is equal to the kernel of $f$ viewed as an additive monoid homomorphism. In other words, $(\ker f).\text{toAddSubgroup} = \ker f_{\text{add}}$, where $f_{\text{add}}$ denotes $f$ considered as an additive monoid homomorphism.

LinearMap.sub_mem_ker_iff theorem

{x y} : x - y ∈ ker f ↔ f x = f y

Full source

theorem sub_mem_ker_iff {x y} : x - y ∈ ker fx - y ∈ ker f ↔ f x = f y := by rw [mem_ker, map_sub, sub_eq_zero]

Kernel Membership Criterion via Difference: $x - y \in \ker f \iff f(x) = f(y)$

Informal description

For any linear map $f \colon M \to M_2$ and elements $x, y \in M$, the difference $x - y$ belongs to the kernel of $f$ if and only if $f(x) = f(y)$. In other words, $x - y \in \ker f \iff f(x) = f(y)$.

LinearMap.disjoint_ker' theorem

{p : Submodule R M} : Disjoint p (ker f) ↔ ∀ x ∈ p, ∀ y ∈ p, f x = f y → x = y

Full source

theorem disjoint_ker' {p : Submodule R M} :
    DisjointDisjoint p (ker f) ↔ ∀ x ∈ p, ∀ y ∈ p, f x = f y → x = y :=
  disjoint_ker.trans
    ⟨fun H x hx y hy h => eq_of_sub_eq_zero <| H _ (sub_mem hx hy) (by simp [h]),
     fun H x h₁ h₂ => H x h₁ 0 (zero_mem _) (by simpa using h₂)⟩

Disjointness of Submodule and Kernel Implies Injectivity on Submodule

Informal description

For a linear map $f \colon M \to M_2$ and a submodule $p$ of $M$, the submodules $p$ and $\ker f$ are disjoint if and only if for any $x, y \in p$, the equality $f(x) = f(y)$ implies $x = y$.

LinearMap.injOn_of_disjoint_ker theorem

{p : Submodule R M} {s : Set M} (h : s ⊆ p) (hd : Disjoint p (ker f)) : Set.InjOn f s

Full source

theorem injOn_of_disjoint_ker {p : Submodule R M} {s : Set M} (h : s ⊆ p)
    (hd : Disjoint p (ker f)) : Set.InjOn f s := fun _ hx _ hy =>
  disjoint_ker'.1 hd _ (h hx) _ (h hy)

Injectivity on Subset via Disjoint Kernel

Informal description

Let $f \colon M \to M_2$ be a linear map, $p$ a submodule of $M$, and $s$ a subset of $M$ such that $s \subseteq p$. If $p$ and the kernel of $f$ are disjoint (i.e., $p \cap \ker f = \{0\}$), then $f$ is injective on $s$.

LinearMapClass.ker_eq_bot theorem

: ker f = ⊥ ↔ Injective f

Full source

theorem _root_.LinearMapClass.ker_eq_bot : kerker f = ⊥ ↔ Injective f := by
  simpa [disjoint_iff_inf_le] using disjoint_ker' (f := f) (p := ⊤)

Trivial Kernel Implies Injective Linear Map

Informal description

For a linear map $f \colon M \to M_2$, the kernel of $f$ is the trivial submodule $\{0\}$ if and only if $f$ is injective.

LinearMap.ker_eq_bot theorem

{f : M →ₛₗ[τ₁₂] M₂} : ker f = ⊥ ↔ Injective f

Full source

theorem ker_eq_bot {f : M →ₛₗ[τ₁₂] M₂} : kerker f = ⊥ ↔ Injective f :=
  LinearMapClass.ker_eq_bot _

Trivial kernel characterization of injective linear maps

Informal description

For a linear map $f \colon M \to M_2$, the kernel of $f$ is the trivial submodule $\{0\}$ if and only if $f$ is injective.

LinearMap.injective_domRestrict_iff theorem

{f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} : Injective (f.domRestrict S) ↔ S ⊓ LinearMap.ker f = ⊥

Full source

@[simp] lemma injective_domRestrict_iff {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} :
    InjectiveInjective (f.domRestrict S) ↔ S ⊓ LinearMap.ker f = ⊥ := by
  rw [← LinearMap.ker_eq_bot]
  refine ⟨fun h ↦ le_bot_iff.1 ?_, fun h ↦ le_bot_iff.1 ?_⟩
  · intro x ⟨hx, h'x⟩
    have : ⟨x, hx⟩⟨x, hx⟩ ∈ LinearMap.ker (LinearMap.domRestrict f S) := by simpa using h'x
    rw [h] at this
    simpa [mk_eq_zero] using this
  · rintro ⟨x, hx⟩ h'x
    have : x ∈ S ⊓ LinearMap.ker f := ⟨hx, h'x⟩
    rw [h] at this
    simpa [mk_eq_zero] using this

Injectivity of Domain-Restricted Linear Map via Kernel Intersection

Informal description

Let $f \colon M \to M_2$ be a linear map and $S$ a submodule of $M$. The domain restriction of $f$ to $S$ is injective if and only if the intersection of $S$ with the kernel of $f$ is the trivial submodule $\{0\}$.

LinearMap.injective_restrict_iff_disjoint theorem

 {p : Submodule R M} {f : M →ₗ[R] M} (hf : ∀ x ∈ p, f x ∈ p) : Injective (f.restrict hf) ↔ Disjoint p (ker f)

Full source

@[simp] theorem injective_restrict_iff_disjoint {p : Submodule R M} {f : M →ₗ[R] M}
    (hf : ∀ x ∈ p, f x ∈ p) :
    InjectiveInjective (f.restrict hf) ↔ Disjoint p (ker f) := by
  rw [← ker_eq_bot, ker_restrict hf, ← ker_domRestrict, ker_eq_bot, injective_domRestrict_iff,
    disjoint_iff]

Injectivity of Restricted Linear Map via Kernel Disjointness

Informal description

Let $M$ be a module over a semiring $R$, $p$ a submodule of $M$, and $f \colon M \to M$ a linear map such that $f(x) \in p$ for all $x \in p$. The restriction $f|_p \colon p \to p$ is injective if and only if $p$ and the kernel of $f$ are disjoint, i.e., $p \cap \ker f = \{0\}$.

LinearMap.ker_smul theorem

(f : V →ₗ[K] V₂) (a : K) (h : a ≠ 0) : ker (a • f) = ker f

Full source

theorem ker_smul (f : V →ₗ[K] V₂) (a : K) (h : a ≠ 0) : ker (a • f) = ker f :=
  Submodule.comap_smul f _ a h

Kernel Invariance under Scalar Multiplication: $\ker(a \cdot f) = \ker f$ for $a \neq 0$

Informal description

Let $V$ and $V₂$ be vector spaces over a field $K$, and let $f : V \to V₂$ be a linear map. For any nonzero scalar $a \in K$, the kernel of the scaled linear map $a \cdot f$ is equal to the kernel of $f$, i.e., \[ \ker(a \cdot f) = \ker f. \]

LinearMap.ker_smul' theorem

(f : V →ₗ[K] V₂) (a : K) : ker (a • f) = ⨅ _ : a ≠ 0, ker f

Full source

theorem ker_smul' (f : V →ₗ[K] V₂) (a : K) : ker (a • f) = ⨅ _ : a ≠ 0, ker f :=
  Submodule.comap_smul' f _ a

Kernel of Scaled Linear Map as Infimum over Nonzero Condition

Informal description

Let $V$ and $V₂$ be vector spaces over a field $K$, and let $f : V \to V₂$ be a linear map. For any scalar $a \in K$, the kernel of the scaled linear map $a \cdot f$ is equal to the infimum of the kernel of $f$ over all proofs that $a \neq 0$, i.e., \[ \ker(a \cdot f) = \bigsqcap_{h : a \neq 0} \ker f. \]

Submodule.comap_bot theorem

(f : F) : comap f ⊥ = ker f

Full source

@[simp]
theorem comap_bot (f : F) : comap f ⊥ = ker f :=
  rfl

Kernel as Pullback of Zero Submodule

Informal description

For any semilinear map $ f : M \to M₂ $ between modules over semirings $ R $ and $ R₂ $ (connected by a ring homomorphism $ \sigma₁₂ : R \to R₂ $), the pullback of the zero submodule along $ f $ equals the kernel of $ f $. That is, \[ \text{comap } f \ \{0\} = \text{ker } f. \]

Submodule.ker_subtype theorem

: ker p.subtype = ⊥

Full source

@[simp]
theorem ker_subtype : ker p.subtype = ⊥ :=
  ker_eq_bot_of_injective fun _ _ => Subtype.ext_val

Trivial Kernel of Submodule Inclusion Map

Informal description

For any submodule $p$ of a module $M$ over a semiring $R$, the kernel of the inclusion map $p \hookrightarrow M$ is the trivial submodule $\{0\}$.

Submodule.ker_inclusion theorem

(p p' : Submodule R M) (h : p ≤ p') : ker (inclusion h) = ⊥

Full source

@[simp]
theorem ker_inclusion (p p' : Submodule R M) (h : p ≤ p') : ker (inclusion h) = ⊥ := by
  rw [inclusion, ker_codRestrict, ker_subtype]

Trivial Kernel of Submodule Inclusion Map

Informal description

For any submodules $p$ and $p'$ of an $R$-module $M$ with $p \subseteq p'$, the kernel of the inclusion map $\text{inclusion} \colon p \to p'$ is the trivial submodule $\{0\}$.

LinearMap.ker_comp_of_ker_eq_bot theorem

 (f : M →ₛₗ[τ₁₂] M₂) {g : M₂ →ₛₗ[τ₂₃] M₃} (hg : ker g = ⊥) : ker (g.comp f : M →ₛₗ[τ₁₃] M₃) = ker f

Full source

theorem ker_comp_of_ker_eq_bot (f : M →ₛₗ[τ₁₂] M₂) {g : M₂ →ₛₗ[τ₂₃] M₃} (hg : ker g = ⊥) :
    ker (g.comp f : M →ₛₗ[τ₁₃] M₃) = ker f := by rw [ker_comp, hg, Submodule.comap_bot]

Kernel of Composition with Injective Map Equals Original Kernel

Informal description

Let $f \colon M \to M₂$ and $g \colon M₂ \to M₃$ be semilinear maps between modules. If the kernel of $g$ is trivial (i.e., $\ker g = \{0\}$), then the kernel of the composition $g \circ f$ equals the kernel of $f$, i.e., \[ \ker(g \circ f) = \ker f. \]

LinearEquiv.ker theorem

: LinearMap.ker (e : M →ₛₗ[σ₁₂] M₂) = ⊥

Full source

@[simp]
protected theorem ker : LinearMap.ker (e : M →ₛₗ[σ₁₂] M₂) = ⊥ :=
  LinearMap.ker_eq_bot_of_injective e.toEquiv.injective

Kernel of a Linear Equivalence is Trivial

Informal description

For any linear equivalence (semilinear isomorphism) $e \colon M \to M_2$ between modules over semirings with respect to a ring homomorphism $\sigma_{12} \colon R \to S$, the kernel of $e$ is the trivial submodule $\{0\}$.

LinearEquiv.ker_comp theorem

 (l : M →ₛₗ[σ₁₂] M₂) : LinearMap.ker (((e'' : M₂ →ₛₗ[σ₂₃] M₃).comp l : M →ₛₗ[σ₁₃] M₃) : M →ₛₗ[σ₁₃] M₃) = LinearMap.ker l

Full source

@[simp]
theorem ker_comp (l : M →ₛₗ[σ₁₂] M₂) :
    LinearMap.ker (((e'' : M₂ →ₛₗ[σ₂₃] M₃).comp l : M →ₛₗ[σ₁₃] M₃) : M →ₛₗ[σ₁₃] M₃) =
    LinearMap.ker l :=
  LinearMap.ker_comp_of_ker_eq_bot _ e''.ker

Kernel Preservation under Composition with Linear Equivalence

Informal description

Let $l \colon M \to M_2$ be a semilinear map between modules over semirings with respect to a ring homomorphism $\sigma_{12} \colon R \to S$, and let $e'' \colon M_2 \to M_3$ be a linear equivalence (semilinear isomorphism) with respect to a ring homomorphism $\sigma_{23} \colon S \to T$. Then the kernel of the composition $e'' \circ l \colon M \to M_3$ equals the kernel of $l$, i.e., \[ \ker(e'' \circ l) = \ker l. \]

Mathlib.Algebra.Module.Submodule.Ker

Main definitions

Notations

Tags