Yamaguchi Lean 4 Library
ProCGroups/InverseSystems/Exactness.lean
ProCGroups/InverseSystems/Exactness/Source

ProCGroups/InverseSystems/Exactness.lean

1import Mathlib.Topology.Algebra.ContinuousMonoidHom
2import ProCGroups.InverseSystems.CompatibilityAndSurjectivity
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/InverseSystems/Exactness.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Inverse systems and inverse limits
15Defines inverse systems of topological groups and proves lift, projection, exactness, quotient, stagewise isomorphism, and finite-stage factorization results.
16-/
18universe u v
20namespace ProCGroups
22namespace InverseSystems.InverseSystem
24variable {I : Type u} [Preorder I]
25variable {S T U : InverseSystems.InverseSystem (I := I)}
26attribute [local instance] InverseSystems.InverseSystem.topologicalSpace
27instance instTopologicalSpaceS (i : I) : TopologicalSpace (S.X i) := S.topologicalSpace i
28instance instTopologicalSpaceT (i : I) : TopologicalSpace (T.X i) := T.topologicalSpace i
29instance instTopologicalSpaceU (i : I) : TopologicalSpace (U.X i) := U.topologicalSpace i
30variable [∀ i, Group (S.X i)] [∀ i, Group (T.X i)] [∀ i, Group (U.X i)]
32/-- A morphism of group-valued inverse systems with homomorphism laws bundled componentwise. -/
33structure GroupMorphism (S T : InverseSystems.InverseSystem (I := I))
34 [∀ i, Group (S.X i)] [∀ i, Group (T.X i)] extends S.Morphism T where
35 map_one' : ∀ i, map i 1 = 1
36 map_mul' : ∀ i (x y : S.X i), map i (x * y) = map i x * map i y
38namespace GroupMorphism
40/-- Build a bundled group morphism from componentwise continuous monoid homomorphisms. -/
42 (φ : ∀ i, S.X i →ₜ* T.X i)
43 (hcomm : ∀ {i j : I} (hij : i ≤ j),
44 T.map hij ∘ φ j = φ i ∘ S.map hij) :
45 GroupMorphism S T where
46 map := fun i => φ i
47 continuous_map := fun i => (φ i).continuous_toFun
48 comm := hcomm
49 map_one' := fun i => (φ i).map_one
50 map_mul' := fun i => (φ i).map_mul
52/-- The group-system morphism built from continuous monoid homomorphisms has the prescribed stage maps. -/
54 (φ : ∀ i, S.X i →ₜ* T.X i)
55 (hcomm : ∀ {i j : I} (hij : i ≤ j),
56 T.map hij ∘ φ j = φ i ∘ S.map hij)
57 (i : I) (x : S.X i) :
58 (ofContinuousMonoidHom (S := S) (T := T) φ hcomm).map i x = φ i x :=
59 rfl
61/-- The identity bundled group morphism. -/
62def id (S : InverseSystems.InverseSystem (I := I))
63 [∀ i, Group (S.X i)] :
64 GroupMorphism S S where
65 toMorphism := InverseSystems.InverseSystem.Morphism.id S
66 map_one' := fun _ => rfl
67 map_mul' := fun _ _ _ => rfl
69/-- The identity group-system morphism acts as the identity at each stage. -/
70@[simp] theorem id_apply
71 (i : I) (x : S.X i) :
72 (id S).map i x = x :=
73 rfl
75/-- Composition of bundled group morphisms. -/
76def comp (Ψ : GroupMorphism T U) (Θ : GroupMorphism S T) :
77 GroupMorphism S U where
78 toMorphism := InverseSystems.InverseSystem.Morphism.comp Ψ.toMorphism Θ.toMorphism
79 map_one' := by
80 intro i
81 simp only [Morphism.comp_apply, Θ.map_one', Ψ.map_one']
82 map_mul' := by
83 intro i x y
84 simp only [Morphism.comp_apply, Θ.map_mul', Ψ.map_mul']
86/-- Composition of group-system morphisms is computed stagewise. -/
87@[simp] theorem comp_apply (Ψ : GroupMorphism T U) (Θ : GroupMorphism S T)
88 (i : I) (x : S.X i) :
89 (comp Ψ Θ).map i x = Ψ.map i (Θ.map i x) :=
90 rfl
94/-- A morphism of group-valued inverse systems induces a homomorphism on inverse limits. -/
95def limMapMonoidHom (Θ : S.Morphism T)
96 (hΘ_one : ∀ i, Θ.map i 1 = 1)
97 (hΘ_mul : ∀ i (x y : S.X i), Θ.map i (x * y) = Θ.map i x * Θ.map i y)
98 [InverseSystems.IsGroupSystem S] [InverseSystems.IsGroupSystem T] :
99 S.inverseLimit →* T.inverseLimit where
100 toFun := S.limMap Θ
101 map_one' := by
102 apply T.ext
103 intro i
104 have hpi := congrFun (S.π_comp_limMap (Θ := Θ) i) (1 : S.inverseLimit)
105 calc
106 T.projection i (S.limMap Θ 1) = Θ.map i (S.projection i 1) := by
107 simpa [Function.comp] using hpi
108 _ = Θ.map i 1 := by rfl
109 _ = 1 := hΘ_one i
110 map_mul' := by
111 intro x y
112 apply T.ext
113 intro i
114 have hxy := congrFun (S.π_comp_limMap (Θ := Θ) i) (x * y)
115 have hx := congrFun (S.π_comp_limMap (Θ := Θ) i) x
116 have hy := congrFun (S.π_comp_limMap (Θ := Θ) i) y
117 have hx' : T.projection i (S.limMap Θ x) = Θ.map i (S.projection i x) := by
118 simpa [Function.comp] using hx
119 have hy' : T.projection i (S.limMap Θ y) = Θ.map i (S.projection i y) := by
120 simpa [Function.comp] using hy
121 calc
122 T.projection i (S.limMap Θ (x * y)) = Θ.map i (S.projection i (x * y)) := by
123 simpa [Function.comp] using hxy
124 _ = Θ.map i (S.projection i x) * Θ.map i (S.projection i y) := by
125 simpa using hΘ_mul i (S.projection i x) (S.projection i y)
126 _ = T.projection i (S.limMap Θ x) * T.projection i (S.limMap Θ y) := by
127 rw [← hx', ← hy']
129/-- Bundled group morphisms induce homomorphisms on inverse limits without repeating the
130componentwise homomorphism laws. -/
131def GroupMorphism.limMapMonoidHom (Θ : GroupMorphism S T)
132 [InverseSystems.IsGroupSystem S] [InverseSystems.IsGroupSystem T] :
133 S.inverseLimit →* T.inverseLimit :=
135 (S := S) (T := T) Θ.toMorphism Θ.map_one' Θ.map_mul'
137/-- The monoid homomorphism induced on inverse limits agrees with the stage map after projection. -/
138@[simp] theorem GroupMorphism.limMapMonoidHom_apply_π
139 (Θ : GroupMorphism S T)
140 [InverseSystems.IsGroupSystem S] [InverseSystems.IsGroupSystem T]
141 (i : I) (x : S.inverseLimit) :
142 T.projection i (Θ.limMapMonoidHom x) = Θ.map i (S.projection i x) := by
143 simpa [GroupMorphism.limMapMonoidHom,
145 congrFun (S.π_comp_limMap (Θ := Θ.toMorphism) i) x
147/-- If the componentwise composite `Ψ_i ∘ Θ_i` is trivial, then the induced morphisms on inverse
148limits also compose to the trivial homomorphism. This isolates the only non-formal part of the
149`range ⊆ ker` direction. -/
151 {Θ : S.Morphism T} {Ψ : T.Morphism U}
152 [InverseSystems.IsGroupSystem S] [InverseSystems.IsGroupSystem T] [InverseSystems.IsGroupSystem U]
153 (hΘ_one : ∀ i, Θ.map i 1 = 1)
154 (hΘ_mul : ∀ i (x y : S.X i), Θ.map i (x * y) = Θ.map i x * Θ.map i y)
155 (hΨ_one : ∀ i, Ψ.map i 1 = 1)
156 (hΨ_mul : ∀ i (x y : T.X i), Ψ.map i (x * y) = Ψ.map i x * Ψ.map i y)
157 (hcomp : ∀ i, Ψ.map i ∘ Θ.map i = fun _ => 1) :
158 limMapMonoidHom (S := T) (T := U) Ψ hΨ_one hΨ_mul ∘
159 limMapMonoidHom (S := S) (T := T) Θ hΘ_one hΘ_mul =
160 fun _ => 1 := by
161 funext x
162 apply U.ext
163 intro i
164 have hπΘ := congrFun (S.π_comp_limMap (Θ := Θ) i) x
165 have hπΨ := congrFun (T.π_comp_limMap (Θ := Ψ) i) (S.limMap Θ x)
166 have hπΘ' : T.projection i (S.limMap Θ x) = Θ.map i (S.projection i x) := by
167 simpa [Function.comp] using hπΘ
168 have hπΨ' :
169 U.projection i (T.limMap Ψ (S.limMap Θ x)) = Ψ.map i (T.projection i (S.limMap Θ x)) := by
170 simpa [Function.comp] using hπΨ
171 have hcomp' : Ψ.map i (Θ.map i (S.projection i x)) = 1 := by
172 simpa [Function.comp] using congrFun (hcomp i) (S.projection i x)
173 calc
174 U.projection i
175 ((limMapMonoidHom (S := T) (T := U) Ψ hΨ_one hΨ_mul)
176 ((limMapMonoidHom (S := S) (T := T) Θ hΘ_one hΘ_mul) x))
177 = Ψ.map i (T.projection i (S.limMap Θ x)) := by
178 simpa [limMapMonoidHom] using hπΨ'
179 _ = Ψ.map i (Θ.map i (S.projection i x)) := by rw [hπΘ']
180 _ = 1 := hcomp'
181 _ = U.projection i (1 : U.inverseLimit) := rfl
183/-- Inverse limits preserve short exact sequences of profinite
184groups when taken over a common directed index category. -/
186 [∀ i, CompactSpace (T.X i)] [∀ i, T2Space (T.X i)] [∀ i, T2Space (U.X i)]
187 [InverseSystems.IsGroupSystem S] [InverseSystems.IsGroupSystem T] [InverseSystems.IsGroupSystem U]
188 {Θ : S.Morphism T} {Ψ : T.Morphism U}
189 (hΘ_one : ∀ i, Θ.map i 1 = 1)
190 (hΘ_mul : ∀ i (x y : S.X i), Θ.map i (x * y) = Θ.map i x * Θ.map i y)
191 (hΨ_one : ∀ i, Ψ.map i 1 = 1)
192 (hΨ_mul : ∀ i (x y : T.X i), Ψ.map i (x * y) = Ψ.map i x * Ψ.map i y)
193 (hdir : Directed (· ≤ ·) (id : I → I))
194 (hΘinj : ∀ i, Function.Injective (Θ.map i))
195 (hΨsurj : ∀ i, Function.Surjective (Ψ.map i))
196 (hcomp : ∀ i, Ψ.map i ∘ Θ.map i = fun _ => 1)
197 (hexact : ∀ i, ∀ y : T.X i, Ψ.map i y = 1 ↔ ∃ x : S.X i, Θ.map i x = y) :
198 Function.Injective (S.limMap Θ) ∧
199 Function.Surjective (T.limMap Ψ) ∧
200 Set.range (limMapMonoidHom (S := S) (T := T) Θ hΘ_one hΘ_mul) =
201 (MonoidHom.ker
202 (limMapMonoidHom (S := T) (T := U) Ψ hΨ_one hΨ_mul) : Set T.inverseLimit) := by
203 have hinj : Function.Injective (S.limMap Θ) :=
204 InverseSystems.InverseSystem.injective_limMap (S := S) (T := T) Θ hΘinj
205 have hsurj : Function.Surjective (T.limMap Ψ) :=
206 InverseSystems.InverseSystem.surjective_limMap (S := T) (T := U) hdir Ψ hΨsurj
207 have hcomp_lim :=
208 limMapMonoidHom_comp_eq_one (S := S) (T := T) (U := U)
209 hΘ_one hΘ_mul hΨ_one hΨ_mul hcomp
210 refine ⟨hinj, hsurj, ?_⟩
211 ext y
212 constructor
213 · rintro ⟨x, rfl⟩
214 change limMapMonoidHom (S := T) (T := U) Ψ hΨ_one hΨ_mul (S.limMap Θ x) = 1
215 simpa [Function.comp, limMapMonoidHom] using congrFun hcomp_lim x
216 · intro hy
217 have hy' :
218 limMapMonoidHom (S := T) (T := U) Ψ hΨ_one hΨ_mul y = 1 := by
219 simpa [MonoidHom.mem_ker] using hy
220 have hycoord :
221 ∀ i, Ψ.map i (T.projection i y) = 1 := by
222 intro i
223 have hpi :=
224 congrArg (fun z : U.inverseLimit => U.projection i z) hy'
225 simpa [limMapMonoidHom, InverseSystems.InverseSystem.limMap] using hpi
226 choose x hx using fun i => (hexact i (T.projection i y)).1 (hycoord i)
227 let xlim : S.inverseLimit := ⟨x, by
228 intro i j hij
229 apply hΘinj i
230 calc
231 Θ.map i (S.map hij (x j))
232 = T.map hij (Θ.map j (x j)) := by
233 exact (congrFun (Θ.comm hij) (x j)).symm
234 _ = T.map hij (T.projection j y) := by rw [hx j]
235 _ = T.projection i y := T.projection_compatible y i j hij
236 _ = Θ.map i (x i) := (hx i).symm⟩
237 refine ⟨xlim, ?_⟩
238 apply T.ext
239 intro i
240 exact hx i
242end InverseSystems.InverseSystem
244end ProCGroups