Quotients by subcomodules

This file equips the quotient of a right comodule by a subcomodule with the induced right-comodule structure. The quotient coaction is the unique linear map whose composite with the quotient map is (N.mkQ ⊗ id) ∘ ρ.

This is Layer 1 infrastructure for the reductive-groups roadmap target on comodules and the finite-dimensional comodule category: after subcomodules, images, and kernels, quotient comodules provide the basic cokernel-style construction used by later representation-category bookkeeping.

Main declarations

• TauCeti.Subcomodule.quotientCoact: the descended coaction on M ⧸ N.
• TauCeti.Subcomodule.instComoduleQuotient: the induced comodule structure.
• TauCeti.Subcomodule.mkQ: the quotient map as a comodule morphism.
• TauCeti.Subcomodule.liftQ: the comodule morphism induced from a morphism killing N.

References

This is the standard quotient comodule construction; see Sweedler, Hopf Algebras, Chapter 2. The formalization uses Mathlib's quotient-module API and tensor-product functoriality.

def TauCeti.Subcomodule.quotientCoact {R : Type u} {C : Type v} {M : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) : M ⧸ N.toSubmodule →ₗ[R] TensorProduct R (M ⧸ N.toSubmodule) C

The coaction induced on the quotient by a subcomodule.

Equations

• N.quotientCoact = N.toSubmodule.liftQ (TensorProduct.map N.toSubmodule.mkQ LinearMap.id ∘ₗ TauCeti.Comodule.coact) ⋯

@[simp]

theorem TauCeti.Subcomodule.quotientCoact_mk {R : Type u} {C : Type v} {M : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) (m : M) : N.quotientCoact (Submodule.Quotient.mk m) = (TensorProduct.map N.toSubmodule.mkQ LinearMap.id) (Comodule.coact m)

The quotient coaction applied to a quotient class.

theorem TauCeti.Subcomodule.quotientCoact_comp_mkQ {R : Type u} {C : Type v} {M : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) : N.quotientCoact ∘ₗ N.toSubmodule.mkQ = TensorProduct.map N.toSubmodule.mkQ LinearMap.id ∘ₗ Comodule.coact

The descended quotient coaction is characterized after precomposition with the quotient map.

@[instance_reducible]

instance TauCeti.Subcomodule.instComoduleQuotient {R : Type u} {C : Type v} {M : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) : Comodule R C (M ⧸ N.toSubmodule)

The quotient of a right comodule by a subcomodule inherits a right-comodule structure.

Equations

• N.instComoduleQuotient = { coact := N.quotientCoact, coassoc := ⋯, lTensor_counit_comp_coact := ⋯ }

@[simp]

theorem TauCeti.Subcomodule.quotient_coact {R : Type u} {C : Type v} {M : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) : Comodule.coact = N.quotientCoact

The coaction on the quotient comodule is Subcomodule.quotientCoact.

def TauCeti.Subcomodule.mkQ {R : Type u} {C : Type v} {M : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) : Comodule.Hom R C M (M ⧸ N.toSubmodule)

The quotient map by a subcomodule as a comodule morphism.

Equations

• N.mkQ = { toLinearMap := N.toSubmodule.mkQ, map_coact := ⋯ }

@[simp]

theorem TauCeti.Subcomodule.mkQ_toLinearMap {R : Type u} {C : Type v} {M : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) : N.mkQ.toLinearMap = N.toSubmodule.mkQ

The underlying linear map of the quotient comodule morphism is the quotient map.

@[simp]

theorem TauCeti.Subcomodule.mkQ_apply {R : Type u} {C : Type v} {M : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) (m : M) : N.mkQ m = Submodule.Quotient.mk m

The quotient comodule morphism sends a vector to its quotient class.

theorem TauCeti.Subcomodule.mkQ_eq_zero_iff {R : Type u} {C : Type v} {M : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) (m : M) : N.mkQ m = 0 ↔ m ∈ N

The quotient comodule morphism sends exactly the subcomodule to zero.

theorem TauCeti.Subcomodule.mkQ_surjective {R : Type u} {C : Type v} {M : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) : Function.Surjective ⇑N.mkQ

The quotient comodule morphism is surjective.

def TauCeti.Subcomodule.liftQ {R : Type u} {C : Type v} {M : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] (f : Comodule.Hom R C M P) (hf : N.toSubmodule ≤ f.ker) : Comodule.Hom R C (M ⧸ N.toSubmodule) P

A comodule morphism out of M that vanishes on N descends to the quotient by N.

Equations

• N.liftQ f hf = { toLinearMap := N.toSubmodule.liftQ f.toLinearMap hf, map_coact := ⋯ }

@[simp]

theorem TauCeti.Subcomodule.liftQ_apply {R : Type u} {C : Type v} {M : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] (f : Comodule.Hom R C M P) (hf : N.toSubmodule ≤ f.ker) (m : M) : (N.liftQ f hf) (Submodule.Quotient.mk m) = f m

The descended quotient morphism applied to a quotient class.

@[simp]

theorem TauCeti.Subcomodule.liftQ_toLinearMap {R : Type u} {C : Type v} {M : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] (f : Comodule.Hom R C M P) (hf : N.toSubmodule ≤ f.ker) : (N.liftQ f hf).toLinearMap = N.toSubmodule.liftQ f.toLinearMap hf

The underlying linear map of the descended quotient morphism is the quotient-module lift.

@[simp]

theorem TauCeti.Subcomodule.liftQ_mkQ {R : Type u} {C : Type v} {M : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] (f : Comodule.Hom R C M P) (hf : N.toSubmodule ≤ f.ker) : (N.liftQ f hf).comp N.mkQ = f

Precomposing the descended quotient morphism with the quotient map recovers the original morphism.

theorem TauCeti.Subcomodule.hom_ext {R : Type u} {C : Type v} {M : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] {f g : Comodule.Hom R C (M ⧸ N.toSubmodule) P} (h : f.comp N.mkQ = g.comp N.mkQ) : f = g

Two morphisms out of a quotient are equal if they agree after precomposition with the quotient map.

theorem TauCeti.Subcomodule.liftQ_unique {R : Type u} {C : Type v} {M : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] (f : Comodule.Hom R C M P) (hf : N.toSubmodule ≤ f.ker) (g : Comodule.Hom R C (M ⧸ N.toSubmodule) P) (hg : g.comp N.mkQ = f) : g = N.liftQ f hf

Uniqueness of the morphism descended to a quotient.

@[simp]

theorem TauCeti.Subcomodule.ker_mkQ {R : Type u} {C : Type v} {M : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup M] [Module R M] [Comodule R C M] (N : Subcomodule R C M) [Module.Flat R C] : N.mkQ.ker = N

The kernel of the quotient comodule morphism is the subcomodule being quotiented.