English
A refined naturality statement for the associator at higher arities, ensuring consistency of associativity maps under morphisms in all arguments.
Русский
Уточнённая естественность ассоциатора для более высоких arity, обеспечивающая согласованность отображений ассоциативности под morphisms во всех аргументах.
LaTeX
$$$\\text{naturality in } F,G,H \\Rightarrow (\\text{associator} F G H) \\text{ is natural in all arguments}$$$
Lean4
theorem pentagon (H K : C ⥤ V) [DayConvolution G H] [DayConvolution (F ⊛ G) H] [DayConvolution F (G ⊛ H)]
[DayConvolution H K] [DayConvolution G (H ⊛ K)] [DayConvolution (G ⊛ H) K] [DayConvolution ((F ⊛ G) ⊛ H) K]
[DayConvolution (F ⊛ G) (H ⊛ K)] [DayConvolution (F ⊛ G ⊛ H) K] [DayConvolution F (G ⊛ H ⊛ K)]
[DayConvolution F ((G ⊛ H) ⊛ K)] :
map (associator F G H).hom (𝟙 K) ≫ (associator F (G ⊛ H) K).hom ≫ map (𝟙 F) (associator G H K).hom =
(associator (F ⊛ G) H K).hom ≫ (associator F G (H ⊛ K)).hom :=
by
-- We repeatedly apply the fact that the functors are left Kan extensions
apply Functor.hom_ext_of_isLeftKanExtension (α := unit ((F ⊛ G) ⊛ H) K)
apply Functor.hom_ext_of_isLeftKanExtension (α := extensionUnitLeft ((F ⊛ G) ⊛ H) (unit (F ⊛ G) H) K)
have :
(((F ⊛ G) ⊠ H) ⊠ K).IsLeftKanExtension (α :=
extensionUnitLeft ((F ⊛ G) ⊠ H) (extensionUnitLeft _ (unit F G) H) K) :=
isPointwiseLeftKanExtensionExtensionUnitLeft _ _ _
(isPointwiseLeftKanExtensionExtensionUnitLeft _ _ _ (isPointwiseLeftKanExtensionUnit F G)) |>.isLeftKanExtension
apply
Functor.hom_ext_of_isLeftKanExtension (α := extensionUnitLeft ((F ⊛ G) ⊠ H) (extensionUnitLeft _ (unit F G) H) K)
-- And then we compute...
ext ⟨⟨⟨i, j⟩, k⟩, l⟩
have aux :
((unit F G).app (i, j) ⊗ₘ (unit H K).app (k, l)) ≫ (unit (F ⊛ G) (H ⊛ K)).app ((i ⊗ j), (k ⊗ l)) =
(α_ (F.obj i) (G.obj j) (H.obj k ⊗ K.obj l)).hom ≫
F.obj i ◁ G.obj j ◁ (unit H K).app (k, l) ≫
F.obj i ◁ (unit G (H ⊛ K)).app (j, (k ⊗ l)) ≫
(unit F (G ⊛ H ⊛ K)).app (i, (j ⊗ k ⊗ l)) ≫
(F ⊛ G ⊛ H ⊛ K).map (α_ i j (k ⊗ l)).inv ≫ (associator F G (H ⊛ K)).inv.app ((i ⊗ j) ⊗ k ⊗ l) :=
by
conv_rhs =>
simp only [Functor.comp_obj, tensor_obj, NatTrans.naturality, associator_inv_unit_unit_assoc,
externalProductBifunctor_obj_obj, Iso.map_hom_inv_id, Category.comp_id]
simp only [tensor_whiskerLeft_symm, Category.assoc, Iso.hom_inv_id_assoc, ← tensorHom_def'_assoc]
dsimp
simp only [MonoidalCategory.whiskerLeft_id, Category.comp_id, unit_app_map_app_assoc,
externalProductBifunctor_obj_obj, NatTrans.id_app, tensorHom_id, associator_hom_unit_unit_assoc, tensor_obj,
NatTrans.naturality]
conv_rhs =>
simp only [whiskerRight_tensor_symm_assoc, Iso.inv_hom_id_assoc, ← tensorHom_def_assoc]
rw [reassoc_of% aux]
simp only [Iso.inv_hom_id_app_assoc, ← comp_whiskerRight_assoc, associator_hom_unit_unit F G H]
simp only [Functor.comp_obj, tensor_obj, comp_whiskerRight, whisker_assoc, Category.assoc,
whiskerRight_comp_unit_app_assoc (F ⊛ G ⊛ H) K l (α_ i j k).inv, NatTrans.naturality_assoc, NatTrans.naturality,
associator_hom_unit_unit_assoc, externalProductBifunctor_obj_obj, unit_app_map_app_assoc, NatTrans.id_app,
id_tensorHom, Iso.inv_hom_id_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc, associator_hom_unit_unit]
simp [← Functor.map_comp, pentagon_inv, pentagon_assoc]
