coev_naturality_app — Mathlib

English

Naturality of coevaluation under change of G to G' in DayConvolutionInternalHom

Русский

Естественность кооценки по отношению к переходу G → G' в DayConvolutionInternalHom.

LaTeX

$$$\\mathrm{coev}_{app} \\circ η = H(η) \\circ (\\mathrm{coev}_{app})$$$

Lean4

theorem coev_naturality_app {G' H' : C ⥤ V} [DayConvolution F G'] (η : G ⟶ G')
    (ℌ' : DayConvolutionInternalHom F (F ⊛ G') H') :
    η ≫ ℌ'.coev_app = ℌ.coev_app ≫ ℌ.map (DayConvolution.map (𝟙 _) η) ℌ' :=
  by
  ext c
  dsimp
  apply Wedge.IsLimit.hom_ext <| ℌ'.isLimitWedge c
  intro j
  apply MonoidalClosed.uncurry_injective
  dsimp
  simp only [Category.assoc, coev_app_π, Functor.comp_obj, tensor_obj, map_app_comp_π, coev_app_π_assoc,
    MonoidalClosed.uncurry_natural_right, MonoidalClosed.uncurry_curry, DayConvolution.unit_app_map_app,
    NatTrans.id_app, id_tensorHom]
  simp [MonoidalClosed.uncurry_natural_left]

Похожие утверждения