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 M → M → M → Prop
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)
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} :
x ≡ y [SMOD U] ↔ submodule.quotient.mk x = submodule.quotient.mk y
@[simp]
theorem
smodeq.top
{R : Type u_1}
[ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{x y : M} :
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} :
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} :