# 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.quotientRel {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) :

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 defeq to the AddSubgroup version, where commutativity can't be assumed.

Equations
Instances For
theorem Submodule.quotientRel_r_def {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) {x : M} {y : M} :
Setoid.r x y x - y p
instance Submodule.hasQuotient {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] :

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

Equations
• Submodule.hasQuotient = { quotient' := fun (p : ) => Quotient p.quotientRel }
def Submodule.Quotient.mk {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {p : } :
MM p

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

Equations
• Submodule.Quotient.mk = Quotient.mk''
Instances For
@[simp]
theorem Submodule.Quotient.mk'_eq_mk' {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {p : } (x : M) :
@[simp]
theorem Submodule.Quotient.mk''_eq_mk {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {p : } (x : M) :
@[simp]
theorem Submodule.Quotient.quot_mk_eq_mk {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {p : } (x : M) :
Quot.mk Setoid.r x =
theorem Submodule.Quotient.eq' {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) {x : M} {y : M} :
-x + y p
theorem Submodule.Quotient.eq {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) {x : M} {y : M} :
x - y p
instance Submodule.Quotient.instZeroQuotient {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) :
Zero (M p)
Equations
• = { zero := }
instance Submodule.Quotient.instInhabitedQuotient {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) :
Equations
• = { default := 0 }
@[simp]
theorem Submodule.Quotient.mk_zero {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) :
@[simp]
theorem Submodule.Quotient.mk_eq_zero {R : Type u_1} {M : Type u_2} {x : M} [Ring R] [] [Module R M] (p : ) :
x p
instance Submodule.Quotient.addCommGroup {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) :
Equations
@[simp]
theorem Submodule.Quotient.mk_add {R : Type u_1} {M : Type u_2} {x : M} {y : M} [Ring R] [] [Module R M] (p : ) :
@[simp]
theorem Submodule.Quotient.mk_neg {R : Type u_1} {M : Type u_2} {x : M} [Ring R] [] [Module R M] (p : ) :
@[simp]
theorem Submodule.Quotient.mk_sub {R : Type u_1} {M : Type u_2} {x : M} {y : M} [Ring R] [] [Module R M] (p : ) :
instance Submodule.Quotient.instSMul' {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {S : Type u_3} [SMul S R] [SMul S M] [] (P : ) :
SMul S (M P)
Equations
instance Submodule.Quotient.instSMul {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (P : ) :
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] [] [Module R M] (p : ) {S : Type u_3} [SMul S R] [SMul S M] [] (r : S) (x : M) :
instance Submodule.Quotient.smulCommClass {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {S : Type u_3} [SMul S R] [SMul S M] [] (P : ) (T : Type u_4) [SMul T R] [SMul T M] [] [] :
SMulCommClass S T (M P)
Equations
• =
instance Submodule.Quotient.isScalarTower {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {S : Type u_3} [SMul S R] [SMul S M] [] (P : ) (T : Type u_4) [SMul T R] [SMul T M] [] [SMul S T] [] :
IsScalarTower S T (M P)
Equations
• =
instance Submodule.Quotient.isCentralScalar {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {S : Type u_3} [SMul S R] [SMul S M] [] (P : ) [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [] [] :
Equations
• =
instance Submodule.Quotient.mulAction' {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {S : Type u_3} [] [SMul S R] [] [] (P : ) :
MulAction S (M P)
Equations
instance Submodule.Quotient.mulAction {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (P : ) :
MulAction R (M P)
Equations
instance Submodule.Quotient.smulZeroClass' {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {S : Type u_3} [SMul S R] [] [] (P : ) :
Equations
• = { toFun := Submodule.Quotient.mk, map_zero' := }.smulZeroClass
instance Submodule.Quotient.smulZeroClass {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (P : ) :
Equations
instance Submodule.Quotient.distribSMul' {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {S : Type u_3} [SMul S R] [] [] (P : ) :
Equations
instance Submodule.Quotient.distribSMul {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (P : ) :
Equations
instance Submodule.Quotient.distribMulAction' {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {S : Type u_3} [] [SMul S R] [] [] (P : ) :
Equations
instance Submodule.Quotient.distribMulAction {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (P : ) :
Equations
instance Submodule.Quotient.module' {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {S : Type u_3} [] [SMul S R] [Module S M] [] (P : ) :
Module S (M P)
Equations
instance Submodule.Quotient.module {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (P : ) :
Module R (M P)
Equations
def Submodule.Quotient.restrictScalarsEquiv {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (S : Type u_3) [Ring S] [SMul S R] [Module S M] [] (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.

Equations
• = let __src := ; { toFun := __src.toFun, map_add' := , map_smul' := , invFun := __src.invFun, left_inv := , right_inv := }
Instances For
@[simp]
theorem Submodule.Quotient.restrictScalarsEquiv_mk {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (S : Type u_3) [Ring S] [SMul S R] [Module S M] [] (P : ) (x : M) :
@[simp]
theorem Submodule.Quotient.restrictScalarsEquiv_symm_mk {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (S : Type u_3) [Ring S] [SMul S R] [Module S M] [] (P : ) (x : M) :
theorem Submodule.Quotient.mk_surjective {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) :
Function.Surjective Submodule.Quotient.mk
theorem Submodule.Quotient.nontrivial_of_lt_top {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (h : p < ) :
instance Submodule.QuotientBot.infinite {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] [] :
Equations
• =
instance Submodule.QuotientTop.unique {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] :
Equations
• Submodule.QuotientTop.unique = { default := 0, uniq := }
instance Submodule.QuotientTop.fintype {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] :
Equations
• Submodule.QuotientTop.fintype =
theorem Submodule.subsingleton_quotient_iff_eq_top {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {p : } :
theorem Submodule.unique_quotient_iff_eq_top {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {p : } :
noncomputable instance Submodule.Quotient.fintype {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] [] (S : ) :
Fintype (M S)
Equations
theorem Submodule.card_eq_card_quotient_mul_card {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (S : ) :
= Nat.card S * Nat.card (M S)
theorem Submodule.quot_hom_ext {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) {M₂ : Type u_3} [] [Module R M₂] (f : M p →ₗ[R] M₂) (g : M p →ₗ[R] M₂) (h : ∀ (x : M), = ) :
f = g
def Submodule.mkQ {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) :
M →ₗ[R] M p

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

Equations
• p.mkQ = { toFun := Submodule.Quotient.mk, map_add' := , map_smul' := }
Instances For
@[simp]
theorem Submodule.mkQ_apply {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (x : M) :
p.mkQ x =
theorem Submodule.mkQ_surjective {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (A : ) :
theorem Submodule.linearMap_qext {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [] [Module R₂ M₂] {τ₁₂ : R →+* R₂} ⦃f : M p →ₛₗ[τ₁₂] M₂ ⦃g : M p →ₛₗ[τ₁₂] M₂ (h : f.comp p.mkQ = g.comp p.mkQ) :
f = g

Two LinearMaps 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] [] [Module R M] (p : ) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : ) :
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
Instances For
@[simp]
theorem Submodule.liftQ_apply {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) {h : } (x : M) :
(p.liftQ f h) = f x
@[simp]
theorem Submodule.liftQ_mkQ {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : ) :
(p.liftQ f h).comp p.mkQ = f
def Submodule.liftQSpanSingleton {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (x : M) (f : M →ₛₗ[τ₁₂] M₂) (h : f x = 0) :
M Submodule.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.

Equations
Instances For
@[simp]
theorem Submodule.liftQSpanSingleton_apply {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [] [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] [] [Module R M] (p : ) :
@[simp]
theorem Submodule.ker_mkQ {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) :
theorem Submodule.le_comap_mkQ {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (p' : Submodule R (M p)) :
p Submodule.comap p.mkQ p'
@[simp]
theorem Submodule.mkQ_map_self {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) :
@[simp]
theorem Submodule.comap_map_mkQ {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (p' : ) :
Submodule.comap p.mkQ (Submodule.map p.mkQ p') = p p'
@[simp]
theorem Submodule.map_mkQ_eq_top {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (p' : ) :
Submodule.map p.mkQ p' = p p' =
def Submodule.mapQ {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (q : Submodule R₂ 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
• p.mapQ q f h = p.liftQ (q.mkQ.comp f)
Instances For
@[simp]
theorem Submodule.mapQ_apply {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (q : Submodule R₂ 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] [] [Module R M] (p : ) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (q : Submodule R₂ 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] [] [Module R M] (p : ) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (q : Submodule R₂ M₂) (h : optParam (p ) ) :
p.mapQ q 0 h = 0
theorem Submodule.mapQ_comp {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {R₃ : Type u_5} {M₃ : Type u_6} [Ring R₃] [] [Module R₃ M₃] (p₂ : Submodule R₂ M₂) (p₃ : Submodule R₃ M₃) {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [RingHomCompTriple τ₁₂ τ₂₃ τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) (hf : p ) (hg : p₂ ) (h : optParam (p Submodule.comap f ()) ) :
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] [] [Module R M] (p : ) (h : optParam (p Submodule.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] [] [Module R M] (p : ) {f : M →ₗ[R] M} (h : p ) (k : ) (h' : optParam (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] [] [Module R M] (p : ) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (q : Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (h : ) :
Submodule.comap (p.liftQ f h) q = Submodule.map p.mkQ ()
theorem Submodule.map_liftQ {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] (f : M →ₛₗ[τ₁₂] M₂) (h : ) (q : Submodule R (M p)) :
Submodule.map (p.liftQ f h) q = Submodule.map f (Submodule.comap p.mkQ q)
theorem Submodule.ker_liftQ {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : ) :
LinearMap.ker (p.liftQ f h) = Submodule.map p.mkQ ()
theorem Submodule.range_liftQ {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] (f : M →ₛₗ[τ₁₂] M₂) (h : ) :
LinearMap.range (p.liftQ f h) =
theorem Submodule.ker_liftQ_eq_bot {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : ) (h' : ) :
LinearMap.ker (p.liftQ f h) =
theorem Submodule.ker_liftQ_eq_bot' {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (f : M →ₛₗ[τ₁₂] M₂) (h : ) :
LinearMap.ker (p.liftQ f ) =
def Submodule.comapMkQRelIso {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) :
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
• One or more equations did not get rendered due to their size.
Instances For
def Submodule.comapMkQOrderEmbedding {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) :
Submodule R (M p) ↪o

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

Equations
Instances For
@[simp]
theorem Submodule.comapMkQOrderEmbedding_eq {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (p' : Submodule R (M p)) :
p.comapMkQOrderEmbedding p' = Submodule.comap p.mkQ p'
theorem Submodule.span_preimage_eq {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {R₂ : Type u_3} {M₂ : Type u_4} [Ring R₂] [] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] {f : M →ₛₗ[τ₁₂] M₂} {s : Set M₂} (h₀ : s.Nonempty) (h₁ : s ()) :
@[simp]
theorem Submodule.Quotient.equiv_symm_apply {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {N : Type u_5} [] [Module R N] (P : ) (Q : ) (f : M ≃ₗ[R] N) (hf : = Q) (a : N Q) :
().symm a = (Q.mapQ P f.symm ) a
@[simp]
theorem Submodule.Quotient.equiv_apply {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {N : Type u_5} [] [Module R N] (P : ) (Q : ) (f : M ≃ₗ[R] N) (hf : = Q) (a : M P) :
() a = (P.mapQ Q f ) a
def Submodule.Quotient.equiv {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {N : Type u_5} [] [Module R N] (P : ) (Q : ) (f : M ≃ₗ[R] N) (hf : = 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
• = let __src := P.mapQ Q f ; { toFun := (P.mapQ Q f ), map_add' := , map_smul' := , invFun := (Q.mapQ P f.symm ), left_inv := , right_inv := }
Instances For
@[simp]
theorem Submodule.Quotient.equiv_symm {R : Type u_5} {M : Type u_6} {N : Type u_7} [] [] [Module R M] [] [Module R N] (P : ) (Q : ) (f : M ≃ₗ[R] N) (hf : = Q) :
().symm = Submodule.Quotient.equiv Q P f.symm
@[simp]
theorem Submodule.Quotient.equiv_trans {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] {N : Type u_5} {O : Type u_6} [] [Module R N] [] [Module R O] (P : ) (Q : ) (S : ) (e : M ≃ₗ[R] N) (f : N ≃ₗ[R] O) (he : = Q) (hf : = S) (hef : Submodule.map (e ≪≫ₗ f) P = S) :
Submodule.Quotient.equiv P S (e ≪≫ₗ f) hef = ≪≫ₗ
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₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] (f : M →ₛₗ[τ₁₂] M₂) :
().mkQ.comp 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₃] [] [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {τ₁₂ : R →+* R₂} {τ₂₃ : R₂ →+* R₃} [] {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₃] M₃} :
().mkQ ∘ₗ ().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₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] {f : M →ₛₗ[τ₁₂] M₂} (h : ∀ (u v : M₂ →ₗ[R₂] M₂ ), u.comp f = v.comp fu = v) :

An epimorphism is surjective.

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

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

Equations
Instances For
@[simp]
theorem Submodule.quotEquivOfEqBot_apply_mk {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (hp : p = ) (x : M) :
(p.quotEquivOfEqBot hp) = x
@[simp]
theorem Submodule.quotEquivOfEqBot_symm_apply {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (hp : p = ) (x : M) :
(p.quotEquivOfEqBot hp).symm x =
@[simp]
theorem Submodule.coe_quotEquivOfEqBot_symm {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (hp : p = ) :
(p.quotEquivOfEqBot hp).symm = p.mkQ
def Submodule.quotEquivOfEq {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (p' : ) (h : p = p') :
(M p) ≃ₗ[R] M p'

Quotienting by equal submodules gives linearly equivalent quotients.

Equations
• p.quotEquivOfEq p' h = let __src := ; { toFun := __src.toFun, map_add' := , map_smul' := , invFun := __src.invFun, left_inv := , right_inv := }
Instances For
@[simp]
theorem Submodule.quotEquivOfEq_mk {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (p : ) (p' : ) (h : p = p') (x : M) :
(p.quotEquivOfEq p' h) =
@[simp]
theorem Submodule.Quotient.equiv_refl {R : Type u_1} {M : Type u_2} [Ring R] [] [Module R M] (P : ) (Q : ) (hf : Submodule.map (()) P = Q) :
Submodule.Quotient.equiv P Q () hf = P.quotEquivOfEq Q
def Submodule.mapQLinear {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [] [] [Module R M] [] [Module R M₂] (p : ) (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.

Equations
• p.mapQLinear q = { toFun := fun (f : (p.compatibleMaps q)) => p.mapQ q f , map_add' := , map_smul' := }
Instances For