ProCGroups/FreeProC/CanonicalData.lean
1import Mathlib.FieldTheory.IsAlgClosed.Basic
2import ProCGroups.Completion.ProCIntegerPrimePower
3import ProCGroups.FreeProC.Basic
4import ProCGroups.ProC.GroupPredicates.Standard
6/-
7PUBLIC_PAGE_SNAPSHOT
8generated_at: 2026-05-27T09:47:29+09:00
9lean_source: lean4/ProCGroups/FreeProC/CanonicalData.lean
10translation_root: data/translation
11purpose: identifies the local data snapshot used to build pages/
12placement: after imports, never before imports
13-/
14/-!
15# Free pro-C groups
17Develops free pro-C groups on spaces and pointed spaces, their universal properties, finite quotient characterizations, and standard comparison isomorphisms.
18-/
20open Set
21open scoped Topology
23namespace ProCGroups.FreeProC
25universe u v
27/-- The usual delta-basis map into a direct product. -/
28noncomputable def deltaBasisMap
29 {X : Type u} {A : Type v} [One A] (a : A) : X → (X → A) := by
30 classical
31 exact fun x y => if y = x then a else 1
33@[simp]
34theorem deltaBasisMap_apply_self
35 {X : Type u} {A : Type v} [One A] (a : A) (x : X) :
36 deltaBasisMap (X := X) (A := A) a x x = a := by
37 classical
38 simp only [deltaBasisMap, ↓reduceIte]
40@[simp]
41theorem deltaBasisMap_apply_ne
42 {X : Type u} {A : Type v} [One A] (a : A) {x y : X} (h : y ≠ x) :
43 deltaBasisMap (X := X) (A := A) a x y = 1 := by
44 classical
45 simp only [deltaBasisMap, h, ↓reduceIte]
48 {G : Type u} [Group G] [TopologicalSpace G] (g : G) :
49 FamilyConvergesToOne (G := G) (Function.const PUnit g) := by
50 exact FamilyConvergesToOne.of_finite_domain (G := G) (Function.const PUnit g)
53 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {g : G}
54 (hg : Generation.TopologicallyGenerates (G := G) ({g} : Set G)) :
55 Generation.TopologicallyGenerates (G := G) (Set.range (Function.const PUnit g)) := by
56 have hrange : Set.range (Function.const PUnit g) = ({g} : Set G) := by
57 ext y
58 simp only [mem_range, Function.const, exists_const, mem_singleton_iff, eq_comm]
59 rw [hrange]
60 exact hg
62/-- The ordinary profinite integers, with their canonical generator, give the expected rank-one
63profinite generating datum. -/
64theorem profiniteInteger_rankOneGeneratingData :
65 ∃ ι : PUnit →
66 Multiplicative
67 (Completion.ProCIntegerLimitCarrier
68 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0})),
70 Multiplicative
71 (Completion.ProCIntegerLimitCarrier
72 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0}))) ∧
73 FamilyConvergesToOne (G :=
74 Multiplicative
75 (Completion.ProCIntegerLimitCarrier
76 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0}))) ι ∧
77 Generation.TopologicallyGenerates (G :=
78 Multiplicative
79 (Completion.ProCIntegerLimitCarrier
80 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0})))
81 (Set.range ι) := by
82 let G : Type := Multiplicative
83 (Completion.ProCIntegerLimitCarrier
84 (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0}))
85 let g : G := Completion.proCIntegerOne
86 (C := (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass.{0}))
87 refine ⟨Function.const PUnit g, ?_, ?_, ?_⟩
88 · exact Completion.isProCGroup_multiplicative_proCInteger_allFinite.1
89 · exact familyConvergesToOne_rankOneBasisMap (G := G) g
91 (G := G) (g := g)
92 Completion.topologicallyGenerates_singleton_proCIntegerOne_allFinite
94/-- The pro-`p` integers, with their canonical generator, give the expected rank-one pro-`p`
95generating datum. -/
96theorem proPInteger_rankOneGeneratingData (p : ℕ) [Fact (Nat.Prime p)] :
97 ∃ ι : PUnit →
98 Multiplicative
99 (Completion.ProCIntegerLimitCarrier
100 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0})),
101 ProCGroups.ProC.proPProC p (G :=
102 Multiplicative
103 (Completion.ProCIntegerLimitCarrier
104 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0}))) ∧
105 FamilyConvergesToOne (G :=
106 Multiplicative
107 (Completion.ProCIntegerLimitCarrier
108 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0}))) ι ∧
109 Generation.TopologicallyGenerates (G :=
110 Multiplicative
111 (Completion.ProCIntegerLimitCarrier
112 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0})))
113 (Set.range ι) := by
114 let G : Type := Multiplicative
115 (Completion.ProCIntegerLimitCarrier
116 (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0}))
117 let g : G := Completion.proCIntegerOne
118 (C := (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass.{0}))
119 refine ⟨Function.const PUnit g, ?_, ?_, ?_⟩
120 · exact Completion.isProPGroup_multiplicative_proCInteger_pGroup (p := p)
121 · exact familyConvergesToOne_rankOneBasisMap (G := G) g
123 (G := G) (g := g)
124 (Completion.topologicallyGenerates_singleton_proCIntegerOne_pGroup (p := p))
126namespace Applications
127namespace FunctionFieldGalois
129/-- Application-specific bundled data for a profinite group modeled on
130`Gal(K(t)^alg/K(t))`. This lives outside the reusable FreeProC API because the
131Galois interpretation is extra mathematical input, not part of the abstract
132free pro-`C` interface. -/
134 (K : Type u) [Field K] [IsAlgClosed K] where
135 carrier : Type u
137 instTopologicalSpace : TopologicalSpace carrier
138 instIsTopologicalGroup : IsTopologicalGroup carrier
139 isGaloisModel : Prop
140 basis : Type u
141 basisCard : Cardinal.mk basis = Cardinal.mk K
142 basisMap : basis → carrier
143 freeProfiniteBasis :
145 (ProC := ProCGroups.ProC.allFiniteProC) basis carrier basisMap
147attribute [instance] ModelData.instGroup
148attribute [instance] ModelData.instTopologicalSpace
149attribute [instance] ModelData.instIsTopologicalGroup
151end FunctionFieldGalois
152end Applications
154end ProCGroups.FreeProC