English
Given finite O, H, there exists S and T making all prescribed triangles commute.
Русский
Для конечного O и H существует S и T, делающие все заданные треугольники коммутирующими.
LaTeX
$$$\exists S, T, \forall X,Y\in O, \forall f: X\to Y, \text{ if }\langle X,Y,\dots,f\rangle \in H \Rightarrow T_X \circ f = T_Y$$$
Lean4
/-- If every finite diagram in `C` admits a cone, then `C` is cofiltered. It is sufficient to
verify this for diagrams whose shape lives in any one fixed universe. -/
theorem of_cone_nonempty (h : ∀ {J : Type w} [SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)) :
IsCofiltered C :=
by
have : Nonempty C := by
obtain ⟨c⟩ := h (Functor.empty _)
exact ⟨c.pt⟩
have : IsCofilteredOrEmpty 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.zero⟩, ?_⟩
have h₁ := c.π.naturality ⟨WalkingParallelPairHom.left⟩
have h₂ := c.π.naturality ⟨WalkingParallelPairHom.right⟩
simp_all
apply IsCofiltered.mk
