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_isModule (R : Type u) [CommRing R] (X Y : CoalgebraCat R) :
(CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).isModule = TensorProduct.instModule
source
@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_tensorUnit_isAddCommGroup (R : Type u) [CommRing R] :
(𝟙_ (CoalgebraCat R)).isAddCommGroup = Ring.toAddCommGroup
source
@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_tensorObj_isAddCommGroup (R : Type u) [CommRing R] (X Y : CoalgebraCat R) :
(CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).isAddCommGroup = TensorProduct.addCommGroup
source
@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_tensorUnit_carrier (R : Type u) [CommRing R] :
↑(𝟙_ (CoalgebraCat R)).toModuleCat = R
source
@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_whiskerLeft (R : Type u) [CommRing R] (X x✝ x✝¹ : CoalgebraCat R) (f : x✝ ⟶ x✝¹) :
CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f = ofHom (CoalgHom.lTensor (↑X.toModuleCat) f.toCoalgHom')
source
@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_tensorObj_carrier (R : Type u) [CommRing R] (X Y : CoalgebraCat R) :
↑(CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).toModuleCat = 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_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_whiskerRight (R : Type u) [CommRing R] {X₁✝ X₂✝ : CoalgebraCat R} (f : X₁✝ ⟶ X₂✝) (X : CoalgebraCat R) :
CategoryTheory.MonoidalCategoryStruct.whiskerRight f X = ofHom (CoalgHom.rTensor (↑X.toModuleCat) f.toCoalgHom')
source
@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_tensorUnit_instCoalgebra (R : Type u) [CommRing R] :
(𝟙_ (CoalgebraCat R)).instCoalgebra = inferInstance
source
@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_tensorHom (R : Type u) [CommRing R] {X₁✝ Y₁✝ X₂✝ Y₂✝ : CoalgebraCat R} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) :
CategoryTheory.MonoidalCategoryStruct.tensorHom f g = ofHom (Coalgebra.TensorProduct.map f.toCoalgHom' g.toCoalgHom')
source
@[simp]
theorem CoalgebraCat.instMonoidalCategoryStruct_tensorObj_instCoalgebra (R : Type u) [CommRing R] (X Y : CoalgebraCat R) :
(CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).instCoalgebra = inferInstance
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_tensorUnit_isModule (R : Type u) [CommRing R] :
(𝟙_ (CoalgebraCat R)).isModule = Semiring.toModule
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] (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
    @[simp]
    theorem CoalgebraCat.MonoidalCategory.inducingFunctorData_εIso (R : Type u) [CommRing R] :
    (inducingFunctorData R).εIso = CategoryTheory.Iso.refl (𝟙_ (ModuleCat R))
    source
    noncomputable instance CoalgebraCat.instMonoidalCategory (R : Type u) [CommRing R] :
    CategoryTheory.MonoidalCategory (CoalgebraCat R)
    Equations