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

Submodule.quotientRel p = QuotientAddGroup.leftRel (Submodule.toAddSubgroup p)

Instances For

source

theorem Submodule.quotientRel_r_def {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) {x : M} {y : M} :

Setoid.r 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 (Submodule.quotientRel p) }

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''

Instances For

source

@[simp]

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 = Submodule.Quotient.mk x

source

@[simp]

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 = Submodule.Quotient.mk x

source

@[simp]

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 Setoid.r x = Submodule.Quotient.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 : M} {y : M} :

Submodule.Quotient.mk x = Submodule.Quotient.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 : M} {y : M} :

Submodule.Quotient.mk x = Submodule.Quotient.mk y ↔ x - y ∈ p

source

instance Submodule.Quotient.instZeroQuotientSubmoduleToSemiringToAddCommMonoidHasQuotient {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.instZeroQuotientSubmoduleToSemiringToAddCommMonoidHasQuotient p = { zero := Quotient.mk'' 0 }

source

instance Submodule.Quotient.instInhabitedQuotientSubmoduleToSemiringToAddCommMonoidHasQuotient {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.instInhabitedQuotientSubmoduleToSemiringToAddCommMonoidHasQuotient 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) :

Submodule.Quotient.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) :

Submodule.Quotient.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 (Submodule.toAddSubgroup p)

source

@[simp]

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

Submodule.Quotient.mk (x + y) = Submodule.Quotient.mk x + Submodule.Quotient.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) :

Submodule.Quotient.mk (-x) = -Submodule.Quotient.mk x

source

@[simp]

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

Submodule.Quotient.mk (x - y) = Submodule.Quotient.mk x - Submodule.Quotient.mk y

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

One or more equations did not get rendered due to their size.

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

Submodule.Quotient.mk (r • x) = r • Submodule.Quotient.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)

Equations

(_ : SMulCommClass S T (M ⧸ P)) = (_ : 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)

Equations

(_ : IsScalarTower S T (M ⧸ P)) = (_ : 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)

Equations

(_ : IsCentralScalar S (M ⧸ P)) = (_ : 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

One or more equations did not get rendered due to their size.

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

One or more equations did not get rendered due to their size.

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

One or more equations did not get rendered due to their size.

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

One or more equations did not get rendered due to their size.

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

One or more equations did not get rendered due to their size.

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

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 ⧸ Submodule.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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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

(Submodule.Quotient.restrictScalarsEquiv S P) (Submodule.Quotient.mk x) = Submodule.Quotient.mk x

source

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

(LinearEquiv.symm (Submodule.Quotient.restrictScalarsEquiv S P)) (Submodule.Quotient.mk x) = Submodule.Quotient.mk 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 Submodule.Quotient.mk

source

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)

source

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

Infinite (M ⧸ ⊥)

Equations

(_ : Infinite (M ⧸ ⊥)) = (_ : Infinite (M ⧸ ⊥))

source

instance Submodule.QuotientTop.unique {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] :

Unique (M ⧸ ⊤)

Equations

Submodule.QuotientTop.unique = { toInhabited := { default := 0 }, uniq := (_ : ∀ (x : M ⧸ ⊤), x = default) }

source

instance Submodule.QuotientTop.fintype {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] :

Fintype (M ⧸ ⊤)

Equations

Submodule.QuotientTop.fintype = Fintype.ofSubsingleton 0

source

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 = ⊤

source

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 = ⊤

source

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)

Equations

Submodule.Quotient.fintype S = Quotient.fintype (Submodule.quotientRel S)

source

