Documentation

Mathlib.Algebra.Category.CoalgebraCat.Monoidal

The monoidal category structure on R-coalgebras #

In Mathlib.RingTheory.Coalgebra.TensorProduct, given two R-coalgebras M, N, we define a coalgebra instance on M ⊗[R] N, as well as the tensor product of two CoalgHoms as a CoalgHom, and the associator and left/right unitors for coalgebras as CoalgEquivs.

In this file, we declare a MonoidalCategory instance on the category of coalgebras, with data fields given by the definitions in Mathlib.RingTheory.Coalgebra.TensorProduct, and Prop fields proved by pulling back the MonoidalCategory instance on the category of modules, using Monoidal.induced.

@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_whiskerRight_toCoalgHom (R : Type u) [CommRing R] :
∀ {X₁ X₂ : CoalgebraCat R} (f : X₁ X₂) (X : CoalgebraCat R), (CategoryTheory.MonoidalCategory.whiskerRight f X).toCoalgHom = CoalgHom.rTensor (↑X.toModuleCat) f.toCoalgHom
@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_tensorHom_toCoalgHom (R : Type u) [CommRing R] :
∀ {X₁ Y₁ X₂ Y₂ : CoalgebraCat R} (f : X₁ Y₁) (g : X₂ Y₂), (CategoryTheory.MonoidalCategory.tensorHom f g).toCoalgHom = Coalgebra.TensorProduct.map f.toCoalgHom g.toCoalgHom
@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_whiskerLeft_toCoalgHom (R : Type u) [CommRing R] (X : CoalgebraCat R) :
∀ (x x_1 : CoalgebraCat R) (f : x x_1), (CategoryTheory.MonoidalCategory.whiskerLeft X f).toCoalgHom = CoalgHom.lTensor (↑X.toModuleCat) f.toCoalgHom
@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_associator (R : Type u) [CommRing R] (X : CoalgebraCat R) (Y : CoalgebraCat R) (Z : CoalgebraCat R) :
CategoryTheory.MonoidalCategory.associator X Y Z = (Coalgebra.TensorProduct.assoc R X.toModuleCat Y.toModuleCat Z.toModuleCat).toCoalgebraCatIso
Equations
  • One or more equations did not get rendered due to their size.

The data needed to induce a MonoidalCategory structure via CoalgebraCat.instMonoidalCategoryStruct and the forgetful functor to modules.

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