of_exists_of_isCofiltered_of_fullyFaithful

English

If D is cofiltered-or-empty and F : C → D is full and faithful, and every d ∈ D receives a morphism from some F(c), then C is cofiltered-or-empty.

Русский

Если D кофильтровано-or-empty и F: C → D полно и верно, и каждый объект d принимает исходящий морфизм из F(c), то 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 [IsCofiltered D] [F.Full] [F.Faithful]
    (h : ∀ d, ∃ c, Nonempty (F.obj c ⟶ d)) : IsCofiltered C :=
  { IsCofilteredOrEmpty.of_exists_of_isCofiltered_of_fullyFaithful F h with
    nonempty := by
      have : Nonempty D := IsCofiltered.nonempty
      obtain ⟨c, -⟩ := h (Classical.arbitrary D)
      exact ⟨c⟩ }

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