Unbundled lax monoidal functors #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Design considerations #
The essential problem I've encountered that requires unbundled functors is
having an existing (non-monoidal) functor F : C ⥤ D between monoidal categories,
and wanting to assert that it has an extension to a lax monoidal functor.
The two options seem to be
- Construct a separate
F' : lax_monoidal_functor C D, and assertF'.to_functor ≅ F. - Introduce unbundled functors and unbundled lax monoidal functors,
and construct
lax_monoidal F.obj, then constructF' := lax_monoidal_functor.of F.obj.
Both have costs, but as for option 2. the cost is in library design, while in option 1. the cost is users having to carry around additional isomorphisms forever, I wanted to introduce unbundled functors.
TODO: later, we may want to do this for strong monoidal functors as well, but the immediate application, for enriched categories, only requires this notion.
@[class]
structure
category_theory.lax_monoidal
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(F : C → D)
[category_theory.functorial F] :
Type (max u₁ v₂)
- ε : 𝟙_ D ⟶ F (𝟙_ C)
- μ : Π (X Y : C), F X ⊗ F Y ⟶ F (X ⊗ Y)
- μ_natural' : (∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (category_theory.map F f ⊗ category_theory.map F g) ≫ category_theory.lax_monoidal.μ F Y Y' = category_theory.lax_monoidal.μ F X X' ≫ category_theory.map F (f ⊗ g)) . "obviously"
- associativity' : (∀ (X Y Z : C), (category_theory.lax_monoidal.μ F X Y ⊗ 𝟙 (F Z)) ≫ category_theory.lax_monoidal.μ F (X ⊗ Y) Z ≫ category_theory.map F (α_ X Y Z).hom = (α_ (F X) (F Y) (F Z)).hom ≫ (𝟙 (F X) ⊗ category_theory.lax_monoidal.μ F Y Z) ≫ category_theory.lax_monoidal.μ F X (Y ⊗ Z)) . "obviously"
- left_unitality' : (∀ (X : C), (λ_ (F X)).hom = (category_theory.lax_monoidal.ε F ⊗ 𝟙 (F X)) ≫ category_theory.lax_monoidal.μ F (𝟙_ C) X ≫ category_theory.map F (λ_ X).hom) . "obviously"
- right_unitality' : (∀ (X : C), (ρ_ (F X)).hom = (𝟙 (F X) ⊗ category_theory.lax_monoidal.ε F) ≫ category_theory.lax_monoidal.μ F X (𝟙_ C) ≫ category_theory.map F (ρ_ X).hom) . "obviously"
An unbundled description of lax monoidal functors.
Instances of this typeclass
Instances of other typeclasses for category_theory.lax_monoidal
- category_theory.lax_monoidal.has_sizeof_inst
@[simp]
theorem
category_theory.lax_monoidal.μ_natural
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
{F : C → D}
[category_theory.functorial F]
[self : category_theory.lax_monoidal F]
{X Y X' Y' : C}
(f : X ⟶ Y)
(g : X' ⟶ Y') :
(category_theory.map F f ⊗ category_theory.map F g) ≫ category_theory.lax_monoidal.μ F Y Y' = category_theory.lax_monoidal.μ F X X' ≫ category_theory.map F (f ⊗ g)
theorem
category_theory.lax_monoidal.left_unitality
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
{F : C → D}
[category_theory.functorial F]
[self : category_theory.lax_monoidal F]
(X : C) :
(λ_ (F X)).hom = (category_theory.lax_monoidal.ε F ⊗ 𝟙 (F X)) ≫ category_theory.lax_monoidal.μ F (𝟙_ C) X ≫ category_theory.map F (λ_ X).hom
theorem
category_theory.lax_monoidal.right_unitality
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
{F : C → D}
[category_theory.functorial F]
[self : category_theory.lax_monoidal F]
(X : C) :
(ρ_ (F X)).hom = (𝟙 (F X) ⊗ category_theory.lax_monoidal.ε F) ≫ category_theory.lax_monoidal.μ F X (𝟙_ C) ≫ category_theory.map F (ρ_ X).hom
@[simp]
theorem
category_theory.lax_monoidal.associativity
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
{F : C → D}
[category_theory.functorial F]
[self : category_theory.lax_monoidal F]
(X Y Z : C) :
(category_theory.lax_monoidal.μ F X Y ⊗ 𝟙 (F Z)) ≫ category_theory.lax_monoidal.μ F (X ⊗ Y) Z ≫ category_theory.map F (α_ X Y Z).hom = (α_ (F X) (F Y) (F Z)).hom ≫ (𝟙 (F X) ⊗ category_theory.lax_monoidal.μ F Y Z) ≫ category_theory.lax_monoidal.μ F X (Y ⊗ Z)
@[simp]
theorem
category_theory.lax_monoidal_functor.of_μ
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(F : C → D)
[I₁ : category_theory.functorial F]
[I₂ : category_theory.lax_monoidal F]
(X Y : C) :
def
category_theory.lax_monoidal_functor.of
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(F : C → D)
[I₁ : category_theory.functorial F]
[I₂ : category_theory.lax_monoidal F] :
Construct a bundled lax_monoidal_functor from the object level function
and functorial and lax_monoidal typeclasses.
Equations
- category_theory.lax_monoidal_functor.of F = {to_functor := {obj := F, map := category_theory.functorial.map I₁, map_id' := _, map_comp' := _}, ε := category_theory.lax_monoidal.ε F I₂, μ := category_theory.lax_monoidal.μ F I₂, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}
@[simp]
theorem
category_theory.lax_monoidal_functor.of_to_functor_map
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(F : C → D)
[I₁ : category_theory.functorial F]
[I₂ : category_theory.lax_monoidal F]
{X Y : C}
(ᾰ : X ⟶ Y) :
@[simp]
theorem
category_theory.lax_monoidal_functor.of_to_functor_obj
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(F : C → D)
[I₁ : category_theory.functorial F]
[I₂ : category_theory.lax_monoidal F]
(ᾰ : C) :
@[simp]
theorem
category_theory.lax_monoidal_functor.of_ε
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(F : C → D)
[I₁ : category_theory.functorial F]
[I₂ : category_theory.lax_monoidal F] :
@[protected, instance]
def
category_theory.lax_monoidal_functor.obj.lax_monoidal
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(F : category_theory.lax_monoidal_functor C D) :
Equations
- category_theory.lax_monoidal_functor.obj.lax_monoidal F = {ε := F.ε, μ := F.μ, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}
@[protected, instance]
def
category_theory.lax_monoidal_id
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C] :
Equations
- category_theory.lax_monoidal_id = {ε := 𝟙 (𝟙_ C), μ := λ (X Y : C), 𝟙 (id X ⊗ id Y), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}