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₂andM →ₗ[R] M₂for the type of semilinear (resp. linear) maps fromMtoM₂over the ring homomorphismσ(resp. over the ringR).
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]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_12}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
(f : F)
:
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
@[simp]
theorem
LinearMap.mem_ker
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_12}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
{y : M}
:
y ∈ LinearMap.ker f ↔ f y = 0
@[simp]
theorem
LinearMap.ker_id
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[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]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_12}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
(f : F)
(x : ↥(LinearMap.ker f))
:
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]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
(f : M →ₛₗ[τ₁₂] M₂)
:
(LinearMap.ker f).toAddSubmonoid = AddMonoidHom.mker f
theorem
LinearMap.comp_ker_subtype
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
(f : M →ₛₗ[τ₁₂] M₂)
:
LinearMap.comp f (Submodule.subtype (LinearMap.ker f)) = 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₂]
[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₃)
:
LinearMap.ker (LinearMap.comp g f) = Submodule.comap f (LinearMap.ker g)
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₂]
[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₃)
:
LinearMap.ker f ≤ LinearMap.ker (LinearMap.comp g f)
theorem
LinearMap.ker_sup_ker_le_ker_comp_of_commute
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{f : M →ₗ[R] M}
{g : M →ₗ[R] M}
(h : Commute f g)
:
LinearMap.ker f ⊔ LinearMap.ker 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]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{p : Submodule R₂ M₂}
(f : M →ₛₗ[τ₁₂] M₂)
:
LinearMap.ker f ≤ Submodule.comap f p
theorem
LinearMap.disjoint_ker
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_12}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
{p : Submodule R M}
:
Disjoint p (LinearMap.ker f) ↔ ∀ x ∈ p, f x = 0 → x = 0
theorem
LinearMap.ker_eq_bot'
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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_of_inverse
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[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 : LinearMap.comp g f = LinearMap.id)
:
LinearMap.ker f = ⊥
theorem
LinearMap.le_ker_iff_map
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_12}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
{f : F}
{p : Submodule R M}
:
p ≤ LinearMap.ker f ↔ Submodule.map f p = ⊥
theorem
LinearMap.ker_codRestrict
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[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)
:
LinearMap.ker (LinearMap.codRestrict p f hf) = LinearMap.ker f
theorem
LinearMap.ker_restrict
{R : Type u_1}
{M : Type u_6}
{M₁ : Type u_7}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₁]
[Module R M₁]
{p : Submodule R M}
{q : Submodule R M₁}
{f : M →ₗ[R] M₁}
(hf : ∀ x ∈ p, f x ∈ q)
:
LinearMap.ker (LinearMap.restrict f hf) = LinearMap.ker (LinearMap.domRestrict f p)
@[simp]
theorem
LinearMap.ker_zero
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
:
LinearMap.ker 0 = ⊤
theorem
LinearMap.ker_eq_top
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{f : M →ₛₗ[τ₁₂] M₂}
:
LinearMap.ker f = ⊤ ↔ f = 0
@[simp]
theorem
AddMonoidHom.coe_toIntLinearMap_ker
{M : Type u_13}
{M₂ : Type u_14}
[AddCommGroup M]
[AddCommGroup M₂]
(f : M →+ M₂)
:
LinearMap.ker (AddMonoidHom.toIntLinearMap f) = AddSubgroup.toIntSubmodule (AddMonoidHom.ker f)
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]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_12}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
(hf : Function.Injective ⇑f)
:
LinearMap.ker f = ⊥
@[simp]
theorem
LinearMap.iterateKer_coe
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(f : M →ₗ[R] M)
(n : ℕ)
:
(LinearMap.iterateKer f) n = LinearMap.ker (f ^ n)
def
LinearMap.iterateKer
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(f : M →ₗ[R] M)
:
The increasing sequence of submodules consisting of the kernels of the iterates of a linear map.
Equations
- LinearMap.iterateKer f = { toFun := fun (n : ℕ) => LinearMap.ker (f ^ n), monotone' := ⋯ }
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₂]
[AddCommGroup M]
[AddCommGroup M₂]
[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₂]
[AddCommGroup M]
[AddCommGroup M₂]
[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 ∈ LinearMap.ker f ↔ 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₂]
[AddCommGroup M]
[AddCommGroup M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_12}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
{p : Submodule R M}
:
Disjoint p (LinearMap.ker f) ↔ ∀ x ∈ p, ∀ y ∈ p, f x = f y → x = 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₂]
[AddCommGroup M]
[AddCommGroup M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_12}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
{p : Submodule R M}
{s : Set M}
(h : s ⊆ ↑p)
(hd : Disjoint p (LinearMap.ker f))
:
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₂]
[AddCommGroup M]
[AddCommGroup M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
(F : Type u_12)
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
:
LinearMap.ker f = ⊥ ↔ Function.Injective ⇑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₂]
[AddCommGroup M]
[AddCommGroup M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{f : M →ₛₗ[τ₁₂] M₂}
:
LinearMap.ker f = ⊥ ↔ Function.Injective ⇑f
@[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₂]
[AddCommGroup M]
[AddCommGroup M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{f : M →ₛₗ[τ₁₂] M₂}
{S : Submodule R M}
:
Function.Injective ⇑(LinearMap.domRestrict f S) ↔ S ⊓ LinearMap.ker f = ⊥
@[simp]
theorem
LinearMap.injective_restrict_iff_disjoint
{R : Type u_1}
{M : Type u_6}
[Ring R]
[AddCommGroup M]
[Module R M]
{p : Submodule R M}
{f : M →ₗ[R] M}
(hf : ∀ x ∈ p, f x ∈ p)
:
Function.Injective ⇑(LinearMap.restrict f hf) ↔ Disjoint p (LinearMap.ker f)
theorem
LinearMap.ker_smul
{K : Type u_5}
{V : Type u_10}
{V₂ : Type u_11}
[Semifield K]
[AddCommMonoid V]
[Module K V]
[AddCommMonoid V₂]
[Module K V₂]
(f : V →ₗ[K] V₂)
(a : K)
(h : a ≠ 0)
:
LinearMap.ker (a • f) = LinearMap.ker f
theorem
LinearMap.ker_smul'
{K : Type u_5}
{V : Type u_10}
{V₂ : Type u_11}
[Semifield K]
[AddCommMonoid V]
[Module K V]
[AddCommMonoid V₂]
[Module K V₂]
(f : V →ₗ[K] V₂)
(a : K)
:
LinearMap.ker (a • f) = ⨅ (_ : a ≠ 0), LinearMap.ker f
@[simp]
theorem
Submodule.comap_bot
{R : Type u_1}
{R₂ : Type u_3}
{M : Type u_6}
{M₂ : Type u_8}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[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}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
:
@[simp]
theorem
Submodule.ker_inclusion
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
(p' : Submodule R M)
(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₂]
[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 : LinearMap.ker g = ⊥)
:
LinearMap.ker (LinearMap.comp g f) = LinearMap.ker 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]
[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₂)
:
LinearMap.ker ↑e = ⊥
@[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₂]
[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₂)
:
LinearMap.ker (LinearMap.comp (↑e'') l) = LinearMap.ker l