Source: ProCGroups.InverseSystems.Exactness

1import Mathlib.Topology.Algebra.ContinuousMonoidHom

2import ProCGroups.InverseSystems.CompatibilityAndSurjectivity

4/-!

5# Exact sequences of group-valued inverse systems

7This module bundles morphisms whose stage maps are group homomorphisms and constructs the

8induced homomorphisms on inverse limits. For compact Hausdorff directed systems with surjective

9transitions, it lifts stagewise kernel-image exactness to exactness of the inverse-limit maps.

10-/

12universe u v

14namespace ProCGroups

16namespace InverseSystems.InverseSystem

18variable {I : Type u} [Preorder I]

19variable {S T U : InverseSystems.InverseSystem (I := I)}

20attribute [local instance] InverseSystems.InverseSystem.topologicalSpace

21/-- Use the topology stored by the source inverse system at stage `i`. -/

22instance instTopologicalSpaceS (i : I) : TopologicalSpace (S.X i) := S.topologicalSpace i

23/-- Use the topology stored by the middle inverse system at stage `i`. -/

24instance instTopologicalSpaceT (i : I) : TopologicalSpace (T.X i) := T.topologicalSpace i

25/-- Use the topology stored by the target inverse system at stage `i`. -/

26instance instTopologicalSpaceU (i : I) : TopologicalSpace (U.X i) := U.topologicalSpace i

27variable [∀ i, Group (S.X i)] [∀ i, Group (T.X i)] [∀ i, Group (U.X i)]

29/-- A morphism of group-valued inverse systems with homomorphism laws bundled componentwise. -/

30structure GroupMorphism (S T : InverseSystems.InverseSystem (I := I))

31 [∀ i, Group (S.X i)] [∀ i, Group (T.X i)] extends S.Morphism T where

32 /-- Each stage map sends the source identity to the target identity. -/

33 map_one' : ∀ i, map i 1 = 1

34 /-- Each stage map preserves multiplication and therefore defines a group homomorphism. -/

35 map_mul' : ∀ i (x y : S.X i), map i (x * y) = map i x * map i y

37namespace GroupMorphism

39/-- A bundled group morphism built from componentwise continuous monoid homomorphisms. -/

40def ofContinuousMonoidHom

41 (φ : ∀ i, S.X i →ₜ* T.X i)

42 (hcomm : ∀ {i j : I} (hij : i ≤ j),

43 T.map hij ∘ φ j = φ i ∘ S.map hij) :

44 GroupMorphism S T where

45 map := fun i => φ i

46 continuous_map := fun i => (φ i).continuous_toFun

47 comm := hcomm

48 map_one' := fun i => (φ i).map_one

49 map_mul' := fun i => (φ i).map_mul

51/--

52The group-system morphism built from continuous monoid homomorphisms has the prescribed stage

53maps.

54-/

55@[simp] theorem ofContinuousMonoidHom_map

56 (φ : ∀ i, S.X i →ₜ* T.X i)

57 (hcomm : ∀ {i j : I} (hij : i ≤ j),

58 T.map hij ∘ φ j = φ i ∘ S.map hij)

59 (i : I) (x : S.X i) :

60 (ofContinuousMonoidHom (S := S) (T := T) φ hcomm).map i x = φ i x :=

61 rfl

63/-- The identity morphism of an inverse system. -/

64def id (S : InverseSystems.InverseSystem (I := I))

65 [∀ i, Group (S.X i)] :

66 GroupMorphism S S where

67 toMorphism := InverseSystems.InverseSystem.Morphism.id S

68 map_one' := fun _ => rfl

69 map_mul' := fun _ _ _ => rfl

71/-- The identity group-system morphism acts as the identity on each stage. -/

72@[simp] theorem id_apply

73 (i : I) (x : S.X i) :

74 (id S).map i x = x :=

75 rfl

