Preadditive structure on finitely generated comodules

This file makes the preadditive structure on the category of finitely generated right comodules over a coalgebra over a commutative ring available from a finite-comodule import. The category is a full subcategory of all comodules, so Mathlib transfers the preadditive structure from ComoduleCat. The forgetful functor to ModuleCat R is additive.

It also records concrete simp lemmas computing the zero, addition, negation, and subtraction of finitely generated comodule morphisms through the underlying ambient comodule morphism .hom, and pointwise on elements, so downstream code never has to unfold the full-subcategory transfer.

This is a small Layer 1 prerequisite for the reductive-groups roadmap's finite-dimensional representation category: additive hom-sets are needed before tensor products, duals, and Tannakian reconstruction can be built on finitely generated comodules.

Main declarations

• TauCeti.FGComoduleCat.hom_zero, hom_add, hom_neg, hom_sub: the additive-group operations on finitely generated comodule morphisms agree with those of the ambient ComoduleCat morphism underneath.
• TauCeti.FGComoduleCat.zero_apply, add_apply, neg_apply, sub_apply: the same operations computed pointwise on elements.

References

This supplies additive-category bookkeeping for ReductiveGroups/README.md in TauCetiRoadmap, Layer 1 target "Comodules over a coalgebra/Hopf algebra": the finite-dimensional comodule category should have additive hom-sets before the rigid monoidal representation category is developed. The transfer mechanism is Mathlib's ObjectProperty.FullSubcategory preadditive instance.

@[instance_reducible]

noncomputable instance TauCeti.FGComoduleCat.instHasForget₂HomCarrierObjComoduleCatIsFGModuleCatLinearMapIdCarrier {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] : CategoryTheory.HasForget₂ (FGComoduleCat R C) (ModuleCat R)

Forget a finite comodule to its underlying module.

Equations

• TauCeti.FGComoduleCat.instHasForget₂HomCarrierObjComoduleCatIsFGModuleCatLinearMapIdCarrier = CategoryTheory.HasForget₂.trans (TauCeti.FGComoduleCat R C) (TauCeti.ComoduleCat R C) (ModuleCat R)

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

@[simp]

theorem TauCeti.FGComoduleCat.hom_zero {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : FGComoduleCat R C} : CategoryTheory.InducedCategory.Hom.hom 0 = 0

The ambient comodule morphism underlying the zero morphism is the zero morphism.

@[simp]

theorem TauCeti.FGComoduleCat.hom_add {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : FGComoduleCat R C} (f g : M ⟶ N) : (f + g).hom = f.hom + g.hom

The ambient comodule morphism underlying a sum is the sum of the underlying morphisms.

@[simp]

theorem TauCeti.FGComoduleCat.hom_neg {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : FGComoduleCat R C} (f : M ⟶ N) : (-f).hom = -f.hom

The ambient comodule morphism underlying a negation is the negation of the underlying morphism.

@[simp]

theorem TauCeti.FGComoduleCat.hom_sub {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : FGComoduleCat R C} (f g : M ⟶ N) : (f - g).hom = f.hom - g.hom

The ambient comodule morphism underlying a difference is the difference of the underlying morphisms.

@[simp]

theorem TauCeti.FGComoduleCat.zero_apply {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : FGComoduleCat R C} (m : ↑M) : (CategoryTheory.ConcreteCategory.hom 0) m = 0

The zero morphism acts as the zero function.

@[simp]

theorem TauCeti.FGComoduleCat.add_apply {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : FGComoduleCat R C} (f g : M ⟶ N) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (f + g)) m = (CategoryTheory.ConcreteCategory.hom f) m + (CategoryTheory.ConcreteCategory.hom g) m

Addition of morphisms acts by pointwise addition.

@[simp]

theorem TauCeti.FGComoduleCat.neg_apply {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : FGComoduleCat R C} (f : M ⟶ N) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (-f)) m = -(CategoryTheory.ConcreteCategory.hom f) m

Negation of morphisms acts by pointwise negation.

@[simp]

theorem TauCeti.FGComoduleCat.sub_apply {R : Type u} [CommRing R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N : FGComoduleCat R C} (f g : M ⟶ N) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (f - g)) m = (CategoryTheory.ConcreteCategory.hom f) m - (CategoryTheory.ConcreteCategory.hom g) m

Subtraction of morphisms acts by pointwise subtraction.