Source: ProCGroups.LocalWeight.LocalWeightTheorems
1import ProCGroups.LocalWeight.ClosedNormalDataAndTransfiniteSeries
3/-!
4# Local weight from convergent generating sets
6This file identifies local weight with the clopen invariant `rho` in the presence of a closed
7generating set, and computes the cardinality of an infinite generating set that converges to the
8identity along open subgroups.
9-/
11open Set
12open TopologicalSpace
13open Order
14open scoped Cardinal
15open scoped Topology Pointwise
17namespace ProCGroups.LocalWeight
19universe u
21open ProCGroups.ProC ProCGroups.Generation
22open ProCGroups.FiniteGeneration
25/-- 6.2(a). Closed generating subsets compute the local weight. -/
26theorem localWeight_eq_rho_of_closedGeneratingSet
27 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
29 (X : Set G) (hXclosed : IsClosed X)
30 (hXgen : TopologicallyGenerates (G := G) X) (hXinfinite : Set.Infinite X) :
31 localWeight G = rho ↥X := by
32 have hGinf : Infinite G := by
33 classical
34 by_contra hfin
35 letI : Finite G := not_infinite_iff_finite.mp hfin
36 exact hXinfinite (Set.toFinite X)
37 letI : Infinite G := hGinf
38 have hle : localWeight G ≤ rho ↥X :=
39 localWeight_le_rho_of_closedGeneratingSet
40 (G := G) X hXclosed hXgen hXinfinite
41 have hrho_le : rho ↥X ≤ localWeight G := by
42 have hBasis : TopologicalSpace.IsTopologicalBasis { U : Set G | IsClopen U } :=
44 calc
45 rho ↥X ≤ rho G :=
46 rho_subtype_le_rho_of_closed (X := G) (A := X) hXclosed
47 _ = weight G := (weight_eq_rho_of_clopenBasis (X := G) hBasis).symm
48 _ = localWeight G :=
49 (localWeight_eq_weight_of_infinite_profiniteGroup (G := G)).symm
50 exact le_antisymm hle hrho_le
52/-- 6.2(b). Infinite generating sets converging to \(1\) have cardinality \(w_0(G)\). -/
53theorem cardinalEqLocalWeight_of_generatesAndConvergesToOneAlongOpenSubgroups_infinite
54 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
55 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
56 (X : Set G)
57 (hX : GeneratesAndConvergesToOneAlongOpenSubgroups (G := G) X) (hXinfinite : Set.Infinite X) :
58 Cardinal.mk X = localWeight G := by
59 have hclosure : closure X = X ∪ ({1} : Set G) := by
60 exact (closure_generatorsConvergingToOne (G := G) hX.2).2 hXinfinite
61 have hClosureInf : Set.Infinite (closure X) := by
62 by_contra hfin
63 exact hXinfinite ((Set.not_infinite.mp hfin).subset subset_closure)
64 have hClosureGen : TopologicallyGenerates (G := G) (closure X) := by
65 exact (topologicallyGenerates_closure_iff (G := G) (X := X)).1 hX.1
66 have hClosureClosed : IsClosed (closure X) := isClosed_closure
67 calc
68 Cardinal.mk X = rho ↥(closure X) := by
69 symm
70 exact rho_closure_eq_cardinal_of_generatesAndConvergesToOneAlongOpenSubgroups_infinite
71 (G := G) X hX hXinfinite hclosure
72 _ = localWeight G := by
73 simpa using
74 (localWeight_eq_rho_of_closedGeneratingSet
75 (G := G) (closure X) hClosureClosed hClosureGen hClosureInf).symm
80end ProCGroups.LocalWeight