Documentation

Mathlib.LinearAlgebra.SModEq

modular equivalence for submodule #

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

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

Equations

(x ≡ y [SMOD U]) = (Submodule.Quotient.mk x = Submodule.Quotient.mk y)

Instances For

def «term_≡_[SMOD_]» :

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

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

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

@[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 ⊤]

@[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

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₂]

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]

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]

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

@SModEq.instIsReflSModEq = @SModEq.instIsReflSModEq.proof_1

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]

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]

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]

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]

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

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]

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]

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]