The abelian category of comodules over a flat coalgebra #
The forgetful functor to modules preserves kernels and cokernels and reflects isomorphisms. Consequently the coimage-to-image comparison is an isomorphism, making comodules an abelian category. In particular this applies to any coalgebra over a field, providing the exact-category structure used in the representation theory of affine groups.
The comparison argument follows Mathlib's FGModuleCat abelian-category construction.
instance
TauCeti.ComoduleCat.instReflectsIsomorphismsModuleCatForget₂HomCarrierLinearMapIdCarrier
{R : Type u}
[CommRing R]
{C : Type v}
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
:
A comodule morphism whose underlying module map is an isomorphism is an isomorphism.
instance
TauCeti.ComoduleCat.instIsIsoCoimageImageComparison
{R : Type u}
[CommRing R]
{C : Type v}
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[Module.Flat R C]
{M N : ComoduleCat R C}
(f : M ⟶ N)
:
@[instance_reducible]
instance
TauCeti.ComoduleCat.instAbelian
{R : Type u}
[CommRing R]
{C : Type v}
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[Module.Flat R C]
:
Comodules over a flat coalgebra over a commutative ring form an abelian category.
instance
TauCeti.ComoduleCat.instPreservesFiniteLimitsModuleCatForget₂HomCarrierLinearMapIdCarrier
{R : Type u}
[CommRing R]
{C : Type v}
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[Module.Flat R C]
:
Forgetting a comodule to its underlying module preserves finite limits.
instance
TauCeti.ComoduleCat.instPreservesFiniteColimitsModuleCatForget₂HomCarrierLinearMapIdCarrier
{R : Type u}
[CommRing R]
{C : Type v}
[AddCommMonoid C]
[Module R C]
[Coalgebra R C]
[Module.Flat R C]
:
Forgetting a comodule to its underlying module preserves finite colimits.