English
The cofiltered limit of a diagram of nonempty finite types is nonempty. In particular, if every object in a finite inverse system of nonempty finite types has a section, then there exists a global nonempty section.
Русский
Кофильтрованный предел диаграммы из непустых конечных типов непустижен и существует не пустая секция.
LaTeX
$$$$ \\operatorname{Nonempty}(F.{\\mathrm{sections}}) $$$$
Lean4
/-- The cofiltered limit of nonempty finite types is nonempty.
See `nonempty_sections_of_finite_inverse_system` for a specialization to inverse limits. -/
theorem nonempty_sections_of_finite_cofiltered_system {J : Type u} [Category.{w} J] [IsCofilteredOrEmpty J]
(F : J ⥤ Type v) [∀ j : J, Finite (F.obj j)] [∀ j : J, Nonempty (F.obj j)] : F.sections.Nonempty := by
-- Step 1: lift everything to the `max u v w` universe.
let J' : Type max w v u := AsSmall.{max w v} J
let down : J' ⥤ J := AsSmall.down
let F' : J' ⥤ Type max u v w := down ⋙ F ⋙ uliftFunctor.{max u w, v}
haveI : ∀ i, Nonempty (F'.obj i) := fun i => ⟨⟨Classical.arbitrary (F.obj (down.obj i))⟩⟩
haveI : ∀ i, Finite (F'.obj i) := fun i => Finite.of_equiv (F.obj (down.obj i)) Equiv.ulift.symm
cases isEmpty_or_nonempty J
· fconstructor <;> apply isEmptyElim
haveI : IsCofiltered J := ⟨⟩
obtain ⟨u, hu⟩ := nonempty_sections_of_finite_cofiltered_system.init F'
use fun j => (u ⟨j⟩).down
intro j j' f
have h := @hu (⟨j⟩ : J') (⟨j'⟩ : J') (ULift.up f)
simp only [F', down, AsSmall.down, Functor.comp_map, uliftFunctor_map] at h
simp_rw [← h]
