Center

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

Statistics

Metric	Count
Definitions Center, f, associator, braidedCategoryCenter, braiding, forget, instCategory, instMonoidalCategory, instMonoidalForget, instMonoidalOfBraided, instQuiver, isoMk, leftUnitor, ofBraided, ofBraidedObj, rightUnitor, tensorHom, tensorObj, tensorUnit, whiskerLeft, whiskerRight, HalfBraiding, β	23
Theorems comm, comm_assoc, ext, ext_iff, associator_hom_f, associator_inv_f, braiding_hom_f, braiding_inv_f, comp_f, ext, ext_iff, forget_map, forget_obj, forget_δ, forget_ε, forget_η, forget_μ, id_f, instReflectsIsomorphismsForget, isIso_of_f_isIso, isoMk_hom, isoMk_inv_f, leftUnitor_hom_f, leftUnitor_inv_f, ofBraidedObj_fst, ofBraidedObj_snd_β, ofBraided_map_f, ofBraided_obj, ofBraided_δ_f, ofBraided_ε_f, ofBraided_η_f, ofBraided_μ_f, rightUnitor_hom_f, rightUnitor_inv_f, tensorHom_f, tensorObj_fst, tensorObj_snd_β, tensorUnit_fst, tensorUnit_snd_β, tensorUnit_β, tensor_f, tensor_fst, tensor_β, whiskerLeft_comm, whiskerLeft_comm_assoc, whiskerLeft_f, whiskerRight_comm, whiskerRight_comm_assoc, whiskerRight_f, monoidal, monoidal_assoc, naturality, naturality_assoc	53
Total	76

CategoryTheory

Definitions

Name	Category	Theorems
Center 📖	CompOp	34 math math: Center.whiskerLeft_f, Center.braiding_inv_f, Center.associator_hom_f, Center.comp_f, Center.forget_η, Center.tensorUnit_β, Center.tensor_β, Center.rightUnitor_inv_f, Center.braiding_hom_f, Center.ofBraided_ε_f, Center.ofBraided_map_f, Center.leftUnitor_hom_f, Center.forget_ε, Center.tensor_fst, Center.ofBraided_δ_f, Center.instReflectsIsomorphismsForget, Center.isoMk_hom, Center.whiskerRight_f, Center.leftUnitor_inv_f, Center.associator_inv_f, Center.id_f, Center.rightUnitor_hom_f, Center.ofBraided_μ_f, Center.forget_obj, Center.isoMk_inv_f, enrichedNatTransYoneda_obj, Center.isIso_of_f_isIso, Center.forget_δ, Center.forget_map, Center.ofBraided_obj, Center.forget_μ, Center.ofBraided_η_f, enrichedNatTransYoneda_map_app, Center.tensor_f
HalfBraiding 📖	CompData	38 math math: Center.whiskerLeft_f, Center.braiding_inv_f, Center.associator_hom_f, Center.comp_f, Center.tensorUnit_β, Center.whiskerLeft_comm, Center.tensor_β, Center.rightUnitor_inv_f, Center.braiding_hom_f, Center.ofBraided_ε_f, Center.tensorUnit_snd_β, Center.leftUnitor_hom_f, Center.tensorHom_f, Center.tensor_fst, Center.ofBraided_δ_f, Center.Hom.comm, Center.tensorObj_fst, Center.ofBraidedObj_fst, Center.ofBraidedObj_snd_β, Center.Hom.comm_assoc, Center.whiskerRight_comm, Center.tensorUnit_fst, Center.whiskerRight_f, Center.leftUnitor_inv_f, Center.associator_inv_f, Center.id_f, Center.rightUnitor_hom_f, GradedNatTrans.naturality_assoc, Center.ofBraided_μ_f, Center.forget_obj, Center.isoMk_inv_f, Center.tensorObj_snd_β, Center.whiskerRight_comm_assoc, Center.ofBraided_η_f, Center.whiskerLeft_comm_assoc, GradedNatTrans.naturality, enrichedNatTransYoneda_map_app, Center.tensor_f

CategoryTheory.Center

Definitions

