ProCGroups/ProC/Quotients/DescendingClosedSubgroupQuotients.lean

1import ProCGroups.ProC.Quotients.OpenSubgroupSections

3/-

4PUBLIC_PAGE_SNAPSHOT

5generated_at: 2026-05-27T09:47:29+09:00

6lean_source: lean4/ProCGroups/ProC/Quotients/DescendingClosedSubgroupQuotients.lean

7translation_root: data/translation

8purpose: identifies the local data snapshot used to build pages/

9placement: after imports, never before imports

10-/

11/-!

12# Pro-C groups and open normal quotients

14Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.

15-/

17open Set

18open scoped Topology Pointwise

20namespace ProCGroups.ProC

22universe u v

24open InverseSystems

26variable {I : Type v} [Preorder I] [Nonempty I]

27variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

29/-- The infimum of a family of closed subgroups, repackaged as a `ClosedSubgroup`. -/

30def closedSubgroup_sInf (L : I → ClosedSubgroup G) : ClosedSubgroup G where

31 toSubgroup := iInf fun i => (L i : Subgroup G)

32 isClosed' := by

33 convert isClosed_iInter fun i => (L i).isClosed' using 1

34 ext x

35 simp only [Subsemigroup.mem_carrier, Submonoid.mem_toSubsemigroup, Subgroup.mem_toSubmonoid,

36 Subgroup.mem_iInf, mem_iInter]

38/-- The infimum subgroup is contained in each term of the family. -/

39theorem closedSubgroup_sInf_le {I : Type v} {G : Type u} [Group G] [TopologicalSpace G]

40 (L : I → ClosedSubgroup G) (i : I) :

41 (closedSubgroup_sInf L : Subgroup G) ≤ (L i : Subgroup G) := by

42 exact iInf_le _ i

44/-- The inverse system of left quotient spaces attached to a decreasing family of closed

45subgroups. -/

46def descendingClosedSubgroupSystem (L : I → ClosedSubgroup G)

47 (hL : ∀ {i j}, i ≤ j → (L j : Subgroup G) ≤ (L i : Subgroup G)) :

48 InverseSystems.InverseSystem (I := I) where

49 X i := G ⧸ (L i : Subgroup G)

50 topologicalSpace i := inferInstance

51 map := fun {i j} hij =>

52 leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij)

53 continuous_map := by

54 intro i j hij

55 exact continuous_leftQuotientProjection

56 (K := (L j : Subgroup G)) (H := (L i : Subgroup G)) (hL hij)

57 map_id := by

58 intro i

59 exact leftQuotientProjection_id (K := (L i : Subgroup G))

60 map_comp := by

61 intro i j k hij hjk

62 exact

63 leftQuotientProjection_comp

64 (K := (L k : Subgroup G)) (H := (L j : Subgroup G)) (L := (L i : Subgroup G))

65 (hL hjk) (hL hij)

67/-- A compatible family of maps into a decreasing family of left quotient spaces lifts uniquely to

68the quotient by the infimum subgroup. -/

69theorem exists_continuous_leftQuotient_lift_of_directed

70 (hG : IsProfiniteGroup G) (L : I → ClosedSubgroup G)

71 (hL : ∀ {i j}, i ≤ j → (L j : Subgroup G) ≤ (L i : Subgroup G))

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

73 {Y : Type v} [TopologicalSpace Y]

74 (η : ∀ i, Y → G ⧸ (L i : Subgroup G))

75 (hηcont : ∀ i, Continuous (η i))

76 (hηcompat : ∀ {i j} (hij : i ≤ j),

77 leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij) ∘ η j = η i)

78 (y0 : Y)

79 (hηone : ∀ i, η i y0 = QuotientGroup.mk (s := (L i : Subgroup G)) (1 : G)) :

