Documentation

Mathlib.Algebra.Category.HopfAlgCat.Monoidal

The monoidal structure on the category of Hopf algebras #

In Mathlib/RingTheory/HopfAlgebra/TensorProduct.lean, given two Hopf R-algebras A, B, we define a Hopf R-algebra instance on A ⊗[R] B.

Here, we use this to declare a MonoidalCategory instance on the category of Hopf algebras, via the existing monoidal structure on BialgCat.

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

The data needed to induce a MonoidalCategory structure via HopfAlgCat.instMonoidalCategoryStruct and the forgetful functor to bialgebras.

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

    forget₂ (HopfAlgCat R) (BialgCat R) is a monoidal functor.

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