Name	Category	Theorems
associator 📖	CompOp	—
braidedCategoryCenter 📖	CompOp	—
braiding 📖	CompOp	2 math math: braiding_inv_f, braiding_hom_f
forget 📖	CompOp	7 math math: forget_η, forget_ε, instReflectsIsomorphismsForget, forget_obj, forget_δ, forget_map, forget_μ
instCategory 📖	CompOp	34 math math: whiskerLeft_f, braiding_inv_f, associator_hom_f, comp_f, forget_η, tensorUnit_β, tensor_β, rightUnitor_inv_f, braiding_hom_f, ofBraided_ε_f, ofBraided_map_f, leftUnitor_hom_f, forget_ε, tensor_fst, ofBraided_δ_f, instReflectsIsomorphismsForget, isoMk_hom, whiskerRight_f, leftUnitor_inv_f, associator_inv_f, id_f, rightUnitor_hom_f, ofBraided_μ_f, forget_obj, isoMk_inv_f, CategoryTheory.enrichedNatTransYoneda_obj, isIso_of_f_isIso, forget_δ, forget_map, ofBraided_obj, forget_μ, ofBraided_η_f, CategoryTheory.enrichedNatTransYoneda_map_app, tensor_f
instMonoidalCategory 📖	CompOp	22 math math: whiskerLeft_f, braiding_inv_f, associator_hom_f, forget_η, tensorUnit_β, tensor_β, rightUnitor_inv_f, braiding_hom_f, ofBraided_ε_f, leftUnitor_hom_f, forget_ε, tensor_fst, ofBraided_δ_f, whiskerRight_f, leftUnitor_inv_f, associator_inv_f, rightUnitor_hom_f, ofBraided_μ_f, forget_δ, forget_μ, ofBraided_η_f, tensor_f
instMonoidalForget 📖	CompOp	4 math math: forget_η, forget_ε, forget_δ, forget_μ
instMonoidalOfBraided 📖	CompOp	4 math math: ofBraided_ε_f, ofBraided_δ_f, ofBraided_μ_f, ofBraided_η_f
instQuiver 📖	CompOp	—
isoMk 📖	CompOp	2 math math: isoMk_hom, isoMk_inv_f
leftUnitor 📖	CompOp	—
ofBraided 📖	CompOp	8 math math: ofBraided_ε_f, ofBraided_map_f, ofBraided_δ_f, ofBraided_μ_f, CategoryTheory.enrichedNatTransYoneda_obj, ofBraided_obj, ofBraided_η_f, CategoryTheory.enrichedNatTransYoneda_map_app
ofBraidedObj 📖	CompOp	4 math math: ofBraided_map_f, ofBraidedObj_fst, ofBraidedObj_snd_β, ofBraided_obj
rightUnitor 📖	CompOp	—
tensorHom 📖	CompOp	1 math math: tensorHom_f
tensorObj 📖	CompOp	7 math math: whiskerLeft_comm, tensorHom_f, tensorObj_fst, whiskerRight_comm, tensorObj_snd_β, whiskerRight_comm_assoc, whiskerLeft_comm_assoc
tensorUnit 📖	CompOp	2 math math: tensorUnit_snd_β, tensorUnit_fst
whiskerLeft 📖	CompOp	—
whiskerRight 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_hom_f 📖	mathematical	—	Hom.f CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Center instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.HalfBraiding	—	—
associator_inv_f 📖	mathematical	—	Hom.f CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Center instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.HalfBraiding	—	CategoryTheory.Iso.inv_ext' associator_hom_f comp_f CategoryTheory.Iso.hom_inv_id
braiding_hom_f 📖	mathematical	—	Hom.f CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Center instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.Iso.hom braiding CategoryTheory.HalfBraiding CategoryTheory.HalfBraiding.β	—	—
braiding_inv_f 📖	mathematical	—	Hom.f CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Center instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.Iso.inv braiding CategoryTheory.HalfBraiding CategoryTheory.HalfBraiding.β	—	CategoryTheory.IsIso.Iso.inv_hom
comp_f 📖	mathematical	—	Hom.f CategoryTheory.CategoryStruct.comp CategoryTheory.Center CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.HalfBraiding	—	—
ext 📖	—	Hom.f	—	—	—
ext_iff 📖	mathematical	—	Hom.f	—	ext
forget_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Center instCategory forget Hom.f	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Center instCategory forget CategoryTheory.HalfBraiding	—	—
forget_δ 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Center instCategory instMonoidalCategory forget CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
forget_ε 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Center instCategory instMonoidalCategory forget CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
forget_η 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Center instCategory instMonoidalCategory forget CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
forget_μ 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Center instCategory instMonoidalCategory forget CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj	—	—
id_f 📖	mathematical	—	Hom.f CategoryTheory.CategoryStruct.id CategoryTheory.Center CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.HalfBraiding	—	—
instReflectsIsomorphismsForget 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms CategoryTheory.Center instCategory forget	—	CategoryTheory.Iso.isIso_hom
isIso_of_f_isIso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Center instCategory	—	CategoryTheory.Iso.isIso_hom
isoMk_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Center instCategory isoMk	—	—
isoMk_inv_f 📖	mathematical	—	Hom.f CategoryTheory.Iso.inv CategoryTheory.Center instCategory isoMk CategoryTheory.inv CategoryTheory.HalfBraiding	—	—
leftUnitor_hom_f 📖	mathematical	—	Hom.f CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Center instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.HalfBraiding	—	—
leftUnitor_inv_f 📖	mathematical	—	Hom.f CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Center instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.HalfBraiding	—	CategoryTheory.Iso.inv_ext' leftUnitor_hom_f comp_f CategoryTheory.Iso.hom_inv_id
ofBraidedObj_fst 📖	mathematical	—	CategoryTheory.HalfBraiding ofBraidedObj	—	—
ofBraidedObj_snd_β 📖	mathematical	—	CategoryTheory.HalfBraiding.β CategoryTheory.HalfBraiding ofBraidedObj CategoryTheory.BraidedCategory.braiding	—	—
ofBraided_map_f 📖	mathematical	—	Hom.f ofBraidedObj CategoryTheory.Functor.map CategoryTheory.Center instCategory ofBraided	—	—
ofBraided_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Center instCategory ofBraided ofBraidedObj	—	—
ofBraided_δ_f 📖	mathematical	—	Hom.f CategoryTheory.Functor.obj CategoryTheory.Center instCategory ofBraided CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalOfBraided CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.HalfBraiding	—	—
ofBraided_ε_f 📖	mathematical	—	Hom.f CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Center instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.Functor.obj ofBraided CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalOfBraided CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.HalfBraiding	—	—
ofBraided_η_f 📖	mathematical	—	Hom.f CategoryTheory.Functor.obj CategoryTheory.Center instCategory ofBraided CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalOfBraided CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.HalfBraiding	—	—
ofBraided_μ_f 📖	mathematical	—	Hom.f CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Center instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.Functor.obj ofBraided CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalOfBraided CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.HalfBraiding	—	—
rightUnitor_hom_f 📖	mathematical	—	Hom.f CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Center instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.HalfBraiding	—	—
rightUnitor_inv_f 📖	mathematical	—	Hom.f CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Center instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.HalfBraiding	—	CategoryTheory.Iso.inv_ext' rightUnitor_hom_f comp_f CategoryTheory.Iso.hom_inv_id
tensorHom_f 📖	mathematical	—	Hom.f tensorObj tensorHom CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.HalfBraiding	—	—
tensorObj_fst 📖	mathematical	—	CategoryTheory.HalfBraiding tensorObj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensorObj_snd_β 📖	mathematical	—	CategoryTheory.HalfBraiding.β CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.HalfBraiding tensorObj CategoryTheory.Iso.trans CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategory.whiskerLeftIso CategoryTheory.Iso.symm CategoryTheory.MonoidalCategory.whiskerRightIso	—	—
tensorUnit_fst 📖	mathematical	—	CategoryTheory.HalfBraiding tensorUnit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensorUnit_snd_β 📖	mathematical	—	CategoryTheory.HalfBraiding.β CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.HalfBraiding tensorUnit CategoryTheory.Iso.trans CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Iso.symm CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	—
tensorUnit_β 📖	mathematical	—	CategoryTheory.HalfBraiding.β CategoryTheory.HalfBraiding CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Center instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.Iso.trans CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.Iso.symm CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	—
tensor_f 📖	mathematical	—	Hom.f CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Center instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.HalfBraiding	—	—
tensor_fst 📖	mathematical	—	CategoryTheory.HalfBraiding CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Center instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory	—	—
tensor_β 📖	mathematical	—	CategoryTheory.HalfBraiding.β CategoryTheory.HalfBraiding CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Center instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.Iso.trans CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategory.whiskerLeftIso CategoryTheory.Iso.symm CategoryTheory.MonoidalCategory.whiskerRightIso	—	—
whiskerLeft_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.HalfBraiding tensorObj CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategoryStruct.whiskerLeft Hom.f CategoryTheory.Iso.hom CategoryTheory.HalfBraiding.β	—	Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_whiskerRight Mathlib.Tactic.Monoidal.eval_whiskerLeft Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_whisker Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of_of Mathlib.Tactic.Monoidal.evalWhiskerRight_nil Mathlib.Tactic.Monoidal.evalWhiskerRightAux_of Mathlib.Tactic.Monoidal.evalComp_cons Mathlib.Tactic.Monoidal.evalComp_nil_nil Mathlib.Tactic.Monoidal.evalComp_nil_cons Mathlib.Tactic.Monoidal.eval_monoidalComp Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_whiskerRight Mathlib.Tactic.Monoidal.naturality_whiskerLeft Mathlib.Tactic.Monoidal.naturality_id Mathlib.Tactic.Monoidal.naturality_associator Mathlib.Tactic.Monoidal.naturality_inv Hom.comm Mathlib.Tactic.Monoidal.evalWhiskerLeft_comp CategoryTheory.MonoidalCategory.whisker_exchange
whiskerLeft_comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.HalfBraiding CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategoryStruct.whiskerLeft Hom.f tensorObj CategoryTheory.Iso.hom CategoryTheory.HalfBraiding.β	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_comm
whiskerLeft_f 📖	mathematical	—	Hom.f CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Center instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.HalfBraiding	—	—
whiskerRight_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.HalfBraiding tensorObj CategoryTheory.MonoidalCategoryStruct.whiskerRight Hom.f CategoryTheory.Iso.hom CategoryTheory.HalfBraiding.β CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_whiskerRight Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of_of Mathlib.Tactic.Monoidal.evalWhiskerRight_nil Mathlib.Tactic.Monoidal.evalWhiskerRightAux_of 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.Monoidal.eval_monoidalComp Mathlib.Tactic.Monoidal.evalWhiskerRight_comp Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_whiskerRight Mathlib.Tactic.Monoidal.naturality_id Mathlib.Tactic.Monoidal.naturality_associator Mathlib.Tactic.Monoidal.naturality_inv Mathlib.Tactic.Monoidal.naturality_whiskerLeft CategoryTheory.MonoidalCategory.whisker_exchange Hom.comm Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_whisker
whiskerRight_comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.HalfBraiding CategoryTheory.MonoidalCategoryStruct.whiskerRight Hom.f tensorObj CategoryTheory.Iso.hom CategoryTheory.HalfBraiding.β CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerRight_comm
whiskerRight_f 📖	mathematical	—	Hom.f CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Center instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.HalfBraiding	—	—

