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.

Main definitions

• Submodule.Quotient.restrictScalarsEquiv: The quotient of P as an S-submodule is the same as the quotient of P as an R-submodule,
• Submodule.liftQ: lift a map M → M₂ to a map M ⧸ p → M₂ if the kernel is contained in p
• Submodule.mapQ: lift a map M → M₂ to a map M ⧸ p → M₂ ⧸ q if the image of p is contained in q

def Submodule.Quotient.restrictScalarsEquiv {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Type u_3) [Ring S] [SMul S R] [Module S M] [IsScalarTower S R M] (P : Submodule R M) : (M ⧸ restrictScalars S P) ≃ₗ[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.

@[simp]

theorem Submodule.Quotient.restrictScalarsEquiv_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Type u_3) [Ring S] [SMul S R] [Module S M] [IsScalarTower S R M] (P : Submodule R M) (x : M) : (restrictScalarsEquiv S P) (mk x) = mk x

@[simp]

theorem Submodule.Quotient.restrictScalarsEquiv_symm_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (S : Type u_3) [Ring S] [SMul S R] [Module S M] [IsScalarTower S R M] (P : Submodule R M) (x : M) : (restrictScalarsEquiv S P).symm (mk x) = mk x

theorem Submodule.Quotient.nontrivial_of_lt_top {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (h : p < ⊤) : Nontrivial (M ⧸ p)

instance Submodule.QuotientBot.infinite {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [Infinite M] : Infinite (M ⧸ ⊥)

instance Submodule.QuotientTop.unique {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] : Unique (M ⧸ ⊤)

instance Submodule.QuotientTop.fintype {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] : Fintype (M ⧸ ⊤)

theorem Submodule.subsingleton_quotient_iff_eq_top {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {p : Submodule R M} : Subsingleton (M ⧸ p) ↔ p = ⊤

theorem Submodule.unique_quotient_iff_eq_top {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {p : Submodule R M} : Nonempty (Unique (M ⧸ p)) ↔ p = ⊤

noncomputable instance Submodule.Quotient.fintype {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [Fintype M] (S : Submodule R M) : Fintype (M ⧸ S)

theorem Submodule.strictMono_comap_prod_map {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : StrictMono fun (m : Submodule R M) => (comap p.subtype m, map p.mkQ m)

def Submodule.liftQ {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ LinearMap.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.

@[simp]

theorem Submodule.liftQ_apply {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) {h : p ≤ LinearMap.ker f} (x : M) : (p.liftQ f h) (Quotient.mk x) = f x

@[simp]

theorem Submodule.liftQ_mkQ {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ LinearMap.ker f) : p.liftQ f h ∘ₛₗ p.mkQ = f

theorem Submodule.pi_liftQ_eq_liftQ_pi {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {ι : Type u_5} {N : ι → Type u_6} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module R (N i)] (f : (i : ι) → M →ₗ[R] N i) {p : Submodule R M} (h : ∀ (i : ι), p ≤ LinearMap.ker (f i)) : (LinearMap.pi fun (i : ι) => p.liftQ (f i) ⋯) = p.liftQ (LinearMap.pi f) ⋯

def Submodule.liftQSpanSingleton {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (x : M) (f : M →ₛₗ[τ₁₂] M₂) (h : f x = 0) : M ⧸ span R {x} →ₛₗ[τ₁₂] M₂

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

@[simp]

theorem Submodule.liftQSpanSingleton_apply {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (x : M) (f : M →ₛₗ[τ₁₂] M₂) (h : f x = 0) (y : M) : (liftQSpanSingleton x f h) (Quotient.mk y) = f y

@[simp]

theorem Submodule.range_mkQ {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : LinearMap.range p.mkQ = ⊤

@[simp]

theorem Submodule.ker_mkQ {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : LinearMap.ker p.mkQ = p

theorem Submodule.le_comap_mkQ {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (p' : Submodule R (M ⧸ p)) : p ≤ comap p.mkQ p'

@[simp]

theorem Submodule.mkQ_map_self {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : map p.mkQ p = ⊥

@[simp]

theorem Submodule.comap_map_mkQ {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p p' : Submodule R M) : comap p.mkQ (map p.mkQ p') = p ⊔ p'

@[simp]

theorem Submodule.map_mkQ_eq_top {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p p' : Submodule R M) : map p.mkQ p' = ⊤ ↔ p ⊔ p' = ⊤

def Submodule.mapQ {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (q : Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ 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.

@[simp]

theorem Submodule.mapQ_apply {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (q : Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) {h : p ≤ comap f q} (x : M) : (p.mapQ q f h) (Quotient.mk x) = Quotient.mk (f x)

theorem Submodule.mapQ_mkQ {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (q : Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) {h : p ≤ comap f q} : p.mapQ q f h ∘ₛₗ p.mkQ = q.mkQ ∘ₛₗ f

@[simp]

theorem Submodule.mapQ_zero {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (q : Submodule R₂ M₂) (h : p ≤ comap 0 q := ⋯) : p.mapQ q 0 h = 0

theorem Submodule.mapQ_comp {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {R₃ : Type u_5} {M₃ : Type u_6} [Ring R₃] [AddCommGroup M₃] [Module R₃ M₃] (p₂ : Submodule R₂ M₂) (p₃ : Submodule R₃ M₃) {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) (hf : p ≤ comap f p₂) (hg : p₂ ≤ comap g p₃) (h : p ≤ comap f (comap g p₃) := ⋯) : p.mapQ p₃ (g ∘ₛₗ f) h = p₂.mapQ p₃ g hg ∘ₛₗ 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] [AddCommGroup M] [Module R M] (p : Submodule R M) (h : p ≤ comap LinearMap.id p := ⋯) : p.mapQ p LinearMap.id h = LinearMap.id

theorem Submodule.mapQ_pow {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {f : M →ₗ[R] M} (h : p ≤ comap f p) (k : ℕ) (h' : p ≤ 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] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (q : Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ LinearMap.ker f) : comap (p.liftQ f h) q = map p.mkQ (comap f q)

theorem Submodule.map_liftQ {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ LinearMap.ker f) (q : Submodule R (M ⧸ p)) : map (p.liftQ f h) q = map f (comap p.mkQ q)

theorem Submodule.ker_liftQ {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ LinearMap.ker f) : LinearMap.ker (p.liftQ f h) = map p.mkQ (LinearMap.ker f)

theorem Submodule.range_liftQ {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ LinearMap.ker f) : LinearMap.range (p.liftQ f h) = LinearMap.range f

theorem Submodule.ker_liftQ_eq_bot {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ LinearMap.ker f) (h' : LinearMap.ker f ≤ p) : LinearMap.ker (p.liftQ f h) = ⊥

theorem Submodule.ker_liftQ_eq_bot' {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : p = LinearMap.ker f) : LinearMap.ker (p.liftQ f ⋯) = ⊥

@[reducible, inline]

abbrev Submodule.factor {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {p p' : Submodule R M} (H : p ≤ p') : M ⧸ p →ₗ[R] M ⧸ p'

The linear map from the quotient by a smaller submodule to the quotient by a larger submodule.

This is the Submodule.Quotient version of Quot.Factor

When the two submodules are of the form I ^ m • ⊤ and I ^ n • ⊤ and n ≤ m, please refer to the dedicated version Submodule.factorPow.

@[simp]

theorem Submodule.factor_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {p p' : Submodule R M} (H : p ≤ p') (x : M) : (factor H) (p.mkQ x) = p'.mkQ x

@[simp]

theorem Submodule.factor_comp_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {p p' : Submodule R M} (H : p ≤ p') : factor H ∘ₗ p.mkQ = p'.mkQ

@[simp]

theorem Submodule.factor_comp {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {p p' p'' : Submodule R M} (H1 : p ≤ p') (H2 : p' ≤ p'') : factor H2 ∘ₗ factor H1 = factor ⋯

@[simp]

theorem Submodule.factor_comp_apply {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {p p' p'' : Submodule R M} (H1 : p ≤ p') (H2 : p' ≤ p'') (x : M ⧸ p) : (factor H2) ((factor H1) x) = (factor ⋯) x

theorem Submodule.factor_surjective {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {p p' : Submodule R M} (H : p ≤ p') : Function.Surjective ⇑(factor H)

def Submodule.comapMkQRelIso {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : Submodule R (M ⧸ p) ≃o ↑(Set.Ici 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.

def Submodule.comapMkQOrderEmbedding {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : Submodule R (M ⧸ p) ↪o Submodule R M

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

@[simp]

theorem Submodule.comapMkQOrderEmbedding_eq {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (p' : Submodule R (M ⧸ p)) : p.comapMkQOrderEmbedding p' = comap p.mkQ p'

theorem Submodule.span_preimage_eq {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {s : Set M₂} (h₀ : s.Nonempty) (h₁ : s ⊆ ↑(LinearMap.range f)) : span R (⇑f ⁻¹' s) = comap f (span R₂ s)

def Submodule.Quotient.equiv {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] (P : Submodule R M) (Q : Submodule R N) (f : M ≃ₗ[R] N) (hf : 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.

@[simp]

theorem Submodule.Quotient.equiv_apply {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] (P : Submodule R M) (Q : Submodule R N) (f : M ≃ₗ[R] N) (hf : map f P = Q) (a : M ⧸ P) : (equiv P Q f hf) a = (P.mapQ Q ↑f ⋯) a

@[simp]

theorem Submodule.Quotient.equiv_symm_apply {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N : Type u_5} [AddCommGroup N] [Module R N] (P : Submodule R M) (Q : Submodule R N) (f : M ≃ₗ[R] N) (hf : map f P = Q) (a : N ⧸ Q) : (equiv P Q f hf).symm a = (Q.mapQ P ↑f.symm ⋯) a

@[simp]

theorem Submodule.Quotient.equiv_symm {R : Type u_5} {M : Type u_6} {N : Type u_7} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : Submodule R M) (Q : Submodule R N) (f : M ≃ₗ[R] N) (hf : map f P = Q) : (equiv P Q f hf).symm = equiv Q P f.symm ⋯

@[simp]

theorem Submodule.Quotient.equiv_trans {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N : Type u_5} {O : Type u_6} [AddCommGroup N] [Module R N] [AddCommGroup 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 : map e P = Q) (hf : map f Q = S) (hef : map (e ≪≫ₗ f) P = S) : equiv P S (e ≪≫ₗ f) hef = equiv P Q e he ≪≫ₗ equiv Q S f hf

theorem LinearMap.range_mkQ_comp {R : Type u_1} {M : Type u_2} {R₂ : Type u_3} {M₂ : Type u_4} [Ring R] [Ring R₂] [AddCommMonoid M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) : (range f).mkQ ∘ₛₗ f = 0

theorem LinearMap.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₃] [AddCommMonoid M] [AddCommGroup M₂] [AddCommMonoid M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₃] M₃} : ker g ≤ range f ↔ (range f).mkQ ∘ₗ (ker g).subtype = 0

theorem LinearMap.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₂] [AddCommMonoid M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} (h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ range f), u ∘ₛₗ f = v ∘ₛₗ f → u = v) : range f = ⊤

An epimorphism is surjective.

def Submodule.quotEquivOfEqBot {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (hp : p = ⊥) : (M ⧸ p) ≃ₗ[R] M

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

@[simp]

theorem Submodule.quotEquivOfEqBot_apply_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (hp : p = ⊥) (x : M) : (p.quotEquivOfEqBot hp) (Quotient.mk x) = x

@[simp]

theorem Submodule.quotEquivOfEqBot_symm_apply {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (hp : p = ⊥) (x : M) : (p.quotEquivOfEqBot hp).symm x = Quotient.mk x

@[simp]

theorem Submodule.coe_quotEquivOfEqBot_symm {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (hp : p = ⊥) : ↑(p.quotEquivOfEqBot hp).symm = p.mkQ

@[simp]

theorem Submodule.Quotient.equiv_refl {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (P Q : Submodule R M) (hf : map (↑(LinearEquiv.refl R M)) P = Q) : equiv P Q (LinearEquiv.refl R M) hf = P.quotEquivOfEq Q ⋯

def Submodule.mapQLinear {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] (p : Submodule R M) (q : Submodule R M₂) : ↥(p.compatibleMaps q) →ₗ[R] M ⧸ p →ₗ[R] M₂ ⧸ q

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.