mathlib documentation

linear_algebra.quotient

Quotients by submodules #

def submodule.quotient_rel {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :

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

Equations
@[protected, instance]
def submodule.has_quotient {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R 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] [add_comm_group M] [module R M] {p : submodule R 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] [add_comm_group M] [module R M] {p : submodule R M} (x : M) :
@[simp]
theorem submodule.quotient.mk'_eq_mk {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {p : submodule R M} (x : M) :
@[simp]
theorem submodule.quotient.quot_mk_eq_mk {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {p : submodule R M} (x : M) :
@[protected]
theorem submodule.quotient.eq {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) {x y : M} :
@[protected, instance]
def submodule.quotient.has_quotient.quotient.has_zero {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
Equations
@[protected, instance]
def submodule.quotient.has_quotient.quotient.inhabited {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
Equations
@[simp]
theorem submodule.quotient.mk_zero {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
@[simp]
theorem submodule.quotient.mk_eq_zero {R : Type u_1} {M : Type u_2} {x : M} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
@[protected, instance]
def submodule.quotient.has_quotient.quotient.has_add {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
has_add (M p)
Equations
@[simp]
theorem submodule.quotient.mk_add {R : Type u_1} {M : Type u_2} {x y : M} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
@[protected, instance]
def submodule.quotient.has_quotient.quotient.has_neg {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
has_neg (M p)
Equations
@[simp]
theorem submodule.quotient.mk_neg {R : Type u_1} {M : Type u_2} {x : M} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
@[protected, instance]
def submodule.quotient.has_quotient.quotient.has_sub {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
has_sub (M p)
Equations
@[simp]
theorem submodule.quotient.mk_sub {R : Type u_1} {M : Type u_2} {x y : M} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
@[protected, instance]
def submodule.quotient.has_scalar' {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {S : Type u_3} [has_scalar S R] [has_scalar S M] [is_scalar_tower S R M] (P : submodule R M) :
has_scalar S (M P)
Equations
@[protected, instance]
def submodule.quotient.has_scalar {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (P : submodule R M) :
has_scalar R (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] [add_comm_group M] [module R M] (p : submodule R M) {S : Type u_3} [has_scalar S R] [has_scalar S M] [is_scalar_tower S R M] (r : S) (x : M) :
@[protected, instance]
def submodule.quotient.smul_comm_class {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {S : Type u_3} [has_scalar S R] [has_scalar S M] [is_scalar_tower S R M] (P : submodule R M) (T : Type u_4) [has_scalar T R] [has_scalar T M] [is_scalar_tower T R M] [smul_comm_class S T M] :
@[protected, instance]
def submodule.quotient.is_scalar_tower {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {S : Type u_3} [has_scalar S R] [has_scalar S M] [is_scalar_tower S R M] (P : submodule R M) (T : Type u_4) [has_scalar T R] [has_scalar T M] [is_scalar_tower T R M] [has_scalar S T] [is_scalar_tower S T M] :
@[protected, instance]
def submodule.quotient.is_central_scalar {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {S : Type u_3} [has_scalar S R] [has_scalar S M] [is_scalar_tower S R M] (P : submodule R M) [has_scalar Sᵐᵒᵖ R] [has_scalar Sᵐᵒᵖ M] [is_scalar_tower Sᵐᵒᵖ R M] [is_central_scalar S M] :
@[protected, instance]
def submodule.quotient.mul_action' {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {S : Type u_3} [monoid S] [has_scalar S R] [mul_action S M] [is_scalar_tower S R M] (P : submodule R M) :
mul_action S (M P)
Equations
@[protected, instance]
def submodule.quotient.mul_action {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (P : submodule R M) :
mul_action R (M P)
Equations
@[protected, instance]
def submodule.quotient.distrib_mul_action' {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {S : Type u_3} [monoid S] [has_scalar S R] [distrib_mul_action S M] [is_scalar_tower S R M] (P : submodule R M) :
Equations
@[protected, instance]
def submodule.quotient.distrib_mul_action {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (P : submodule R M) :
Equations
@[protected, instance]
def submodule.quotient.module' {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {S : Type u_3} [semiring S] [has_scalar S R] [module S M] [is_scalar_tower S R M] (P : submodule R M) :
module S (M P)
Equations
@[protected, instance]
def submodule.quotient.module {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (P : submodule R M) :
module R (M P)
Equations
def submodule.quotient.restrict_scalars_equiv {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (S : Type u_3) [ring S] [has_scalar S R] [module S M] [is_scalar_tower S R M] (P : submodule R M) :

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] [add_comm_group M] [module R M] (S : Type u_3) [ring S] [has_scalar S R] [module S M] [is_scalar_tower S R M] (P : submodule R M) (x : M) :
@[simp]
theorem submodule.quotient.restrict_scalars_equiv_symm_mk {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (S : Type u_3) [ring S] [has_scalar S R] [module S M] [is_scalar_tower S R M] (P : submodule R M) (x : M) :
theorem submodule.quotient.mk_surjective {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
theorem submodule.quotient.nontrivial_of_lt_top {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) (h : p < ) :
theorem submodule.quot_hom_ext {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) {M₂ : Type u_3} [add_comm_group M₂] [module R M₂] ⦃f g : M p →ₗ[R] M₂⦄ (h : ∀ (x : M), f (submodule.quotient.mk x) = g (submodule.quotient.mk x)) :
f = g
def submodule.mkq {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R 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] [add_comm_group M] [module R M] (p : submodule R M) (x : M) :
@[ext]
theorem submodule.linear_map_qext {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R 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.

See note [partially-applied ext lemmas].

def submodule.liftq {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R 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 f.ker) :
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] [add_comm_group M] [module R M] (p : submodule R 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 f.ker} (x : M) :
@[simp]
theorem submodule.liftq_mkq {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R 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 f.ker) :
(p.liftq f h).comp p.mkq = f
@[simp]
theorem submodule.range_mkq {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
@[simp]
theorem submodule.ker_mkq {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
p.mkq.ker = p
theorem submodule.le_comap_mkq {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) (p' : submodule R (M p)) :
@[simp]
theorem submodule.mkq_map_self {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
@[simp]
theorem submodule.comap_map_mkq {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p p' : submodule R M) :
@[simp]
theorem submodule.map_mkq_eq_top {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p p' : submodule R M) :
def submodule.mapq {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} (q : submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (h : p submodule.comap f q) :
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] [add_comm_group M] [module R M] (p : submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} (q : submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) {h : p submodule.comap f q} (x : M) :
theorem submodule.mapq_mkq {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} (q : submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) {h : p submodule.comap f q} :
(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] [add_comm_group M] [module R M] (p : submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} (q : submodule R₂ M₂) (h : p submodule.comap 0 q := _) :
p.mapq q 0 h = 0
theorem submodule.mapq_comp {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R 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₂ : submodule R₂ M₂) (p₃ : submodule R₃ M₃) {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [ring_hom_comp_triple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) (hf : p submodule.comap f p₂) (hg : p₂ submodule.comap g p₃) (h : p submodule.comap f (submodule.comap g 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] [add_comm_group M] [module R M] (p : submodule R M) (h : p submodule.comap linear_map.id p := _) :
theorem submodule.mapq_pow {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) {f : M →ₗ[R] M} (h : p submodule.comap f 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] [add_comm_group M] [module R M] (p : submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [ring R₂] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} (q : submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (h : p f.ker) :
theorem submodule.map_liftq {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule 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₂) (h : p f.ker) (q : submodule R (M p)) :
theorem submodule.ker_liftq {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R 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 f.ker) :
theorem submodule.range_liftq {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule 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₂) (h : p f.ker) :
(p.liftq f h).range = f.range
theorem submodule.ker_liftq_eq_bot {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R 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 f.ker) (h' : f.ker p) :
(p.liftq f h).ker =
def submodule.comap_mkq.rel_iso {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
submodule R (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] [add_comm_group M] [module R M] (p : submodule R M) :

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

Equations
@[simp]
theorem submodule.comap_mkq_embedding_eq {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) (p' : submodule R (M p)) :
theorem submodule.span_preimage_eq {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module 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.range)) :
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_monoid M] [add_comm_group M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
f.range.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_monoid M] [add_comm_group M₂] [add_comm_monoid M₃] [module R 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_monoid M] [add_comm_group M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} (h : ∀ (u v : M₂ →ₗ[R₂] M₂ f.range), 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] [add_comm_group M] [module R M] (p : submodule R 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] [add_comm_group M] [module R M] (p : submodule R 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] [add_comm_group M] [module R M] (p : submodule R 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] [add_comm_group M] [module R M] (p : submodule R M) (hp : p = ) :
def submodule.quot_equiv_of_eq {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p p' : submodule R 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] [add_comm_group M] [module R M] (p p' : submodule R 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] [add_comm_group M] [module R M] [add_comm_group M₂] [module R M₂] (p : submodule R M) (q : submodule R 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