Documentation

Mathlib.Algebra.Category.HopfAlgebraCat.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 BialgebraCat.

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

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

    forget₂ (HopfAlgebraCat R) (BialgebraCat R) is a monoidal functor.

    Equations