The submodule of elements x : M such that f x = g x #
Main declarations #
LinearMap.eqLocus: the submodule of elementsx : Msuch thatf x = g x
Tags #
linear algebra, vector space, module
Properties of linear maps #
def
LinearMap.eqLocus
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_3}
{M₂ : Type u_4}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_5}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
(f : F)
(g : F)
:
Submodule R M
A linear map version of AddMonoidHom.eqLocusM
Equations
- LinearMap.eqLocus f g = let __src := (↑f).eqLocusM ↑g; { carrier := {x : M | f x = g x}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
@[simp]
theorem
LinearMap.mem_eqLocus
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_3}
{M₂ : Type u_4}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_5}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{x : M}
{f : F}
{g : F}
:
x ∈ LinearMap.eqLocus f g ↔ f x = g x
theorem
LinearMap.eqLocus_toAddSubmonoid
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_3}
{M₂ : Type u_4}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_5}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
(f : F)
(g : F)
:
(LinearMap.eqLocus f g).toAddSubmonoid = (↑f).eqLocusM ↑g
@[simp]
theorem
LinearMap.eqLocus_eq_top
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_3}
{M₂ : Type u_4}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_5}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
{g : F}
:
LinearMap.eqLocus f g = ⊤ ↔ f = g
@[simp]
theorem
LinearMap.eqLocus_same
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_3}
{M₂ : Type u_4}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_5}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
(f : F)
:
LinearMap.eqLocus f f = ⊤
theorem
LinearMap.le_eqLocus
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_3}
{M₂ : Type u_4}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_5}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
{g : F}
{S : Submodule R M}
:
S ≤ LinearMap.eqLocus f g ↔ Set.EqOn ⇑f ⇑g ↑S
theorem
LinearMap.eqOn_sup
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_3}
{M₂ : Type u_4}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_5}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
{g : F}
{S : Submodule R M}
{T : Submodule R M}
(hS : Set.EqOn ⇑f ⇑g ↑S)
(hT : Set.EqOn ⇑f ⇑g ↑T)
:
theorem
LinearMap.ext_on_codisjoint
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_3}
{M₂ : Type u_4}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_5}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
{g : F}
{S : Submodule R M}
{T : Submodule R M}
(hST : Codisjoint S T)
(hS : Set.EqOn ⇑f ⇑g ↑S)
(hT : Set.EqOn ⇑f ⇑g ↑T)
:
f = g
theorem
LinearMap.eqLocus_eq_ker_sub
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_3}
{M₂ : Type u_4}
[Ring R]
[Ring R₂]
[AddCommGroup M]
[AddCommGroup M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
(f : M →ₛₗ[τ₁₂] M₂)
(g : M →ₛₗ[τ₁₂] M₂)
:
LinearMap.eqLocus f g = LinearMap.ker (f - g)