Documentation

Mathlib.LinearAlgebra.SModEq

modular equivalence for submodule #

source
def SModEq {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] (U : Submodule R M) (x : M) (y : M) :
Prop

A predicate saying two elements of a module are equivalent modulo a submodule.

Equations
Instances For
    source
    theorem SModEq.def {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} {y : M} :
    x ≡ y [SMOD U] ↔ Submodule.Quotient.mk x = Submodule.Quotient.mk y
    source
    theorem SModEq.sub_mem {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} {y : M} :
    x ≡ y [SMOD U] ↔ x - y ∈ U
    source
    @[simp]
    theorem SModEq.top {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {x : M} {y : M} :
    x ≡ y [SMOD ⊤]
    source
    @[simp]
    theorem SModEq.bot {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {x : M} {y : M} :
    x ≡ y [SMOD ⊥] ↔ x = y
    source
    theorem SModEq.mono {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U₁ : Submodule R M} {U₂ : Submodule R M} {x : M} {y : M} (HU : U₁ ≤ U₂) (hxy : x ≡ y [SMOD U₁]) :
    x ≡ y [SMOD U₂]
    source
    theorem SModEq.refl {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} (x : M) :
    x ≡ x [SMOD U]
    source
    theorem SModEq.rfl {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} :
    x ≡ x [SMOD U]
    source
    instance SModEq.instIsRefl {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} :
    IsRefl M (SModEq U)
    Equations
    • ⋯ = ⋯
    source
    theorem SModEq.symm {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} {y : M} (hxy : x ≡ y [SMOD U]) :
    y ≡ x [SMOD U]
    source
    theorem SModEq.trans {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} {y : M} {z : M} (hxy : x ≡ y [SMOD U]) (hyz : y ≡ z [SMOD U]) :
    x ≡ z [SMOD U]
    source
    instance SModEq.instTrans {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} :
    Trans (SModEq U) (SModEq U) (SModEq U)
    Equations
    • SModEq.instTrans = { trans := ⋯ }
    source
    theorem SModEq.add {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x₁ : M} {x₂ : M} {y₁ : M} {y₂ : M} (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) :
    x₁ + x₂ ≡ y₁ + y₂ [SMOD U]
    source
    theorem SModEq.smul {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} {y : M} (hxy : x ≡ y [SMOD U]) (c : R) :
    c • x ≡ c • y [SMOD U]
    source
    theorem SModEq.nsmul {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} {y : M} (hxy : x ≡ y [SMOD U]) (n : ℕ) :
    n • x ≡ n • y [SMOD U]
    source
    theorem SModEq.zsmul {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} {y : M} (hxy : x ≡ y [SMOD U]) (n : ℤ) :
    n • x ≡ n • y [SMOD U]
    source
    theorem SModEq.mul {A : Type u_2} [CommRing A] {I : Ideal A} {x₁ : A} {x₂ : A} {y₁ : A} {y₂ : A} (hxy₁ : x₁ ≡ y₁ [SMOD I]) (hxy₂ : x₂ ≡ y₂ [SMOD I]) :
    x₁ * x₂ ≡ y₁ * y₂ [SMOD I]
    source
    theorem SModEq.pow {A : Type u_2} [CommRing A] {I : Ideal A} {x : A} {y : A} (n : ℕ) (hxy : x ≡ y [SMOD I]) :
    x ^ n ≡ y ^ n [SMOD I]
    source
    theorem SModEq.neg {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} {y : M} (hxy : x ≡ y [SMOD U]) :
    -x ≡ -y [SMOD U]
    source
    theorem SModEq.sub {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x₁ : M} {x₂ : M} {y₁ : M} {y₂ : M} (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) :
    x₁ - x₂ ≡ y₁ - y₂ [SMOD U]
    source
    theorem SModEq.zero {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} :
    x ≡ 0 [SMOD U] ↔ x ∈ U
    source
    theorem SModEq.map {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} {y : M} {N : Type u_4} [AddCommGroup N] [Module R N] (hxy : x ≡ y [SMOD U]) (f : M →ₗ[R] N) :
    f x ≡ f y [SMOD Submodule.map f U]
    source
    theorem SModEq.comap {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {x : M} {y : M} {N : Type u_4} [AddCommGroup N] [Module R N] (V : Submodule R N) {f : M →ₗ[R] N} (hxy : f x ≡ f y [SMOD V]) :
    x ≡ y [SMOD Submodule.comap f V]
    source
    theorem SModEq.eval {R : Type u_5} [CommRing R] {I : Ideal R} {x : R} {y : R} (h : x ≡ y [SMOD I]) (f : Polynomial R) :
    Polynomial.eval x f ≡ Polynomial.eval y f [SMOD I]