unit_app_ev_app_app — Mathlib

English

A natural computation expresses the interaction between the unit of the Day convolution and the ev_app, relating to the curry-uncurry structure.

Русский

Единичный элемент Day конволюции и работать с ev_app описывают связь между карри и анкарри (curry-uncurry).

LaTeX

$$$((\\mathrm{DayConvolution.unit} \\! F \\! H)_{c}) \\circ (\\mathcal{H}.ev_{app})_{(x,y)} = \\mathrm{MonoidalClosed.uncurry}(\\mathcal{H}.\\pi_{y,x})$$$

Lean4

@[reassoc (attr := simp)]
theorem unit_app_ev_app_app (x y : C) :
    ((DayConvolution.unit F H).app (x, y) ≫ (ℌ.ev_app).app (x ⊗ y)) = MonoidalClosed.uncurry (ℌ.π y x) :=
  by
  have := Functor.descOfIsLeftKanExtension_fac_app (F ⊛ H) (DayConvolution.unit F H) G
  dsimp at this
  simp [this, ev_app]

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