English
For any functor F: J ⥤ C with J finite, there exists a cone over F.
Русский
Для любой функтор-функции F: J ⥤ C с конечным J существует конус над F.
LaTeX
$$$\exists \mathrm{Cone}\ F$$$
Lean4
/-- If we have `IsCofiltered C`, then for any functor `F : J ⥤ C` with `FinCategory J`,
there exists a cone over `F`.
-/
theorem cone_nonempty (F : J ⥤ C) : Nonempty (Cone 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⟩ := inf_exists O H
refine ⟨⟨Z, ⟨fun X => f (by simp [O]), ?_⟩⟩⟩
intro j j' g
dsimp
simp only [Category.id_comp]
symm
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⟩
