Monoidal

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

Statistics

Metric	Count
Definitions braidedCategory, closedCounit, closedUnit, ihom, instBraidedForallEval, instBraidedForallPi, instBraidedForallPi', instLaxBraidedForallPi, instLaxBraidedForallPi', instMonoidalForallEval, laxMonoidalPi, laxMonoidalPi', monoidalCategory, monoidalCategoryStruct, monoidalClosed, monoidalPi, monoidalPi', opLaxMonoidalPi, opLaxMonoidalPi', symmetricCategory	20
Theorems associator_hom_apply, associator_inv_apply, braiding_hom_apply, braiding_inv_apply, closedCounit_app, closedUnit_app, ihom_map, ihom_obj, instIsMonoidalForallPi, instIsMonoidalForallPi', isoApp_associator, isoApp_braiding, isoApp_left_unitor, isoApp_right_unitor, laxMonoidalPi'_ε, laxMonoidalPi'_μ, laxMonoidalPi_ε, laxMonoidalPi_μ, left_unitor_hom_apply, left_unitor_inv_apply, monoidalCategoryStruct_tensorHom, monoidalCategoryStruct_tensorObj, monoidalCategoryStruct_tensorUnit, monoidalCategoryStruct_whiskerLeft, monoidalCategoryStruct_whiskerRight, monoidalClosed_closed_adj_counit, monoidalClosed_closed_adj_unit, monoidalClosed_closed_rightAdj, monoidalPi'_δ, monoidalPi'_ε, monoidalPi'_η, monoidalPi'_μ, monoidalPi_δ, monoidalPi_ε, monoidalPi_η, monoidalPi_μ, opLaxMonoidalPi'_δ, opLaxMonoidalPi'_η, opLaxMonoidalPi_δ, opLaxMonoidalPi_η, right_unitor_hom_apply, right_unitor_inv_apply, δ_def, ε_def, η_def, μ_def	46
Total	66

CategoryTheory.Pi

Definitions

