Yamaguchi Lean 4 Library
ProCGroups/FreeProC/Characterization/InverseLimitTowers.lean
ProCGroups/FreeProC/Characterization/InverseLimitTowers/Source

ProCGroups/FreeProC/Characterization/InverseLimitTowers.lean

1import ProCGroups.FreeProC.Characterization.EmbeddingProblems
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/FreeProC/Characterization/InverseLimitTowers.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Free pro-C groups
14Develops free pro-C groups on spaces and pointed spaces, their universal properties, finite quotient characterizations, and standard comparison isomorphisms.
15-/
17namespace ProCGroups.FreeProC.Characterization
19open ProCGroups.FreeProC
20open ProCGroups.InverseSystems
21open Set
22open scoped Topology
24universe u
26/-- A countable surjective inverse system of free pro-`C` groups.
28This record stores the transition maps for all `m ≤ n`, together with the identity and
29composition laws. Its limit is the canonical subtype inverse limit supplied by
30`InverseSystems.InverseSystem`. -/
33 stage : ℕ → FreeProCGroupOnConvergingSetData (ProC := ProC)
34 transition :
35 ∀ {m n : ℕ}, m ≤ n → (stage n).carrier →* (stage m).carrier
36 continuous_transition :
37 ∀ {m n : ℕ} (hmn : m ≤ n), Continuous (transition hmn)
38 transition_id :
39 ∀ n : ℕ, transition (le_rfl : n ≤ n) = MonoidHom.id (stage n).carrier
40 transition_comp :
41 ∀ {l m n : ℕ} (hlm : l ≤ m) (hmn : m ≤ n),
42 (transition hlm).comp (transition hmn) = transition (hlm.trans hmn)
43 surjective_transition :
44 ∀ {m n : ℕ} (hmn : m ≤ n), Function.Surjective (transition hmn)
50/-- The adjacent bonding map in the countable system. -/
51def bonding (T : CountableSurjectiveFreeProCSystem ProC) (n : ℕ) :
52 (T.stage (n + 1)).carrier →* (T.stage n).carrier :=
53 T.transition (Nat.le_succ n)
56 Continuous (T.bonding n) :=
57 T.continuous_transition (Nat.le_succ n)
60 Function.Surjective (T.bonding n) :=
61 T.surjective_transition (Nat.le_succ n)
63/-- The underlying inverse system associated to the countable tower data. -/
65 InverseSystem (I := ℕ) where
66 X := fun n => (T.stage n).carrier
67 topologicalSpace := fun n => inferInstance
68 map := fun {_m _n} hmn => T.transition hmn
69 continuous_map := fun {_m _n} hmn => T.continuous_transition hmn
70 map_id := by
71 intro n
72 funext x
73 simpa using congrArg (fun f : (T.stage n).carrier →* (T.stage n).carrier => f x)
74 (T.transition_id n)
75 map_comp := by
76 intro l m n hlm hmn
77 funext x
78 simpa [Function.comp, MonoidHom.comp_apply] using
79 congrArg (fun f : (T.stage n).carrier →* (T.stage l).carrier => f x)
80 (T.transition_comp hlm hmn)
83 (n : ℕ) : Group (T.inverseSystem.X n) := by
84 change Group (T.stage n).carrier
85 infer_instance
88 (n : ℕ) : IsTopologicalGroup (T.inverseSystem.X n) := by
89 change IsTopologicalGroup (T.stage n).carrier
90 infer_instance
92/-- The associated inverse system is group-valued. -/
94 IsGroupSystem T.inverseSystem where
95 map_one := by
96 intro m n hmn
97 exact (T.transition hmn).map_one
98 map_mul := by
99 intro m n hmn x y
100 exact (T.transition hmn).map_mul x y
101 map_inv := by
102 intro m n hmn x
103 exact (T.transition hmn).map_inv x
105/-- The canonical inverse-limit carrier of a countable surjective free pro-`C` system. -/
107 T.inverseSystem.inverseLimit
110 Group T.limitCarrier := by
111 letI : IsGroupSystem T.inverseSystem := T.isGroupSystem
112 infer_instance
115 TopologicalSpace T.limitCarrier := by
116 infer_instance
119 IsTopologicalGroup T.limitCarrier := by
120 letI : IsGroupSystem T.inverseSystem := T.isGroupSystem
121 infer_instance
123/-- The canonical projection homomorphism from the inverse limit to a stage. -/
124def projection (T : CountableSurjectiveFreeProCSystem ProC) (n : ℕ) :
125 T.limitCarrier →* (T.stage n).carrier := by
126 letI : IsGroupSystem T.inverseSystem := T.isGroupSystem
127 exact projectionHom (S := T.inverseSystem) n
129theorem continuous_projection (T : CountableSurjectiveFreeProCSystem ProC) (n : ℕ) :
130 Continuous (T.projection n) := by
131 simpa [projection, projectionHom] using T.inverseSystem.continuous_projection n
134 (x : T.limitCarrier) :
135 T.bonding n (T.projection (n + 1) x) = T.projection n x := by
136 simpa [bonding, projection, inverseSystem] using
137 T.inverseSystem.projection_compatible x n (n + 1) (Nat.le_succ n)
139/-- The canonical projection family satisfies the inverse-limit universal property. -/
140theorem isInverseLimit_projection (T : CountableSurjectiveFreeProCSystem ProC) :
141 T.inverseSystem.IsInverseLimit (fun n => T.projection n) := by
142 letI : IsGroupSystem T.inverseSystem := T.isGroupSystem
143 simpa [projection] using T.inverseSystem.isInverseLimit_projection
147/-- External freeness input for countable surjective inverse systems.
149The inverse-system data now determines the limit object itself; this criterion only records the
150additional mathematical input needed to identify that canonical limit as a free pro-`C` group. -/
153 (T : CountableSurjectiveFreeProCSystem ProC) : Prop where
154 free_limit_of_countable_generating_family :
155 Nonempty (ConvergingGeneratingMap ℕ T.limitCarrier) →
156 ∃ Fdata : FreeProCGroupOnConvergingSetData (ProC := ProC),
157 Nonempty (Fdata.carrier ≃ₜ* T.limitCarrier)
161/-- Apply the freeness criterion to the canonical inverse limit of a countable system. -/
162theorem apply
166 (hcount : Nonempty (ConvergingGeneratingMap ℕ T.limitCarrier)) :
167 ∃ Fdata : FreeProCGroupOnConvergingSetData (ProC := ProC),
168 Nonempty (Fdata.carrier ≃ₜ* T.limitCarrier) :=
169 hcrit.free_limit_of_countable_generating_family hcount
173end ProCGroups.FreeProC.Characterization