# mathlibdocumentation

linear_algebra.quotient

# Quotients by submodules #

• If p is a submodule of M, M ⧸ p is the quotient of M with respect to p: that is, elements of M are identified if their difference is in p. This is itself a module.
def submodule.quotient_rel {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) :

The equivalence relation associated to a submodule p, defined by x ≈ y iff -x + y ∈ p.

Note this is equivalent to y - x ∈ p, but defined this way to be be defeq to the add_subgroup version, where commutativity can't be assumed.

Equations
theorem submodule.quotient_rel_r_def {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {x y : M} :
y x - y p
@[protected, instance]
def submodule.has_quotient {R : Type u_1} {M : Type u_2} [ring R] [ M] :
M)

The quotient of a module M by a submodule p ⊆ M.

Equations
def submodule.quotient.mk {R : Type u_1} {M : Type u_2} [ring R] [ M] {p : M} :
M → M p

Map associating to an element of M the corresponding element of M/p, when p is a submodule of M.

Equations
@[simp]
theorem submodule.quotient.mk_eq_mk {R : Type u_1} {M : Type u_2} [ring R] [ M] {p : M} (x : M) :
@[simp]
theorem submodule.quotient.mk'_eq_mk {R : Type u_1} {M : Type u_2} [ring R] [ M] {p : M} (x : M) :
@[simp]
theorem submodule.quotient.quot_mk_eq_mk {R : Type u_1} {M : Type u_2} [ring R] [ M] {p : M} (x : M) :
quot.mk setoid.r x =
@[protected]
theorem submodule.quotient.eq' {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {x y : M} :
-x + y p
@[protected]
theorem submodule.quotient.eq {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {x y : M} :
x - y p
@[protected, instance]
def submodule.quotient.has_quotient.quotient.has_zero {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) :
Equations
@[protected, instance]
def submodule.quotient.has_quotient.quotient.inhabited {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) :
Equations
@[simp]
theorem submodule.quotient.mk_zero {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) :
@[simp]
theorem submodule.quotient.mk_eq_zero {R : Type u_1} {M : Type u_2} {x : M} [ring R] [ M] (p : M) :
x p
@[protected, instance]
def submodule.quotient.add_comm_group {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) :
Equations
@[simp]
theorem submodule.quotient.mk_add {R : Type u_1} {M : Type u_2} {x y : M} [ring R] [ M] (p : M) :
@[simp]
theorem submodule.quotient.mk_neg {R : Type u_1} {M : Type u_2} {x : M} [ring R] [ M] (p : M) :
@[simp]
theorem submodule.quotient.mk_sub {R : Type u_1} {M : Type u_2} {x y : M} [ring R] [ M] (p : M) :
@[protected, instance]
def submodule.quotient.has_smul' {R : Type u_1} {M : Type u_2} [ring R] [ M] {S : Type u_3} [ R] [ M] [ M] (P : M) :
(M P)
Equations
@[protected, instance]
def submodule.quotient.has_smul {R : Type u_1} {M : Type u_2} [ring R] [ M] (P : M) :
(M P)

Shortcut to help the elaborator in the common case.

Equations
@[simp]
theorem submodule.quotient.mk_smul {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {S : Type u_3} [ R] [ M] [ M] (r : S) (x : M) :
@[protected, instance]
def submodule.quotient.smul_comm_class {R : Type u_1} {M : Type u_2} [ring R] [ M] {S : Type u_3} [ R] [ M] [ M] (P : M) (T : Type u_4) [ R] [ M] [ M] [ M] :
(M P)
@[protected, instance]
def submodule.quotient.is_scalar_tower {R : Type u_1} {M : Type u_2} [ring R] [ M] {S : Type u_3} [ R] [ M] [ M] (P : M) (T : Type u_4) [ R] [ M] [ M] [ T] [ M] :
(M P)
@[protected, instance]
def submodule.quotient.is_central_scalar {R : Type u_1} {M : Type u_2} [ring R] [ M] {S : Type u_3} [ R] [ M] [ M] (P : M) [ R] [ M] [ M] [ M] :
(M P)
@[protected, instance]
def submodule.quotient.mul_action' {R : Type u_1} {M : Type u_2} [ring R] [ M] {S : Type u_3} [monoid S] [ R] [ M] [ M] (P : M) :
(M P)
Equations
@[protected, instance]
def submodule.quotient.mul_action {R : Type u_1} {M : Type u_2} [ring R] [ M] (P : M) :
(M P)
Equations
@[protected, instance]
def submodule.quotient.distrib_mul_action' {R : Type u_1} {M : Type u_2} [ring R] [ M] {S : Type u_3} [monoid S] [ R] [ M] [ M] (P : M) :
(M P)
Equations
@[protected, instance]
def submodule.quotient.distrib_mul_action {R : Type u_1} {M : Type u_2} [ring R] [ M] (P : M) :
(M P)
Equations
@[protected, instance]
def submodule.quotient.module' {R : Type u_1} {M : Type u_2} [ring R] [ M] {S : Type u_3} [semiring S] [ R] [ M] [ M] (P : M) :
(M P)
Equations
@[protected, instance]
def submodule.quotient.module {R : Type u_1} {M : Type u_2} [ring R] [ M] (P : M) :
(M P)
Equations
def submodule.quotient.restrict_scalars_equiv {R : Type u_1} {M : Type u_2} [ring R] [ M] (S : Type u_3) [ring S] [ R] [ M] [ M] (P : M) :
(M ≃ₗ[S] M P

The quotient of P as an S-submodule is the same as the quotient of P as an R-submodule, where P : submodule R M.

Equations
@[simp]
theorem submodule.quotient.restrict_scalars_equiv_mk {R : Type u_1} {M : Type u_2} [ring R] [ M] (S : Type u_3) [ring S] [ R] [ M] [ M] (P : M) (x : M) :
@[simp]
theorem submodule.quotient.restrict_scalars_equiv_symm_mk {R : Type u_1} {M : Type u_2} [ring R] [ M] (S : Type u_3) [ring S] [ R] [ M] [ M] (P : M) (x : M) :
theorem submodule.quotient.mk_surjective {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) :
theorem submodule.quotient.nontrivial_of_lt_top {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) (h : p < ) :
theorem submodule.quot_hom_ext {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {M₂ : Type u_3} [add_comm_group M₂] [ M₂] ⦃f g : M p →ₗ[R] M₂⦄ (h : ∀ (x : M), = ) :
f = g
def submodule.mkq {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) :
M →ₗ[R] M p

The map from a module M to the quotient of M by a submodule p as a linear map.

Equations
@[simp]
theorem submodule.mkq_apply {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) (x : M) :
(p.mkq) x =
theorem submodule.mkq_surjective {R : Type u_1} {M : Type u_2} [ring R] [ M] (A : M) :
@[ext]
theorem submodule.linear_map_qext {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} ⦃f g : M p →ₛₗ[τ₁₂] M₂⦄ (h : f.comp p.mkq = g.comp p.mkq) :
f = g

Two linear_maps from a quotient module are equal if their compositions with submodule.mkq are equal.

def submodule.liftq {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : p ) :
M p →ₛₗ[τ₁₂] M₂

The map from the quotient of M by a submodule p to M₂ induced by a linear map f : M → M₂ vanishing on p, as a linear map.

Equations
@[simp]
theorem submodule.liftq_apply {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) {h : p } (x : M) :
(p.liftq f h) = f x
@[simp]
theorem submodule.liftq_mkq {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : p ) :
(p.liftq f h).comp p.mkq = f
def submodule.liftq_span_singleton {R : Type u_1} {M : Type u_2} [ring R] [ M] {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} (x : M) (f : M →ₛₗ[τ₁₂] M₂) (h : f x = 0) :
M {x} →ₛₗ[τ₁₂] M₂

Special case of liftq when p is the span of x. In this case, the condition on f simply becomes vanishing at x.

Equations
@[simp]
theorem submodule.liftq_span_singleton_apply {R : Type u_1} {M : Type u_2} [ring R] [ M] {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} (x : M) (f : M →ₛₗ[τ₁₂] M₂) (h : f x = 0) (y : M) :
= f y
@[simp]
theorem submodule.range_mkq {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) :
@[simp]
theorem submodule.ker_mkq {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) :
theorem submodule.le_comap_mkq {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) (p' : (M p)) :
p p'
@[simp]
theorem submodule.mkq_map_self {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) :
p =
@[simp]
theorem submodule.comap_map_mkq {R : Type u_1} {M : Type u_2} [ring R] [ M] (p p' : M) :
p') = p p'
@[simp]
theorem submodule.map_mkq_eq_top {R : Type u_1} {M : Type u_2} [ring R] [ M] (p p' : M) :
p' = p p' =
def submodule.mapq {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} (q : M₂) (f : M →ₛₗ[τ₁₂] M₂) (h : p ) :
M p →ₛₗ[τ₁₂] M₂ q

The map from the quotient of M by submodule p to the quotient of M₂ by submodule q along f : M → M₂ is linear.

Equations
@[simp]
theorem submodule.mapq_apply {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} (q : M₂) (f : M →ₛₗ[τ₁₂] M₂) {h : p } (x : M) :
(p.mapq q f h) =
theorem submodule.mapq_mkq {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} (q : M₂) (f : M →ₛₗ[τ₁₂] M₂) {h : p } :
(p.mapq q f h).comp p.mkq = q.mkq.comp f
@[simp]
theorem submodule.mapq_zero {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} (q : M₂) (h : p := _) :
p.mapq q 0 h = 0
theorem submodule.mapq_comp {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} {R₃ : Type u_5} {M₃ : Type u_6} [ring R₃] [add_comm_group M₃] [module R₃ M₃] (p₂ : M₂) (p₃ : M₃) {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) (hf : p p₂) (hg : p₂ p₃) (h : p p₃) := _) :
p.mapq p₃ (g.comp f) h = (p₂.mapq p₃ g hg).comp (p.mapq p₂ f hf)

Given submodules p ⊆ M, p₂ ⊆ M₂, p₃ ⊆ M₃ and maps f : M → M₂, g : M₂ → M₃ inducing mapq f : M ⧸ p → M₂ ⧸ p₂ and mapq g : M₂ ⧸ p₂ → M₃ ⧸ p₃ then mapq (g ∘ f) = (mapq g) ∘ (mapq f).

@[simp]
theorem submodule.mapq_id {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) (h : := _) :
theorem submodule.mapq_pow {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {f : M →ₗ[R] M} (h : p ) (k : ) (h' : p submodule.comap (f ^ k) p := _) :
p.mapq p (f ^ k) h' = p.mapq p f h ^ k
theorem submodule.comap_liftq {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} (q : M₂) (f : M →ₛₗ[τ₁₂] M₂) (h : p ) :
submodule.comap (p.liftq f h) q = q)
theorem submodule.map_liftq {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (h : p ) (q : (M p)) :
submodule.map (p.liftq f h) q = q)
theorem submodule.ker_liftq {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : p ) :
theorem submodule.range_liftq {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (h : p ) :
theorem submodule.ker_liftq_eq_bot {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : p ) (h' : p) :
def submodule.comap_mkq.rel_iso {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) :
(M p) ≃o {p' // p p'}

The correspondence theorem for modules: there is an order isomorphism between submodules of the quotient of M by p, and submodules of M larger than p.

Equations
def submodule.comap_mkq.order_embedding {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) :
(M p) ↪o M

The ordering on submodules of the quotient of M by p embeds into the ordering on submodules of M.

Equations
• = (λ (p' : M), p p'))
@[simp]
theorem submodule.comap_mkq_embedding_eq {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) (p' : (M p)) :
theorem submodule.span_preimage_eq {R : Type u_1} {M : Type u_2} [ring R] [ M] {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {s : set M₂} (h₀ : s.nonempty) (h₁ : s ) :
(f ⁻¹' s) = s)
theorem linear_map.range_mkq_comp {R : Type u_1} {M : Type u_2} {R₂ : Type u_3} {M₂ : Type u_4} [ring R] [ring R₂] [add_comm_group M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
.mkq.comp f = 0
theorem linear_map.ker_le_range_iff {R : Type u_1} {M : Type u_2} {R₂ : Type u_3} {M₂ : Type u_4} {R₃ : Type u_5} {M₃ : Type u_6} [ring R] [ring R₂] [ring R₃] [add_comm_group M₂] [add_comm_monoid M₃] [ M] [module R₂ M₂] [module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₃] M₃} :
theorem linear_map.range_eq_top_of_cancel {R : Type u_1} {M : Type u_2} {R₂ : Type u_3} {M₂ : Type u_4} [ring R] [ring R₂] [add_comm_group M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} (h : ∀ (u v : M₂ →ₗ[R₂] M₂ , u.comp f = v.comp fu = v) :

An epimorphism is surjective.

def submodule.quot_equiv_of_eq_bot {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) (hp : p = ) :
(M p) ≃ₗ[R] M

If p = ⊥, then M / p ≃ₗ[R] M.

Equations
• = _ _
@[simp]
theorem submodule.quot_equiv_of_eq_bot_apply_mk {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) (hp : p = ) (x : M) :
@[simp]
theorem submodule.quot_equiv_of_eq_bot_symm_apply {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) (hp : p = ) (x : M) :
@[simp]
theorem submodule.coe_quot_equiv_of_eq_bot_symm {R : Type u_1} {M : Type u_2} [ring R] [ M] (p : M) (hp : p = ) :
def submodule.quot_equiv_of_eq {R : Type u_1} {M : Type u_2} [ring R] [ M] (p p' : M) (h : p = p') :
(M p) ≃ₗ[R] M p'

Quotienting by equal submodules gives linearly equivalent quotients.

Equations
@[simp]
theorem submodule.quot_equiv_of_eq_mk {R : Type u_1} {M : Type u_2} [ring R] [ M] (p p' : M) (h : p = p') (x : M) :
def submodule.mapq_linear {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [comm_ring R] [ M] [add_comm_group M₂] [ M₂] (p : M) (q : M₂) :

Given modules M, M₂ over a commutative ring, together with submodules p ⊆ M, q ⊆ M₂, the natural map $\{f ∈ Hom(M, M₂) | f(p) ⊆ q \} \to Hom(M/p, M₂/q)$ is linear.

Equations