77/-- Group-valued inverse-system morphisms compose stagewise, preserving their homomorphism laws. -/

78def comp (Ψ : GroupMorphism T U) (Θ : GroupMorphism S T) :

79 GroupMorphism S U where

80 toMorphism := InverseSystems.InverseSystem.Morphism.comp Ψ.toMorphism Θ.toMorphism

81 map_one' := by

82 intro i

83 simp only [Morphism.comp_apply, Θ.map_one', Ψ.map_one']

84 map_mul' := by

85 intro i x y

86 simp only [Morphism.comp_apply, Θ.map_mul', Ψ.map_mul']

88/-- At each stage, the composite group morphism applies `Θ` first and then `Ψ`. -/

89@[simp] theorem comp_apply (Ψ : GroupMorphism T U) (Θ : GroupMorphism S T)

90 (i : I) (x : S.X i) :

91 (comp Ψ Θ).map i x = Ψ.map i (Θ.map i x) :=

92 rfl

94end GroupMorphism

96/-- A morphism of group-valued inverse systems induces a homomorphism on inverse limits. -/

97def limMapMonoidHom (Θ : S.Morphism T)

98 (hΘ_one : ∀ i, Θ.map i 1 = 1)

99 (hΘ_mul : ∀ i (x y : S.X i), Θ.map i (x * y) = Θ.map i x * Θ.map i y)

100 [InverseSystems.IsGroupSystem S] [InverseSystems.IsGroupSystem T] :

101 S.inverseLimit →* T.inverseLimit where

102 toFun := S.limMap Θ

103 map_one' := by

104 apply T.ext

105 intro i

106 have hpi := congrFun (S.π_comp_limMap (Θ := Θ) i) (1 : S.inverseLimit)

107 calc

108 T.projection i (S.limMap Θ 1) = Θ.map i (S.projection i 1) := by

109 simpa [Function.comp] using hpi

110 _ = Θ.map i 1 := by rfl

111 _ = 1 := hΘ_one i

112 map_mul' := by

113 intro x y

114 apply T.ext

115 intro i

116 have hxy := congrFun (S.π_comp_limMap (Θ := Θ) i) (x * y)

117 have hx := congrFun (S.π_comp_limMap (Θ := Θ) i) x

118 have hy := congrFun (S.π_comp_limMap (Θ := Θ) i) y

119 have hx' : T.projection i (S.limMap Θ x) = Θ.map i (S.projection i x) := by

120 simpa [Function.comp] using hx

121 have hy' : T.projection i (S.limMap Θ y) = Θ.map i (S.projection i y) := by

122 simpa [Function.comp] using hy

123 calc

124 T.projection i (S.limMap Θ (x * y)) = Θ.map i (S.projection i (x * y)) := by

125 simpa [Function.comp] using hxy

126 _ = Θ.map i (S.projection i x * S.projection i y) := by rfl

127 _ = Θ.map i (S.projection i x) * Θ.map i (S.projection i y) :=

128 hΘ_mul i (S.projection i x) (S.projection i y)

129 _ = T.projection i (S.limMap Θ x) * T.projection i (S.limMap Θ y) := by

130 rw [← hx', ← hy']

131

132/--

133Bundled group morphisms induce homomorphisms on inverse limits without repeating the

134componentwise homomorphism laws.

135-/

136def GroupMorphism.limMapMonoidHom (Θ : GroupMorphism S T)

137 [InverseSystems.IsGroupSystem S] [InverseSystems.IsGroupSystem T] :

138 S.inverseLimit →* T.inverseLimit :=

139 ProCGroups.InverseSystems.InverseSystem.limMapMonoidHom

140 (S := S) (T := T) Θ.toMorphism Θ.map_one' Θ.map_mul'

141

142/--

143The inverse-limit homomorphism evaluates at each stage by applying the corresponding stage

144homomorphism after projection.

145-/

146@[simp] theorem GroupMorphism.limMapMonoidHom_apply_π

