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.

@[implicit_reducible]

noncomputable instance BialgCat.instMonoidalCategoryStruct (R : Type u) [CommRing R] : CategoryTheory.MonoidalCategoryStruct (BialgCat R)

@[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

@[simp]

theorem BialgCat.leftUnitor_def (R : Type u) [CommRing R] (X : BialgCat R) : CategoryTheory.MonoidalCategoryStruct.leftUnitor X = (Bialgebra.TensorProduct.lid R X.carrier).toBialgIso

@[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')

@[simp]

theorem BialgCat.tensorUnit_def (R : Type u) [CommRing R] : CategoryTheory.MonoidalCategoryStruct.tensorUnit (BialgCat R) = of R R

@[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)

@[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')

@[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

@[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')

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.

@[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✝¹))

@[simp]

theorem BialgCat.MonoidalCategory.inducingFunctorData_εIso (R : Type u) [CommRing R] : (inducingFunctorData R).εIso = CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorUnit (AlgCat R))

@[implicit_reducible]

noncomputable instance BialgCat.instMonoidalCategory (R : Type u) [CommRing R] : CategoryTheory.MonoidalCategory (BialgCat R)

@[implicit_reducible]

noncomputable instance BialgCat.instMonoidalAlgCatForget₂BialgHomCarrierAlgHomCarrier (R : Type u) [CommRing R] : (CategoryTheory.forget₂ (BialgCat R) (AlgCat R)).Monoidal

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

@[implicit_reducible]

noncomputable instance BialgCat.instMonoidalCoalgCatForget₂BialgHomCarrierCoalgHomCarrier (R : Type u) [CommRing R] : (CategoryTheory.forget₂ (BialgCat R) (CoalgCat R)).Monoidal

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