of_exists_of_isCofiltered_of_fullyFaithful

English

If D is cofiltered-or-empty and F : C → D is full and faithful and for every d ∈ D there exists c with a morphism F(c) → d, then C is cofiltered-or-empty.

Русский

Если D — кофильтровано-or-empty, F : C → D полно и верно, и для каждого d ∈ D существует c с морфизмом F(c) → d, тогда C — кофильтрованно-or-empty.

LaTeX

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

Lean4

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

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