English
The sections of F are in bijection with the sections of F.toEventualRanges.
Русский
Разделы F взаимно однозначно соответствуют разделам F.toEventualRanges.
LaTeX
$$$ F.toEventualRanges.sections \cong F.sections $$$
Lean4
/-- This bootstraps `nonempty_sections_of_finite_inverse_system`. In this version,
the `F` functor is between categories of the same universe, and it is an easy
corollary to `TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system`. -/
theorem init {J : Type u} [SmallCategory J] [IsCofilteredOrEmpty J] (F : J ⥤ Type u) [hf : ∀ j, Finite (F.obj j)]
[hne : ∀ j, Nonempty (F.obj j)] : F.sections.Nonempty :=
by
let F' : J ⥤ TopCat := F ⋙ TopCat.discrete
haveI : ∀ j, DiscreteTopology (F'.obj j) := fun _ => ⟨rfl⟩
haveI : ∀ j, Finite (F'.obj j) := hf
haveI : ∀ j, Nonempty (F'.obj j) := hne
obtain ⟨⟨u, hu⟩⟩ := TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system.{u} F'
exact ⟨u, hu⟩
