English
Every locally constant map from the limit to α factors through one component of the diagram.
Русский
Каждое локально константное отображение из предела в α факторизуется через одну компоненту диаграммы.
LaTeX
$$$\\forall α,\\,\\exists j,\\exists g:\\mathrm{LocallyConstant}(F(j),α),\\ f= g\\circ (C.\\pi.app j).hom$$$
Lean4
/-- Any locally constant function from a cofiltered limit of profinite sets factors through
one of the components. -/
theorem exists_locallyConstant {α : Type*} (hC : IsLimit C) (f : LocallyConstant C.pt α) :
∃ (j : J) (g : LocallyConstant (F.obj j) α), f = g.comap (C.π.app _).hom :=
by
let S := f.discreteQuotient
let ff : S → α := f.lift
cases isEmpty_or_nonempty S
· suffices ∃ j, IsEmpty (F.obj j) by
refine this.imp fun j hj => ?_
refine ⟨⟨hj.elim, fun A => ?_⟩, ?_⟩
· suffices (fun a ↦ IsEmpty.elim hj a) ⁻¹' A = ∅ by
rw [this]
exact isOpen_empty
exact @Set.eq_empty_of_isEmpty _ hj _
· ext x
exact hj.elim' (C.π.app j x)
by_contra! h
haveI : ∀ j : J, Nonempty ((F ⋙ Profinite.toTopCat).obj j) := h
haveI : ∀ j : J, T2Space ((F ⋙ Profinite.toTopCat).obj j) := fun j => (inferInstance : T2Space (F.obj j))
haveI : ∀ j : J, CompactSpace ((F ⋙ Profinite.toTopCat).obj j) := fun j => (inferInstance : CompactSpace (F.obj j))
have cond := TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system.{u} (F ⋙ Profinite.toTopCat)
suffices Nonempty C.pt from IsEmpty.false (S.proj this.some)
let D := Profinite.toTopCat.mapCone C
have hD : IsLimit D := isLimitOfPreserves Profinite.toTopCat hC
have CD := (hD.conePointUniqueUpToIso (TopCat.limitConeIsLimit.{v, max u v} _)).inv
exact cond.map CD
· let f' : LocallyConstant C.pt S := ⟨S.proj, S.proj_isLocallyConstant⟩
obtain ⟨j, g', hj⟩ := exists_locallyConstant_finite_nonempty _ hC f'
refine ⟨j, ⟨ff ∘ g', g'.isLocallyConstant.comp _⟩, ?_⟩
ext1 t
apply_fun fun e => e t at hj
dsimp at hj ⊢
rw [← hj]
rfl
