Structures · Category theory
CategoryTheory.Adjunction.IsMonoidal
When adj : F ⊣ G is an adjunction, with F oplax monoidal and G lax-monoidal,
this typeclass expresses compatibilities between the adjunction and the (op)lax
monoidal structures.
- Defined in
- Mathlib.CategoryTheory.Monoidal.Functor
- Shape
- One type argument · adds leftAdjoint_ε, leftAdjoint_μ
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by26
- CategoryTheory.Adjunction.map_ε_comp_counit_app_unit
- CategoryTheory.Adjunction.unit_app_unit_comp_map_η
- CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ
- CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor
- CategoryTheory.Adjunction.ε_comp_map_ε
- CategoryTheory.Adjunction.IsMonoidal.leftAdjoint_μ
- CategoryTheory.Adjunction.mapMon
- CategoryTheory.Adjunction.IsMonoidal.leftAdjoint_ε
- CategoryTheory.Adjunction.mapAddMon
- CategoryTheory.Adjunction.mapCommMon
- CategoryTheory.Adjunction.map_η_comp_η
- CategoryTheory.Adjunction.IsMonoidal.instIsMonoidalCounit
- CategoryTheory.Adjunction.IsMonoidal.instIsMonoidalUnit
- CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor_assoc
- CategoryTheory.Adjunction.map_ε_comp_counit_app_unit_assoc
- CategoryTheory.Adjunction.ε_comp_map_ε_assoc
- CategoryTheory.Adjunction.mapAddMon_counit
- CategoryTheory.Adjunction.mapMon_counit
- CategoryTheory.Adjunction.mapMon_unit
- CategoryTheory.Adjunction.unit_app_unit_comp_map_η_assoc
- CategoryTheory.Adjunction.mapCommMon_counit
- CategoryTheory.Adjunction.map_η_comp_η_assoc
- CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ_assoc
- CategoryTheory.Adjunction.mapCommMon_unit
- CategoryTheory.Adjunction.isMonoidal_comp
- CategoryTheory.Adjunction.mapAddMon_unit
Ancestors0
No ancestors.