theorem Submodule.card_eq_card_quotient_mul_card {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [Fintype M] (S : Submodule R M) [DecidablePred fun (x : M) => x ∈ S] :

Fintype.card M = Fintype.card ↥S * Fintype.card (M ⧸ S)

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 : M ⧸ p →ₗ[R] M₂) (g : M ⧸ p →ₗ[R] M₂) (h : ∀ (x : M), f (Submodule.Quotient.mk x) = g (Submodule.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

One or more equations did not get rendered due to their size.

Instances For

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

(Submodule.mkQ p) x = Submodule.Quotient.mk x

source

theorem Submodule.mkQ_surjective {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (A : Submodule R M) :

Function.Surjective ⇑(Submodule.mkQ A)

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 : M ⧸ p →ₛₗ[τ₁₂] M₂⦄ ⦃g : M ⧸ p →ₛₗ[τ₁₂] M₂⦄ (h : LinearMap.comp f (Submodule.mkQ p) = LinearMap.comp g (Submodule.mkQ p)) :

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

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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

(Submodule.liftQ p f h) (Submodule.Quotient.mk x) = f x

source

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

LinearMap.comp (Submodule.liftQ p f h) (Submodule.mkQ p) = f

source

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 ⧸ 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

Submodule.liftQSpanSingleton x f h = Submodule.liftQ (Submodule.span R {x}) f (_ : Submodule.span R {x} ≤ LinearMap.ker f)

Instances For

source

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

(Submodule.liftQSpanSingleton x f h) (Submodule.Quotient.mk y) = f y

source

@[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 (Submodule.mkQ p) = ⊤

source

@[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 (Submodule.mkQ p) = p

source

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 ≤ Submodule.comap (Submodule.mkQ p) p'

source

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

Submodule.map (Submodule.mkQ p) p = ⊥

source

@[simp]

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

Submodule.comap (Submodule.mkQ p) (Submodule.map (Submodule.mkQ p) p') = p ⊔ p'

source

@[simp]

theorem Submodule.map_mkQ_eq_top {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (p' : Submodule R M) :

Submodule.map (Submodule.mkQ p) p' = ⊤ ↔ p ⊔ p' = ⊤

source

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 ≤ 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

Submodule.mapQ p q f h = Submodule.liftQ p (LinearMap.comp (Submodule.mkQ q) f) (_ : p ≤ LinearMap.ker (LinearMap.comp (Submodule.mkQ q) f))

Instances For

source

@[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 ≤ Submodule.comap f q} (x : M) :

(Submodule.mapQ p q f h) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (f x)

source

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 ≤ Submodule.comap f q} :

LinearMap.comp (Submodule.mapQ p q f h) (Submodule.mkQ p) = LinearMap.comp (Submodule.mkQ q) f

source

@[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 : optParam (p ≤ Submodule.comap 0 q) (_ : p ≤ Submodule.comap 0 q)) :

Submodule.mapQ p q 0 h = 0

source

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 ≤ Submodule.comap f p₂) (hg : p₂ ≤ Submodule.comap g p₃) (h : optParam (p ≤ Submodule.comap f (Submodule.comap g p₃)) (_ : p ≤ Submodule.comap f (Submodule.comap g p₃))) :

Submodule.mapQ p p₃ (LinearMap.comp g f) h = LinearMap.comp (Submodule.mapQ p₂ p₃ g hg) (Submodule.mapQ p 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).

source

@[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 : optParam (p ≤ Submodule.comap LinearMap.id p) (_ : p ≤ Submodule.comap LinearMap.id p)) :

Submodule.mapQ p p LinearMap.id h = LinearMap.id

source

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 ≤ Submodule.comap f p) (k : ℕ) (h' : optParam (p ≤ Submodule.comap (f ^ k) p) (_ : p ≤ Submodule.comap (f ^ k) p)) :

Submodule.mapQ p p (f ^ k) h' = Submodule.mapQ p p f h ^ k

source

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

Submodule.comap (Submodule.liftQ p f h) q = Submodule.map (Submodule.mkQ p) (Submodule.comap f q)

source

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

Submodule.map (Submodule.liftQ p f h) q = Submodule.map f (Submodule.comap (Submodule.mkQ p) q)

source

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 (Submodule.liftQ p f h) = Submodule.map (Submodule.mkQ p) (LinearMap.ker f)

source

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 (Submodule.liftQ p f h) = LinearMap.range f

source

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 (Submodule.liftQ p f h) = ⊥

source

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 { p' : Submodule R M // 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

source

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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

(Submodule.comapMkQOrderEmbedding p) p' = Submodule.comap (Submodule.mkQ p) p'

source

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₀ : Set.Nonempty s) (h₁ : s ⊆ ↑(LinearMap.range f)) :

Submodule.span R (⇑f ⁻¹' s) = Submodule.comap f (Submodule.span R₂ s)

source

@[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 : Submodule.map f P = Q) (a : N ⧸ Q) :

(LinearEquiv.symm (Submodule.Quotient.equiv P Q f hf)) a = (Submodule.mapQ Q P ↑(LinearEquiv.symm f) (_ : ∀ x ∈ Q, x ∈ Submodule.comap (↑(LinearEquiv.symm f)) P)) a

source

@[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 : Submodule.map f P = Q) (a : M ⧸ P) :

(Submodule.Quotient.equiv P Q f hf) a = (Submodule.mapQ P Q ↑f (_ : ∀ x ∈ P, x ∈ Submodule.comap (↑f) Q)) a

source

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

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

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

LinearEquiv.symm (Submodule.Quotient.equiv P Q f hf) = Submodule.Quotient.equiv Q P (LinearEquiv.symm f) (_ : Submodule.map (LinearEquiv.symm f) Q = P)

source

@[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 : Submodule.map e P = Q) (hf : Submodule.map f Q = S) (hef : Submodule.map (e ≪≫ₗ f) P = S) :

Submodule.Quotient.equiv P S (e ≪≫ₗ f) hef = Submodule.Quotient.equiv P Q e he ≪≫ₗ Submodule.Quotient.equiv Q S f hf

source

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

LinearMap.comp (Submodule.mkQ (LinearMap.range f)) f = 0

source

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₃} :

LinearMap.ker g ≤ LinearMap.range f ↔ Submodule.mkQ (LinearMap.range f) ∘ₗ Submodule.subtype (LinearMap.ker g) = 0

source

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₂ ⧸ LinearMap.range f), LinearMap.comp u f = LinearMap.comp v f → u = v) :

LinearMap.range f = ⊤

An epimorphism is surjective.

source

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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

(Submodule.quotEquivOfEqBot p hp) (Submodule.Quotient.mk x) = x

source

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

(LinearEquiv.symm (Submodule.quotEquivOfEqBot p hp)) x = Submodule.Quotient.mk x

source

@[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 = ⊥) :

↑(LinearEquiv.symm (Submodule.quotEquivOfEqBot p hp)) = Submodule.mkQ p

source

def Submodule.quotEquivOfEq {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (p' : Submodule R M) (h : p = p') :

(M ⧸ p) ≃ₗ[R] M ⧸ p'

Quotienting by equal submodules gives linearly equivalent quotients.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

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

(Submodule.quotEquivOfEq p p' h) (Submodule.Quotient.mk x) = Submodule.Quotient.mk x

source

@[simp]

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

Submodule.Quotient.equiv P Q (LinearEquiv.refl R M) hf = Submodule.quotEquivOfEq P Q (_ : P = Q)

source

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

↥(Submodule.compatibleMaps p 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

One or more equations did not get rendered due to their size.

Instances For

Documentation

Mathlib.LinearAlgebra.Quotient

Quotients by submodules #