Structures · Category theory
CategoryTheory.MorphismProperty.IsMonoidal
A 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.
- Shape
- One type argument · adds whiskerLeft, whiskerRight
Extends1
Extended by1
Concrete types that are instances1
- CategoryTheory.Functor
How is a type an instance?
Loading the hierarchy index…
Assumed by95
- CategoryTheory.LocalizedMonoidal
- CategoryTheory.Localization.Monoidal.toMonoidalCategory
- CategoryTheory.Localization.Monoidal.tensorBifunctor
- CategoryTheory.Localization.Monoidal.μ
- CategoryTheory.Localization.Monoidal.braidingNatIso
- CategoryTheory.Localization.Monoidal.associator_naturality
- CategoryTheory.Localization.Monoidal.ε'
- CategoryTheory.Localization.Monoidal.whiskerLeft_id
- CategoryTheory.Localization.Monoidal.id_tensorHom
- CategoryTheory.Localization.Monoidal.whiskerRight_id
- CategoryTheory.Localization.Monoidal.μ_natural_left
- CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app
- CategoryTheory.Localization.Monoidal.whiskerLeft_comp
- CategoryTheory.Localization.Monoidal.tensorHom_id
- CategoryTheory.Localization.Monoidal.μ_natural_right
- CategoryTheory.Localization.Monoidal.tensor_comp
- CategoryTheory.Localization.Monoidal.whiskerRight_comp_assoc
- CategoryTheory.Localization.Monoidal.id_tensorHom_id
- CategoryTheory.Localization.Monoidal.triangle_aux₁
- CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_right
- CategoryTheory.Localization.Monoidal.whiskerRight_comp
- CategoryTheory.Localization.Monoidal.tensorBifunctorIso
- CategoryTheory.Localization.Monoidal.associator_hom_app
- CategoryTheory.Localization.Monoidal.tensor_comp_assoc
- CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_left
- CategoryTheory.MorphismProperty.whiskerLeft_mem
- CategoryTheory.Localization.Monoidal.associator_naturality_assoc
- CategoryTheory.MorphismProperty.whiskerRight_mem
- CategoryTheory.Localization.Monoidal.pentagon_aux₂
- CategoryTheory.Localization.Monoidal.associator_naturality₃
- CategoryTheory.Localization.Monoidal.μ_inv_natural_right_assoc
- CategoryTheory.Localization.Monoidal.associator_naturality₁_assoc
- CategoryTheory.Localization.Monoidal.associator_naturality₃_assoc
- CategoryTheory.Localization.Monoidal.pentagon_aux₃
- CategoryTheory.Localization.Monoidal.rightUnitor_naturality
- CategoryTheory.Localization.Monoidal.map_hexagon_forward
- CategoryTheory.associator_inv
- CategoryTheory.Localization.Monoidal.μ_inv_natural_right
- CategoryTheory.Localization.Monoidal.associator
- CategoryTheory.Localization.Monoidal.pentagon_aux₁
- CategoryTheory.Localization.Monoidal.μ_natural_left_assoc
- CategoryTheory.MorphismProperty.IsMonoidal.whiskerRight
- CategoryTheory.MorphismProperty.IsMonoidal.whiskerLeft
- CategoryTheory.Localization.Monoidal.whisker_exchange_assoc
- CategoryTheory.Localization.Monoidal.triangle_aux₃
- CategoryTheory.Localization.Monoidal.map_hexagon_reverse
- CategoryTheory.Localization.Monoidal.rightUnitor_hom_app
- CategoryTheory.Localization.Monoidal.leftUnitor_hom_app
- CategoryTheory.Localization.Monoidal.triangle_aux₂
- CategoryTheory.Localization.Monoidal.associator_naturality₁