Products of finitely generated comodules

This file packages the direct-sum product comodule inside FGComoduleCat. The ambient category ComoduleCat already has the product comodule on the cartesian product of the underlying modules; finite generation is preserved by binary products of modules, so this construction stays in the full subcategory of finitely generated comodules. The same concrete object is registered as the categorical binary product, which is upgraded to a biproduct over a commutative ring. Downstream code then uses Mathlib's generic M ⨯ N / M ⊞ N API.

This is a small Layer 1 prerequisite for the reductive-groups roadmap target on the finite-dimensional comodule representation category: products and biproducts are needed before tensor products, duals, and the rigid monoidal category can be built.

Main declarations

• TauCeti.FGComoduleCat.hasBinaryProduct: the categorical binary product instance using the concrete product object.
• TauCeti.FGComoduleCat.hasBinaryProducts, hasFiniteProducts: product infrastructure induced by the binary product and the existing zero object.
• TauCeti.FGComoduleCat.hasBinaryBiproduct: the ring/preadditive biproduct instance induced by the binary product.
• TauCeti.FGComoduleCat.hasBinaryBiproducts, hasFiniteBiproducts: aggregate ring/preadditive biproduct infrastructure.

References

This supplies finite-category packaging for ReductiveGroups/README.md in TauCetiRoadmap, Layer 1 target "Comodules over a coalgebra/Hopf algebra": the finite-dimensional comodule category should have additive finite products before the rigid monoidal representation category is developed. The construction reuses the direct-sum comodule from TauCeti.Algebra.Coalgebra.Comodule.Product.

instance TauCeti.FGComoduleCat.hasBinaryProduct {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : FGComoduleCat R C) : CategoryTheory.Limits.HasBinaryProduct M N

The concrete product supplies the categorical binary product of finitely generated comodules.

instance TauCeti.FGComoduleCat.hasBinaryProducts {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] : CategoryTheory.Limits.HasBinaryProducts (FGComoduleCat R C)

Finitely generated comodules have categorical binary products.

instance TauCeti.FGComoduleCat.hasFiniteProducts {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] : CategoryTheory.Limits.HasFiniteProducts (FGComoduleCat R C)

Finitely generated comodules have finite products.

instance TauCeti.FGComoduleCat.hasBinaryBiproduct {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : FGComoduleCat R C) : CategoryTheory.Limits.HasBinaryBiproduct M N

The preadditive binary product is also a binary biproduct.

instance TauCeti.FGComoduleCat.hasBinaryBiproducts {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] : CategoryTheory.Limits.HasBinaryBiproducts (FGComoduleCat R C)

Finitely generated comodules over a commutative ring have binary biproducts.

instance TauCeti.FGComoduleCat.hasFiniteBiproducts {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] : CategoryTheory.Limits.HasFiniteBiproducts (FGComoduleCat R C)

Finitely generated comodules over a commutative ring have finite biproducts.