isoLimit_inv_π — Mathlib

English

If E is a pointwise right Kan extension, then there exists a corresponding left/right universal property establishing E as a pointwise right Kan extension.

Русский

Если E является точечным правым Кан-расширением, существует соответствующая универсальная собственность, устанавливающая E как точное правое Кан-расширение.

LaTeX

$$$\\text{HasPointwiseRightKanExtension}(L,F)$$$

Lean4

@[reassoc (attr := simp)]
theorem isoLimit_inv_π (g : StructuredArrow Y L) :
    h.isoLimit.inv ≫ E.left.map g.hom ≫ E.hom.app g.right = limit.π (StructuredArrow.proj Y L ⋙ F) g := by
  simpa using h.conePointUniqueUpToIso_inv_comp (limit.isLimit _) g

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