final_comp_equivalence — Mathlib

English

Final F is equivalent to: for all G, IsIso (colimit.pre G F).

Русский

Финальность F эквивалентна тому, что для всех G: D ⥤ Type, IsIso (colimit.pre G F).

LaTeX

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

Lean4

/-- See also the strictly more general `final_comp` below. -/
theorem final_comp_equivalence [Final F] [IsEquivalence G] : Final (F ⋙ G) :=
  let i : F ≅ (F ⋙ G) ⋙ G.inv := isoWhiskerLeft F G.asEquivalence.unitIso
  have : Final ((F ⋙ G) ⋙ G.inv) := final_of_natIso i
  final_of_comp_full_faithful (F ⋙ G) G.inv

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