over — Mathlib

English

The forgetful functor from the over category Over c to C is initial when C is cofiltered-or-empty.

Русский

Функтор забывания из Over c в C начальный при условии, что C кофильтрована или пустая.

LaTeX

$$Instance Over.forget.initial (c) : Initial (Over.forget c) with [IsCofilteredOrEmpty C]$$

Lean4

/-- Any over category on a cofiltered or empty category is cofiltered.
(Note that over categories are always filtered since they have a terminal object.) -/
instance over [IsCofilteredOrEmpty C] (c : C) : IsCofiltered (Over c) :=
  isCofiltered_costructuredArrow_of_isCofiltered_of_exists _ (fun c' => ⟨c', ⟨𝟙 _⟩⟩)
    (fun s s' => IsCofilteredOrEmpty.cone_maps s s') c

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