English
Let F : C → D be full and faithful, with D filtered-or-empty and Axiom h: for every d ∈ D there exists c ∈ C and a morphism d → F(c). Then C is filtered-or-empty.
Русский
Пусть F: C → D полно и верно полно; D — фильтрованный или пустой; и для каждого d ∈ D существует c ∈ C и морфизм d → F(c). Тогда C — фильтрованный или пустой.
LaTeX
$$[IsFilteredOrEmpty D] [F.Full] [F.Faithful] (h : ∀ d, ∃ c, Nonempty (d ⟶ F.obj c)) → IsFilteredOrEmpty 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 [IsFilteredOrEmpty D] [F.Full] [F.Faithful]
(h : ∀ d, ∃ c, Nonempty (d ⟶ F.obj c)) : IsFilteredOrEmpty C
where
cocone_objs c
c' := by
obtain ⟨c₀, ⟨f⟩⟩ := h (IsFiltered.max (F.obj c) (F.obj c'))
exact ⟨c₀, F.preimage (IsFiltered.leftToMax _ _ ≫ f), F.preimage (IsFiltered.rightToMax _ _ ≫ f), trivial⟩
cocone_maps {c c'} f
g := by
obtain ⟨c₀, ⟨f₀⟩⟩ := h (IsFiltered.coeq (F.map f) (F.map g))
refine ⟨_, F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀), F.map_injective ?_⟩
simp [reassoc_of% (IsFiltered.coeq_condition (F.map f) (F.map g))]
