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.

source
noncomputable instance CoalgebraCat.instMonoidalCategoryStruct (R : Type u) [CommRing R] :
CategoryTheory.MonoidalCategoryStruct (CoalgebraCat R)
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_tensorObj (R : Type u) [CommRing R] (X Y : CoalgebraCat R) :
CategoryTheory.MonoidalCategoryStruct.tensorObj X Y = of R (TensorProduct R ↑X.toModuleCat ↑Y.toModuleCat)
source
@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_rightUnitor (R : Type u) [CommRing R] (X : CoalgebraCat R) :
CategoryTheory.MonoidalCategoryStruct.rightUnitor X = (Coalgebra.TensorProduct.rid R ↑X.toModuleCat).toCoalgebraCatIso
source
@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_whiskerRight_toCoalgHom (R : Type u) [CommRing R] {X₁✝ X₂✝ : CoalgebraCat R} (f : X₁✝ ⟶ X₂✝) (X : CoalgebraCat R) :
(CategoryTheory.MonoidalCategoryStruct.whiskerRight f X).toCoalgHom = CoalgHom.rTensor (↑X.toModuleCat) f.toCoalgHom
source
@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_whiskerLeft_toCoalgHom (R : Type u) [CommRing R] (X x✝ x✝¹ : CoalgebraCat R) (f : x✝ ⟶ x✝¹) :
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).toCoalgHom = CoalgHom.lTensor (↑X.toModuleCat) f.toCoalgHom
source
@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_associator (R : Type u) [CommRing R] (X Y Z : CoalgebraCat R) :
CategoryTheory.MonoidalCategoryStruct.associator X Y Z = (Coalgebra.TensorProduct.assoc R ↑X.toModuleCat ↑Y.toModuleCat ↑Z.toModuleCat).toCoalgebraCatIso
source
@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_leftUnitor (R : Type u) [CommRing R] (X : CoalgebraCat R) :
CategoryTheory.MonoidalCategoryStruct.leftUnitor X = (Coalgebra.TensorProduct.lid R ↑X.toModuleCat).toCoalgebraCatIso
source
@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_tensorHom_toCoalgHom (R : Type u) [CommRing R] {X₁✝ Y₁✝ X₂✝ Y₂✝ : CoalgebraCat R} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) :
(CategoryTheory.MonoidalCategoryStruct.tensorHom f g).toCoalgHom = Coalgebra.TensorProduct.map f.toCoalgHom g.toCoalgHom
source
@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_tensorUnit (R : Type u) [CommRing R] :
𝟙_ (CoalgebraCat R) = of R R
source
noncomputable def CoalgebraCat.MonoidalCategory.inducingFunctorData (R : Type u) [CommRing R] :
CategoryTheory.Monoidal.InducingFunctorData (CategoryTheory.forget₂ (CoalgebraCat R) (ModuleCat R))

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
    source
    @[simp]
    theorem CoalgebraCat.MonoidalCategory.inducingFunctorData_εIso (R : Type u) [CommRing R] :
    (inducingFunctorData R).εIso = CategoryTheory.Iso.refl (𝟙_ (ModuleCat R))
    source
    @[simp]
    theorem CoalgebraCat.MonoidalCategory.inducingFunctorData_μIso (R : Type u) [CommRing R] (x✝ x✝¹ : CoalgebraCat R) :
    (inducingFunctorData R).μIso x✝ x✝¹ = CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.forget₂ (CoalgebraCat R) (ModuleCat R)).obj x✝) ((CategoryTheory.forget₂ (CoalgebraCat R) (ModuleCat R)).obj x✝¹))
    source
    noncomputable instance CoalgebraCat.instMonoidalCategory (R : Type u) [CommRing R] :
    CategoryTheory.MonoidalCategory (CoalgebraCat R)
    Equations