final_iff_isIso_colimit_pre — Mathlib

English

Final F is equivalent to: for every functor G: D ⥤ Type, the morphism colimit.pre G F is an isomorphism.

Русский

Финальность F эквивалентна тому, что для любого г Functor G: D ⥤ Type, морфизм colimit.pre G F является изоморфизмом.

LaTeX

$$$\\mathrm{Final}(F) \\iff \\forall G: D \\to \\mathbf{Type}, \\ \\mathrm{IsIso}(\\operatorname{colimit.pre} G F).$$$

Lean4

theorem final_iff_isIso_colimit_pre : Final F ↔ ∀ G : D ⥤ Type v, IsIso (colimit.pre G F) :=
  ⟨fun _ => inferInstance, fun _ =>
    final_of_colimit_comp_coyoneda_iso_pUnit _ fun _ => Final.colimitCompCoyonedaIso _ _⟩

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