isIso_hom_app — Mathlib

English

For a pointwise right Kan extension h, each component E.hom.app X is an isomorphism when L is full and faithful.

Русский

Для точечного правого Кан-расширения h каждая компонента E.hom.app X является изоморфизмом при условии полноты и верности L.

LaTeX

$$$\\text{IsIso}(E.hom.app X)$$$

Lean4

theorem isIso_hom_app {X : C} (h : E.IsPointwiseRightKanExtensionAt (L.obj X)) [L.Full] [L.Faithful] :
    IsIso (E.hom.app X) := by simpa using h.isIso_π_app_of_isInitial _ StructuredArrow.mkIdInitial

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