Source: ProCGroups.FreeProC.CanonicalData
1import ProCGroups.Completion.ProCIntegerPrimePower
2import ProCGroups.FreeProC.Basic
3import ProCGroups.ProC.InverseLimits.Predicates
5/-!
6# Pro C Groups / Free pro-C / Canonical Data
8This module supplies canonical basis maps and proves the rank-one free
9pro-\(p\) description of the pro-\(p\) integers.
10-/
12open Set
13open scoped Topology
15namespace ProCGroups.FreeProC
17universe u
19/--
20The rank-one basis map converges to the identity in the one-point compactification basis space.
21-/
22theorem familyConvergesToOneAlongOpenSubgroups_rankOneBasisMap
23 {G : Type u} [Group G] [TopologicalSpace G] (g : G) :
24 FamilyConvergesToOneAlongOpenSubgroups (G := G) (Function.const PUnit g) := by
25 exact FamilyConvergesToOneAlongOpenSubgroups.of_finite_domain (G := G) (Function.const PUnit g)
27/-- The rank-one basis map topologically generates the target cyclic pro-\(C\) group. -/
28theorem topologicallyGenerates_rankOneBasisMap
29 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {g : G}
30 (hg : Generation.TopologicallyGenerates (G := G) ({g} : Set G)) :
31 Generation.TopologicallyGenerates (G := G) (Set.range (Function.const PUnit g)) := by
32 have hrange : Set.range (Function.const PUnit g) = ({g} : Set G) := by
33 ext y
34 simp only [mem_range, Function.const, exists_const, mem_singleton_iff, eq_comm]
35 rw [hrange]
36 exact hg
38/--
39The ordinary profinite integers, with their canonical generator, give the expected rank-one
40profinite generating datum.
41-/
42theorem profiniteInteger_rankOneGeneratingData :
43 ∃ ι : PUnit →
44 Multiplicative
45 (Completion.ProCIntegerLimitCarrier
46 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0})),
48 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0})
49 (Multiplicative
50 (Completion.ProCIntegerLimitCarrier
51 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0}))) ∧
52 FamilyConvergesToOneAlongOpenSubgroups (G :=
53 Multiplicative
54 (Completion.ProCIntegerLimitCarrier
55 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0}))) ι ∧
56 Generation.TopologicallyGenerates (G :=
57 Multiplicative
58 (Completion.ProCIntegerLimitCarrier
59 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0})))
60 (Set.range ι) := by
61 let G : Type := Multiplicative
62 (Completion.ProCIntegerLimitCarrier
63 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0}))
64 let g : G := Completion.proCIntegerOne
65 (C := (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0}))
66 refine ⟨Function.const PUnit g, ?_, ?_, ?_⟩
67 · exact Completion.hasOpenNormalBasisInClass_multiplicative_proCInteger_allFinite
68 · exact familyConvergesToOneAlongOpenSubgroups_rankOneBasisMap (G := G) g
69 · exact topologicallyGenerates_rankOneBasisMap
70 (G := G) (g := g)
71 Completion.topologicallyGenerates_singleton_proCIntegerOne_allFinite
73/--
74The pro-\(p\) integers, with their canonical generator, give the expected rank-one pro-\(p\)
75generating datum.
76-/
77theorem proPInteger_rankOneGeneratingData (p : ℕ) [Fact (Nat.Prime p)] :
78 ∃ ι : PUnit →
79 Multiplicative
80 (Completion.ProCIntegerLimitCarrier
81 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0})),
83 (Multiplicative
84 (Completion.ProCIntegerLimitCarrier
85 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0}))) ∧
86 FamilyConvergesToOneAlongOpenSubgroups (G :=
87 Multiplicative
88 (Completion.ProCIntegerLimitCarrier
89 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0}))) ι ∧
90 Generation.TopologicallyGenerates (G :=
91 Multiplicative
92 (Completion.ProCIntegerLimitCarrier
93 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0})))
94 (Set.range ι) := by
95 let G : Type := Multiplicative
96 (Completion.ProCIntegerLimitCarrier
97 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0}))
98 let g : G := Completion.proCIntegerOne
99 (C := (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0}))
100 refine ⟨Function.const PUnit g, ?_, ?_, ?_⟩
101 · exact Completion.hasPGroupOpenNormalBasis_multiplicative_proCInteger_pGroup (p := p)
102 · exact familyConvergesToOneAlongOpenSubgroups_rankOneBasisMap (G := G) g
103 · exact topologicallyGenerates_rankOneBasisMap
104 (G := G) (g := g)
105 (Completion.topologicallyGenerates_singleton_proCIntegerOne_pGroup (p := p))
107end ProCGroups.FreeProC