Endofunctors as a monoidal category. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We give the monoidal category structure on C ⥤ C,
and show that when C itself is monoidal, it embeds via a monoidal functor into C ⥤ C.
TODO #
Can we use this to show coherence results, e.g. a cheap proof that λ_ (𝟙_ C) = ρ_ (𝟙_ C)?
I suspect this is harder than is usually made out.
The category of endofunctors of any category is a monoidal category, with tensor product given by composition of functors (and horizontal composition of natural transformations).
Equations
- category_theory.endofunctor_monoidal_category C = {tensor_obj := λ (F G : C ⥤ C), F ⋙ G, tensor_hom := λ (F G F' G' : C ⥤ C) (α : F ⟶ G) (β : F' ⟶ G'), α ◫ β, tensor_id' := _, tensor_comp' := _, tensor_unit := 𝟭 C _inst_1, associator := λ (F G H : C ⥤ C), F.associator G H, associator_naturality' := _, left_unitor := λ (F : C ⥤ C), F.left_unitor, left_unitor_naturality' := _, right_unitor := λ (F : C ⥤ C), F.right_unitor, right_unitor_naturality' := _, pentagon' := _, triangle' := _}
@[simp]
def
category_theory.tensoring_right_monoidal
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
category_theory.monoidal_functor C (C ⥤ C)
Tensoring on the right gives a monoidal functor from C into endofunctors of C.
Equations
- category_theory.tensoring_right_monoidal C = {to_lax_monoidal_functor := {to_functor := {obj := (category_theory.monoidal_category.tensoring_right C).obj, map := (category_theory.monoidal_category.tensoring_right C).map, map_id' := _, map_comp' := _}, ε := (category_theory.monoidal_category.right_unitor_nat_iso C).inv, μ := λ (X Y : C), {app := λ (Z : C), (α_ Z X Y).hom, naturality' := _}, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := _, μ_is_iso := _}
@[simp]
theorem
category_theory.tensoring_right_monoidal_to_lax_monoidal_functor_μ_app
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y Z : C) :
((category_theory.tensoring_right_monoidal C).to_lax_monoidal_functor.μ X Y).app Z = (α_ Z X Y).hom
@[simp]
@[simp]
theorem
category_theory.μ_hom_inv_app
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(i j : M)
(X : C) :
(F.to_lax_monoidal_functor.μ i j).app X ≫ (F.μ_iso i j).inv.app X = 𝟙 ((F.to_lax_monoidal_functor.to_functor.obj i ⊗ F.to_lax_monoidal_functor.to_functor.obj j).obj X)
@[simp]
theorem
category_theory.μ_hom_inv_app_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(i j : M)
(X : C)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj i ⊗ F.to_lax_monoidal_functor.to_functor.obj j).obj X ⟶ X') :
@[simp]
theorem
category_theory.μ_inv_hom_app_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(i j : M)
(X : C)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj (i ⊗ j)).obj X ⟶ X') :
@[simp]
theorem
category_theory.μ_inv_hom_app
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(i j : M)
(X : C) :
(F.μ_iso i j).inv.app X ≫ (F.to_lax_monoidal_functor.μ i j).app X = 𝟙 ((F.to_lax_monoidal_functor.to_functor.obj (i ⊗ j)).obj X)
@[simp]
theorem
category_theory.ε_hom_inv_app
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(X : C) :
@[simp]
theorem
category_theory.ε_hom_inv_app_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(X : C)
{X' : C}
(f' : (𝟙_ (C ⥤ C)).obj X ⟶ X') :
@[simp]
theorem
category_theory.ε_inv_hom_app
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(X : C) :
F.ε_iso.inv.app X ≫ F.to_lax_monoidal_functor.ε.app X = 𝟙 ((F.to_lax_monoidal_functor.to_functor.obj (𝟙_ M)).obj X)
@[simp]
theorem
category_theory.ε_inv_hom_app_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(X : C)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj (𝟙_ M)).obj X ⟶ X') :
@[simp]
theorem
category_theory.ε_naturality_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{X Y : C}
(f : X ⟶ Y)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj (𝟙_ M)).obj Y ⟶ X') :
F.to_lax_monoidal_functor.ε.app X ≫ (F.to_lax_monoidal_functor.to_functor.obj (𝟙_ M)).map f ≫ f' = f ≫ F.to_lax_monoidal_functor.ε.app Y ≫ f'
@[simp]
theorem
category_theory.ε_naturality
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{X Y : C}
(f : X ⟶ Y) :
F.to_lax_monoidal_functor.ε.app X ≫ (F.to_lax_monoidal_functor.to_functor.obj (𝟙_ M)).map f = f ≫ F.to_lax_monoidal_functor.ε.app Y
@[simp]
theorem
category_theory.ε_inv_naturality
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{X Y : C}
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.ε_inv_naturality_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{X Y : C}
(f : X ⟶ Y)
{X' : C}
(f' : (𝟙_ (C ⥤ C)).obj Y ⟶ X') :
@[simp]
theorem
category_theory.μ_naturality
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{m n : M}
{X Y : C}
(f : X ⟶ Y) :
(F.to_lax_monoidal_functor.to_functor.obj n).map ((F.to_lax_monoidal_functor.to_functor.obj m).map f) ≫ (F.to_lax_monoidal_functor.μ m n).app Y = (F.to_lax_monoidal_functor.μ m n).app X ≫ (F.to_lax_monoidal_functor.to_functor.obj (m ⊗ n)).map f
@[simp]
theorem
category_theory.μ_naturality_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{m n : M}
{X Y : C}
(f : X ⟶ Y)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj (m ⊗ n)).obj Y ⟶ X') :
(F.to_lax_monoidal_functor.to_functor.obj n).map ((F.to_lax_monoidal_functor.to_functor.obj m).map f) ≫ (F.to_lax_monoidal_functor.μ m n).app Y ≫ f' = (F.to_lax_monoidal_functor.μ m n).app X ≫ (F.to_lax_monoidal_functor.to_functor.obj (m ⊗ n)).map f ≫ f'
theorem
category_theory.μ_inv_naturality
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{m n : M}
{X Y : C}
(f : X ⟶ Y) :
(F.μ_iso m n).inv.app X ≫ (F.to_lax_monoidal_functor.to_functor.obj n).map ((F.to_lax_monoidal_functor.to_functor.obj m).map f) = (F.to_lax_monoidal_functor.to_functor.obj (m ⊗ n)).map f ≫ (F.μ_iso m n).inv.app Y
theorem
category_theory.μ_inv_naturality_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{m n : M}
{X Y : C}
(f : X ⟶ Y)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj n).obj ((F.to_lax_monoidal_functor.to_functor.obj m).obj Y) ⟶ X') :
(F.μ_iso m n).inv.app X ≫ (F.to_lax_monoidal_functor.to_functor.obj n).map ((F.to_lax_monoidal_functor.to_functor.obj m).map f) ≫ f' = (F.to_lax_monoidal_functor.to_functor.obj (m ⊗ n)).map f ≫ (F.μ_iso m n).inv.app Y ≫ f'
theorem
category_theory.μ_naturality₂_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{m n m' n' : M}
(f : m ⟶ m')
(g : n ⟶ n')
(X : C)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj (m' ⊗ n')).obj X ⟶ X') :
(F.to_lax_monoidal_functor.to_functor.map g).app ((F.to_lax_monoidal_functor.to_functor.obj m).obj X) ≫ (F.to_lax_monoidal_functor.to_functor.obj n').map ((F.to_lax_monoidal_functor.to_functor.map f).app X) ≫ (F.to_lax_monoidal_functor.μ m' n').app X ≫ f' = (F.to_lax_monoidal_functor.μ m n).app X ≫ (F.to_lax_monoidal_functor.to_functor.map (f ⊗ g)).app X ≫ f'
theorem
category_theory.μ_naturality₂
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{m n m' n' : M}
(f : m ⟶ m')
(g : n ⟶ n')
(X : C) :
(F.to_lax_monoidal_functor.to_functor.map g).app ((F.to_lax_monoidal_functor.to_functor.obj m).obj X) ≫ (F.to_lax_monoidal_functor.to_functor.obj n').map ((F.to_lax_monoidal_functor.to_functor.map f).app X) ≫ (F.to_lax_monoidal_functor.μ m' n').app X = (F.to_lax_monoidal_functor.μ m n).app X ≫ (F.to_lax_monoidal_functor.to_functor.map (f ⊗ g)).app X
@[simp]
theorem
category_theory.μ_naturalityₗ
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{m n m' : M}
(f : m ⟶ m')
(X : C) :
(F.to_lax_monoidal_functor.to_functor.obj n).map ((F.to_lax_monoidal_functor.to_functor.map f).app X) ≫ (F.to_lax_monoidal_functor.μ m' n).app X = (F.to_lax_monoidal_functor.μ m n).app X ≫ (F.to_lax_monoidal_functor.to_functor.map (f ⊗ 𝟙 n)).app X
@[simp]
theorem
category_theory.μ_naturalityₗ_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{m n m' : M}
(f : m ⟶ m')
(X : C)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj (m' ⊗ n)).obj X ⟶ X') :
(F.to_lax_monoidal_functor.to_functor.obj n).map ((F.to_lax_monoidal_functor.to_functor.map f).app X) ≫ (F.to_lax_monoidal_functor.μ m' n).app X ≫ f' = (F.to_lax_monoidal_functor.μ m n).app X ≫ (F.to_lax_monoidal_functor.to_functor.map (f ⊗ 𝟙 n)).app X ≫ f'
@[simp]
theorem
category_theory.μ_naturalityᵣ
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{m n n' : M}
(g : n ⟶ n')
(X : C) :
(F.to_lax_monoidal_functor.to_functor.map g).app ((F.to_lax_monoidal_functor.to_functor.obj m).obj X) ≫ (F.to_lax_monoidal_functor.μ m n').app X = (F.to_lax_monoidal_functor.μ m n).app X ≫ (F.to_lax_monoidal_functor.to_functor.map (𝟙 m ⊗ g)).app X
@[simp]
theorem
category_theory.μ_naturalityᵣ_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{m n n' : M}
(g : n ⟶ n')
(X : C)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj (m ⊗ n')).obj X ⟶ X') :
(F.to_lax_monoidal_functor.to_functor.map g).app ((F.to_lax_monoidal_functor.to_functor.obj m).obj X) ≫ (F.to_lax_monoidal_functor.μ m n').app X ≫ f' = (F.to_lax_monoidal_functor.μ m n).app X ≫ (F.to_lax_monoidal_functor.to_functor.map (𝟙 m ⊗ g)).app X ≫ f'
@[simp]
theorem
category_theory.μ_inv_naturalityₗ
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{m n m' : M}
(f : m ⟶ m')
(X : C) :
(F.μ_iso m n).inv.app X ≫ (F.to_lax_monoidal_functor.to_functor.obj n).map ((F.to_lax_monoidal_functor.to_functor.map f).app X) = (F.to_lax_monoidal_functor.to_functor.map (f ⊗ 𝟙 n)).app X ≫ (F.μ_iso m' n).inv.app X
@[simp]
theorem
category_theory.μ_inv_naturalityₗ_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{m n m' : M}
(f : m ⟶ m')
(X : C)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj n).obj ((F.to_lax_monoidal_functor.to_functor.obj m').obj X) ⟶ X') :
(F.μ_iso m n).inv.app X ≫ (F.to_lax_monoidal_functor.to_functor.obj n).map ((F.to_lax_monoidal_functor.to_functor.map f).app X) ≫ f' = (F.to_lax_monoidal_functor.to_functor.map (f ⊗ 𝟙 n)).app X ≫ (F.μ_iso m' n).inv.app X ≫ f'
@[simp]
theorem
category_theory.μ_inv_naturalityᵣ_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{m n n' : M}
(g : n ⟶ n')
(X : C)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj n').obj ((F.to_lax_monoidal_functor.to_functor.obj m).obj X) ⟶ X') :
(F.μ_iso m n).inv.app X ≫ (F.to_lax_monoidal_functor.to_functor.map g).app ((F.to_lax_monoidal_functor.to_functor.obj m).obj X) ≫ f' = (F.to_lax_monoidal_functor.to_functor.map (𝟙 m ⊗ g)).app X ≫ (F.μ_iso m n').inv.app X ≫ f'
@[simp]
theorem
category_theory.μ_inv_naturalityᵣ
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{m n n' : M}
(g : n ⟶ n')
(X : C) :
(F.μ_iso m n).inv.app X ≫ (F.to_lax_monoidal_functor.to_functor.map g).app ((F.to_lax_monoidal_functor.to_functor.obj m).obj X) = (F.to_lax_monoidal_functor.to_functor.map (𝟙 m ⊗ g)).app X ≫ (F.μ_iso m n').inv.app X
theorem
category_theory.left_unitality_app_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(n : M)
(X : C)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj n).obj X ⟶ X') :
(F.to_lax_monoidal_functor.to_functor.obj n).map (F.to_lax_monoidal_functor.ε.app X) ≫ (F.to_lax_monoidal_functor.μ (𝟙_ M) n).app X ≫ (F.to_lax_monoidal_functor.to_functor.map (λ_ n).hom).app X ≫ f' = f'
theorem
category_theory.left_unitality_app
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(n : M)
(X : C) :
(F.to_lax_monoidal_functor.to_functor.obj n).map (F.to_lax_monoidal_functor.ε.app X) ≫ (F.to_lax_monoidal_functor.μ (𝟙_ M) n).app X ≫ (F.to_lax_monoidal_functor.to_functor.map (λ_ n).hom).app X = 𝟙 ((F.to_lax_monoidal_functor.to_functor.obj n).obj ((𝟙_ (C ⥤ C)).obj X))
theorem
category_theory.obj_ε_app_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(n : M)
(X : C)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj n).obj ((F.to_lax_monoidal_functor.to_functor.obj (𝟙_ M)).obj X) ⟶ X') :
(F.to_lax_monoidal_functor.to_functor.obj n).map (F.to_lax_monoidal_functor.ε.app X) ≫ f' = (F.to_lax_monoidal_functor.to_functor.map (λ_ n).inv).app X ≫ (F.μ_iso (𝟙_ M) n).inv.app X ≫ f'
@[simp]
theorem
category_theory.obj_ε_app
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(n : M)
(X : C) :
(F.to_lax_monoidal_functor.to_functor.obj n).map (F.to_lax_monoidal_functor.ε.app X) = (F.to_lax_monoidal_functor.to_functor.map (λ_ n).inv).app X ≫ (F.μ_iso (𝟙_ M) n).inv.app X
@[simp]
theorem
category_theory.obj_ε_inv_app
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(n : M)
(X : C) :
(F.to_lax_monoidal_functor.to_functor.obj n).map (F.ε_iso.inv.app X) = (F.to_lax_monoidal_functor.μ (𝟙_ M) n).app X ≫ (F.to_lax_monoidal_functor.to_functor.map (λ_ n).hom).app X
theorem
category_theory.obj_ε_inv_app_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(n : M)
(X : C)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj n).obj ((𝟙_ (C ⥤ C)).obj X) ⟶ X') :
(F.to_lax_monoidal_functor.to_functor.obj n).map (F.ε_iso.inv.app X) ≫ f' = (F.to_lax_monoidal_functor.μ (𝟙_ M) n).app X ≫ (F.to_lax_monoidal_functor.to_functor.map (λ_ n).hom).app X ≫ f'
theorem
category_theory.right_unitality_app
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(n : M)
(X : C) :
F.to_lax_monoidal_functor.ε.app ((F.to_lax_monoidal_functor.to_functor.obj n).obj X) ≫ (F.to_lax_monoidal_functor.μ n (𝟙_ M)).app X ≫ (F.to_lax_monoidal_functor.to_functor.map (ρ_ n).hom).app X = 𝟙 ((𝟙_ (C ⥤ C)).obj ((F.to_lax_monoidal_functor.to_functor.obj n).obj X))
theorem
category_theory.right_unitality_app_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(n : M)
(X : C)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj n).obj X ⟶ X') :
F.to_lax_monoidal_functor.ε.app ((F.to_lax_monoidal_functor.to_functor.obj n).obj X) ≫ (F.to_lax_monoidal_functor.μ n (𝟙_ M)).app X ≫ (F.to_lax_monoidal_functor.to_functor.map (ρ_ n).hom).app X ≫ f' = f'
@[simp]
theorem
category_theory.ε_app_obj
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(n : M)
(X : C) :
F.to_lax_monoidal_functor.ε.app ((F.to_lax_monoidal_functor.to_functor.obj n).obj X) = (F.to_lax_monoidal_functor.to_functor.map (ρ_ n).inv).app X ≫ (F.μ_iso n (𝟙_ M)).inv.app X
@[simp]
theorem
category_theory.ε_inv_app_obj
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(n : M)
(X : C) :
F.ε_iso.inv.app ((F.to_lax_monoidal_functor.to_functor.obj n).obj X) = (F.to_lax_monoidal_functor.μ n (𝟙_ M)).app X ≫ (F.to_lax_monoidal_functor.to_functor.map (ρ_ n).hom).app X
theorem
category_theory.associativity_app_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(m₁ m₂ m₃ : M)
(X : C)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj (m₁ ⊗ m₂ ⊗ m₃)).obj X ⟶ X') :
(F.to_lax_monoidal_functor.to_functor.obj m₃).map ((F.to_lax_monoidal_functor.μ m₁ m₂).app X) ≫ (F.to_lax_monoidal_functor.μ (m₁ ⊗ m₂) m₃).app X ≫ (F.to_lax_monoidal_functor.to_functor.map (α_ m₁ m₂ m₃).hom).app X ≫ f' = (F.to_lax_monoidal_functor.μ m₂ m₃).app ((F.to_lax_monoidal_functor.to_functor.obj m₁).obj X) ≫ (F.to_lax_monoidal_functor.μ m₁ (m₂ ⊗ m₃)).app X ≫ f'
theorem
category_theory.associativity_app
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(m₁ m₂ m₃ : M)
(X : C) :
(F.to_lax_monoidal_functor.to_functor.obj m₃).map ((F.to_lax_monoidal_functor.μ m₁ m₂).app X) ≫ (F.to_lax_monoidal_functor.μ (m₁ ⊗ m₂) m₃).app X ≫ (F.to_lax_monoidal_functor.to_functor.map (α_ m₁ m₂ m₃).hom).app X = (F.to_lax_monoidal_functor.μ m₂ m₃).app ((F.to_lax_monoidal_functor.to_functor.obj m₁).obj X) ≫ (F.to_lax_monoidal_functor.μ m₁ (m₂ ⊗ m₃)).app X
theorem
category_theory.obj_μ_app_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(m₁ m₂ m₃ : M)
(X : C)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj m₃).obj ((F.to_lax_monoidal_functor.to_functor.obj (m₁ ⊗ m₂)).obj X) ⟶ X') :
(F.to_lax_monoidal_functor.to_functor.obj m₃).map ((F.to_lax_monoidal_functor.μ m₁ m₂).app X) ≫ f' = (F.to_lax_monoidal_functor.μ m₂ m₃).app ((F.to_lax_monoidal_functor.to_functor.obj m₁).obj X) ≫ (F.to_lax_monoidal_functor.μ m₁ (m₂ ⊗ m₃)).app X ≫ (F.to_lax_monoidal_functor.to_functor.map (α_ m₁ m₂ m₃).inv).app X ≫ (F.μ_iso (m₁ ⊗ m₂) m₃).inv.app X ≫ f'
@[simp]
theorem
category_theory.obj_μ_app
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(m₁ m₂ m₃ : M)
(X : C) :
(F.to_lax_monoidal_functor.to_functor.obj m₃).map ((F.to_lax_monoidal_functor.μ m₁ m₂).app X) = (F.to_lax_monoidal_functor.μ m₂ m₃).app ((F.to_lax_monoidal_functor.to_functor.obj m₁).obj X) ≫ (F.to_lax_monoidal_functor.μ m₁ (m₂ ⊗ m₃)).app X ≫ (F.to_lax_monoidal_functor.to_functor.map (α_ m₁ m₂ m₃).inv).app X ≫ (F.μ_iso (m₁ ⊗ m₂) m₃).inv.app X
theorem
category_theory.obj_μ_inv_app_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(m₁ m₂ m₃ : M)
(X : C)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj m₃).obj ((F.to_lax_monoidal_functor.to_functor.obj m₁ ⊗ F.to_lax_monoidal_functor.to_functor.obj m₂).obj X) ⟶ X') :
(F.to_lax_monoidal_functor.to_functor.obj m₃).map ((F.μ_iso m₁ m₂).inv.app X) ≫ f' = (F.to_lax_monoidal_functor.μ (m₁ ⊗ m₂) m₃).app X ≫ (F.to_lax_monoidal_functor.to_functor.map (α_ m₁ m₂ m₃).hom).app X ≫ (F.μ_iso m₁ (m₂ ⊗ m₃)).inv.app X ≫ (F.μ_iso m₂ m₃).inv.app ((F.to_lax_monoidal_functor.to_functor.obj m₁).obj X) ≫ f'
@[simp]
theorem
category_theory.obj_μ_inv_app
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(m₁ m₂ m₃ : M)
(X : C) :
(F.to_lax_monoidal_functor.to_functor.obj m₃).map ((F.μ_iso m₁ m₂).inv.app X) = (F.to_lax_monoidal_functor.μ (m₁ ⊗ m₂) m₃).app X ≫ (F.to_lax_monoidal_functor.to_functor.map (α_ m₁ m₂ m₃).hom).app X ≫ (F.μ_iso m₁ (m₂ ⊗ m₃)).inv.app X ≫ (F.μ_iso m₂ m₃).inv.app ((F.to_lax_monoidal_functor.to_functor.obj m₁).obj X)
@[simp]
theorem
category_theory.obj_zero_map_μ_app_assoc
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{m : M}
{X Y : C}
(f : X ⟶ (F.to_lax_monoidal_functor.to_functor.obj m).obj Y)
{X' : C}
(f' : (F.to_lax_monoidal_functor.to_functor.obj (m ⊗ 𝟙_ M)).obj Y ⟶ X') :
(F.to_lax_monoidal_functor.to_functor.obj (𝟙_ M)).map f ≫ (F.to_lax_monoidal_functor.μ m (𝟙_ M)).app Y ≫ f' = F.ε_iso.inv.app X ≫ f ≫ (F.to_lax_monoidal_functor.to_functor.map (ρ_ m).inv).app Y ≫ f'
@[simp]
theorem
category_theory.obj_zero_map_μ_app
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
{m : M}
{X Y : C}
(f : X ⟶ (F.to_lax_monoidal_functor.to_functor.obj m).obj Y) :
(F.to_lax_monoidal_functor.to_functor.obj (𝟙_ M)).map f ≫ (F.to_lax_monoidal_functor.μ m (𝟙_ M)).app Y = F.ε_iso.inv.app X ≫ f ≫ (F.to_lax_monoidal_functor.to_functor.map (ρ_ m).inv).app Y
@[simp]
theorem
category_theory.obj_μ_zero_app
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(m₁ m₂ : M)
(X : C) :
(F.to_lax_monoidal_functor.to_functor.obj m₂).map ((F.to_lax_monoidal_functor.μ m₁ (𝟙_ M)).app X) = (F.to_lax_monoidal_functor.μ (𝟙_ M) m₂).app ((F.to_lax_monoidal_functor.to_functor.obj m₁).obj X) ≫ (F.to_lax_monoidal_functor.to_functor.map (λ_ m₂).hom).app ((F.to_lax_monoidal_functor.to_functor.obj m₁).obj X) ≫ (F.to_lax_monoidal_functor.to_functor.obj m₂).map ((F.to_lax_monoidal_functor.to_functor.map (ρ_ m₁).inv).app X)
@[simp]
theorem
category_theory.unit_of_tensor_iso_unit_hom_app
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(m n : M)
(h : m ⊗ n ≅ 𝟙_ M)
(X : C) :
(category_theory.unit_of_tensor_iso_unit F m n h).hom.app X = (F.to_lax_monoidal_functor.μ m n).app X ≫ (F.to_lax_monoidal_functor.to_functor.map h.hom).app X ≫ F.ε_iso.inv.app X
noncomputable
def
category_theory.unit_of_tensor_iso_unit
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(m n : M)
(h : m ⊗ n ≅ 𝟙_ M) :
If m ⊗ n ≅ 𝟙_M, then F.obj m is a left inverse of F.obj n.
Equations
- category_theory.unit_of_tensor_iso_unit F m n h = F.μ_iso m n ≪≫ F.to_lax_monoidal_functor.to_functor.map_iso h ≪≫ F.ε_iso.symm
@[simp]
theorem
category_theory.unit_of_tensor_iso_unit_inv_app
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(m n : M)
(h : m ⊗ n ≅ 𝟙_ M)
(X : C) :
(category_theory.unit_of_tensor_iso_unit F m n h).inv.app X = F.to_lax_monoidal_functor.ε.app X ≫ (F.to_lax_monoidal_functor.to_functor.map h.inv).app X ≫ (F.μ_iso m n).inv.app X
noncomputable
def
category_theory.equiv_of_tensor_iso_unit
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(m n : M)
(h₁ : m ⊗ n ≅ 𝟙_ M)
(h₂ : n ⊗ m ≅ 𝟙_ M)
(H : (h₁.hom ⊗ 𝟙 m) ≫ (λ_ m).hom = (α_ m n m).hom ≫ (𝟙 m ⊗ h₂.hom) ≫ (ρ_ m).hom) :
C ≌ C
If m ⊗ n ≅ 𝟙_M and n ⊗ m ≅ 𝟙_M (subject to some commuting constraints),
then F.obj m and F.obj n forms a self-equivalence of C.
Equations
- category_theory.equiv_of_tensor_iso_unit F m n h₁ h₂ H = {functor := F.to_lax_monoidal_functor.to_functor.obj m, inverse := F.to_lax_monoidal_functor.to_functor.obj n, unit_iso := (category_theory.unit_of_tensor_iso_unit F m n h₁).symm, counit_iso := category_theory.unit_of_tensor_iso_unit F n m h₂, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.equiv_of_tensor_iso_unit_unit_iso
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(m n : M)
(h₁ : m ⊗ n ≅ 𝟙_ M)
(h₂ : n ⊗ m ≅ 𝟙_ M)
(H : (h₁.hom ⊗ 𝟙 m) ≫ (λ_ m).hom = (α_ m n m).hom ≫ (𝟙 m ⊗ h₂.hom) ≫ (ρ_ m).hom) :
(category_theory.equiv_of_tensor_iso_unit F m n h₁ h₂ H).unit_iso = (category_theory.unit_of_tensor_iso_unit F m n h₁).symm
@[simp]
theorem
category_theory.equiv_of_tensor_iso_unit_functor
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(m n : M)
(h₁ : m ⊗ n ≅ 𝟙_ M)
(h₂ : n ⊗ m ≅ 𝟙_ M)
(H : (h₁.hom ⊗ 𝟙 m) ≫ (λ_ m).hom = (α_ m n m).hom ≫ (𝟙 m ⊗ h₂.hom) ≫ (ρ_ m).hom) :
(category_theory.equiv_of_tensor_iso_unit F m n h₁ h₂ H).functor = F.to_lax_monoidal_functor.to_functor.obj m
@[simp]
theorem
category_theory.equiv_of_tensor_iso_unit_counit_iso
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(m n : M)
(h₁ : m ⊗ n ≅ 𝟙_ M)
(h₂ : n ⊗ m ≅ 𝟙_ M)
(H : (h₁.hom ⊗ 𝟙 m) ≫ (λ_ m).hom = (α_ m n m).hom ≫ (𝟙 m ⊗ h₂.hom) ≫ (ρ_ m).hom) :
(category_theory.equiv_of_tensor_iso_unit F m n h₁ h₂ H).counit_iso = category_theory.unit_of_tensor_iso_unit F n m h₂
@[simp]
theorem
category_theory.equiv_of_tensor_iso_unit_inverse
{C : Type u}
[category_theory.category C]
{M : Type u_1}
[category_theory.category M]
[category_theory.monoidal_category M]
(F : category_theory.monoidal_functor M (C ⥤ C))
(m n : M)
(h₁ : m ⊗ n ≅ 𝟙_ M)
(h₂ : n ⊗ m ≅ 𝟙_ M)
(H : (h₁.hom ⊗ 𝟙 m) ≫ (λ_ m).hom = (α_ m n m).hom ≫ (𝟙 m ⊗ h₂.hom) ≫ (ρ_ m).hom) :
(category_theory.equiv_of_tensor_iso_unit F m n h₁ h₂ H).inverse = F.to_lax_monoidal_functor.to_functor.obj n