English
Construct a terminal object in the over category. This is not necessarily the canonical terminal object in Over, but a concrete one.
Русский
Построим терминальный объект в over-категории. Это не обязательно канонический терминальный объект, но конкретный пример.
LaTeX
$$$\text{HasTerminal}(Over B)$$$
Lean4
/-- Construct terminal object in the over category. This isn't an instance as it's not typically the
way we want to define terminal objects.
(For instance, this gives a terminal object which is different from the generic one given by
`over_product_of_widePullback` above.)
-/
theorem over_hasTerminal (B : C) : HasTerminal (Over B) where
has_limit
F :=
HasLimit.mk
{ cone :=
{ pt := Over.mk (𝟙 _)
π := { app := fun p => p.as.elim } }
isLimit :=
{ lift := fun s => Over.homMk s.pt.hom
fac := fun _ j => j.as.elim
uniq := fun s m _ => by
simp only
ext
rw [Over.homMk_left _]
have := m.w
dsimp at this
rwa [Category.comp_id, Category.comp_id] at this } }
