Kernels and cokernels of comodules

For a flat coalgebra over a commutative ring, kernels of comodule morphisms carry the induced coaction. Cokernels carry the quotient coaction, without a flatness assumption. These concrete constructions satisfy the categorical universal properties, and the forgetful functor to modules preserves them. This allows exact sequences of representations to be computed on their underlying modules.

The constructions use Subcomodule.subtype, Comodule.Hom.codRestrict, and Subcomodule.liftQ. The categorical packaging follows Mathlib's ModuleCat.kernelIsLimit and ModuleCat.cokernelIsColimit.

noncomputable def TauCeti.ComoduleCat.kernelCone {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f : M ⟶ N) [Module.Flat R C] : CategoryTheory.Limits.KernelFork f

The kernel fork given by the kernel subcomodule.

Equations

• TauCeti.ComoduleCat.kernelCone f = CategoryTheory.Limits.KernelFork.ofι (TauCeti.ComoduleCat.ofHom R C (TauCeti.Comodule.Hom.ker f).subtype) ⋯

noncomputable def TauCeti.ComoduleCat.kernelIsLimit {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f : M ⟶ N) [Module.Flat R C] : CategoryTheory.Limits.IsLimit (kernelCone f)

The kernel subcomodule is a categorical kernel.

Equations

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

instance TauCeti.ComoduleCat.instHasKernels {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] : CategoryTheory.Limits.HasKernels (ComoduleCat R C)

noncomputable def TauCeti.ComoduleCat.kernelIsoKer {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f : M ⟶ N) [Module.Flat R C] : CategoryTheory.Limits.kernel f ≅ of R C ↥(Comodule.Hom.ker f)

The categorical kernel is the concrete kernel subcomodule.

Equations

• TauCeti.ComoduleCat.kernelIsoKer f = CategoryTheory.Limits.limit.isoLimitCone { cone := TauCeti.ComoduleCat.kernelCone f, isLimit := TauCeti.ComoduleCat.kernelIsLimit f }

@[simp]

theorem TauCeti.ComoduleCat.kernelIsoKer_inv_kernel_ι {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f : M ⟶ N) [Module.Flat R C] : CategoryTheory.CategoryStruct.comp (kernelIsoKer f).inv (CategoryTheory.Limits.kernel.ι f) = ofHom R C (Comodule.Hom.ker f).subtype

instance TauCeti.ComoduleCat.instPreservesLimitModuleCatWalkingParallelPairParallelPairOfNatHomForget₂HomCarrierLinearMapIdCarrier {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f : M ⟶ N) [Module.Flat R C] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) (CategoryTheory.forget₂ (ComoduleCat R C) (ModuleCat R))

def TauCeti.ComoduleCat.cokernelCocone {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f : M ⟶ N) : CategoryTheory.Limits.CokernelCofork f

The cokernel cofork given by the quotient by the range subcomodule.

Equations

• TauCeti.ComoduleCat.cokernelCocone f = CategoryTheory.Limits.CokernelCofork.ofπ (TauCeti.ComoduleCat.ofHom R C (TauCeti.Comodule.Hom.range f).mkQ) ⋯

def TauCeti.ComoduleCat.cokernelIsColimit {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f : M ⟶ N) : CategoryTheory.Limits.IsColimit (cokernelCocone f)

The quotient by the range subcomodule is a categorical cokernel.

Equations

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

instance TauCeti.ComoduleCat.instHasCokernels {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] : CategoryTheory.Limits.HasCokernels (ComoduleCat R C)

noncomputable def TauCeti.ComoduleCat.cokernelIsoRangeQuotient {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f : M ⟶ N) : CategoryTheory.Limits.cokernel f ≅ of R C (↑N.toSemimoduleCat ⧸ (Comodule.Hom.range f).toSubmodule)

The categorical cokernel is the quotient by the concrete range subcomodule.

Equations

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

@[simp]

theorem TauCeti.ComoduleCat.cokernel_π_cokernelIsoRangeQuotient_hom {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) (cokernelIsoRangeQuotient f).hom = ofHom R C (Comodule.Hom.range f).mkQ

instance TauCeti.ComoduleCat.instPreservesColimitModuleCatWalkingParallelPairParallelPairOfNatHomForget₂HomCarrierLinearMapIdCarrier {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : ComoduleCat R C} (f : M ⟶ N) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) (CategoryTheory.forget₂ (ComoduleCat R C) (ModuleCat R))