initial_of_exists_of_isCofiltered_of_fullyFaithful

English

Let F : C → D be a fully faithful functor with D cofiltered-or-empty and h: ∀d, ∃ c, F.obj c ⟶ d. Then F.Initial.

Русский

Пусть F : C → D есть полно-фиделю функтор, D — кофильтрован или пуст и для каждого d существует c с F(obj c) ⟶ d. Тогда F начальный.

LaTeX

$$[IsCofilteredOrEmpty D] [F.Full] [F.Faithful] (h : ∀ d, ∃ c, Nonempty (F.obj c ⟶ d)) → F.Initial$$

Lean4

/-- In this situation, `C` is also cofiltered, see
`IsCofilteredOrEmpty.of_exists_of_isCofiltered_of_fullyFaithful`. -/
theorem initial_of_exists_of_isCofiltered_of_fullyFaithful [IsCofilteredOrEmpty D] [F.Full] [Faithful F]
    (h : ∀ d, ∃ c, Nonempty (F.obj c ⟶ d)) : Initial F :=
  by
  suffices Final F.op from initial_of_final_op _
  refine Functor.final_of_exists_of_isFiltered_of_fullyFaithful F.op (fun d => ?_)
  obtain ⟨c, ⟨f⟩⟩ := h d.unop
  exact ⟨op c, ⟨f.op⟩⟩

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