English
If the universal morphism colimit.pre (coyoneda.obj(op d)) F is an isomorphism for each d, then colimit (F ⋙ coyoneda.obj(op d)) is canonically isomorphic to PUnit.
Русский
Если универсальный морфизм colimit.pre (coyoneda.obj(op d)) F является изоморфизмом для каждого d, то colimit (F ⋙ coyoneda.obj(op d)) канонически изоморфен PUnit.
LaTeX
$$$\\forall d,\\ [\\operatorname{IsIso}(\\operatorname{colimit.pre}(\\operatorname{coyoneda.obj}(\\operatorname{op} d)) F)] \\Rightarrow \\operatorname{colimit}(F \\circ \\operatorname{coyoneda.obj}(\\operatorname{op} d)) \\cong PUnit.$$
Lean4
/-- If `colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit` for all `d : D`, then `F` is final.
-/
theorem final_of_colimit_comp_coyoneda_iso_pUnit (I : ∀ d, colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit) : Final F :=
⟨fun d =>
by
have : Nonempty (StructuredArrow d F) := by
have := (I d).inv PUnit.unit
obtain ⟨j, y, rfl⟩ := Limits.Types.jointly_surjective'.{v, v} this
exact ⟨StructuredArrow.mk y⟩
apply zigzag_isConnected
rintro ⟨⟨⟨⟩⟩, X₁, f₁⟩ ⟨⟨⟨⟩⟩, X₂, f₂⟩
let y₁ := colimit.ι (F ⋙ coyoneda.obj (op d)) X₁ f₁
let y₂ := colimit.ι (F ⋙ coyoneda.obj (op d)) X₂ f₂
have e : y₁ = y₂ := by
apply (I d).toEquiv.injective
ext
have t := Types.colimit_eq.{v, v} e
clear e y₁ y₂
exact Final.zigzag_of_eqvGen_colimitTypeRel t⟩
