mathlib documentation

linear_algebra.smodeq

modular equivalence for submodule

def smodeq {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] :
submodule R MM → M → Prop

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

Equations
theorem smodeq.def {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {U : submodule R M} {x y : M} :

@[simp]
theorem smodeq.top {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {x y : M} :

@[simp]
theorem smodeq.bot {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {x y : M} :
x y [SMOD ] x = y

theorem smodeq.mono {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {U₁ U₂ : submodule R M} {x y : M} :
U₁ U₂x y [SMOD U₁]x y [SMOD U₂]

theorem smodeq.refl {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {U : submodule R M} {x : M} :
x x [SMOD U]

theorem smodeq.symm {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {U : submodule R M} {x y : M} :
x y [SMOD U]y x [SMOD U]

theorem smodeq.trans {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {U : submodule R M} {x y z : M} :
x y [SMOD U]y z [SMOD U]x z [SMOD U]

theorem smodeq.add {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {U : submodule R M} {x₁ x₂ y₁ y₂ : M} :
x₁ y₁ [SMOD U]x₂ y₂ [SMOD U]x₁ + x₂ y₁ + y₂ [SMOD U]

theorem smodeq.smul {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group 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.zero {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group 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} [add_comm_group M] [module R M] {U : submodule R M} {x y : M} {N : Type u_3} [add_comm_group N] [module R N] (hxy : x y [SMOD U]) (f : M →ₗ[R] N) :

theorem smodeq.comap {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {x y : M} {N : Type u_3} [add_comm_group N] [module R N] (V : submodule R N) {f : M →ₗ[R] N} :
f x f y [SMOD V]x y [SMOD submodule.comap f V]