HepLean Documentation

Mathlib.LinearAlgebra.SModEq

modular equivalence for submodule #

def SModEq {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] (U : Submodule R M) (x 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_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x 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_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y : M} :

x ≡ y [SMOD U] ↔ x - y ∈ U

@[simp]

theorem SModEq.top {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {x y : M} :

x ≡ y [SMOD ⊤]

@[simp]

theorem SModEq.bot {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {x y : M} :

x ≡ y [SMOD ⊥] ↔ x = y

theorem SModEq.mono {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U₁ U₂ : Submodule R M} {x 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_3} [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_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x : M} :

x ≡ x [SMOD U]

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

⋯ = ⋯

theorem SModEq.symm {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y : M} (hxy : x ≡ y [SMOD U]) :

y ≡ x [SMOD U]

theorem SModEq.trans {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y z : M} (hxy : x ≡ y [SMOD U]) (hyz : y ≡ z [SMOD U]) :

x ≡ z [SMOD U]

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 := ⋯ }

theorem SModEq.add {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x₁ x₂ y₁ 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_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y : M} (hxy : x ≡ y [SMOD U]) (c : R) :

c • x ≡ c • y [SMOD U]

theorem SModEq.nsmul {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y : M} (hxy : x ≡ y [SMOD U]) (n : ℕ) :

n • x ≡ n • y [SMOD U]

theorem SModEq.zsmul {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y : M} (hxy : x ≡ y [SMOD U]) (n : ℤ) :

n • x ≡ n • y [SMOD U]

theorem SModEq.mul {A : Type u_2} [CommRing A] {I : Ideal A} {x₁ x₂ y₁ y₂ : A} (hxy₁ : x₁ ≡ y₁ [SMOD I]) (hxy₂ : x₂ ≡ y₂ [SMOD I]) :

x₁ * x₂ ≡ y₁ * y₂ [SMOD I]

theorem SModEq.pow {A : Type u_2} [CommRing A] {I : Ideal A} {x y : A} (n : ℕ) (hxy : x ≡ y [SMOD I]) :

x ^ n ≡ y ^ n [SMOD I]

theorem SModEq.neg {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x y : M} (hxy : x ≡ y [SMOD U]) :

-x ≡ -y [SMOD U]

theorem SModEq.sub {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x₁ x₂ y₁ y₂ : M} (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) :

x₁ - x₂ ≡ y₁ - y₂ [SMOD U]

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

theorem SModEq.map {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {U : Submodule R M} {x 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]

theorem SModEq.comap {R : Type u_1} [Ring R] {M : Type u_3} [AddCommGroup M] [Module R M] {x 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]

theorem SModEq.eval {R : Type u_5} [CommRing R] {I : Ideal R} {x y : R} (h : x ≡ y [SMOD I]) (f : Polynomial R) :

Polynomial.eval x f ≡ Polynomial.eval y f [SMOD I]