English
A comprehensive pentagon coherence identity for Day convolution across several layers of convolution, ensuring associativity coherence across multiple compositions.
Русский
Полная пентагональная когерентность Day-конволюции на нескольких уровнях конволюций, обеспечивающая когерентность ассоциативности.
LaTeX
$$$\\text{Pentagon} = \\text{Pentagon}$$$
Lean4
theorem associator_naturality {F' G' H' : C ⥤ V} [DayConvolution F' G'] [DayConvolution G' H']
[DayConvolution F' (G' ⊛ H')] [DayConvolution (F' ⊛ G') H'] (f : F ⟶ F') (g : G ⟶ G') (h : H ⟶ H') :
map (map f g) h ≫ (associator F' G' H').hom = (associator F G H).hom ≫ map f (map g h) :=
by
apply (corepresentableBy₂' F G H) |>.homEquiv.injective
dsimp
ext
simp only [externalProductBifunctor_obj_obj, Functor.comp_obj, Functor.prod_obj, tensor_obj, Functor.id_obj,
Functor.homEquivOfIsLeftKanExtension_apply_app, externalProductBifunctor_map_app, Functor.leftUnitor_inv_app,
whiskerLeft_id, Category.comp_id, corepresentableBy_homEquiv_apply_app, NatTrans.comp_app, unit_app_map_app_assoc]
rw [associator_hom_unit_unit_assoc]
simp only [tensorHom_def, Category.assoc, externalProductBifunctor_obj_obj, tensor_obj, NatTrans.naturality,
unit_app_map_app_assoc]
rw [← comp_whiskerRight_assoc, unit_app_map_app]
simp only [Functor.comp_obj, tensor_obj, comp_whiskerRight, Category.assoc]
rw [← whisker_exchange_assoc, associator_hom_unit_unit, whisker_exchange_assoc, ←
MonoidalCategory.whiskerLeft_comp_assoc, unit_app_map_app]
simp [tensorHom_def]
