Documentation

Mathlib.Algebra.Category.BialgebraCat.Monoidal

The monoidal structure on the category of bialgebras #

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

source
noncomputable instance BialgebraCat.instMonoidalCategoryStruct (R : Type u) [CommRing R] :
CategoryTheory.MonoidalCategoryStruct (BialgebraCat R)
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem BialgebraCat.instMonoidalCategoryStruct_leftUnitor (R : Type u) [CommRing R] (X : BialgebraCat R) :
CategoryTheory.MonoidalCategoryStruct.leftUnitor X = (Bialgebra.TensorProduct.lid R X.carrier).toBialgebraCatIso
source
@[simp]
theorem BialgebraCat.instMonoidalCategoryStruct_whiskerLeft (R : Type u) [CommRing R] (X x✝ x✝¹ : BialgebraCat R) (f : x✝ ⟶ x✝¹) :
CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f = ofHom (BialgHom.lTensor X.carrier f.toBialgHom')
source
@[simp]
theorem BialgebraCat.instMonoidalCategoryStruct_associator (R : Type u) [CommRing R] (X Y Z : BialgebraCat R) :
CategoryTheory.MonoidalCategoryStruct.associator X Y Z = (Bialgebra.TensorProduct.assoc R X.carrier Y.carrier Z.carrier).toBialgebraCatIso
source
@[simp]
theorem BialgebraCat.instMonoidalCategoryStruct_rightUnitor (R : Type u) [CommRing R] (X : BialgebraCat R) :
CategoryTheory.MonoidalCategoryStruct.rightUnitor X = (Bialgebra.TensorProduct.rid R X.carrier).toBialgebraCatIso
source
@[simp]
theorem BialgebraCat.instMonoidalCategoryStruct_whiskerRight (R : Type u) [CommRing R] {X₁✝ X₂✝ : BialgebraCat R} (f : X₁✝ ⟶ X₂✝) (X : BialgebraCat R) :
CategoryTheory.MonoidalCategoryStruct.whiskerRight f X = ofHom (BialgHom.rTensor X.carrier f.toBialgHom')
source
@[simp]
theorem BialgebraCat.instMonoidalCategoryStruct_tensorObj (R : Type u) [CommRing R] (X Y : BialgebraCat R) :
CategoryTheory.MonoidalCategoryStruct.tensorObj X Y = of R (TensorProduct R X.carrier Y.carrier)
source
@[simp]
theorem BialgebraCat.instMonoidalCategoryStruct_tensorUnit (R : Type u) [CommRing R] :
𝟙_ (BialgebraCat R) = of R R
source
@[simp]
theorem BialgebraCat.instMonoidalCategoryStruct_tensorHom (R : Type u) [CommRing R] {X₁✝ Y₁✝ X₂✝ Y₂✝ : BialgebraCat R} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) :
CategoryTheory.MonoidalCategoryStruct.tensorHom f g = ofHom (Bialgebra.TensorProduct.map f.toBialgHom' g.toBialgHom')
source
noncomputable def BialgebraCat.MonoidalCategory.inducingFunctorData (R : Type u) [CommRing R] :
CategoryTheory.Monoidal.InducingFunctorData (CategoryTheory.forget₂ (BialgebraCat R) (AlgebraCat R))

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

    forget₂ (BialgebraCat R) (AlgebraCat R) as a monoidal functor.

    Equations
    source
    noncomputable instance BialgebraCat.instMonoidalCoalgebraCatForget₂ (R : Type u) [CommRing R] :
    (CategoryTheory.forget₂ (BialgebraCat R) (CoalgebraCat R)).Monoidal

    forget₂ (BialgebraCat R) (CoalgebraCat R) as a monoidal functor.

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