English
If every finite diagram in C admits a cocone, then C is filtered.
Русский
Если для каждой конечной диаграммы в C существует кокон, то C является фильтрованной.
LaTeX
$$$\\Bigl( \\forall J [SmallCategory J] [FinCategory J] (F : J \\to C), \\operatorname{Nonempty}(\\operatorname{Cocone}(F)) \\Bigr) \\Rightarrow \\operatorname{IsFiltered}(C).$$$
Lean4
/-- If every finite diagram in `C` admits a cocone, then `C` is filtered. It is sufficient to verify
this for diagrams whose shape lives in any one fixed universe. -/
theorem of_cocone_nonempty (h : ∀ {J : Type w} [SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)) :
IsFiltered C :=
by
have : Nonempty C := by
obtain ⟨c⟩ := h (Functor.empty _)
exact ⟨c.pt⟩
have : IsFilteredOrEmpty C := by
refine ⟨?_, ?_⟩
· intro X Y
obtain ⟨c⟩ := h (ULiftHom.down ⋙ ULift.downFunctor ⋙ pair X Y)
exact ⟨c.pt, c.ι.app ⟨⟨WalkingPair.left⟩⟩, c.ι.app ⟨⟨WalkingPair.right⟩⟩, trivial⟩
· intro X Y f g
obtain ⟨c⟩ := h (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
refine ⟨c.pt, c.ι.app ⟨WalkingParallelPair.one⟩, ?_⟩
have h₁ := c.ι.naturality ⟨WalkingParallelPairHom.left⟩
have h₂ := c.ι.naturality ⟨WalkingParallelPairHom.right⟩
simp_all
apply IsFiltered.mk
