category_theory.monoidal.functor

source

structure category_theory.lax_monoidal_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (D : Type u₂) [category_theory.category D] [category_theory.monoidal_category D] :

Type (max u₁ u₂ v₁ v₂)

to_functor : C ⥤ D
ε : 𝟙_ D ⟶ c.to_functor.obj (𝟙_ C)
μ : Π (X Y : C), c.to_functor.obj X ⊗ c.to_functor.obj Y ⟶ c.to_functor.obj (X ⊗ Y)
μ_natural' : (∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (c.to_functor.map f ⊗ c.to_functor.map g) ≫ c.μ Y Y' = c.μ X X' ≫ c.to_functor.map (f ⊗ g)) . "obviously"
associativity' : (∀ (X Y Z : C), (c.μ X Y ⊗ 𝟙 (c.to_functor.obj Z)) ≫ c.μ (X ⊗ Y) Z ≫ c.to_functor.map (α_ X Y Z).hom = (α_ (c.to_functor.obj X) (c.to_functor.obj Y) (c.to_functor.obj Z)).hom ≫ (𝟙 (c.to_functor.obj X) ⊗ c.μ Y Z) ≫ c.μ X (Y ⊗ Z)) . "obviously"
left_unitality' : (∀ (X : C), (λ_ (c.to_functor.obj X)).hom = (c.ε ⊗ 𝟙 (c.to_functor.obj X)) ≫ c.μ (𝟙_ C) X ≫ c.to_functor.map (λ_ X).hom) . "obviously"
right_unitality' : (∀ (X : C), (ρ_ (c.to_functor.obj X)).hom = (𝟙 (c.to_functor.obj X) ⊗ c.ε) ≫ c.μ X (𝟙_ C) ≫ c.to_functor.map (ρ_ X).hom) . "obviously"

A lax monoidal functor is a functor F : C ⥤ D between monoidal categories, equipped with morphisms ε : 𝟙 _D ⟶ F.obj (𝟙_ C) and μ X Y : F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y), satisfying the appropriate coherences.

source

@[simp]

theorem category_theory.lax_monoidal_functor.μ_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] (c : category_theory.lax_monoidal_functor C D) {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :

(c.to_functor.map f ⊗ c.to_functor.map g) ≫ c.μ Y Y' = c.μ X X' ≫ c.to_functor.map (f ⊗ g)

source

@[simp]

theorem category_theory.lax_monoidal_functor.μ_natural_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (c : category_theory.lax_monoidal_functor C D) {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') {X'_1 : D} (f' : c.to_functor.obj (Y ⊗ Y') ⟶ X'_1) :

(c.to_functor.map f ⊗ c.to_functor.map g) ≫ c.μ Y Y' ≫ f' = c.μ X X' ≫ c.to_functor.map (f ⊗ g) ≫ f'

source

@[simp]

theorem category_theory.lax_monoidal_functor.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] (c : category_theory.lax_monoidal_functor C D) (X : C) :

(λ_ (c.to_functor.obj X)).hom = (c.ε ⊗ 𝟙 (c.to_functor.obj X)) ≫ c.μ (𝟙_ C) X ≫ c.to_functor.map (λ_ X).hom

source

@[simp]

theorem category_theory.lax_monoidal_functor.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] (c : category_theory.lax_monoidal_functor C D) (X : C) :

(ρ_ (c.to_functor.obj X)).hom = (𝟙 (c.to_functor.obj X) ⊗ c.ε) ≫ c.μ X (𝟙_ C) ≫ c.to_functor.map (ρ_ X).hom

source

@[simp]

theorem category_theory.lax_monoidal_functor.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] (c : category_theory.lax_monoidal_functor C D) (X Y Z : C) :

(c.μ X Y ⊗ 𝟙 (c.to_functor.obj Z)) ≫ c.μ (X ⊗ Y) Z ≫ c.to_functor.map (α_ X Y Z).hom = (α_ (c.to_functor.obj X) (c.to_functor.obj Y) (c.to_functor.obj Z)).hom ≫ (𝟙 (c.to_functor.obj X) ⊗ c.μ Y Z) ≫ c.μ X (Y ⊗ Z)

source

@[simp]

