left_triangle_components — Mathlib

English

In a Day convolution with inner hom, a left triangle identity holds: map(id_F) ∘ ev_app ∘ π = identity

Русский

В левом треугольнике Day конволюции с внутренним гом выполняется тождество: map(id_F) ∘ ev_app ∘ π = идентичность.

LaTeX

$$$\\mathrm{DayConvolution.map}(\\mathrm{Id} F) \\;\\circ\\; \\mathcal{H}.\\mathrm{ev}_{app} \\circ \\mathcal{H}.\\mathrm{π} = \\mathrm{Id}$$$

Lean4

theorem left_triangle_components (G : C ⥤ V) [DayConvolution F G] (ℌ : DayConvolutionInternalHom F (F ⊛ G) H)
    [DayConvolution F H] : DayConvolution.map (𝟙 F) ℌ.coev_app ≫ ℌ.ev_app = 𝟙 (F ⊛ G) :=
  by
  apply DayConvolution.corepresentableBy F G |>.homEquiv.injective
  dsimp
  ext ⟨x, y⟩
  apply MonoidalClosed.curry_injective
  simp [MonoidalClosed.curry_natural_left]

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