English
A triangular identity for the Day convolution associator and unit maps, expressed via Kan extension data.
Русский
Треугольная идентичность ассоциатора Day-конволюции и единичных отображений через данные распрямления Кан.
LaTeX
$$$ (\text{triangle}) : \; (\text{associator} \; F U G)^{} \circ \text{map}(\mathrm{id}_F) \circ (\text{leftUnitor}(U) G)^{} = \text{map}(\text{rightUnitor}(U F), \mathrm{id}_G) $$$
Lean4
theorem triangle (F G U : C ⥤ V) [DayConvolutionUnit U] [DayConvolution F U] [DayConvolution U G]
[DayConvolution F (U ⊛ G)] [DayConvolution (F ⊛ U) G] [DayConvolution F G] :
(DayConvolution.associator F U G).hom ≫ DayConvolution.map (𝟙 F) (DayConvolutionUnit.leftUnitor U G).hom =
DayConvolution.map (DayConvolutionUnit.rightUnitor U F).hom (𝟙 G) :=
by
apply Functor.hom_ext_of_isLeftKanExtension _ (DayConvolution.unit _ _) _
apply Functor.hom_ext_of_isLeftKanExtension (α := extensionUnitLeft (F ⊛ U) (DayConvolution.unit F U) G)
have :
(F ⊠ U) ⊠ G |>.IsLeftKanExtension (α :=
extensionUnitLeft (F ⊠ U) (extensionUnitRight U (DayConvolutionUnit.φ U) F) G) :=
isPointwiseLeftKanExtensionExtensionUnitLeft (F ⊠ U) _ G
(isPointwiseLeftKanExtensionExtensionUnitRight U (DayConvolutionUnit.φ U) F <|
DayConvolutionUnit.isPointwiseLeftKanExtensionCan (F := U)) |>.isLeftKanExtension
apply
Functor.hom_ext_of_isLeftKanExtension (α :=
extensionUnitLeft (F ⊠ U) (extensionUnitRight U (DayConvolutionUnit.φ U) F) G)
ext
dsimp
simp only [MonoidalCategory.whiskerRight_id, Category.id_comp, Iso.hom_inv_id, whisker_assoc,
MonoidalCategory.whiskerLeft_id, Category.comp_id, DayConvolution.associator_hom_unit_unit_assoc,
externalProductBifunctor_obj_obj, tensor_obj, NatTrans.naturality, unit_app_map_app_assoc, NatTrans.id_app,
id_tensorHom, Category.assoc, Iso.inv_hom_id_assoc, unit_app_map_app, Functor.comp_obj, tensorHom_id,
Iso.cancel_iso_hom_left]
simp only [← MonoidalCategory.whiskerLeft_comp_assoc, leftUnitor_hom_unit_app, associator_inv_naturality_middle_assoc,
← comp_whiskerRight_assoc, rightUnitor_hom_unit_app]
simp [← Functor.map_comp]
