English
The forgetful functor of the over category on any cofiltered-or-empty category is initial.
Русский
Функтор забывания из Over forget для любой кофильтрованной или пустой категории начальный.
LaTeX
$$Instance initial_forget [IsCofilteredOrEmpty C] (c : C) : Initial (Over.forget c)$$
Lean4
/-- The forgetful functor of the over category on any cofiltered or empty category is initial. -/
instance initial_forget [IsCofilteredOrEmpty C] (c : C) : Initial (Over.forget c) :=
initial_of_exists_of_isCofiltered _ (fun c' => ⟨mk (IsCofiltered.minToLeft c c'), ⟨IsCofiltered.minToRight c c'⟩⟩)
(fun {_} {x} s s' => by
use mk (IsCofiltered.eqHom s s' ≫ x.hom)
use homMk (IsCofiltered.eqHom s s') (by simp)
simp only [forget_obj, mk_left, forget_map, homMk_left]
rw [IsCofiltered.eq_condition])
