final_of_isTerminal_colimit_comp_yoneda

English

If the colimit of F ⋙ yoneda is terminal, then F is final.

Русский

Если колимит F ⋙ Yoneda тождественно терминируется, то F финальный.

LaTeX

$$$\\mathrm{IsTerminal}(\\operatorname{colimit}(F \\circ \\mathrm{yoneda})) \\Rightarrow \\mathrm{Final}(F).$$$

Lean4

/-- A variant of `final_of_colimit_comp_coyoneda_iso_pUnit` where we bind the various claims
about `colimit (F ⋙ coyoneda.obj (Opposite.op d))` for each `d : D` into a single claim about
the presheaf `colimit (F ⋙ yoneda)`. -/
theorem final_of_isTerminal_colimit_comp_yoneda (h : IsTerminal (colimit (F ⋙ yoneda))) : Final F :=
  by
  refine final_of_colimit_comp_coyoneda_iso_pUnit _ (fun d => ?_)
  refine Types.isTerminalEquivIsoPUnit _ ?_
  let b := IsTerminal.isTerminalObj ((evaluation _ _).obj (Opposite.op d)) _ h
  exact b.ofIso <| preservesColimitIso ((evaluation _ _).obj (Opposite.op d)) (F ⋙ yoneda)

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