80 ∃ ηinf : Y → G ⧸ ((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G),

81 Continuous ηinf ∧

82 (∀ i,

83 leftQuotientProjection

84 (((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G))

85 (L i : Subgroup G)

86 (closedSubgroup_sInf_le (L := L) i) ∘ ηinf = η i) ∧

87 ηinf y0 =

88 QuotientGroup.mk (s := (((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G)))

89 (1 : G) := by

90 classical

91 let Linf : ClosedSubgroup G := closedSubgroup_sInf L

92 let S : InverseSystems.InverseSystem (I := I) := descendingClosedSubgroupSystem L hL

93 letI : CompactSpace G := IsProfiniteGroup.compactSpace hG

94 letI : T2Space G := IsProfiniteGroup.t2Space hG

95 letI : IsClosed (((Linf : ClosedSubgroup G) : Subgroup G) : Set G) := Linf.isClosed'

96 letI : ∀ i, IsClosed (((L i : ClosedSubgroup G) : Subgroup G) : Set G) := fun i => (L i).isClosed'

97 letI : ∀ i, T2Space (S.X i) := fun i => by

98 change T2Space (G ⧸ (L i : Subgroup G))

99 infer_instance

100 let ψ : ∀ i, G ⧸ ((Linf : ClosedSubgroup G) : Subgroup G) → S.X i := fun i =>

101 leftQuotientProjection

102 (((Linf : ClosedSubgroup G) : Subgroup G))

103 (L i : Subgroup G)

104 (closedSubgroup_sInf_le (L := L) i)

105 have hψcont : ∀ i, Continuous (ψ i) := by

106 intro i

107 exact continuous_leftQuotientProjection

108 (K := (((Linf : ClosedSubgroup G) : Subgroup G)))

109 (H := (L i : Subgroup G))

110 (closedSubgroup_sInf_le (L := L) i)

111 have hψcompat : S.CompatibleMaps ψ := by

112 intro i j hij

113 convert

114 (leftQuotientProjection_comp

115 (K := (((Linf : ClosedSubgroup G) : Subgroup G)))

116 (H := (L j : Subgroup G))

117 (L := (L i : Subgroup G))

118 (closedSubgroup_sInf_le (L := L) j) (hL hij)) using 1

119 let φ : G ⧸ ((Linf : ClosedSubgroup G) : Subgroup G) → S.inverseLimit :=

120 S.inverseLimitLift ψ hψcompat

121 have hφcont : Continuous φ := S.continuous_inverseLimitLift ψ hψcont hψcompat

122 have hψsurj : ∀ i, Function.Surjective (ψ i) := by

123 intro i

124 exact surjective_leftQuotientProjection

125 (K := (((Linf : ClosedSubgroup G) : Subgroup G)))

126 (H := (L i : Subgroup G))

127 (closedSubgroup_sInf_le (L := L) i)

128 have hφsurj : Function.Surjective φ :=

129 S.surjective_inverseLimitLift ψ hψcont hψcompat hψsurj hdir

130 have hφinj : Function.Injective φ := by

131 intro x y hxy

132 rcases Quotient.exists_rep x with ⟨gx, rfl⟩

133 rcases Quotient.exists_rep y with ⟨gy, rfl⟩

134 apply QuotientGroup.eq.2

135 have hcoord :

136 ∀ i, gx⁻¹ * gy ∈ (L i : Subgroup G) := by

137 intro i

138 have hi : ψ i (QuotientGroup.mk (s := (((Linf : ClosedSubgroup G) : Subgroup G))) gx) =

139 ψ i (QuotientGroup.mk (s := (((Linf : ClosedSubgroup G) : Subgroup G))) gy) := by

140 exact congrArg (fun z : S.inverseLimit => S.projection i z) hxy

141 exact QuotientGroup.eq.1 hi

142 change gx⁻¹ * gy ∈ iInf fun i => (L i : Subgroup G)

143 rw [Subgroup.mem_iInf]

144 exact hcoord

145 let eTop : G ⧸ ((Linf : ClosedSubgroup G) : Subgroup G) ≃ₜ S.inverseLimit :=

146 hφcont.homeoOfBijectiveCompactToT2 ⟨hφinj, hφsurj⟩

147 let ηinf : Y → G ⧸ ((Linf : ClosedSubgroup G) : Subgroup G) :=

148 eTop.symm ∘ S.inverseLimitLift η (by

149 intro i j hij

150 simpa only [S, descendingClosedSubgroupSystem, Function.comp] using hηcompat hij)

151 have hηinf_continuous : Continuous ηinf := by

152 exact eTop.continuous_invFun.comp <| S.continuous_inverseLimitLift η hηcont <| by

153 intro i j hij

154 simpa only [S, descendingClosedSubgroupSystem, Function.comp] using hηcompat hij

155 have hηinf_fac :

156 ∀ i,

157 leftQuotientProjection

158 (((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G))

159 (L i : Subgroup G)

160 (closedSubgroup_sInf_le (L := L) i) ∘ ηinf = η i := by

161 intro i

162 funext y

163 have hfac :=

164 congrFun (S.projection_comp_inverseLimitLift η

165 (by

166 intro i j hij

167 simpa only [S, descendingClosedSubgroupSystem, Function.comp] using hηcompat hij) i) y

168 have hcoord :

169 S.projection i (eTop (ηinf y)) = η i y := by

170 simpa [ηinf, Function.comp] using hfac

171 exact hcoord

172 have hηinf_one :

173 ηinf y0 =

174 QuotientGroup.mk (s := (((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G)))

175 (1 : G) := by

176 apply eTop.injective

177 apply S.ext

178 intro i

179 have hy0 := congrFun (hηinf_fac i) y0

180 change leftQuotientProjection

181 (((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G))

182 (L i : Subgroup G)

183 (closedSubgroup_sInf_le (L := L) i) (ηinf y0) =

184 leftQuotientProjection

185 (((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G))

186 (L i : Subgroup G)

187 (closedSubgroup_sInf_le (L := L) i)

188 (QuotientGroup.mk

189 (s := (((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G))) (1 : G))

190 simpa [hηone i]

191 using hy0

192 exact ⟨ηinf, hηinf_continuous, hηinf_fac, hηinf_one⟩

193

194end ProCGroups.ProC