The abelian category of finite comodules

Finitely generated comodules over a flat coalgebra over a Noetherian commutative ring form an abelian category. Their kernels and cokernels are computed in the category of all comodules. In particular, finite-dimensional comodules over a field form an abelian category, with an exact forgetful functor to vector spaces. For coordinate Hopf algebras this supplies the abelian and exact structures of the Tannakian representation category.

The full-subcategory argument uses Mathlib's ObjectProperty kernel and cokernel closure API.

instance TauCeti.ComoduleCat.isFG_isClosedUnderCokernels {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] : (isFG R C).IsClosedUnderCokernels

Cokernels of morphisms between finite comodules are finite.

instance TauCeti.ComoduleCat.isFG_isClosedUnderKernels {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] [IsNoetherianRing R] [Module.Flat R C] : (isFG R C).IsClosedUnderKernels

Kernels of morphisms between finite comodules are finite over a Noetherian base.

@[instance_reducible]

instance TauCeti.FGComoduleCat.instAbelian {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] [IsNoetherianRing R] [Module.Flat R C] : CategoryTheory.Abelian (FGComoduleCat R C)

Finite comodules over a flat coalgebra over a Noetherian commutative ring are abelian.

Equations

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

instance TauCeti.FGComoduleCat.instPreservesLimitComoduleCatWalkingParallelPairParallelPairOfNatHomIncl {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] [IsNoetherianRing R] [Module.Flat R C] {M N : FGComoduleCat R C} (f : M ⟶ N) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) incl

instance TauCeti.FGComoduleCat.instPreservesColimitComoduleCatWalkingParallelPairParallelPairOfNatHomIncl {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : FGComoduleCat R C} (f : M ⟶ N) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) incl

instance TauCeti.FGComoduleCat.instPreservesFiniteLimitsComoduleCatIncl {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] [IsNoetherianRing R] [Module.Flat R C] : CategoryTheory.Limits.PreservesFiniteLimits incl

Inclusion of finite comodules preserves finite limits.

instance TauCeti.FGComoduleCat.instPreservesFiniteColimitsComoduleCatIncl {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] : CategoryTheory.Limits.PreservesFiniteColimits incl

Inclusion of finite comodules preserves finite colimits.

instance TauCeti.FGComoduleCat.instPreservesFiniteLimitsModuleCatForget₂HomCarrierObjComoduleCatIsFGLinearMapIdCarrier {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] [IsNoetherianRing R] [Module.Flat R C] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget₂ (FGComoduleCat R C) (ModuleCat R))

The underlying-module functor on finite comodules preserves finite limits.

instance TauCeti.FGComoduleCat.instPreservesFiniteColimitsModuleCatForget₂HomCarrierObjComoduleCatIsFGLinearMapIdCarrier {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] [Module.Flat R C] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.forget₂ (FGComoduleCat R C) (ModuleCat R))

The underlying-module functor on finite comodules preserves finite colimits.