mathlib3 documentation

linear_algebra.smodeq

modular equivalence for submodule #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
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
Instances for smodeq
source
@[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
source
theorem smodeq.sub_mem {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] ↔ x - y ∈ U
source
@[simp]
theorem smodeq.top {R : Type u_1} [ring R] {M : Type u_2} [add_comm_group M] [module R M] {x y : M} :
x ≡ y [SMOD ⊤]
source
@[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
source
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} (HU : U₁ ≤ U₂) (hxy : x ≡ y [SMOD U₁]) :
x ≡ y [SMOD U₂]
source
@[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) :
x ≡ x [SMOD U]
source
@[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} :
x ≡ x [SMOD U]
source
@[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} :
is_refl M (smodeq U)
source
@[symm]
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} (hxy : x ≡ y [SMOD U]) :
y ≡ x [SMOD U]
source
@[trans]
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} (hxy : x ≡ y [SMOD U]) (hyz : y ≡ z [SMOD U]) :
x ≡ z [SMOD U]
source
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} (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) :
x₁ + x₂ ≡ y₁ + y₂ [SMOD U]
source
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]
source
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
source
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) :
⇑f x ≡ ⇑f y [SMOD submodule.map f U]
source
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]
source
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]