Hopf_

📁 Source: Mathlib/CategoryTheory/Monoidal/Hopf_.lean

Statistics

Metric	Count
Definitions Hopf, X, hopf, instCategory, toBimon, HopfObj, antipode, term𝒮, toBimonObj, «term𝒮[_]»	10
Theorems antipode_antipode, antipode_comul, antipode_comul₁, antipode_comul₂, antipode_counit, antipode_counit_assoc, antipode_left, antipode_left_assoc, antipode_right, antipode_right_assoc, hom_antipode, mul_antipode, mul_antipode₁, mul_antipode₂, one_antipode, one_antipode_assoc	16
Total	26

CategoryTheory

Definitions

Name	Category	Theorems
Hopf 📖	CompData	—
HopfObj 📖	CompData	—

CategoryTheory.Hopf

Definitions

Name	Category	Theorems
X 📖	CompOp	—
hopf 📖	CompOp	—
instCategory 📖	CompOp	—
toBimon 📖	CompOp	—

CategoryTheory.HopfObj

Definitions

Name	Category	Theorems
antipode 📖	CompOp	16 math math: mul_antipode, one_antipode, antipode_left, antipode_comul, antipode_comul₂, antipode_left_assoc, mul_antipode₁, antipode_right_assoc, antipode_comul₁, antipode_antipode, mul_antipode₂, antipode_counit, antipode_right, antipode_counit_assoc, one_antipode_assoc, hom_antipode
term𝒮 📖	CompOp	—
toBimonObj 📖	CompOp	14 math math: mul_antipode, one_antipode, antipode_left, antipode_comul, antipode_comul₂, antipode_left_assoc, mul_antipode₁, antipode_right_assoc, antipode_comul₁, mul_antipode₂, antipode_counit, antipode_right, antipode_counit_assoc, one_antipode_assoc
«term𝒮[_]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antipode_antipode 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding CategoryTheory.MonObj.mul CategoryTheory.BimonObj.toMonObj toBimonObj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct antipode CategoryTheory.CategoryStruct.id	—	left_inv_eq_right_inv CategoryTheory.Conv.mul_eq CategoryTheory.Conv.one_eq CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.tensorHom_def_assoc mul_antipode antipode_left_assoc one_antipode CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.id_comp antipode_left
antipode_comul 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct antipode CategoryTheory.ComonObj.comul CategoryTheory.BimonObj.toComonObj toBimonObj CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding CategoryTheory.MonoidalCategoryStruct.tensorHom	—	left_inv_eq_right_inv CategoryTheory.Conv.mul_eq CategoryTheory.Conv.one_eq CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.MonoidalCategory.tensor_whiskerLeft CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc antipode_comul₁ CategoryTheory.MonoidalCategory.whiskerLeft_comp antipode_comul₂
antipode_comul₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.ComonObj.comul CategoryTheory.BimonObj.toComonObj toBimonObj CategoryTheory.MonoidalCategoryStruct.whiskerRight antipode CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.inv CategoryTheory.BraidedCategory.braiding CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.BimonObj.toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.ComonObj.counit CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonObj.one	—	CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.associator_naturality_right CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.Bimon.compatibility antipode_left CategoryTheory.BimonObj.one_comul
antipode_comul₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.ComonObj.comul CategoryTheory.BimonObj.toComonObj toBimonObj CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.BraidedCategory.braiding CategoryTheory.MonoidalCategoryStruct.tensorHom antipode CategoryTheory.Iso.inv CategoryTheory.MonObj.mul CategoryTheory.BimonObj.toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.ComonObj.counit CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonObj.one	—	CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.tensorHom_def' CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.MonoidalCategory.associator_inv_naturality_middle CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.BraidedCategory.braiding_naturality_right CategoryTheory.MonoidalCategory.associator_naturality_left CategoryTheory.BraidedCategory.braiding_naturality_left CategoryTheory.MonoidalCategory.associator_inv_naturality_right CategoryTheory.MonoidalCategory.whisker_exchange CategoryTheory.BraidedCategory.hexagon_reverse_assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.ComonObj.comul_assoc_flip_assoc CategoryTheory.ComonObj.comul_assoc CategoryTheory.MonoidalCategory.associator_naturality_middle_assoc CategoryTheory.Iso.hom_inv_id_assoc antipode_right CategoryTheory.ComonObj.counit_comul CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc CategoryTheory.braiding_tensorUnit_left CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor_inv CategoryTheory.MonoidalCategory.whiskerRight_id CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom_assoc antipode_right_assoc CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality_assoc CategoryTheory.MonoidalCategory.tensorHom_def Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.eval_whiskerRight Mathlib.Tactic.Monoidal.evalWhiskerRight_id Mathlib.Tactic.Monoidal.evalComp_cons Mathlib.Tactic.Monoidal.evalComp_nil_nil Mathlib.Tactic.Monoidal.evalComp_nil_cons Mathlib.Tactic.Monoidal.eval_whiskerLeft Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_id Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_inv Mathlib.Tactic.Monoidal.naturality_rightUnitor Mathlib.Tactic.Monoidal.naturality_leftUnitor Mathlib.Tactic.Monoidal.naturality_whiskerLeft
antipode_counit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct antipode CategoryTheory.ComonObj.counit CategoryTheory.BimonObj.toComonObj toBimonObj	—	CategoryTheory.MonoidalCategory.whiskerRight_id CategoryTheory.MonoidalCategory.unitors_equal CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.ComonObj.comul_counit_assoc CategoryTheory.BimonObj.one_counit CategoryTheory.MonoidalCategory.whisker_exchange_assoc CategoryTheory.MonoidalCategory.tensorHom_def' CategoryTheory.Bimon.mul_counit antipode_left_assoc
antipode_counit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct antipode CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.ComonObj.counit CategoryTheory.BimonObj.toComonObj toBimonObj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' antipode_counit
antipode_left 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.ComonObj.comul CategoryTheory.BimonObj.toComonObj toBimonObj CategoryTheory.MonoidalCategoryStruct.whiskerRight antipode CategoryTheory.MonObj.mul CategoryTheory.BimonObj.toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.ComonObj.counit CategoryTheory.MonObj.one	—	—
antipode_left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.ComonObj.comul CategoryTheory.BimonObj.toComonObj toBimonObj CategoryTheory.MonoidalCategoryStruct.whiskerRight antipode CategoryTheory.MonObj.mul CategoryTheory.BimonObj.toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.ComonObj.counit CategoryTheory.MonObj.one	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' antipode_left
antipode_right 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.ComonObj.comul CategoryTheory.BimonObj.toComonObj toBimonObj CategoryTheory.MonoidalCategoryStruct.whiskerLeft antipode CategoryTheory.MonObj.mul CategoryTheory.BimonObj.toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.ComonObj.counit CategoryTheory.MonObj.one	—	—
antipode_right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.ComonObj.comul CategoryTheory.BimonObj.toComonObj toBimonObj CategoryTheory.MonoidalCategoryStruct.whiskerLeft antipode CategoryTheory.MonObj.mul CategoryTheory.BimonObj.toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.ComonObj.counit CategoryTheory.MonObj.one	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' antipode_right
hom_antipode 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct antipode	—	left_inv_eq_right_inv CategoryTheory.Conv.mul_eq CategoryTheory.Conv.one_eq CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.whisker_exchange CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.IsComonHom.hom_comul CategoryTheory.IsBimonHom.toIsComonHom antipode_left CategoryTheory.IsComonHom.hom_counit CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.IsMonHom.mul_hom CategoryTheory.IsBimonHom.toIsMonHom antipode_right CategoryTheory.IsMonHom.one_hom
mul_antipode 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.mul CategoryTheory.BimonObj.toMonObj toBimonObj antipode CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding	—	left_inv_eq_right_inv CategoryTheory.Conv.mul_eq CategoryTheory.Conv.one_eq CategoryTheory.Comon.tensorObj_comul CategoryTheory.MonoidalCategory.whiskerRight_tensor CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.pentagon_hom_inv_inv_inv_inv_assoc mul_antipode₁ CategoryTheory.BraidedCategory.braiding_naturality_assoc CategoryTheory.MonoidalCategory.whiskerLeft_comp mul_antipode₂
mul_antipode₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul CategoryTheory.BimonObj.toComonObj toBimonObj CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.BraidedCategory.braiding CategoryTheory.MonObj.mul CategoryTheory.BimonObj.toMonObj antipode CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.ComonObj.counit CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonObj.one	—	CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.associator_naturality_left CategoryTheory.MonoidalCategory.whisker_exchange CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_hom_inv_assoc CategoryTheory.Bimon.compatibility_assoc antipode_left CategoryTheory.BimonObj.mul_counit_assoc
mul_antipode₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul CategoryTheory.BimonObj.toComonObj toBimonObj CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.BraidedCategory.braiding CategoryTheory.MonObj.mul CategoryTheory.BimonObj.toMonObj antipode CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.ComonObj.counit CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonObj.one	—	CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.associator_naturality_left CategoryTheory.MonoidalCategory.whisker_exchange CategoryTheory.MonObj.mul_assoc_flip CategoryTheory.MonoidalCategory.associator_inv_naturality_left CategoryTheory.MonObj.mul_assoc CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.MonoidalCategory.tensor_whiskerLeft CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_hom_inv_assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.id_comp CategoryTheory.BraidedCategory.hexagon_forward CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_inv_inv CategoryTheory.MonoidalCategory.whisker_assoc CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom_assoc CategoryTheory.BraidedCategory.braiding_naturality_right CategoryTheory.MonoidalCategory.tensorHom_def' CategoryTheory.MonoidalCategory.associator_naturality_right CategoryTheory.MonoidalCategory.associator_inv_naturality_middle_assoc CategoryTheory.Iso.hom_inv_id_assoc antipode_right CategoryTheory.MonObj.one_mul CategoryTheory.BraidedCategory.braiding_naturality_left CategoryTheory.MonoidalCategory.associator_naturality_middle_assoc CategoryTheory.braiding_tensorUnit_right CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor CategoryTheory.MonoidalCategory.rightUnitor_naturality CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_tensorHom Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.evalHorizontalComp_cons_cons Mathlib.Tactic.Monoidal.evalHorizontalCompAux_of Mathlib.Tactic.Monoidal.evalHorizontalComp_nil_nil Mathlib.Tactic.Monoidal.evalComp_cons Mathlib.Tactic.Monoidal.evalComp_nil_nil Mathlib.Tactic.Monoidal.evalComp_nil_cons Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_tensorHom Mathlib.Tactic.Monoidal.naturality_id Mathlib.Tactic.Monoidal.naturality_rightUnitor Mathlib.Tactic.Monoidal.naturality_leftUnitor
one_antipode 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.one CategoryTheory.BimonObj.toMonObj toBimonObj antipode	—	CategoryTheory.MonoidalCategory.whiskerRight_id CategoryTheory.MonObj.mul_one CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.BimonObj.one_counit_assoc CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality_assoc CategoryTheory.MonoidalCategory.whisker_exchange_assoc CategoryTheory.MonoidalCategory.unitors_inv_equal CategoryTheory.MonoidalCategory.tensorHom_def_assoc CategoryTheory.Bimon.one_comul_assoc antipode_left
one_antipode_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.one CategoryTheory.BimonObj.toMonObj toBimonObj antipode	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' one_antipode

---

← Back to Index