English
The limit cone point underlying subtype is compact, ensuring a well-behaved compact topology on the limit carrier.
Русский
Точка предела на уровне каркаса носит компактную топологию, что обеспечивает хорошие свойства компактизма предела.
LaTeX
$$$\text{CompactSpace}(\mathrm{limitConePtAux}(F))$$$
Lean4
/-- An auxiliary result, superseded by `toLimit_surjective` -/
theorem denseRange_toLimit (P : ProfiniteGrp.{u}) : DenseRange (toLimit P) :=
by
apply dense_iff_inter_open.mpr
rintro U ⟨s, hsO, hsv⟩ ⟨⟨spc, hspc⟩, uDefaultSpec⟩
simp_rw [← hsv, Set.mem_preimage] at uDefaultSpec
rcases (isOpen_pi_iff.mp hsO) _ uDefaultSpec with ⟨J, fJ, hJ1, hJ2⟩
let M := iInf (fun (j : J) => j.1.1.1)
have hM : M.Normal := Subgroup.normal_iInf_normal fun j => j.1.isNormal'
have hMOpen : IsOpen (M : Set P) := by
rw [Subgroup.coe_iInf]
exact isOpen_iInter_of_finite fun i => i.1.1.isOpen'
let m : OpenNormalSubgroup P := { M with isOpen' := hMOpen }
rcases QuotientGroup.mk'_surjective M (spc m) with ⟨origin, horigin⟩
use (toLimit P) origin
refine ⟨?_, origin, rfl⟩
rw [← hsv]
apply hJ2
intro a a_in_J
let M_to_Na : m ⟶ a := (iInf_le (fun (j : J) => j.1.1.1) ⟨a, a_in_J⟩).hom
rw [← (P.toLimit origin).property M_to_Na]
change (P.toFiniteQuotientFunctor.map M_to_Na) (QuotientGroup.mk' M origin) ∈ _
rw [horigin]
exact Set.mem_of_eq_of_mem (hspc M_to_Na) (hJ1 a a_in_J).2
