Documentation

Mathlib.CategoryTheory.Monoidal.Hopf_

The category of Hopf monoids in a braided monoidal category. #

TODO #

source
class Hopf_Class {C : Type uā‚} [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) extends Bimon_Class X :
Type vā‚

A Hopf monoid in a braided category C is a bimonoid object in C equipped with an antipode.

Instances
    source
    def Hopf_Class.termš’® :
    Lean.ParserDescr

    The antipode is an endomorphism of the underlying object of the Hopf monoid.

    Equations
    Instances For
      source
      def Hopf_Class.Ā«termš’®[_]Ā» :
      Lean.ParserDescr

      The antipode is an endomorphism of the underlying object of the Hopf monoid.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Hopf_Class.antipode_right'_assoc {C : Type uā‚} {instāœ : CategoryTheory.Category.{vā‚, uā‚} C} {instāœĀ¹ : CategoryTheory.MonoidalCategory C} {instāœĀ² : CategoryTheory.BraidedCategory C} {X : C} [self : Hopf_Class X] {Z : C} (h : X āŸ¶ Z) :
        CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X Hopf_Class.antipode) (CategoryTheory.CategoryStruct.comp Mon_Class.mul h)) = CategoryTheory.CategoryStruct.comp Comon_Class.counit (CategoryTheory.CategoryStruct.comp Mon_Class.one h)
        source
        theorem Hopf_Class.antipode_left'_assoc {C : Type uā‚} {instāœ : CategoryTheory.Category.{vā‚, uā‚} C} {instāœĀ¹ : CategoryTheory.MonoidalCategory C} {instāœĀ² : CategoryTheory.BraidedCategory C} {X : C} [self : Hopf_Class X] {Z : C} (h : X āŸ¶ Z) :
        CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Hopf_Class.antipode X) (CategoryTheory.CategoryStruct.comp Mon_Class.mul h)) = CategoryTheory.CategoryStruct.comp Comon_Class.counit (CategoryTheory.CategoryStruct.comp Mon_Class.one h)
        source
        @[simp]
        theorem Hopf_Class.antipode_left {C : Type uā‚} [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) [Hopf_Class X] :
        CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Hopf_Class.antipode X) Mon_Class.mul) = CategoryTheory.CategoryStruct.comp Comon_Class.counit Mon_Class.one

        The object is provided as an explicit argument.

        source
        @[simp]
        theorem Hopf_Class.antipode_left_assoc {C : Type uā‚} [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) [Hopf_Class X] {Z : C} (h : X āŸ¶ Z) :
        CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Hopf_Class.antipode X) (CategoryTheory.CategoryStruct.comp Mon_Class.mul h)) = CategoryTheory.CategoryStruct.comp Comon_Class.counit (CategoryTheory.CategoryStruct.comp Mon_Class.one h)
        source
        @[simp]
        theorem Hopf_Class.antipode_right {C : Type uā‚} [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) [Hopf_Class X] :
        CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X Hopf_Class.antipode) Mon_Class.mul) = CategoryTheory.CategoryStruct.comp Comon_Class.counit Mon_Class.one

        The object is provided as an explicit argument.

        source
        @[simp]
        theorem Hopf_Class.antipode_right_assoc {C : Type uā‚} [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) [Hopf_Class X] {Z : C} (h : X āŸ¶ Z) :
        CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X Hopf_Class.antipode) (CategoryTheory.CategoryStruct.comp Mon_Class.mul h)) = CategoryTheory.CategoryStruct.comp Comon_Class.counit (CategoryTheory.CategoryStruct.comp Mon_Class.one h)
        source
        structure Hopf_ (C : Type uā‚) [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
        Type (max uā‚ vā‚)

        A Hopf monoid in a braided category C is a bimonoid object in C equipped with an antipode.

        Instances For
          source
          @[simp]
          theorem Hopf_.antipode_left_assoc {C : Type uā‚} [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (self : Hopf_ C) {Z : C} (h : self.X.X.X āŸ¶ Z) :
          CategoryTheory.CategoryStruct.comp self.X.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.antipode self.X.X.X) (CategoryTheory.CategoryStruct.comp self.X.X.mul h)) = CategoryTheory.CategoryStruct.comp self.X.counit.hom (CategoryTheory.CategoryStruct.comp self.X.X.one h)
          source
          @[simp]
          theorem Hopf_.antipode_right_assoc {C : Type uā‚} [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (self : Hopf_ C) {Z : C} (h : self.X.X.X āŸ¶ Z) :
          CategoryTheory.CategoryStruct.comp self.X.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft self.X.X.X self.antipode) (CategoryTheory.CategoryStruct.comp self.X.X.mul h)) = CategoryTheory.CategoryStruct.comp self.X.counit.hom (CategoryTheory.CategoryStruct.comp self.X.X.one h)
          source
          instance Hopf_.instCategory (C : Type uā‚) [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :
          CategoryTheory.Category.{vā‚, max uā‚ vā‚} (Hopf_ C)

          Morphisms of Hopf monoids are just morphisms of the underlying bimonoids. In fact they automatically intertwine the antipodes, proved below.

          Equations
          source
          theorem Hopf_.hom_antipode {C : Type uā‚} [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : Hopf_ C} (f : A āŸ¶ B) :
          CategoryTheory.CategoryStruct.comp f.hom.hom B.antipode = CategoryTheory.CategoryStruct.comp A.antipode f.hom.hom

          Morphisms of Hopf monoids intertwine the antipodes.

          source
          @[simp]
          theorem Hopf_.one_antipode {C : Type uā‚} [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) :
          CategoryTheory.CategoryStruct.comp A.X.X.one A.antipode = A.X.X.one
          source
          @[simp]
          theorem Hopf_.one_antipode_assoc {C : Type uā‚} [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) {Z : C} (h : A.X.X.X āŸ¶ Z) :
          CategoryTheory.CategoryStruct.comp A.X.X.one (CategoryTheory.CategoryStruct.comp A.antipode h) = CategoryTheory.CategoryStruct.comp A.X.X.one h
          source
          @[simp]
          theorem Hopf_.antipode_counit {C : Type uā‚} [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) :
          CategoryTheory.CategoryStruct.comp A.antipode A.X.counit.hom = A.X.counit.hom
          source
          @[simp]
          theorem Hopf_.antipode_counit_assoc {C : Type uā‚} [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) {Z : C} (h : (šŸ™_ (Mon_ C)).X āŸ¶ Z) :
          CategoryTheory.CategoryStruct.comp A.antipode (CategoryTheory.CategoryStruct.comp A.X.counit.hom h) = CategoryTheory.CategoryStruct.comp A.X.counit.hom h

          The antipode is an antihomomorphism with respect to both the monoid and comonoid structures. #

          source
          theorem Hopf_.antipode_comulā‚ {C : Type uā‚} [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) :
          CategoryTheory.CategoryStruct.comp A.X.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight A.antipode A.X.X.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight A.X.comul.hom A.X.X.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X A.X.comul.hom)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.whiskerRight (Ī²_ A.X.X.X A.X.X.X).hom A.X.X.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X (CategoryTheory.MonoidalCategory.tensorObj A.X.X.X A.X.X.X)).inv (CategoryTheory.MonoidalCategory.tensorHom A.X.X.mul A.X.X.mul))))))))) = CategoryTheory.CategoryStruct.comp A.X.counit.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (šŸ™_ C)).inv (CategoryTheory.MonoidalCategory.tensorHom A.X.X.one A.X.X.one))
          source
          theorem Hopf_.antipode_comulā‚‚ {C : Type uā‚} [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) :
          CategoryTheory.CategoryStruct.comp A.X.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight A.X.comul.hom A.X.X.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X A.X.comul.hom)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (Ī²_ A.X.X.X A.X.X.X).hom)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.tensorHom A.antipode A.antipode))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.whiskerRight (Ī²_ A.X.X.X A.X.X.X).hom A.X.X.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X (CategoryTheory.MonoidalCategory.tensorObj A.X.X.X A.X.X.X)).inv (CategoryTheory.MonoidalCategory.tensorHom A.X.X.mul A.X.X.mul)))))))))) = CategoryTheory.CategoryStruct.comp A.X.counit.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (šŸ™_ C)).inv (CategoryTheory.MonoidalCategory.tensorHom A.X.X.one A.X.X.one))

          Auxiliary calculation for antipode_comul. This calculation calls for some ASCII art out of This Week's Finds.

          | | n n | \ / | | / | | / \ | | | S S | | \ / | | / | | /

          \ / \ / v v \ / v |

          We move the left antipode up through the crossing, the right antipode down through the crossing, the right multiplication down across the strand, reassociate the comultiplications, then use antipode_right then antipode_left to simplify.

          source
          theorem Hopf_.antipode_comul {C : Type uā‚} [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) :
          CategoryTheory.CategoryStruct.comp A.antipode A.X.comul.hom = CategoryTheory.CategoryStruct.comp A.X.comul.hom (CategoryTheory.CategoryStruct.comp (Ī²_ A.X.X.X A.X.X.X).hom (CategoryTheory.MonoidalCategory.tensorHom A.antipode A.antipode))
          source
          theorem Hopf_.mul_antipodeā‚ {C : Type uā‚} [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom A.X.comul.hom A.X.comul.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X (CategoryTheory.MonoidalCategory.tensorObj A.X.X.X A.X.X.X)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.whiskerRight (Ī²_ A.X.X.X A.X.X.X).hom A.X.X.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X.X.X (CategoryTheory.MonoidalCategory.tensorObj A.X.X.X A.X.X.X) A.X.X.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).inv A.X.X.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerRight A.X.X.mul A.X.X.X) A.X.X.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerRight A.antipode A.X.X.X) A.X.X.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X A.X.X.mul) A.X.X.mul))))))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom A.X.counit.hom A.X.counit.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (šŸ™_ C)).hom A.X.X.one)
          source
          theorem Hopf_.mul_antipodeā‚‚ {C : Type uā‚} [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom A.X.comul.hom A.X.comul.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X (CategoryTheory.MonoidalCategory.tensorObj A.X.X.X A.X.X.X)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.whiskerRight (Ī²_ A.X.X.X A.X.X.X).hom A.X.X.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X.X.X (CategoryTheory.MonoidalCategory.tensorObj A.X.X.X A.X.X.X) A.X.X.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).inv A.X.X.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerRight A.X.X.mul A.X.X.X) A.X.X.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (Ī²_ A.X.X.X A.X.X.X).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.tensorHom A.antipode A.antipode)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X A.X.X.mul) A.X.X.mul)))))))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom A.X.counit.hom A.X.counit.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (šŸ™_ C)).hom A.X.X.one)

          Auxiliary calculation for mul_antipode.

             |
   n
  /  \
 |   n
 |  / \
 |  S S
 |  \ /
 n   /
/ \ / \
|  /  |
\ / \ /
 v   v
 |   |

          We move the leftmost multiplication up, so we can reassociate. We then move the rightmost comultiplication under the strand, and simplify using antipode_right.

          source
          theorem Hopf_.mul_antipode {C : Type uā‚} [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) :
          CategoryTheory.CategoryStruct.comp A.X.X.mul A.antipode = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom A.antipode A.antipode) (CategoryTheory.CategoryStruct.comp (Ī²_ A.X.X.X A.X.X.X).hom A.X.X.mul)
          source
          theorem Hopf_.antipode_antipode {C : Type uā‚} [CategoryTheory.Category.{vā‚, uā‚} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) (comm : CategoryTheory.CategoryStruct.comp (Ī²_ A.X.X.X A.X.X.X).hom A.X.X.mul = A.X.X.mul) :
          CategoryTheory.CategoryStruct.comp A.antipode A.antipode = CategoryTheory.CategoryStruct.id A.X.X.X

          In a commutative Hopf algebra, the antipode squares to the identity.