ev_naturality_app — Mathlib

English

Naturality of ev_app with respect to a morphism η: G → G' expresses a commutation with map and application

Русский

Естественность ev_app по отношению к морфизму η: G → G' выражается через commuting с map и приложением.

LaTeX

$$$\\mathrm{ev}_{app} \\circ DayConvolution.map(\\mathrm{Id}_F, η) \\;=\\; η \\circ \\mathrm{ev}_{app}$$$

Lean4

theorem ev_naturality_app {G' H' : C ⥤ V} (ℌ' : DayConvolutionInternalHom F G' H') [DayConvolution F H'] (η : G ⟶ G') :
    DayConvolution.map (𝟙 F) (ℌ.map η ℌ') ≫ ℌ'.ev_app = ℌ.ev_app ≫ η :=
  by
  apply DayConvolution.corepresentableBy F H |>.homEquiv.injective
  dsimp
  ext ⟨x, y⟩
  simp [MonoidalClosed.uncurry_eq, ← whiskerLeft_comp_assoc]

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