Name	Category	Theorems
braidedCategory 📖	CompOp	3 math math: braiding_inv_apply, isoApp_braiding, braiding_hom_apply
closedCounit 📖	CompOp	2 math math: monoidalClosed_closed_adj_counit, closedCounit_app
closedUnit 📖	CompOp	2 math math: closedUnit_app, monoidalClosed_closed_adj_unit
ihom 📖	CompOp	7 math math: monoidalClosed_closed_adj_counit, closedCounit_app, closedUnit_app, monoidalClosed_closed_rightAdj, monoidalClosed_closed_adj_unit, ihom_map, ihom_obj
instBraidedForallEval 📖	CompOp	—
instBraidedForallPi 📖	CompOp	—
instBraidedForallPi' 📖	CompOp	—
instLaxBraidedForallPi 📖	CompOp	—
instLaxBraidedForallPi' 📖	CompOp	—
instMonoidalForallEval 📖	CompOp	4 math math: η_def, δ_def, μ_def, ε_def
laxMonoidalPi 📖	CompOp	3 math math: laxMonoidalPi_ε, instIsMonoidalForallPi, laxMonoidalPi_μ
laxMonoidalPi' 📖	CompOp	2 math math: laxMonoidalPi'_ε, laxMonoidalPi'_μ
monoidalCategory 📖	CompOp	29 math math: monoidalPi'_η, monoidalPi_δ, opLaxMonoidalPi_η, braiding_inv_apply, laxMonoidalPi'_ε, monoidalClosed_closed_adj_counit, closedCounit_app, closedUnit_app, laxMonoidalPi'_μ, monoidalClosed_closed_rightAdj, η_def, opLaxMonoidalPi'_η, opLaxMonoidalPi_δ, monoidalClosed_closed_adj_unit, monoidalPi_ε, δ_def, monoidalPi'_δ, monoidalPi'_ε, laxMonoidalPi_ε, monoidalPi_μ, isoApp_braiding, monoidalPi_η, instIsMonoidalForallPi, braiding_hom_apply, μ_def, ε_def, opLaxMonoidalPi'_δ, laxMonoidalPi_μ, monoidalPi'_μ
monoidalCategoryStruct 📖	CompOp	14 math math: monoidalCategoryStruct_tensorHom, associator_hom_apply, monoidalCategoryStruct_whiskerLeft, left_unitor_inv_apply, left_unitor_hom_apply, isoApp_left_unitor, monoidalCategoryStruct_tensorUnit, monoidalCategoryStruct_tensorObj, isoApp_associator, monoidalCategoryStruct_whiskerRight, right_unitor_inv_apply, associator_inv_apply, isoApp_right_unitor, right_unitor_hom_apply
monoidalClosed 📖	CompOp	3 math math: monoidalClosed_closed_adj_counit, monoidalClosed_closed_rightAdj, monoidalClosed_closed_adj_unit
monoidalPi 📖	CompOp	4 math math: monoidalPi_δ, monoidalPi_ε, monoidalPi_μ, monoidalPi_η
monoidalPi' 📖	CompOp	4 math math: monoidalPi'_η, monoidalPi'_δ, monoidalPi'_ε, monoidalPi'_μ
opLaxMonoidalPi 📖	CompOp	2 math math: opLaxMonoidalPi_η, opLaxMonoidalPi_δ
opLaxMonoidalPi' 📖	CompOp	2 math math: opLaxMonoidalPi'_η, opLaxMonoidalPi'_δ
symmetricCategory 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_hom_apply 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.pi CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
associator_inv_apply 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.pi CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
braiding_hom_apply 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.pi CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct monoidalCategory CategoryTheory.BraidedCategory.braiding braidedCategory	—	—
braiding_inv_apply 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.pi CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct monoidalCategory CategoryTheory.BraidedCategory.braiding braidedCategory	—	—
closedCounit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.pi CategoryTheory.Functor.comp ihom CategoryTheory.MonoidalCategory.tensorLeft monoidalCategory CategoryTheory.Functor.id closedCounit CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed CategoryTheory.ihom.ev	—	—
closedUnit_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.pi CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.MonoidalCategory.tensorLeft monoidalCategory ihom closedUnit CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed CategoryTheory.ihom.coev	—	—
ihom_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.pi ihom CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed	—	—
ihom_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.pi ihom CategoryTheory.ihom CategoryTheory.MonoidalClosed.closed	—	—
instIsMonoidalForallPi 📖	mathematical	CategoryTheory.NatTrans.IsMonoidal	CategoryTheory.pi monoidalCategory CategoryTheory.Functor.pi CategoryTheory.NatTrans.pi laxMonoidalPi	—	ext CategoryTheory.NatTrans.IsMonoidal.unit CategoryTheory.NatTrans.IsMonoidal.tensor
instIsMonoidalForallPi' 📖	mathematical	CategoryTheory.NatTrans.IsMonoidal CategoryTheory.Functor.comp CategoryTheory.pi eval CategoryTheory.Functor.LaxMonoidal.comp monoidalCategory CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalForallEval	CategoryTheory.NatTrans.pi'	—	ext CategoryTheory.Category.id_comp CategoryTheory.NatTrans.IsMonoidal.unit CategoryTheory.NatTrans.IsMonoidal.tensor
isoApp_associator 📖	mathematical	—	isoApp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.pi monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
isoApp_braiding 📖	mathematical	—	isoApp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.pi CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct monoidalCategory CategoryTheory.BraidedCategory.braiding braidedCategory	—	—
isoApp_left_unitor 📖	mathematical	—	isoApp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.pi monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
isoApp_right_unitor 📖	mathematical	—	isoApp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.pi monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
laxMonoidalPi'_ε 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.pi monoidalCategory CategoryTheory.Functor.pi' laxMonoidalPi'	—	—
laxMonoidalPi'_μ 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.pi monoidalCategory CategoryTheory.Functor.pi' laxMonoidalPi'	—	—
laxMonoidalPi_ε 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.pi monoidalCategory CategoryTheory.Functor.pi laxMonoidalPi	—	—
laxMonoidalPi_μ 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.pi monoidalCategory CategoryTheory.Functor.pi laxMonoidalPi	—	—
left_unitor_hom_apply 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.pi CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
left_unitor_inv_apply 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.pi CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
monoidalCategoryStruct_tensorHom 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.pi monoidalCategoryStruct CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
monoidalCategoryStruct_tensorObj 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.pi monoidalCategoryStruct CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
monoidalCategoryStruct_tensorUnit 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.pi monoidalCategoryStruct CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
monoidalCategoryStruct_whiskerLeft 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.pi monoidalCategoryStruct CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
monoidalCategoryStruct_whiskerRight 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.pi monoidalCategoryStruct CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
monoidalClosed_closed_adj_counit 📖	mathematical	—	CategoryTheory.Adjunction.counit CategoryTheory.pi CategoryTheory.MonoidalCategory.tensorLeft monoidalCategory ihom CategoryTheory.Closed.adj CategoryTheory.MonoidalClosed.closed monoidalClosed closedCounit	—	—
monoidalClosed_closed_adj_unit 📖	mathematical	—	CategoryTheory.Adjunction.unit CategoryTheory.pi CategoryTheory.MonoidalCategory.tensorLeft monoidalCategory ihom CategoryTheory.Closed.adj CategoryTheory.MonoidalClosed.closed monoidalClosed closedUnit	—	—
monoidalClosed_closed_rightAdj 📖	mathematical	—	CategoryTheory.Closed.rightAdj CategoryTheory.pi monoidalCategory CategoryTheory.MonoidalClosed.closed monoidalClosed ihom	—	—
monoidalPi'_δ 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.pi monoidalCategory CategoryTheory.Functor.pi' CategoryTheory.Functor.Monoidal.toOplaxMonoidal monoidalPi'	—	—
monoidalPi'_ε 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.pi monoidalCategory CategoryTheory.Functor.pi' CategoryTheory.Functor.Monoidal.toLaxMonoidal monoidalPi'	—	—
monoidalPi'_η 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.pi monoidalCategory CategoryTheory.Functor.pi' CategoryTheory.Functor.Monoidal.toOplaxMonoidal monoidalPi'	—	—
monoidalPi'_μ 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.pi monoidalCategory CategoryTheory.Functor.pi' CategoryTheory.Functor.Monoidal.toLaxMonoidal monoidalPi'	—	—
monoidalPi_δ 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.pi monoidalCategory CategoryTheory.Functor.pi CategoryTheory.Functor.Monoidal.toOplaxMonoidal monoidalPi	—	—
monoidalPi_ε 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.pi monoidalCategory CategoryTheory.Functor.pi CategoryTheory.Functor.Monoidal.toLaxMonoidal monoidalPi	—	—
monoidalPi_η 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.pi monoidalCategory CategoryTheory.Functor.pi CategoryTheory.Functor.Monoidal.toOplaxMonoidal monoidalPi	—	—
monoidalPi_μ 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.pi monoidalCategory CategoryTheory.Functor.pi CategoryTheory.Functor.Monoidal.toLaxMonoidal monoidalPi	—	—
opLaxMonoidalPi'_δ 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.pi monoidalCategory CategoryTheory.Functor.pi' opLaxMonoidalPi'	—	—
opLaxMonoidalPi'_η 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.pi monoidalCategory CategoryTheory.Functor.pi' opLaxMonoidalPi'	—	—
opLaxMonoidalPi_δ 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.pi monoidalCategory CategoryTheory.Functor.pi opLaxMonoidalPi	—	—
opLaxMonoidalPi_η 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.pi monoidalCategory CategoryTheory.Functor.pi opLaxMonoidalPi	—	—
right_unitor_hom_apply 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.pi CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
right_unitor_inv_apply 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.pi CategoryTheory.MonoidalCategoryStruct.tensorObj monoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
δ_def 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.pi monoidalCategory eval CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalForallEval CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
ε_def 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.pi monoidalCategory eval CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalForallEval CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
η_def 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.pi monoidalCategory eval CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalForallEval CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
μ_def 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.pi monoidalCategory eval CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalForallEval CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—

---

← Back to Index