Documentation

Mathlib.Algebra.Category.BialgCat.Monoidal

The monoidal structure on the category of bialgebras #

In Mathlib/RingTheory/Bialgebra/TensorProduct.lean, given two R-bialgebras A, B, we define a bialgebra instance on A ⊗[R] B as well as the tensor product of two BialgHoms as a BialgHom, and the associator and left/right unitors for bialgebras as BialgEquivs. In this file, we declare a MonoidalCategory instance on the category of bialgebras, with data fields given by the definitions in Mathlib/RingTheory/Bialgebra/TensorProduct.lean, and Prop fields proved by pulling back the MonoidalCategory instance on the category of algebras, using Monoidal.induced.

source
noncomputable instance BialgCat.instMonoidalCategoryStruct (R : Type u) [CommRing R] :
CategoryTheory.MonoidalCategoryStruct (BialgCat R)
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem BialgCat.rightUnitor_def (R : Type u) [CommRing R] (X : BialgCat R) :
CategoryTheory.MonoidalCategoryStruct.rightUnitor X = (Bialgebra.TensorProduct.rid R R X.carrier).toBialgIso
source
@[simp]
theorem BialgCat.leftUnitor_def (R : Type u) [CommRing R] (X : BialgCat R) :
CategoryTheory.MonoidalCategoryStruct.leftUnitor X = (Bialgebra.TensorProduct.lid R X.carrier).toBialgIso
source
@[simp]
theorem BialgCat.tensorObj_def (R : Type u) [CommRing R] (X Y : BialgCat R) :
CategoryTheory.MonoidalCategoryStruct.tensorObj X Y = of R (TensorProduct R X.carrier Y.carrier)
source
@[simp]
theorem BialgCat.tensorUnit_def (R : Type u) [CommRing R] :
CategoryTheory.MonoidalCategoryStruct.tensorUnit (BialgCat R) = of R R
source
@[simp]
theorem BialgCat.whiskerLeft_def (R : Type u) [CommRing R] (X x✝ x✝¹ : BialgCat R) (f : x✝ ⟶ x✝¹) :
CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f = ofHom (BialgHom.lTensor X.carrier f.toBialgHom')
source
@[simp]
theorem BialgCat.tensorHom_def (R : Type u) [CommRing R] {X₁✝ Y₁✝ X₂✝ Y₂✝ : BialgCat R} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) :
CategoryTheory.MonoidalCategoryStruct.tensorHom f g = ofHom (Bialgebra.TensorProduct.map f.toBialgHom' g.toBialgHom')
source
@[simp]
theorem BialgCat.associator_def (R : Type u) [CommRing R] (X Y Z : BialgCat R) :
CategoryTheory.MonoidalCategoryStruct.associator X Y Z = (Bialgebra.TensorProduct.assoc R R X.carrier Y.carrier Z.carrier).toBialgIso
source
@[simp]
theorem BialgCat.whiskerRight_def (R : Type u) [CommRing R] {X₁✝ X₂✝ : BialgCat R} (f : X₁✝ ⟶ X₂✝) (X : BialgCat R) :
CategoryTheory.MonoidalCategoryStruct.whiskerRight f X = ofHom (BialgHom.rTensor X.carrier f.toBialgHom')
source
noncomputable def BialgCat.MonoidalCategory.inducingFunctorData (R : Type u) [CommRing R] :
CategoryTheory.Monoidal.InducingFunctorData (CategoryTheory.forget₂ (BialgCat R) (AlgCat R))

The data needed to induce a MonoidalCategory structure via BialgCat.instMonoidalCategoryStruct and the forgetful functor to algebras.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem BialgCat.MonoidalCategory.inducingFunctorData_εIso (R : Type u) [CommRing R] :
    (inducingFunctorData R).εIso = CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorUnit (AlgCat R))
    source
    @[simp]
    theorem BialgCat.MonoidalCategory.inducingFunctorData_μIso (R : Type u) [CommRing R] (x✝ x✝¹ : BialgCat R) :
    (inducingFunctorData R).μIso x✝ x✝¹ = CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.forget₂ (BialgCat R) (AlgCat R)).obj x✝) ((CategoryTheory.forget₂ (BialgCat R) (AlgCat R)).obj x✝¹))
    source
    noncomputable instance BialgCat.instMonoidalCategory (R : Type u) [CommRing R] :
    CategoryTheory.MonoidalCategory (BialgCat R)
    Equations
    source
    noncomputable instance BialgCat.instMonoidalAlgCatForget₂ (R : Type u) [CommRing R] :
    (CategoryTheory.forget₂ (BialgCat R) (AlgCat R)).Monoidal

    forget₂ (BialgCat R) (AlgCat R) as a monoidal functor.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    noncomputable instance BialgCat.instMonoidalCoalgCatForget₂ (R : Type u) [CommRing R] :
    (CategoryTheory.forget₂ (BialgCat R) (CoalgCat R)).Monoidal

    forget₂ (BialgCat R) (CoalgCat R) as a monoidal functor.

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