right_triangle_components — Mathlib

English

In Day convolution internal hom, a right triangle identity expresses that the composite of coevaluation with the mapped ev_app equals the identity on H.

Русский

В Day-конволюции внутренней гомологии, правая треугольная идентичность выражает, что композиция коэверации с отображённым ev_app даёт тождество на H.

LaTeX

$$$\\text{coev} \\circ (\\text{ev-app}) = \\mathrm{id}_H$$$

Lean4

theorem right_triangle_components (G : C ⥤ V) [DayConvolution F H] (ℌ : DayConvolutionInternalHom F G H) {H' : C ⥤ V}
    (ℌ' : DayConvolutionInternalHom F (F ⊛ H) H') : ℌ'.coev_app ≫ ℌ'.map ℌ.ev_app ℌ = 𝟙 H :=
  by
  ext c
  apply Wedge.IsLimit.hom_ext <| ℌ.isLimitWedge c
  intro j
  apply MonoidalClosed.uncurry_injective
  simp [MonoidalClosed.uncurry_natural_right]

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