CategoryTheory.Center.Hom

Definitions

Name	Category	Theorems
f 📖	CompOp	29 math math: CategoryTheory.Center.whiskerLeft_f, CategoryTheory.Center.braiding_inv_f, CategoryTheory.Center.associator_hom_f, ext_iff, CategoryTheory.Center.comp_f, CategoryTheory.Center.whiskerLeft_comm, CategoryTheory.Center.rightUnitor_inv_f, CategoryTheory.Center.braiding_hom_f, CategoryTheory.Center.ofBraided_ε_f, CategoryTheory.Center.ofBraided_map_f, CategoryTheory.Center.leftUnitor_hom_f, CategoryTheory.Center.tensorHom_f, CategoryTheory.Center.ofBraided_δ_f, comm, comm_assoc, CategoryTheory.Center.whiskerRight_comm, CategoryTheory.Center.whiskerRight_f, CategoryTheory.Center.leftUnitor_inv_f, CategoryTheory.Center.associator_inv_f, CategoryTheory.Center.id_f, CategoryTheory.Center.rightUnitor_hom_f, CategoryTheory.Center.ext_iff, CategoryTheory.Center.ofBraided_μ_f, CategoryTheory.Center.isoMk_inv_f, CategoryTheory.Center.whiskerRight_comm_assoc, CategoryTheory.Center.forget_map, CategoryTheory.Center.ofBraided_η_f, CategoryTheory.Center.whiskerLeft_comm_assoc, CategoryTheory.Center.tensor_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.HalfBraiding CategoryTheory.MonoidalCategoryStruct.whiskerRight f CategoryTheory.Iso.hom CategoryTheory.HalfBraiding.β CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	—
comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.HalfBraiding CategoryTheory.MonoidalCategoryStruct.whiskerRight f CategoryTheory.Iso.hom CategoryTheory.HalfBraiding.β CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm
ext 📖	—	f	—	—	—
ext_iff 📖	mathematical	—	f	—	ext

CategoryTheory.HalfBraiding

Definitions

Name	Category	Theorems
β 📖	CompOp	19 math math: CategoryTheory.Center.braiding_inv_f, naturality_assoc, CategoryTheory.Center.tensorUnit_β, naturality, CategoryTheory.Center.whiskerLeft_comm, CategoryTheory.Center.tensor_β, CategoryTheory.Center.braiding_hom_f, CategoryTheory.Center.tensorUnit_snd_β, CategoryTheory.Center.Hom.comm, CategoryTheory.Center.ofBraidedObj_snd_β, CategoryTheory.Center.Hom.comm_assoc, monoidal_assoc, CategoryTheory.Center.whiskerRight_comm, CategoryTheory.GradedNatTrans.naturality_assoc, CategoryTheory.Center.tensorObj_snd_β, CategoryTheory.Center.whiskerRight_comm_assoc, monoidal, CategoryTheory.Center.whiskerLeft_comm_assoc, CategoryTheory.GradedNatTrans.naturality

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
monoidal 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct β CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	—
monoidal_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom β CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' monoidal
naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.hom β CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—
naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.hom β CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' naturality

---

← Back to Index