isCoskeletal_iff_isIso — Mathlib

English

Analogous universality statement holds in the simplicial setting for IsCoskeletal and right Kan extensions.

Русский

Аналогично в симпликциальной настройке справедливо утверждение об универсальности для IsCoskeletal и правого Кан-расширения.

LaTeX

$$$[X.IsCoskeletal\ n] : \text{IsUniversal} (\mathrm{RightExtension\; unit}).$$$

Lean4

theorem isCoskeletal_iff_isIso : X.IsCoskeletal n ↔ IsIso ((coskAdj n).unit.app X) :=
  by
  rw [isCoskeletal_iff]
  exact
    isRightKanExtension_iff_isIso ((coskAdj n).unit.app X) ((coskAdj n).counit.app _) (𝟙 _)
      ((coskAdj n).left_triangle_components X)

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