Monoidal

📁 Source: Mathlib/AlgebraicTopology/SimplexCategory/Augmented/Monoidal.lean

Statistics

Metric	Count
Definitions associator, inl, inl', inr, inr', instMonoidalCategory, instMonoidalCategoryStruct, leftUnitor, rightUnitor, tensorHom, tensorHomOf, tensorObj, tensorObjOf, tensorUnit	14
Theorems eqToHom_toOrderHom, id_star_whiskerRight, id_tensorHom, inl'_eval, inl_comp_inl_comp_associator, inl_comp_inl_comp_associator_assoc, inl_comp_tensorHom, inl_comp_tensorHom_assoc, inr'_eval, inr_comp_associator, inr_comp_associator_assoc, inr_comp_inl_comp_associator, inr_comp_inl_comp_associator_assoc, inr_comp_tensorHom, inr_comp_tensorHom_assoc, tensorHom_comp_tensorHom, tensorHom_id, tensorObj_hom_ext, tensorObj_hom_ext_iff, tensor_id, whiskerLeft_id_star	21
Total	35

AugmentedSimplexCategory

Definitions

Name	Category	Theorems
associator 📖	CompOp	—
inl 📖	CompOp	7 math math: inr_comp_inl_comp_associator, inr_comp_inl_comp_associator_assoc, inl_comp_inl_comp_associator_assoc, tensorObj_hom_ext_iff, inl_comp_tensorHom, inl_comp_inl_comp_associator, inl_comp_tensorHom_assoc
inl' 📖	CompOp	1 math math: inl'_eval
inr 📖	CompOp	7 math math: inr_comp_associator, inr_comp_inl_comp_associator, inr_comp_inl_comp_associator_assoc, tensorObj_hom_ext_iff, inr_comp_associator_assoc, inr_comp_tensorHom, inr_comp_tensorHom_assoc
inr' 📖	CompOp	1 math math: inr'_eval
instMonoidalCategory 📖	CompOp	—
instMonoidalCategoryStruct 📖	CompOp	17 math math: inr_comp_associator, whiskerLeft_id_star, inr_comp_inl_comp_associator, inr_comp_inl_comp_associator_assoc, inl_comp_inl_comp_associator_assoc, tensorObj_hom_ext_iff, inr_comp_associator_assoc, inl_comp_tensorHom, id_star_whiskerRight, inl_comp_inl_comp_associator, tensor_id, tensorHom_id, id_tensorHom, inr_comp_tensorHom, inl_comp_tensorHom_assoc, inr_comp_tensorHom_assoc, tensorHom_comp_tensorHom
leftUnitor 📖	CompOp	—
rightUnitor 📖	CompOp	—
tensorHom 📖	CompOp	—
tensorHomOf 📖	CompOp	—
tensorObj 📖	CompOp	—
tensorObjOf 📖	CompOp	2 math math: inl'_eval, inr'_eval
tensorUnit 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqToHom_toOrderHom 📖	mathematical	CategoryTheory.WithInitial.of SimplexCategory	SimplexCategory.Hom.toOrderHom CategoryTheory.WithInitial.down SimplexCategory.smallCategory CategoryTheory.eqToHom CategoryTheory.WithInitial CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.instCategory OrderEmbedding.toOrderHom SimplexCategory.len PartialOrder.toPreorder Fin.instPartialOrder OrderIso.toOrderEmbedding Fin.castOrderIso	—	SimplexCategory.eqToHom_toOrderHom
id_star_whiskerRight 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.WithInitial SimplexCategory CategoryTheory.WithInitial.instCategory SimplexCategory.smallCategory instMonoidalCategoryStruct CategoryTheory.WithInitial.star CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	—
id_tensorHom 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorHom AugmentedSimplexCategory CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory instMonoidalCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	—
inl'_eval 📖	mathematical	—	DFunLike.coe OrderHom SimplexCategory.len tensorObjOf PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike SimplexCategory.Hom.toOrderHom inl'	—	Monotone.comp OrderEmbedding.monotone CategoryTheory.Category.id_comp SimplexCategory.eqToHom_toOrderHom
inl_comp_inl_comp_associator 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AugmentedSimplexCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct inl CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	SimplexCategory.Hom.ext OrderHom.ext inl'_eval eqToHom_toOrderHom
inl_comp_inl_comp_associator_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AugmentedSimplexCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct inl CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_comp_inl_comp_associator
inl_comp_tensorHom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AugmentedSimplexCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct inl CategoryTheory.MonoidalCategoryStruct.tensorHom	—	SimplexCategory.Hom.ext OrderHom.ext inl'_eval SimplexCategory.eqToHom_toOrderHom CategoryTheory.WithInitial.false_of_to_star
inl_comp_tensorHom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AugmentedSimplexCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct inl CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_comp_tensorHom
inr'_eval 📖	mathematical	—	DFunLike.coe OrderHom SimplexCategory.len tensorObjOf PartialOrder.toPreorder Fin.instPartialOrder OrderHom.instFunLike SimplexCategory.Hom.toOrderHom inr'	—	Monotone.comp OrderEmbedding.monotone CategoryTheory.Category.id_comp SimplexCategory.eqToHom_toOrderHom
inr_comp_associator 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AugmentedSimplexCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct inr CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	SimplexCategory.Hom.ext OrderHom.ext eqToHom_toOrderHom inr'_eval
inr_comp_associator_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AugmentedSimplexCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct inr CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_comp_associator
inr_comp_inl_comp_associator 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AugmentedSimplexCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct inr inl CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	SimplexCategory.Hom.ext OrderHom.ext inl'_eval inr'_eval eqToHom_toOrderHom
inr_comp_inl_comp_associator_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AugmentedSimplexCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct inr inl CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_comp_inl_comp_associator
inr_comp_tensorHom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AugmentedSimplexCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct inr CategoryTheory.MonoidalCategoryStruct.tensorHom	—	SimplexCategory.Hom.ext OrderHom.ext inr'_eval SimplexCategory.eqToHom_toOrderHom CategoryTheory.WithInitial.false_of_to_star
inr_comp_tensorHom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AugmentedSimplexCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct inr CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_comp_tensorHom
tensorHom_comp_tensorHom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AugmentedSimplexCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom	—	tensorObj_hom_ext inl_comp_tensorHom_assoc inl_comp_tensorHom CategoryTheory.Category.assoc inr_comp_tensorHom_assoc inr_comp_tensorHom CategoryTheory.WithInitial.false_of_to_star
tensorHom_id 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorHom AugmentedSimplexCategory CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory instMonoidalCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—
tensorObj_hom_ext 📖	—	CategoryTheory.CategoryStruct.comp AugmentedSimplexCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct inl inr	—	—	CategoryTheory.ConcreteCategory.ext OrderHom.ext OrderHom.ext_iff SimplexCategory.Hom.ext_iff CategoryTheory.Category.id_comp CategoryTheory.Limits.IsInitial.to_self whiskerLeft_id_star CategoryTheory.Category.assoc id_star_whiskerRight
tensorObj_hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AugmentedSimplexCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory CategoryTheory.MonoidalCategoryStruct.tensorObj instMonoidalCategoryStruct inl inr	—	tensorObj_hom_ext
tensor_id 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorHom AugmentedSimplexCategory CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory instMonoidalCategoryStruct CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	tensorObj_hom_ext CategoryTheory.Category.assoc CategoryTheory.Category.comp_id tensorHom_comp_tensorHom
whiskerLeft_id_star 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.whiskerLeft AugmentedSimplexCategory CategoryTheory.WithInitial.instCategory SimplexCategory SimplexCategory.smallCategory instMonoidalCategoryStruct CategoryTheory.WithInitial.star CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj	—	—

---

← Back to Index