147 (Θ : GroupMorphism S T)

148 [InverseSystems.IsGroupSystem S] [InverseSystems.IsGroupSystem T]

149 (i : I) (x : S.inverseLimit) :

150 T.projection i (Θ.limMapMonoidHom x) = Θ.map i (S.projection i x) := by

151 simpa [GroupMorphism.limMapMonoidHom,

152 ProCGroups.InverseSystems.InverseSystem.limMapMonoidHom] using

153 congrFun (S.π_comp_limMap (Θ := Θ.toMorphism) i) x

154

155/--

156If the componentwise composite \(\Psi_i \circ \Theta_i\) is trivial, then the induced morphisms

157on inverse limits also compose to the trivial homomorphism. This isolates the only

158non-mathematical part of the range \(\subseteq\) kernel direction.

159-/

160theorem limMapMonoidHom_comp_eq_one

161 {Θ : S.Morphism T} {Ψ : T.Morphism U}

162 [InverseSystems.IsGroupSystem S] [InverseSystems.IsGroupSystem T]

163 [InverseSystems.IsGroupSystem U]

164 (hΘ_one : ∀ i, Θ.map i 1 = 1)

165 (hΘ_mul : ∀ i (x y : S.X i), Θ.map i (x * y) = Θ.map i x * Θ.map i y)

166 (hΨ_one : ∀ i, Ψ.map i 1 = 1)

167 (hΨ_mul : ∀ i (x y : T.X i), Ψ.map i (x * y) = Ψ.map i x * Ψ.map i y)

168 (hcomp : ∀ i, Ψ.map i ∘ Θ.map i = fun _ => 1) :

169 limMapMonoidHom (S := T) (T := U) Ψ hΨ_one hΨ_mul ∘

170 limMapMonoidHom (S := S) (T := T) Θ hΘ_one hΘ_mul =

171 fun _ => 1 := by

172 funext x

173 apply U.ext

174 intro i

175 have hπΘ := congrFun (S.π_comp_limMap (Θ := Θ) i) x

176 have hπΨ := congrFun (T.π_comp_limMap (Θ := Ψ) i) (S.limMap Θ x)

177 have hπΘ' : T.projection i (S.limMap Θ x) = Θ.map i (S.projection i x) := by

178 simpa [Function.comp] using hπΘ

179 have hπΨ' :

180 U.projection i (T.limMap Ψ (S.limMap Θ x)) = Ψ.map i (T.projection i (S.limMap Θ x)) := by

181 simpa [Function.comp] using hπΨ

182 have hcomp' : Ψ.map i (Θ.map i (S.projection i x)) = 1 := by

183 simpa [Function.comp] using congrFun (hcomp i) (S.projection i x)

184 calc

185 U.projection i

186 ((limMapMonoidHom (S := T) (T := U) Ψ hΨ_one hΨ_mul)

187 ((limMapMonoidHom (S := S) (T := T) Θ hΘ_one hΘ_mul) x))

188 = Ψ.map i (T.projection i (S.limMap Θ x)) := by

189 simpa [limMapMonoidHom] using hπΨ'

