modular equivalence for submodule #
def
smodeq
{R : Type u_1}
[ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
(U : submodule R M)
(x y : 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)
Instances for smodeq
@[protected]
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} :
@[protected, refl]
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) :
@[protected]
theorem
smodeq.rfl
{R : Type u_1}
[ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{U : submodule R M}
{x : M} :
@[protected, instance]
def
smodeq.is_refl
{R : Type u_1}
[ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{U : submodule R 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}
(hxy : ⇑f x ≡ ⇑f y [SMOD V]) :
x ≡ y [SMOD submodule.comap f V]
theorem
smodeq.eval
{R : Type u_1}
[comm_ring 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]