Documentation

Mathlib.LinearAlgebra.SModEq

modular equivalence for submodule #

source
def SModEq {R : Type u_1} [Ring R] {M : Type u_2} [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
    def «term_≡_[SMOD_]» :
    Lean.TrailingParserDescr
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem SModEq.def' {R : Type u_1} [Ring R] {M : Type u_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} :
      x ≡ x [SMOD U]
      source
      instance SModEq.instIsReflSModEq {R : Type u_1} [Ring R] {M : Type u_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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.zero {R : Type u_1} [Ring R] {M : Type u_2} [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_2} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} {y : M} {N : Type u_3} [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_2} [AddCommGroup M] [Module R M] {x : M} {y : M} {N : Type u_3} [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_4} [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]