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 #

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) :

A linear map version of AddMonoidHom.eqLocusM

Equations
  • LinearMap.eqLocus f 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} :
    @[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) :
    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) :
    Set.EqOn f g (S 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₂) :