Documentation

Mathlib.Algebra.Category.CoalgCat.Monoidal

The monoidal category structure on R-coalgebras #

In Mathlib/RingTheory/Coalgebra/TensorProduct.lean, 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.lean, and Prop fields proved by pulling back the MonoidalCategory instance on the category of modules, using Monoidal.induced.

source
noncomputable instance CoalgCat.instMonoidalCategoryStruct (R : Type u) [CommRing R] :
CategoryTheory.MonoidalCategoryStruct (CoalgCat R)
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CoalgCat.whiskerRight_def (R : Type u) [CommRing R] {X₁✝ X₂✝ : CoalgCat R} (f : X₁✝ ⟶ X₂✝) (X : CoalgCat R) :
CategoryTheory.MonoidalCategoryStruct.whiskerRight f X = ofHom (CoalgHom.rTensor (↑X.toModuleCat) f.toCoalgHom')
source
@[simp]
theorem CoalgCat.associator_def (R : Type u) [CommRing R] (X Y Z : CoalgCat R) :
CategoryTheory.MonoidalCategoryStruct.associator X Y Z = (Coalgebra.TensorProduct.assoc R R ↑X.toModuleCat ↑Y.toModuleCat ↑Z.toModuleCat).toCoalgIso
source
@[simp]
theorem CoalgCat.tensorUnit_instCoalgebra (R : Type u) [CommRing R] :
(CategoryTheory.MonoidalCategoryStruct.tensorUnit (CoalgCat R)).instCoalgebra = inferInstance
source
@[simp]
theorem CoalgCat.tensorObj_instCoalgebra (R : Type u) [CommRing R] (X Y : CoalgCat R) :
(CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).instCoalgebra = inferInstance
source
@[simp]
theorem CoalgCat.rightUnitor_def (R : Type u) [CommRing R] (X : CoalgCat R) :
CategoryTheory.MonoidalCategoryStruct.rightUnitor X = (Coalgebra.TensorProduct.rid R R ↑X.toModuleCat).toCoalgIso
source
@[simp]
theorem CoalgCat.tensorUnit_carrier (R : Type u) [CommRing R] :
↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (CoalgCat R)).toModuleCat = R
source
@[simp]
theorem CoalgCat.tensorObj_carrier (R : Type u) [CommRing R] (X Y : CoalgCat R) :
↑(CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).toModuleCat = TensorProduct R ↑X.toModuleCat ↑Y.toModuleCat
source
@[simp]
theorem CoalgCat.tensorUnit_isAddCommGroup (R : Type u) [CommRing R] :
(CategoryTheory.MonoidalCategoryStruct.tensorUnit (CoalgCat R)).isAddCommGroup = inst✝.toAddCommGroup
source
@[simp]
theorem CoalgCat.tensorUnit_isModule (R : Type u) [CommRing R] :
(CategoryTheory.MonoidalCategoryStruct.tensorUnit (CoalgCat R)).isModule = Semiring.toModule
source
@[simp]
theorem CoalgCat.tensorHom_def (R : Type u) [CommRing R] {X₁✝ Y₁✝ X₂✝ Y₂✝ : CoalgCat R} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) :
CategoryTheory.MonoidalCategoryStruct.tensorHom f g = ofHom (Coalgebra.TensorProduct.map f.toCoalgHom' g.toCoalgHom')
source
@[simp]
theorem CoalgCat.tensorObj_isAddCommGroup (R : Type u) [CommRing R] (X Y : CoalgCat R) :
(CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).isAddCommGroup = TensorProduct.addCommGroup
source
@[simp]
theorem CoalgCat.tensorObj_isModule (R : Type u) [CommRing R] (X Y : CoalgCat R) :
(CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).isModule = TensorProduct.instModule
source
@[simp]
theorem CoalgCat.whiskerLeft_def (R : Type u) [CommRing R] (X x✝ x✝¹ : CoalgCat R) (f : x✝ ⟶ x✝¹) :
CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f = ofHom (CoalgHom.lTensor (↑X.toModuleCat) f.toCoalgHom')
source
@[simp]
theorem CoalgCat.leftUnitor_def (R : Type u) [CommRing R] (X : CoalgCat R) :
CategoryTheory.MonoidalCategoryStruct.leftUnitor X = (Coalgebra.TensorProduct.lid R ↑X.toModuleCat).toCoalgIso
source
noncomputable def CoalgCat.MonoidalCategory.inducingFunctorData (R : Type u) [CommRing R] :
CategoryTheory.Monoidal.InducingFunctorData (CategoryTheory.forget₂ (CoalgCat R) (ModuleCat R))

The data needed to induce a MonoidalCategory structure via CoalgCat.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 CoalgCat.MonoidalCategory.inducingFunctorData_εIso (R : Type u) [CommRing R] :
    (inducingFunctorData R).εIso = CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R))
    source
    @[simp]
    theorem CoalgCat.MonoidalCategory.inducingFunctorData_μIso (R : Type u) [CommRing R] (x✝ x✝¹ : CoalgCat R) :
    (inducingFunctorData R).μIso x✝ x✝¹ = CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.forget₂ (CoalgCat R) (ModuleCat R)).obj x✝) ((CategoryTheory.forget₂ (CoalgCat R) (ModuleCat R)).obj x✝¹))
    source
    noncomputable instance CoalgCat.instMonoidalCategory (R : Type u) [CommRing R] :
    CategoryTheory.MonoidalCategory (CoalgCat R)
    Equations