English
If C is a filtered category, then for every finite diagram F : J ⥤ C (with J a finite category) there exists a cocone over F.
Русский
Если C — фильтрованная категория, то для любой конечной диаграммы F : J ⥤ C существует кокон над F.
LaTeX
$$$\operatorname{IsFiltered}(C) \;\Rightarrow\; \forall {J} \ [\text{SmallCategory } J] [\text{FinCategory } J] \; (F : J \to C) \;\mapsto\; \operatorname{Nonempty}(\operatorname{Cocone}(F))$$$
Lean4
/-- If we have `IsFiltered C`, then for any functor `F : J ⥤ C` with `FinCategory J`,
there exists a cocone over `F`.
-/
theorem cocone_nonempty (F : J ⥤ C) : Nonempty (Cocone F) := by
classical
let O := Finset.univ.image F.obj
let H : Finset (Σ' (X Y : C) (_ : X ∈ O) (_ : Y ∈ O), X ⟶ Y) :=
Finset.univ.biUnion fun X : J =>
Finset.univ.biUnion fun Y : J =>
Finset.univ.image fun f : X ⟶ Y => ⟨F.obj X, F.obj Y, by simp [O], by simp [O], F.map f⟩
obtain ⟨Z, f, w⟩ := sup_exists O H
refine ⟨⟨Z, ⟨fun X => f (by simp [O]), ?_⟩⟩⟩
intro j j' g
dsimp
simp only [Category.comp_id]
apply w
simp only [O, H, Finset.mem_biUnion, Finset.mem_univ, Finset.mem_image, PSigma.mk.injEq, true_and, exists_and_left]
exact ⟨j, rfl, j', g, by simp⟩
