Documentation

Mathlib.Algebra.Module.Submodule.EqLocus

The submodule of elements x : M such that f x = g x #

Main declarations #

Tags #

linear algebra, vector space, module

Properties of linear maps #

source
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 g : M →ₛₗ[τ₁₂] M₂) :
Submodule R M

A linear map version of AddMonoidHom.eqLocusM

Equations
  • f.eqLocus g = { carrier := {x : M | f x = g x}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
    source
    @[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₂} {x : M} {f g : M →ₛₗ[τ₁₂] M₂} :
    x ∈ f.eqLocus g ↔ f x = g x
    source
    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 g : M →ₛₗ[τ₁₂] M₂) :
    (f.eqLocus g).toAddSubmonoid = (↑f).eqLocusM ↑g
    source
    @[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 g : M →ₛₗ[τ₁₂] M₂} :
    f.eqLocus g = ⊤ ↔ f = g
    source
    @[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 : M →ₛₗ[τ₁₂] M₂) :
    f.eqLocus f = ⊤
    source
    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 g : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} :
    S ≤ f.eqLocus g ↔ Set.EqOn ⇑f ⇑g ↑S
    source
    theorem LinearMap.eqOn_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 g : M →ₛₗ[τ₁₂] M₂} :
    Set.EqOn ⇑f ⇑g ↑(f.eqLocus g)
    source
    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 g : F} {S T : Submodule R M} (hS : Set.EqOn ⇑f ⇑g ↑S) (hT : Set.EqOn ⇑f ⇑g ↑T) :
    Set.EqOn ⇑f ⇑g ↑(S ⊔ T)
    source
    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 g : F} {S T : Submodule R M} (hST : Codisjoint S T) (hS : Set.EqOn ⇑f ⇑g ↑S) (hT : Set.EqOn ⇑f ⇑g ↑T) :
    f = g
    source
    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 g : M →ₛₗ[τ₁₂] M₂) :
    f.eqLocus g = (f - g).ker