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.mk: a function sending an element of M to M ⧸ p
• Submodule.Quotient.module: M ⧸ p is a module
• Submodule.Quotient.mkQ: a linear map sending an element of M to M ⧸ p
• Submodule.quotEquivOfEq: if p and p' are equal, their quotients are equivalent

def Submodule.quotientRel {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : Setoid 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 defeq to the AddSubgroup version, where commutativity can't be assumed.

theorem Submodule.quotientRel_def {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {x y : M} : p.quotientRel x y ↔ x - y ∈ p

instance Submodule.hasQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] : HasQuotient M (Submodule R M)

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

def Submodule.Quotient.mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup 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.

theorem Submodule.Quotient.mk'_eq_mk' {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {p : Submodule R M} (x : M) : Quotient.mk' x = mk x

theorem Submodule.Quotient.mk''_eq_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {p : Submodule R M} (x : M) : Quotient.mk'' x = mk x

theorem Submodule.Quotient.quot_mk_eq_mk {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {p : Submodule R M} (x : M) : Quot.mk (⇑p.quotientRel) x = mk x

theorem Submodule.Quotient.eq' {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {x y : M} : mk x = mk y ↔ -x + y ∈ p

theorem Submodule.Quotient.eq {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {x y : M} : mk x = mk y ↔ x - y ∈ p

instance Submodule.Quotient.instZeroQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : Zero (M ⧸ p)

instance Submodule.Quotient.instInhabitedQuotient {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : Inhabited (M ⧸ p)

@[simp]

theorem Submodule.Quotient.mk_zero {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : mk 0 = 0

@[simp]

theorem Submodule.Quotient.mk_eq_zero {R : Type u_1} {M : Type u_2} {x : M} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : mk x = 0 ↔ x ∈ p

instance Submodule.Quotient.addCommGroup {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : AddCommGroup (M ⧸ p)

@[simp]

theorem Submodule.Quotient.mk_add {R : Type u_1} {M : Type u_2} {x y : M} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : mk (x + y) = mk x + mk y

@[simp]

theorem Submodule.Quotient.mk_neg {R : Type u_1} {M : Type u_2} {x : M} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : mk (-x) = -mk x

@[simp]

theorem Submodule.Quotient.mk_sub {R : Type u_1} {M : Type u_2} {x y : M} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : mk (x - y) = mk x - mk y

theorem Submodule.Quotient.forall {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {P : M ⧸ p → Prop} : (∀ (a : M ⧸ p), P a) ↔ ∀ (a : M), P (mk a)

theorem Submodule.Quotient.subsingleton_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : Subsingleton (M ⧸ p) ↔ ∀ (x : M), x ∈ p

instance Submodule.Quotient.instSMul' {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {S : Type u_3} [SMul S R] [SMul S M] [IsScalarTower S R M] (P : Submodule R M) : SMul S (M ⧸ P)

instance Submodule.Quotient.instSMul {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (P : Submodule R M) : SMul R (M ⧸ P)

Shortcut to help the elaborator in the common case.

@[simp]

theorem Submodule.Quotient.mk_smul {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {S : Type u_3} [SMul S R] [SMul S M] [IsScalarTower S R M] (r : S) (x : M) : mk (r • x) = r • mk x

instance Submodule.Quotient.smulCommClass {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {S : Type u_3} [SMul S R] [SMul S M] [IsScalarTower S R M] (P : Submodule R M) (T : Type u_4) [SMul T R] [SMul T M] [IsScalarTower T R M] [SMulCommClass S T M] : SMulCommClass S T (M ⧸ P)

instance Submodule.Quotient.isScalarTower {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {S : Type u_3} [SMul S R] [SMul S M] [IsScalarTower S R M] (P : Submodule R M) (T : Type u_4) [SMul T R] [SMul T M] [IsScalarTower T R M] [SMul S T] [IsScalarTower S T M] : IsScalarTower S T (M ⧸ P)

instance Submodule.Quotient.isCentralScalar {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {S : Type u_3} [SMul S R] [SMul S M] [IsScalarTower S R M] (P : Submodule R M) [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] : IsCentralScalar S (M ⧸ P)

instance Submodule.Quotient.mulAction' {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {S : Type u_3} [Monoid S] [SMul S R] [MulAction S M] [IsScalarTower S R M] (P : Submodule R M) : MulAction S (M ⧸ P)

instance Submodule.Quotient.mulAction {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (P : Submodule R M) : MulAction R (M ⧸ P)

instance Submodule.Quotient.smulZeroClass' {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {S : Type u_3} [SMul S R] [SMulZeroClass S M] [IsScalarTower S R M] (P : Submodule R M) : SMulZeroClass S (M ⧸ P)

instance Submodule.Quotient.smulZeroClass {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (P : Submodule R M) : SMulZeroClass R (M ⧸ P)

instance Submodule.Quotient.distribSMul' {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {S : Type u_3} [SMul S R] [DistribSMul S M] [IsScalarTower S R M] (P : Submodule R M) : DistribSMul S (M ⧸ P)

instance Submodule.Quotient.distribSMul {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (P : Submodule R M) : DistribSMul R (M ⧸ P)

instance Submodule.Quotient.distribMulAction' {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {S : Type u_3} [Monoid S] [SMul S R] [DistribMulAction S M] [IsScalarTower S R M] (P : Submodule R M) : DistribMulAction S (M ⧸ P)

instance Submodule.Quotient.distribMulAction {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (P : Submodule R M) : DistribMulAction R (M ⧸ P)

instance Submodule.Quotient.module' {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {S : Type u_3} [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] (P : Submodule R M) : Module S (M ⧸ P)

instance Submodule.Quotient.module {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (P : Submodule R M) : Module R (M ⧸ P)

theorem Submodule.Quotient.induction_on {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {C : M ⧸ p → Prop} (x : M ⧸ p) (H : ∀ (z : M), C (mk z)) : C x

theorem Submodule.Quotient.mk_surjective {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : Function.Surjective mk

theorem Submodule.quot_hom_ext {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {M₂ : Type u_3} [AddCommGroup M₂] [Module R M₂] (f g : M ⧸ p →ₗ[R] M₂) (h : ∀ (x : M), f (Quotient.mk x) = g (Quotient.mk x)) : f = g

def Submodule.mkQ {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup 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.

@[simp]

theorem Submodule.mkQ_apply {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (x : M) : p.mkQ x = Quotient.mk x

theorem Submodule.mkQ_surjective {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : Function.Surjective ⇑p.mkQ

theorem Submodule.linearMap_qext {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 g : M ⧸ p →ₛₗ[τ₁₂] M₂⦄ (h : f ∘ₛₗ p.mkQ = g ∘ₛₗ 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].

theorem Submodule.linearMap_qext_iff {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 g : M ⧸ p →ₛₗ[τ₁₂] M₂} : f = g ↔ f ∘ₛₗ p.mkQ = g ∘ₛₗ p.mkQ

def Submodule.quotEquivOfEq {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'

Quotienting by equal submodules gives linearly equivalent quotients.

@[simp]

theorem Submodule.quotEquivOfEq_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) : (p.quotEquivOfEq p' h) (Quotient.mk x) = Quotient.mk x