theorem category_theory.lax_monoidal_functor.associativity_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (c : category_theory.lax_monoidal_functor C D) (X Y Z : C) {X' : D} (f' : c.to_functor.obj (X ⊗ (Y ⊗ Z)) ⟶ X') :

(c.μ X Y ⊗ 𝟙 (c.to_functor.obj Z)) ≫ c.μ (X ⊗ Y) Z ≫ c.to_functor.map (α_ X Y Z).hom ≫ f' = (α_ (c.to_functor.obj X) (c.to_functor.obj Y) (c.to_functor.obj Z)).hom ≫ (𝟙 (c.to_functor.obj X) ⊗ c.μ Y Z) ≫ c.μ X (Y ⊗ Z) ≫ f'

source

structure category_theory.monoidal_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (D : Type u₂) [category_theory.category D] [category_theory.monoidal_category D] :

Type (max u₁ u₂ v₁ v₂)

to_lax_monoidal_functor : category_theory.lax_monoidal_functor C D
ε_is_iso : category_theory.is_iso c.to_lax_monoidal_functor.ε . "apply_instance"
μ_is_iso : (∀ (X Y : C), category_theory.is_iso (c.to_lax_monoidal_functor.μ X Y)) . "apply_instance"

A monoidal functor is a lax monoidal functor for which the tensorator and unitor as isomorphisms.

See https://stacks.math.columbia.edu/tag/0FFL.

source

def category_theory.monoidal_functor.ε_iso {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.monoidal_functor C D) :

𝟙_ D ≅ F.to_lax_monoidal_functor.to_functor.obj (𝟙_ C)

The unit morphism of a (strong) monoidal functor as an isomorphism.

Equations

F.ε_iso = category_theory.as_iso F.to_lax_monoidal_functor.ε

source

def category_theory.monoidal_functor.μ_iso {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.monoidal_functor C D) (X Y : C) :

F.to_lax_monoidal_functor.to_functor.obj X ⊗ F.to_lax_monoidal_functor.to_functor.obj Y ≅ F.to_lax_monoidal_functor.to_functor.obj (X ⊗ Y)

The tensorator of a (strong) monoidal functor as an isomorphism.

Equations

F.μ_iso X Y = category_theory.as_iso (F.to_lax_monoidal_functor.μ X Y)

source

@[simp]

theorem category_theory.lax_monoidal_functor.id_μ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

(category_theory.lax_monoidal_functor.id C).μ X Y = 𝟙 ({obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj X ⊗ {obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj Y)

source

def category_theory.lax_monoidal_functor.id (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.lax_monoidal_functor C C

The identity lax monoidal functor.

Equations

category_theory.lax_monoidal_functor.id C = {to_functor := {obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}, ε := 𝟙 (𝟙_ C), μ := λ (X Y : C), 𝟙 ({obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj X ⊗ {obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj Y), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}

source

@[simp]

theorem category_theory.lax_monoidal_functor.id_ε (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

(category_theory.lax_monoidal_functor.id C).ε = 𝟙 (𝟙_ C)

source

@[simp]

theorem category_theory.lax_monoidal_functor.id_to_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

(category_theory.lax_monoidal_functor.id C).to_functor = 𝟭 C

source

@[instance]

def category_theory.lax_monoidal_functor.inhabited (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

inhabited (category_theory.lax_monoidal_functor C C)

Equations

category_theory.lax_monoidal_functor.inhabited C = {default := category_theory.lax_monoidal_functor.id C _inst_2}

source

theorem category_theory.monoidal_functor.map_tensor {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.monoidal_functor C D) {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :

F.to_lax_monoidal_functor.to_functor.map (f ⊗ g) = category_theory.inv (F.to_lax_monoidal_functor.μ X X') ≫ (F.to_lax_monoidal_functor.to_functor.map f ⊗ F.to_lax_monoidal_functor.to_functor.map g) ≫ F.to_lax_monoidal_functor.μ Y Y'

source

theorem category_theory.monoidal_functor.map_left_unitor {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.monoidal_functor C D) (X : C) :

F.to_lax_monoidal_functor.to_functor.map (λ_ X).hom = category_theory.inv (F.to_lax_monoidal_functor.μ (𝟙_ C) X) ≫ (category_theory.inv F.to_lax_monoidal_functor.ε ⊗ 𝟙 (F.to_lax_monoidal_functor.to_functor.obj X)) ≫ (λ_ (F.to_lax_monoidal_functor.to_functor.obj X)).hom

source

theorem category_theory.monoidal_functor.map_right_unitor {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.monoidal_functor C D) (X : C) :

F.to_lax_monoidal_functor.to_functor.map (ρ_ X).hom = category_theory.inv (F.to_lax_monoidal_functor.μ X (𝟙_ C)) ≫ (𝟙 (F.to_lax_monoidal_functor.to_functor.obj X) ⊗ category_theory.inv F.to_lax_monoidal_functor.ε) ≫ (ρ_ (F.to_lax_monoidal_functor.to_functor.obj X)).hom

source

def category_theory.monoidal_functor.μ_nat_iso {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.monoidal_functor C D) :

F.to_lax_monoidal_functor.to_functor.prod F.to_lax_monoidal_functor.to_functor ⋙ category_theory.monoidal_category.tensor D ≅ category_theory.monoidal_category.tensor C ⋙ F.to_lax_monoidal_functor.to_functor

The tensorator as a natural isomorphism.

Equations

F.μ_nat_iso = category_theory.nat_iso.of_components (λ (X : C × C), F.μ_iso X.fst X.snd) _

source

def category_theory.monoidal_functor.id (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.monoidal_functor C C

The identity monoidal functor.

Equations

category_theory.monoidal_functor.id C = {to_lax_monoidal_functor := {to_functor := {obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}, ε := 𝟙 (𝟙_ C), μ := λ (X Y : C), 𝟙 ({obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj X ⊗ {obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj Y), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := _, μ_is_iso := _}

source

@[simp]

theorem category_theory.monoidal_functor.id_to_lax_monoidal_functor_ε (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

(category_theory.monoidal_functor.id C).to_lax_monoidal_functor.ε = 𝟙 (𝟙_ C)

source

@[simp]

theorem category_theory.monoidal_functor.id_to_lax_monoidal_functor_μ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (X Y : C) :

(category_theory.monoidal_functor.id C).to_lax_monoidal_functor.μ X Y = 𝟙 ({obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj X ⊗ {obj := (𝟭 C).obj, map := (𝟭 C).map, map_id' := _, map_comp' := _}.obj Y)

source

@[simp]

theorem category_theory.monoidal_functor.id_to_lax_monoidal_functor_to_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

(category_theory.monoidal_functor.id C).to_lax_monoidal_functor.to_functor = 𝟭 C

source

@[instance]

def category_theory.monoidal_functor.inhabited (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

inhabited (category_theory.monoidal_functor C C)

Equations

category_theory.monoidal_functor.inhabited C = {default := category_theory.monoidal_functor.id C _inst_2}

source

@[simp]

theorem category_theory.lax_monoidal_functor.comp_ε {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] (F : category_theory.lax_monoidal_functor C D) (G : category_theory.lax_monoidal_functor D E) :

(F ⊗⋙ G).ε = G.ε ≫ G.to_functor.map F.ε

source

@[simp]

theorem category_theory.lax_monoidal_functor.comp_to_functor {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] (F : category_theory.lax_monoidal_functor C D) (G : category_theory.lax_monoidal_functor D E) :

(F ⊗⋙ G).to_functor = F.to_functor ⋙ G.to_functor

source

def category_theory.lax_monoidal_functor.comp {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] (F : category_theory.lax_monoidal_functor C D) (G : category_theory.lax_monoidal_functor D E) :

category_theory.lax_monoidal_functor C E

The composition of two lax monoidal functors is again lax monoidal.

Equations

F ⊗⋙ G = {to_functor := {obj := (F.to_functor ⋙ G.to_functor).obj, map := (F.to_functor ⋙ G.to_functor).map, map_id' := _, map_comp' := _}, ε := G.ε ≫ G.to_functor.map F.ε, μ := λ (X Y : C), G.μ (F.to_functor.obj X) (F.to_functor.obj Y) ≫ G.to_functor.map (F.μ X Y), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}

source

@[simp]

theorem category_theory.lax_monoidal_functor.comp_μ {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] (F : category_theory.lax_monoidal_functor C D) (G : category_theory.lax_monoidal_functor D E) (X Y : C) :

(F ⊗⋙ G).μ X Y = G.μ (F.to_functor.obj X) (F.to_functor.obj Y) ≫ G.to_functor.map (F.μ X Y)

source

@[simp]

theorem category_theory.monoidal_functor.comp_to_lax_monoidal_functor {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] (F : category_theory.monoidal_functor C D) (G : category_theory.monoidal_functor D E) :

(F ⊗⋙ G).to_lax_monoidal_functor = F.to_lax_monoidal_functor ⊗⋙ G.to_lax_monoidal_functor

source

def category_theory.monoidal_functor.comp {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {E : Type u₃} [category_theory.category E] [category_theory.monoidal_category E] (F : category_theory.monoidal_functor C D) (G : category_theory.monoidal_functor D E) :

category_theory.monoidal_functor C E

The composition of two monoidal functors is again monoidal.

Equations

F ⊗⋙ G = {to_lax_monoidal_functor := {to_functor := (F.to_lax_monoidal_functor ⊗⋙ G.to_lax_monoidal_functor).to_functor, ε := (F.to_lax_monoidal_functor ⊗⋙ G.to_lax_monoidal_functor).ε, μ := (F.to_lax_monoidal_functor ⊗⋙ G.to_lax_monoidal_functor).μ, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := _, μ_is_iso := _}

source

@[simp]

theorem category_theory.monoidal_adjoint_to_functor {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.monoidal_functor C D) {G : D ⥤ C} (h : F.to_lax_monoidal_functor.to_functor ⊣ G) :

(category_theory.monoidal_adjoint F h).to_functor = G

source

@[simp]

theorem category_theory.monoidal_adjoint_μ {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.monoidal_functor C D) {G : D ⥤ C} (h : F.to_lax_monoidal_functor.to_functor ⊣ G) (X Y : D) :

(category_theory.monoidal_adjoint F h).μ X Y = ⇑(h.hom_equiv (G.obj X ⊗ G.obj Y) (X ⊗ Y)) (category_theory.inv (F.to_lax_monoidal_functor.μ (G.obj X) (G.obj Y)) ≫ (h.counit.app X ⊗ h.counit.app Y))

source

@[simp]

theorem category_theory.monoidal_adjoint_ε {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.monoidal_functor C D) {G : D ⥤ C} (h : F.to_lax_monoidal_functor.to_functor ⊣ G) :

(category_theory.monoidal_adjoint F h).ε = ⇑(h.hom_equiv (𝟙_ C) (𝟙_ D)) (category_theory.inv F.to_lax_monoidal_functor.ε)

source

def category_theory.monoidal_adjoint {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.monoidal_functor C D) {G : D ⥤ C} (h : F.to_lax_monoidal_functor.to_functor ⊣ G) :

category_theory.lax_monoidal_functor D C

If we have a right adjoint functor G to a monoidal functor F, then G has a lax monoidal structure as well.

Equations

category_theory.monoidal_adjoint F h = {to_functor := G, ε := ⇑(h.hom_equiv (𝟙_ C) (𝟙_ D)) (category_theory.inv F.to_lax_monoidal_functor.ε), μ := λ (X Y : D), ⇑(h.hom_equiv (G.obj X ⊗ G.obj Y) (X ⊗ Y)) (category_theory.inv (F.to_lax_monoidal_functor.μ (G.obj X) (G.obj Y)) ≫ (h.counit.app X ⊗ h.counit.app Y)), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}

source

def category_theory.monoidal_inverse {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.monoidal_functor C D) [category_theory.is_equivalence F.to_lax_monoidal_functor.to_functor] :

category_theory.monoidal_functor D C

If a monoidal functor F is an equivalence of categories then its inverse is also monoidal.

Equations

category_theory.monoidal_inverse F = {to_lax_monoidal_functor := category_theory.monoidal_adjoint F F.to_lax_monoidal_functor.to_functor.as_equivalence.to_adjunction, ε_is_iso := _, μ_is_iso := _}

source

@[simp]

theorem category_theory.monoidal_inverse_to_functor {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.monoidal_functor C D) [category_theory.is_equivalence F.to_lax_monoidal_functor.to_functor] :

(category_theory.monoidal_inverse F).to_lax_monoidal_functor.to_functor = F.to_lax_monoidal_functor.to_functor.inv

mathlib documentation

(Lax) monoidal functors #

Future work #

References #