English
In a cofiltered limit of profinite spaces, any clopen subset of the limit is the inverse image of a clopen subset from one of the factors.
Русский
В коллектном пределе профинидальных пространств любой клэповый множество предела является обратным образом предстоящего клэпового множества из одного из факторов.
LaTeX
$$$\\exists j:(F.obj j)\\;\\exists V\\subseteq F.obj j,\\ IsClopen(V) \\land U=C.\\pi.app j^{-1}(V).$$$
Lean4
/-- If `X` is a cofiltered limit of profinite sets, then any clopen subset of `X` arises from
a clopen set in one of the terms in the limit.
-/
theorem exists_isClopen_of_cofiltered {U : Set C.pt} (hC : IsLimit C) (hU : IsClopen U) :
∃ (j : J) (V : Set (F.obj j)), IsClopen V ∧ U = C.π.app j ⁻¹' V := by
-- First, we have the topological basis of the cofiltered limit obtained by pulling back
-- clopen sets from the factors in the limit. By continuity, all such sets are again clopen.
have hB :=
TopCat.isTopologicalBasis_cofiltered_limit.{u, v} (F ⋙ Profinite.toTopCat) (Profinite.toTopCat.mapCone C)
(isLimitOfPreserves _ hC) (fun j => {W | IsClopen W}) ?_ (fun i => isClopen_univ)
(fun i U1 U2 hU1 hU2 => hU1.inter hU2) ?_
rotate_left
· intro i
change TopologicalSpace.IsTopologicalBasis {W : Set (F.obj i) | IsClopen W}
apply isTopologicalBasis_isClopen
· rintro i j f V (hV : IsClopen _)
refine ⟨hV.1.preimage ?_, hV.2.preimage ?_⟩ <;>
continuity
-- Using this, since `U` is open, we can write `U` as a union of clopen sets all of which
-- are preimages of clopens from the factors in the limit.
obtain ⟨S, hS, h⟩ := hB.open_eq_sUnion hU.2
clear hB
let j : S → J := fun s => (hS s.2).choose
let V : ∀ s : S, Set (F.obj (j s)) := fun s => (hS s.2).choose_spec.choose
have hV : ∀ s : S, IsClopen (V s) ∧ s.1 = C.π.app (j s) ⁻¹' V s := fun s => (hS s.2).choose_spec.choose_spec
have hUo : ∀ (i : ↑S), IsOpen ((fun s ↦ (C.π.app (j s)) ⁻¹' V s) i) :=
by
intro s
exact (hV s).1.2.preimage (C.π.app (j s)).hom.continuous
have hsU : U ⊆ ⋃ (i : ↑S), (fun s ↦ C.π.app (j s) ⁻¹' V s) i :=
by
dsimp only
rw [h]
rintro x ⟨T, hT, hx⟩
refine ⟨_, ⟨⟨T, hT⟩, rfl⟩, ?_⟩
dsimp only
rwa [← (hV ⟨T, hT⟩).2]
have := hU.1.isCompact.elim_finite_subcover (fun s : S => C.π.app (j s) ⁻¹' V s) hUo hsU
obtain ⟨G, hG⟩ := this
classical
obtain ⟨j0, hj0⟩ := IsCofiltered.inf_objs_exists (G.image j)
let f : ∀ s ∈ G, j0 ⟶ j s := fun s hs => (hj0 (Finset.mem_image.mpr ⟨s, hs, rfl⟩)).some
let W : S → Set (F.obj j0) := fun s => if hs : s ∈ G then F.map (f s hs) ⁻¹' V s else Set.univ
refine ⟨j0, ⋃ (s : S) (_ : s ∈ G), W s, ?_, ?_⟩
· apply isClopen_biUnion_finset
intro s hs
dsimp [W]
rw [dif_pos hs]
refine ⟨(hV s).1.1.preimage ?_, (hV s).1.2.preimage ?_⟩ <;> fun_prop
· ext x
constructor
· intro hx
simp_rw [W, Set.preimage_iUnion, Set.mem_iUnion]
obtain ⟨_, ⟨s, rfl⟩, _, ⟨hs, rfl⟩, hh⟩ := hG hx
refine ⟨s, hs, ?_⟩
rwa [dif_pos hs, ← Set.preimage_comp, ← CompHausLike.coe_comp, C.w]
· intro hx
simp_rw [W, Set.preimage_iUnion, Set.mem_iUnion] at hx
obtain ⟨s, hs, hx⟩ := hx
rw [h]
refine ⟨s.1, s.2, ?_⟩
rw [(hV s).2]
rwa [dif_pos hs, ← Set.preimage_comp, ← CompHausLike.coe_comp, C.w] at hx
