Theorems · Inductive type · category theory
CategoryTheory.MorphismProperty.IsMonoidal
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] →
CategoryTheory.MorphismProperty C → [CategoryTheory.MonoidalCategory C] → PropA class of morphisms W in a monoidal category is monoidal if it is multiplicative
and stable under left and right whiskering. Under this condition, the localized
category can be equipped with a monoidal category structure, see LocalizedMonoidal.
- Cited by
- 64 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
- CategoryTheory.MonoidalCategorystatement · cited by 3,095
- CategoryTheory.MorphismPropertystatement · cited by 2,179
Cited by81
Results whose statement or proof uses this declaration.
- CategoryTheory.LocalizedMonoidalstatement and proof · cited by 55
- CategoryTheory.Localization.Monoidal.toMonoidalCategorystatement and proof · cited by 28
- CategoryTheory.Localization.Monoidal.tensorBifunctorstatement and proof · cited by 19
- CategoryTheory.Localization.Monoidal.μstatement and proof · cited by 14
- CategoryTheory.Localization.Monoidal.braidingNatIsostatement and proof · cited by 9
- CategoryTheory.Localization.Monoidal.associator_naturalitystatement and proof · cited by 5
- CategoryTheory.Localization.Monoidal.whiskerLeft_idstatement and proof · cited by 5
- CategoryTheory.Localization.Monoidal.ε'statement and proof · cited by 5
- CategoryTheory.Localization.Monoidal.id_tensorHomstatement and proof · cited by 4
- CategoryTheory.Localization.Monoidal.whiskerRight_idstatement and proof · cited by 4
- CategoryTheory.Localization.Monoidal.braidingNatIso_hom_appstatement and proof · cited by 3
- CategoryTheory.Localization.Monoidal.tensorHom_idstatement and proof · cited by 3