Products of comodules

This file equips the product of two right comodules over a fixed coalgebra with the direct-sum coaction. For comodules M and N, the coaction on M × N is ρ(m, n) = (inl ⊗ id) (ρ m) + (inr ⊗ id) (ρ n).

The file also records that the four standard linear maps for a product, fst, snd, inl, and inr, are comodule morphisms for this coaction. This is additive infrastructure for the finite-dimensional comodule representation category in the reductive-groups roadmap.

Main declarations

• TauCeti.Comodule.Prod: the direct-sum comodule structure on M × N.
• TauCeti.Comodule.prodFst, prodSnd, prodInl, prodInr: the four canonical comodule morphisms.
• TauCeti.ComoduleCat.prod: the bundled product comodule, with projections, inclusions, prodLift, and prodDesc.

References

This supplies a prerequisite for TauCetiRoadmap/ReductiveGroups/README.md, Layer 1 target "Comodules over a coalgebra/Hopf algebra": the finite-dimensional comodule category should be an additive category before tensor products, duals, and Tannakian reconstruction are built on top. The construction is the standard direct sum of comodules; see Sweedler, Hopf Algebras, Chapter 2.

def TauCeti.Comodule.prodCoact {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : M × N →ₗ[R] TensorProduct R (M × N) C

The direct-sum coaction on the product of two comodules.

Equations

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

@[simp]

theorem TauCeti.Comodule.prodCoact_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (x : M × N) : prodCoact x = (TensorProduct.map (LinearMap.inl R M N) LinearMap.id) (coact x.1) + (TensorProduct.map (LinearMap.inr R M N) LinearMap.id) (coact x.2)

The product coaction evaluated on a pair.

theorem TauCeti.Comodule.prodCoact_inl {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (m : M) : prodCoact ((LinearMap.inl R M N) m) = (TensorProduct.map (LinearMap.inl R M N) LinearMap.id) (coact m)

The product coaction after the left inclusion.

theorem TauCeti.Comodule.prodCoact_inr {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (n : N) : prodCoact ((LinearMap.inr R M N) n) = (TensorProduct.map (LinearMap.inr R M N) LinearMap.id) (coact n)

The product coaction after the right inclusion.

theorem TauCeti.Comodule.prodCoact_coassoc {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : ↑(TensorProduct.assoc R (M × N) C C) ∘ₗ LinearMap.rTensor C prodCoact ∘ₗ prodCoact = LinearMap.lTensor (M × N) CoalgebraStruct.comul ∘ₗ prodCoact

theorem TauCeti.Comodule.prodCoact_counit {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : LinearMap.lTensor (M × N) CoalgebraStruct.counit ∘ₗ prodCoact = (TensorProduct.mk R (M × N) R).flip 1

@[implicit_reducible]

def TauCeti.Comodule.Prod {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : Comodule R C (M × N)

The product of two right comodules, with the direct-sum coaction.

Equations

• TauCeti.Comodule.Prod = { coact := TauCeti.Comodule.prodCoact, coassoc := ⋯, lTensor_counit_comp_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.Prod_coact {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : coact = prodCoact

The coaction in Comodule.Prod is Comodule.prodCoact.

def TauCeti.Comodule.prodFst {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : Hom R C (M × N) M

The first projection from the product comodule.

Equations

• TauCeti.Comodule.prodFst = { toLinearMap := LinearMap.fst R M N, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.prodFst_toLinearMap {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : prodFst.toLinearMap = LinearMap.fst R M N

The underlying linear map of the first projection from the product comodule.

@[simp]

theorem TauCeti.Comodule.prodFst_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (x : M × N) : prodFst x = x.1

Evaluating the first projection from the product comodule returns the first component.

def TauCeti.Comodule.prodSnd {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : Hom R C (M × N) N

The second projection from the product comodule.

Equations

• TauCeti.Comodule.prodSnd = { toLinearMap := LinearMap.snd R M N, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.prodSnd_toLinearMap {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : prodSnd.toLinearMap = LinearMap.snd R M N

The underlying linear map of the second projection from the product comodule.

@[simp]

theorem TauCeti.Comodule.prodSnd_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (x : M × N) : prodSnd x = x.2

Evaluating the second projection from the product comodule returns the second component.

def TauCeti.Comodule.prodInl {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : Hom R C M (M × N)

The left inclusion into the product comodule.

Equations

• TauCeti.Comodule.prodInl = { toLinearMap := LinearMap.inl R M N, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.prodInl_toLinearMap {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : prodInl.toLinearMap = LinearMap.inl R M N

The underlying linear map of the left inclusion into the product comodule.

@[simp]

theorem TauCeti.Comodule.prodInl_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (m : M) : prodInl m = (m, 0)

Evaluating the left inclusion into the product comodule gives a pair with zero right component.

def TauCeti.Comodule.prodInr {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : Hom R C N (M × N)

The right inclusion into the product comodule.

Equations

• TauCeti.Comodule.prodInr = { toLinearMap := LinearMap.inr R M N, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.prodInr_toLinearMap {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] : prodInr.toLinearMap = LinearMap.inr R M N

The underlying linear map of the right inclusion into the product comodule.

@[simp]

theorem TauCeti.Comodule.prodInr_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] (n : N) : prodInr n = (0, n)

Evaluating the right inclusion into the product comodule gives a pair with zero left component.

def TauCeti.Comodule.prodLift {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] (f : Hom R C P M) (g : Hom R C P N) : Hom R C P (M × N)

The product morphism induced by two morphisms with a common source.

Equations

• TauCeti.Comodule.prodLift f g = { toLinearMap := f.prod g.toLinearMap, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.prodLift_toLinearMap {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] (f : Hom R C P M) (g : Hom R C P N) : (prodLift f g).toLinearMap = f.prod g.toLinearMap

The underlying linear map of Comodule.prodLift.

@[simp]

theorem TauCeti.Comodule.prodLift_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] (f : Hom R C P M) (g : Hom R C P N) (p : P) : (prodLift f g) p = (f p, g p)

Evaluating Comodule.prodLift gives the pair of evaluations.

def TauCeti.Comodule.prodDesc {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] (f : Hom R C M P) (g : Hom R C N P) : Hom R C (M × N) P

The product morphism induced by two morphisms with a common target.

Equations

• TauCeti.Comodule.prodDesc f g = { toLinearMap := f.coprod g.toLinearMap, map_coact := ⋯ }

@[simp]

theorem TauCeti.Comodule.prodDesc_toLinearMap {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] (f : Hom R C M P) (g : Hom R C N P) : (prodDesc f g).toLinearMap = f.coprod g.toLinearMap

The underlying linear map of Comodule.prodDesc.

@[simp]

theorem TauCeti.Comodule.prodDesc_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M : Type w} {N : Type x} [AddCommMonoid M] [Module R M] [Comodule R C M] [AddCommMonoid N] [Module R N] [Comodule R C N] {P : Type u_1} [AddCommMonoid P] [Module R P] [Comodule R C P] (f : Hom R C M P) (g : Hom R C N P) (x : M × N) : (prodDesc f g) x = f x.1 + g x.2

Evaluating Comodule.prodDesc adds the evaluations of its two components.

@[reducible, inline]

abbrev TauCeti.ComoduleCat.prod (R : Type u) [CommSemiring R] (C : Type v) [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) : ComoduleCat R C

The product of two bundled comodules, carried by the product of the underlying modules.

Equations

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

@[reducible, inline]

abbrev TauCeti.ComoduleCat.prodFst {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) : prod R C M N ⟶ M

The first projection from the bundled product comodule.

Equations

• M.prodFst N = TauCeti.Comodule.prodFst

@[reducible, inline]

abbrev TauCeti.ComoduleCat.prodSnd {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) : prod R C M N ⟶ N

The second projection from the bundled product comodule.

Equations

• M.prodSnd N = TauCeti.Comodule.prodSnd

@[reducible, inline]

abbrev TauCeti.ComoduleCat.prodLift {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {P M N : ComoduleCat R C} (f : P ⟶ M) (g : P ⟶ N) : P ⟶ prod R C M N

The morphism into the bundled product induced by a pair of morphisms.

Equations

• TauCeti.ComoduleCat.prodLift f g = TauCeti.Comodule.prodLift f g

@[reducible, inline]

abbrev TauCeti.ComoduleCat.prodInl {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) : M ⟶ prod R C M N

The left inclusion into the bundled product comodule.

Equations

• M.prodInl N = TauCeti.Comodule.prodInl

@[reducible, inline]

abbrev TauCeti.ComoduleCat.prodInr {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) : N ⟶ prod R C M N

The right inclusion into the bundled product comodule.

Equations

• M.prodInr N = TauCeti.Comodule.prodInr

@[reducible, inline]

abbrev TauCeti.ComoduleCat.prodDesc {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N P : ComoduleCat R C} (f : M ⟶ P) (g : N ⟶ P) : prod R C M N ⟶ P

The morphism out of the bundled product induced by a pair of morphisms.

Equations

• TauCeti.ComoduleCat.prodDesc f g = TauCeti.Comodule.prodDesc f g

@[simp]

theorem TauCeti.ComoduleCat.prodFst_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) (x : ↑(prod R C M N).toSemimoduleCat) : (CategoryTheory.ConcreteCategory.hom (M.prodFst N)) x = x.1

Evaluating the bundled first projection returns the first component.

@[simp]

theorem TauCeti.ComoduleCat.prodSnd_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) (x : ↑(prod R C M N).toSemimoduleCat) : (CategoryTheory.ConcreteCategory.hom (M.prodSnd N)) x = x.2

Evaluating the bundled second projection returns the second component.

@[simp]

theorem TauCeti.ComoduleCat.prodLift_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {P M N : ComoduleCat R C} (f : P ⟶ M) (g : P ⟶ N) (p : ↑P.toSemimoduleCat) : (CategoryTheory.ConcreteCategory.hom (prodLift f g)) p = ((CategoryTheory.ConcreteCategory.hom f) p, (CategoryTheory.ConcreteCategory.hom g) p)

Evaluating the bundled product lift gives the pair of evaluations.

@[simp]

theorem TauCeti.ComoduleCat.prodInl_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) (m : ↑M.toSemimoduleCat) : (CategoryTheory.ConcreteCategory.hom (M.prodInl N)) m = (m, 0)

Evaluating the bundled left inclusion gives a pair with zero right component.

@[simp]

theorem TauCeti.ComoduleCat.prodInr_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) (n : ↑N.toSemimoduleCat) : (CategoryTheory.ConcreteCategory.hom (M.prodInr N)) n = (0, n)

Evaluating the bundled right inclusion gives a pair with zero left component.

@[simp]

theorem TauCeti.ComoduleCat.prodDesc_apply {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N P : ComoduleCat R C} (f : M ⟶ P) (g : N ⟶ P) (x : ↑(prod R C M N).toSemimoduleCat) : (CategoryTheory.ConcreteCategory.hom (prodDesc f g)) x = (CategoryTheory.ConcreteCategory.hom f) x.1 + (CategoryTheory.ConcreteCategory.hom g) x.2

Evaluating the bundled product desc adds the evaluations of its two components.

@[simp]

theorem TauCeti.ComoduleCat.prodLift_fst {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {P M N : ComoduleCat R C} (f : P ⟶ M) (g : P ⟶ N) : CategoryTheory.CategoryStruct.comp (prodLift f g) (M.prodFst N) = f

The first projection after the bundled product lift is the first morphism.

@[simp]

theorem TauCeti.ComoduleCat.prodLift_snd {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {P M N : ComoduleCat R C} (f : P ⟶ M) (g : P ⟶ N) : CategoryTheory.CategoryStruct.comp (prodLift f g) (M.prodSnd N) = g

The second projection after the bundled product lift is the second morphism.

@[simp]

theorem TauCeti.ComoduleCat.prodInl_desc {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N P : ComoduleCat R C} (f : M ⟶ P) (g : N ⟶ P) : CategoryTheory.CategoryStruct.comp (M.prodInl N) (prodDesc f g) = f

The bundled product desc after the left inclusion is the first morphism.

@[simp]

theorem TauCeti.ComoduleCat.prodInr_desc {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N P : ComoduleCat R C} (f : M ⟶ P) (g : N ⟶ P) : CategoryTheory.CategoryStruct.comp (M.prodInr N) (prodDesc f g) = g

The bundled product desc after the right inclusion is the second morphism.

@[simp]

theorem TauCeti.ComoduleCat.prodInl_fst {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) : CategoryTheory.CategoryStruct.comp (M.prodInl N) (M.prodFst N) = CategoryTheory.CategoryStruct.id M

The first projection after the left inclusion is the identity.

@[simp]

theorem TauCeti.ComoduleCat.prodInl_snd {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) : CategoryTheory.CategoryStruct.comp (M.prodInl N) (M.prodSnd N) = 0

The second projection after the left inclusion is zero.

@[simp]

theorem TauCeti.ComoduleCat.prodInr_fst {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) : CategoryTheory.CategoryStruct.comp (M.prodInr N) (M.prodFst N) = 0

The first projection after the right inclusion is zero.

@[simp]

theorem TauCeti.ComoduleCat.prodInr_snd {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) : CategoryTheory.CategoryStruct.comp (M.prodInr N) (M.prodSnd N) = CategoryTheory.CategoryStruct.id N

The second projection after the right inclusion is the identity.

@[simp]

theorem TauCeti.ComoduleCat.prod_fst_inl_add_snd_inr {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] (M N : ComoduleCat R C) : CategoryTheory.CategoryStruct.comp (M.prodFst N) (M.prodInl N) + CategoryTheory.CategoryStruct.comp (M.prodSnd N) (M.prodInr N) = CategoryTheory.CategoryStruct.id (prod R C M N)

The two projection-inclusion composites reconstruct the identity of the bundled product.

theorem TauCeti.ComoduleCat.prod_hom_ext {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {P M N : ComoduleCat R C} {f g : P ⟶ prod R C M N} (hfst : CategoryTheory.CategoryStruct.comp f (M.prodFst N) = CategoryTheory.CategoryStruct.comp g (M.prodFst N)) (hsnd : CategoryTheory.CategoryStruct.comp f (M.prodSnd N) = CategoryTheory.CategoryStruct.comp g (M.prodSnd N)) : f = g

Morphisms into the bundled product are determined by their projections.

theorem TauCeti.ComoduleCat.prod_hom_ext_iff {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {P M N : ComoduleCat R C} {f g : P ⟶ prod R C M N} : f = g ↔ CategoryTheory.CategoryStruct.comp f (M.prodFst N) = CategoryTheory.CategoryStruct.comp g (M.prodFst N) ∧ CategoryTheory.CategoryStruct.comp f (M.prodSnd N) = CategoryTheory.CategoryStruct.comp g (M.prodSnd N)

theorem TauCeti.ComoduleCat.prod_hom_ext' {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N P : ComoduleCat R C} {f g : prod R C M N ⟶ P} (hinl : CategoryTheory.CategoryStruct.comp (M.prodInl N) f = CategoryTheory.CategoryStruct.comp (M.prodInl N) g) (hinr : CategoryTheory.CategoryStruct.comp (M.prodInr N) f = CategoryTheory.CategoryStruct.comp (M.prodInr N) g) : f = g

Morphisms out of the bundled product are determined by their values on the inclusions.

theorem TauCeti.ComoduleCat.prod_hom_ext'_iff {R : Type u} [CommSemiring R] {C : Type v} [AddCommMonoid C] [Module R C] [Coalgebra R C] {M N P : ComoduleCat R C} {f g : prod R C M N ⟶ P} : f = g ↔ CategoryTheory.CategoryStruct.comp (M.prodInl N) f = CategoryTheory.CategoryStruct.comp (M.prodInl N) g ∧ CategoryTheory.CategoryStruct.comp (M.prodInr N) f = CategoryTheory.CategoryStruct.comp (M.prodInr N) g

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

The concrete product of comodules is their categorical binary product.

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

Comodules have binary products.

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

Comodules have finite products.