190 _ = Ψ.map i (Θ.map i (S.projection i x)) := by rw [hπΘ']

191 _ = 1 := hcomp'

192 _ = U.projection i (1 : U.inverseLimit) := rfl

193

194/--

195Inverse limits preserve short exact sequences of profinite groups when taken over a common

196directed index category.

197-/

198theorem limMap_exact

199 [∀ i, CompactSpace (T.X i)] [∀ i, T2Space (T.X i)] [∀ i, T2Space (U.X i)]

200 [InverseSystems.IsGroupSystem S] [InverseSystems.IsGroupSystem T]

201 [InverseSystems.IsGroupSystem U]

202 {Θ : S.Morphism T} {Ψ : T.Morphism U}

203 (hΘ_one : ∀ i, Θ.map i 1 = 1)

204 (hΘ_mul : ∀ i (x y : S.X i), Θ.map i (x * y) = Θ.map i x * Θ.map i y)

205 (hΨ_one : ∀ i, Ψ.map i 1 = 1)

206 (hΨ_mul : ∀ i (x y : T.X i), Ψ.map i (x * y) = Ψ.map i x * Ψ.map i y)

207 (hdir : Directed (· ≤ ·) (id : I → I))

208 (hΘinj : ∀ i, Function.Injective (Θ.map i))

209 (hΨsurj : ∀ i, Function.Surjective (Ψ.map i))

210 (hcomp : ∀ i, Ψ.map i ∘ Θ.map i = fun _ => 1)

211 (hexact : ∀ i, ∀ y : T.X i, Ψ.map i y = 1 ↔ ∃ x : S.X i, Θ.map i x = y) :

212 Function.Injective (S.limMap Θ) ∧

213 Function.Surjective (T.limMap Ψ) ∧

214 Set.range (limMapMonoidHom (S := S) (T := T) Θ hΘ_one hΘ_mul) =

215 (MonoidHom.ker

216 (limMapMonoidHom (S := T) (T := U) Ψ hΨ_one hΨ_mul) : Set T.inverseLimit) := by

217 have hinj : Function.Injective (S.limMap Θ) :=

218 InverseSystems.InverseSystem.injective_limMap (S := S) (T := T) Θ hΘinj

219 have hsurj : Function.Surjective (T.limMap Ψ) :=

220 InverseSystems.InverseSystem.surjective_limMap (S := T) (T := U) hdir Ψ hΨsurj

221 have hcomp_lim :=

222 limMapMonoidHom_comp_eq_one (S := S) (T := T) (U := U)

223 hΘ_one hΘ_mul hΨ_one hΨ_mul hcomp

224 refine ⟨hinj, hsurj, ?_⟩

225 ext y

226 constructor

227 · rintro ⟨x, rfl⟩

228 change limMapMonoidHom (S := T) (T := U) Ψ hΨ_one hΨ_mul (S.limMap Θ x) = 1

229 simpa [Function.comp, limMapMonoidHom] using congrFun hcomp_lim x

230 · intro hy

231 have hy' :

232 limMapMonoidHom (S := T) (T := U) Ψ hΨ_one hΨ_mul y = 1 := by

233 simpa [MonoidHom.mem_ker] using hy

234 have hycoord :

235 ∀ i, Ψ.map i (T.projection i y) = 1 := by

236 intro i

237 calc

238 Ψ.map i (T.projection i y) =

239 U.projection i

240 (limMapMonoidHom (S := T) (T := U) Ψ hΨ_one hΨ_mul y) := by

241 symm

242 exact GroupMorphism.limMapMonoidHom_apply_π

243 (Θ :=

244 { toMorphism := Ψ

245 map_one' := hΨ_one

246 map_mul' := hΨ_mul }) i y

247 _ = U.projection i 1 := congrArg (fun z : U.inverseLimit => U.projection i z) hy'

248 _ = 1 := rfl

249 choose x hx using fun i => (hexact i (T.projection i y)).1 (hycoord i)

250 let xlim : S.inverseLimit := ⟨x, by

251 intro i j hij

252 apply hΘinj i

253 calc

254 Θ.map i (S.map hij (x j))

255 = T.map hij (Θ.map j (x j)) := by

256 exact (congrFun (Θ.comm hij) (x j)).symm

257 _ = T.map hij (T.projection j y) := by rw [hx j]

258 _ = T.projection i y := T.projection_compatible y i j hij

259 _ = Θ.map i (x i) := (hx i).symm⟩

260 refine ⟨xlim, ?_⟩

261 apply T.ext

262 intro i

263 exact hx i

264

265end InverseSystems.InverseSystem

266

267end ProCGroups