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
def submodule.quotient {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
Type u_2

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 → p.quotient

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) :
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} :
@[instance]
def submodule.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
@[instance]
def submodule.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) :
@[instance]
def submodule.quotient.has_add {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_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) :
@[instance]
def submodule.quotient.has_neg {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_neg {R : Type u_1} {M : Type u_2} {x : M} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
@[instance]
def submodule.quotient.has_sub {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_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) :
@[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) :
Equations
@[simp]
theorem submodule.quotient.mk_smul {R : Type u_1} {M : Type u_2} {r : R} {x : M} [ring R] [add_comm_group M] [module R M] (p : submodule R M) :
@[simp]
theorem submodule.quotient.mk_nsmul {R : Type u_1} {M : Type u_2} {x : M} [ring R] [add_comm_group M] [module R M] (p : submodule R M) (n : ) :
@[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) :
Equations
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 : p.quotient →ₗ[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) :

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 : p.quotient →ₛₗ[τ₁₂] 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) :
p.quotient →ₛₗ[τ₁₂] 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 p.quotient) :
@[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) :

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
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 p.quotient) :
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 p.quotient ≃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 p.quotient) :
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₂] f.range.quotient), 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 = ) :

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') :

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