of_exists_of_isFiltered_of_fullyFaithful

English

If D is filtered and F : C → D is full and faithful, and for every d there exists c with d → F(c), then C is filtered.

Русский

Если D фильтрован и F полно и верно, и для каждого d существует c с d → F(c), то C фильтрован.

LaTeX

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

Lean4

/-- In this situation, `F` is also final, see
`Functor.final_of_exists_of_isFiltered_of_fullyFaithful`. -/
theorem of_exists_of_isFiltered_of_fullyFaithful [IsFiltered D] [F.Full] [F.Faithful]
    (h : ∀ d, ∃ c, Nonempty (d ⟶ F.obj c)) : IsFiltered C :=
  { IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful F h with
    nonempty := by
      have : Nonempty D := IsFiltered.nonempty
      obtain ⟨c, -⟩ := h (Classical.arbitrary D)
      exact ⟨c⟩ }

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