English
The forgetful functor of the under category on any filtered or empty category is final.
Русский
Функтор забывания из Under.forget c для любой фильтрованной или пустой категории является финальным.
LaTeX
$$Instance final_forget [IsFilteredOrEmpty C] (c : C) : Final (Under.forget c)$$
Lean4
/-- The forgetful functor of the under category on any filtered or empty category is final. -/
instance final_forget [IsFilteredOrEmpty C] (c : C) : Final (Under.forget c) :=
final_of_exists_of_isFiltered _ (fun c' => ⟨mk (IsFiltered.leftToMax c c'), ⟨IsFiltered.rightToMax c c'⟩⟩)
(fun {_} {x} s s' => by
use mk (x.hom ≫ IsFiltered.coeqHom s s')
use homMk (IsFiltered.coeqHom s s') (by simp)
simp only [forget_obj, id_obj, mk_right, forget_map, homMk_right]
rw [IsFiltered.coeq_condition])
