mathlib3 documentation

linear_algebra.quotient

Quotients by submodules #

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

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 -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] [add_comm_group M] [module R M] (p : submodule R M) {x y : M} :
setoid.r x y x - y p
@[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]
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]
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) :
@[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) :
@[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) :
@[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_smul' {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {S : Type u_3} [has_smul S R] [has_smul S M] [is_scalar_tower S R M] (P : submodule R M) :
has_smul S (M P)
Equations
@[protected, instance]
def submodule.quotient.has_smul {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (P : submodule R M) :
has_smul 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_smul S R] [has_smul 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_smul S R] [has_smul S M] [is_scalar_tower S R M] (P : submodule R M) (T : Type u_4) [has_smul T R] [has_smul 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_smul S R] [has_smul S M] [is_scalar_tower S R M] (P : submodule R M) (T : Type u_4) [has_smul T R] [has_smul T M] [is_scalar_tower T R M] [has_smul S T] [is_scalar_tower S T M] :
@[protected, instance]
@[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_smul 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.smul_zero_class' {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {S : Type u_3} [has_smul S R] [smul_zero_class S M] [is_scalar_tower S R M] (P : submodule R M) :
Equations
@[protected, instance]
def submodule.quotient.distrib_smul' {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {S : Type u_3} [has_smul S R] [distrib_smul S M] [is_scalar_tower S R M] (P : submodule R M) :
Equations
@[protected, instance]
def submodule.quotient.distrib_smul {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_smul 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_smul 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
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 < ) :
@[protected, instance]
def submodule.quotient_bot.infinite {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [infinite M] :
@[protected, instance]
def submodule.quotient_top.unique {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] :
Equations
@[protected, instance]
def submodule.quotient_top.fintype {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] :
Equations
theorem submodule.subsingleton_quotient_iff_eq_top {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {p : submodule R M} :
theorem submodule.unique_quotient_iff_eq_top {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {p : submodule R M} :
@[protected, instance]
noncomputable def submodule.quotient.fintype {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [fintype M] (S : submodule R M) :
fintype (M S)
Equations
theorem submodule.card_eq_card_quotient_mul_card {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [fintype M] (S : submodule R M) [decidable_pred (λ (_x : M), _x S)] :
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) :
theorem submodule.mkq_surjective {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (A : submodule R 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 linear_map.ker f) :
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 linear_map.ker f} (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 linear_map.ker f) :
(p.liftq f h).comp p.mkq = f
def submodule.liftq_span_singleton {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₂} (x : M) (f : M →ₛₗ[τ₁₂] M₂) (h : f x = 0) :
M submodule.span R {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] [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₂} (x : M) (f : M →ₛₗ[τ₁₂] M₂) (h : f x = 0) (y : M) :
@[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) :
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 linear_map.ker f) :
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 linear_map.ker f) (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 linear_map.ker f) :
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 linear_map.ker f) :
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 linear_map.ker f) (h' : linear_map.ker f p) :
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 (linear_map.range f)) :
@[simp]
theorem submodule.quotient.equiv_symm_apply {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] (P : submodule R M) (Q : submodule R N) (f : M ≃ₗ[R] N) (hf : submodule.map f P = Q) (ᾰ : N Q) :
((submodule.quotient.equiv P Q f hf).symm) = (Q.mapq P (f.symm) _)
def submodule.quotient.equiv {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] (P : submodule R M) (Q : submodule R N) (f : M ≃ₗ[R] N) (hf : submodule.map f P = Q) :
(M P) ≃ₗ[R] N Q

If P is a submodule of M and Q a submodule of N, and f : M ≃ₗ N maps P to Q, then M ⧸ P is equivalent to N ⧸ Q.

Equations
@[simp]
theorem submodule.quotient.equiv_apply {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {N : Type u_3} [add_comm_group N] [module R N] (P : submodule R M) (Q : submodule R N) (f : M ≃ₗ[R] N) (hf : submodule.map f P = Q) (ᾰ : M P) :
(submodule.quotient.equiv P Q f hf) = (P.mapq Q f _)
@[simp]
theorem submodule.quotient.equiv_symm {R : Type u_1} {M : Type u_2} {N : Type u_3} [comm_ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] (P : submodule R M) (Q : submodule R N) (f : M ≃ₗ[R] N) (hf : submodule.map f P = Q) :
@[simp]
theorem submodule.quotient.equiv_trans {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {N : Type u_3} {O : Type u_4} [add_comm_group N] [module R N] [add_comm_group O] [module R O] (P : submodule R M) (Q : submodule R N) (S : submodule R O) (e : M ≃ₗ[R] N) (f : N ≃ₗ[R] O) (he : submodule.map e P = Q) (hf : submodule.map f Q = S) (hef : submodule.map (e.trans f) P = 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_monoid M] [add_comm_group M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
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₂ linear_map.range f), u.comp f = v.comp f u = 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) :
@[simp]
theorem submodule.quotient.equiv_refl {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (P Q : submodule R M) (hf : submodule.map (linear_equiv.refl R M) P = Q) :
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