Structures · Category theory
CategoryTheory.Functor.OplaxMonoidal
A functor F : C ⥤ D between monoidal categories is oplax monoidal if it is
equipped with morphisms η : F.obj (𝟙_ C) ⟶ 𝟙 _D and δ X Y : F.obj (X ⊗ Y) ⟶ F.obj X ⊗ F.obj Y,
satisfying the appropriate coherences.
- Defined in
- Mathlib.CategoryTheory.Monoidal.Functor
- Shape
- One type argument · adds η, δ, δ_natural_left, δ_natural_right, oplax_associativity, oplax_left_unitality, oplax_right_unitality
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances4
- CategoryTheory.Functor
- Action
- CategoryTheory.Skeleton
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by109
- CategoryTheory.Functor.OplaxMonoidal.δ
- CategoryTheory.Functor.OplaxMonoidal.η
- CategoryTheory.Functor.OplaxMonoidal.δ_snd
- CategoryTheory.Functor.OplaxMonoidal.δ_fst
- CategoryTheory.Adjunction.map_ε_comp_counit_app_unit
- CategoryTheory.Functor.OplaxMonoidal.left_unitality
- CategoryTheory.Functor.mapComon
- CategoryTheory.Adjunction.unit_app_unit_comp_map_η
- CategoryTheory.Functor.OplaxMonoidal.right_unitality
- CategoryTheory.Functor.OplaxMonoidal.δ_natural_right
- CategoryTheory.Functor.OplaxMonoidal.δ_natural_left_assoc
- CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ
- CategoryTheory.Functor.OplaxMonoidal.associativity
- CategoryTheory.Functor.FullyFaithful.monObj
- CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor
- CategoryTheory.Functor.FullyFaithful.addMonObj
- CategoryTheory.Functor.OplaxMonoidal.lift_δ
- CategoryTheory.Functor.OplaxMonoidal.δ_natural_right_assoc
- CategoryTheory.Functor.CoreMonoidal.ofOplaxMonoidal
- CategoryTheory.Functor.OplaxMonoidal.δ_natural_left
- CategoryTheory.Functor.OplaxMonoidal.associativity_inv_assoc
- CategoryTheory.Adjunction.rightAdjointLaxMonoidal
- CategoryTheory.Functor.OplaxMonoidal.associativity_assoc
- CategoryTheory.Functor.obj.ε_def
- CategoryTheory.Functor.OplaxMonoidal.δ_comp_whiskerLeft_δ
- CategoryTheory.η_naturality
- CategoryTheory.Functor.OplaxMonoidal.δ_natural
- CategoryTheory.Functor.OplaxMonoidal.left_unitality_hom
- CategoryTheory.Functor.OplaxMonoidal.oplax_associativity
- CategoryTheory.δ_naturalityₗ
- CategoryTheory.Functor.OplaxMonoidal.δ_of_cartesianMonoidalCategory
- CategoryTheory.δ_naturality
- CategoryTheory.δ_naturalityᵣ
- CategoryTheory.Functor.OplaxMonoidal.left_unitality_hom_assoc
- CategoryTheory.Functor.OplaxMonoidal.δ_comp_tensorHom_η
- CategoryTheory.Functor.OplaxMonoidal.right_unitality_hom
- CategoryTheory.Functor.OplaxMonoidal.δ_comp_δ_whiskerRight
- CategoryTheory.Functor.obj.Δ_def
- CategoryTheory.Functor.OplaxMonoidal.δ_comp_η_tensorHom
- CategoryTheory.Functor.OplaxMonoidal.right_unitality_hom_assoc
- CategoryTheory.Functor.OplaxMonoidal.associativity_inv
- CategoryTheory.Functor.OplaxMonoidal.oplax_right_unitality
- CategoryTheory.Functor.OplaxMonoidal.oplax_left_unitality
- CategoryTheory.η_naturality_assoc
- CategoryTheory.Functor.OplaxMonoidal.left_unitality_assoc
- CategoryTheory.Functor.mapComon_obj_X
- CategoryTheory.Functor.OplaxMonoidal.δ_comp_η_tensorHom_assoc
- CategoryTheory.Functor.obj.Δ_def_assoc
- CategoryTheory.Functor.prod_δ_fst
- CategoryTheory.Functor.prod'_η_fst
Ancestors0
No ancestors.