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

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

p.quotientRel = QuotientAddGroup.leftRel p.toAddSubgroup

source

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

source

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.

Equations

Submodule.hasQuotient = { quotient' := fun (p : Submodule R M) => Quotient p.quotientRel }

source

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.

Equations

Submodule.Quotient.mk = Quotient.mk''

source

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

source

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

source

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

source

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

source

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

source

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)

Equations

Submodule.Quotient.instZeroQuotient p = { zero := Quotient.mk'' 0 }

source

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)

Equations

Submodule.Quotient.instInhabitedQuotient p = { default := 0 }

source

@[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

source

@[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

source

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)

Equations

Submodule.Quotient.addCommGroup p = QuotientAddGroup.Quotient.addCommGroup p.toAddSubgroup

source

@[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

source

@[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

source

@[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

source

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)

source

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

source

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)

Equations

Submodule.Quotient.instSMul' P = { smul := fun (a : S) => Quotient.map' (fun (x : M) => a • x) ⋯ }

source

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.

Equations

Submodule.Quotient.instSMul P = Submodule.Quotient.instSMul' P

source

@[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

source

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)

source

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)

source

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)

source

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)

Equations

Submodule.Quotient.mulAction' P = { toSMul := Submodule.Quotient.instSMul' P, one_smul := ⋯, mul_smul := ⋯ }

source

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)

Equations

Submodule.Quotient.mulAction P = Submodule.Quotient.mulAction' P

source

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)

Equations

Submodule.Quotient.smulZeroClass' P = { toFun := Submodule.Quotient.mk, map_zero' := ⋯ }.smulZeroClass ⋯

source

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)

Equations

Submodule.Quotient.smulZeroClass P = Submodule.Quotient.smulZeroClass' P

source

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)

Equations

Submodule.Quotient.distribSMul' P = { toSMulZeroClass := Submodule.Quotient.smulZeroClass' P, smul_add := ⋯ }

source

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)

Equations

Submodule.Quotient.distribSMul P = Submodule.Quotient.distribSMul' P

source

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)

Equations

Submodule.Quotient.distribMulAction' P = { toMulAction := Submodule.Quotient.mulAction' P, smul_zero := ⋯, smul_add := ⋯ }

source

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)

Equations

Submodule.Quotient.distribMulAction P = Submodule.Quotient.distribMulAction' P

source

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)

Equations

Submodule.Quotient.module' P = { toDistribMulAction := Submodule.Quotient.distribMulAction' P, add_smul := ⋯, zero_smul := ⋯ }

source

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)

Equations

Submodule.Quotient.module P = Submodule.Quotient.module' P

source

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

source

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

source

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

source

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.

Equations

p.mkQ = { toFun := Submodule.Quotient.mk, map_add' := ⋯, map_smul' := ⋯ }

source

@[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

source

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

source

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].

source

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

source

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.

Equations

p.quotEquivOfEq p' h = { toFun := (Quotient.congr (Equiv.refl M) ⋯).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (Quotient.congr (Equiv.refl M) ⋯).invFun, left_inv := ⋯, right_inv := ⋯ }

source

@[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

Documentation

Mathlib.LinearAlgebra.Quotient.Defs

Quotients by submodules #

Main definitions #