FenchelNielsenZomorrodian/Profinite/SmoothQuotient.lean

1import FenchelNielsenZomorrodian.Profinite.TorsionFrontier

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/FenchelNielsenZomorrodian/Profinite/SmoothQuotient.lean

7translation_root: data/translation

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

9placement: after imports, never before imports

10-/

11/-!

12# Finite smooth quotients of profinite Fenchel groups

14Packages finite quotient maps whose inertia images have exactly the prescribed period and derives

15torsion-free kernels with bounded derived length.

16-/

18namespace FenchelNielsen

20universe u v

22open ProCGroups.FiniteStepSolvableQuotients

23open ProCGroups.ProC

25namespace ProfiniteFGroup

27/-- A finite smooth quotient of a profinite `F`-group.

29The datum is the profinite analogue of the finite smooth quotient data used on the discrete side:

30the target is finite and discrete, the quotient has derived length at most `m`, and each inertia

31generator maps to an element of exactly the prescribed period.

32-/

33structure ProfiniteSmoothQuotientData

34 (Δ : ProfiniteFGroup.{u}) (m : ℕ) where

35 Q : Type u

36 [group : Group Q]

37 [topologicalSpace : TopologicalSpace Q]

38 [discreteTopology : DiscreteTopology Q]

39 [isTopologicalGroup : IsTopologicalGroup Q]

40 [finite : Finite Q]

41 φ : Δ.carrier →ₜ* Q

42 derived_length : profiniteDerivedSeries Q m = ⊥

43 inertia_exact :

44 ∀ i : Fin Δ.signature.numPeriods,

45 orderOf (φ (Δ.inertia i)) = Δ.signature.periods i

47attribute [instance] ProfiniteSmoothQuotientData.group

48attribute [instance] ProfiniteSmoothQuotientData.topologicalSpace

49attribute [instance] ProfiniteSmoothQuotientData.discreteTopology

50attribute [instance] ProfiniteSmoothQuotientData.isTopologicalGroup

51attribute [instance] ProfiniteSmoothQuotientData.finite

53namespace ProfiniteSmoothQuotientData

55/-- The open normal kernel attached to a finite smooth quotient. -/

56def kernelOpenNormal {Δ : ProfiniteFGroup.{u}} {m : ℕ}

57 (D : ProfiniteSmoothQuotientData Δ m) :

58 OpenNormalSubgroup Δ.carrier :=

59 OpenNormalSubgroup.ker D.φ

61/-- Membership in the kernel open normal subgroup is equality to `1` after applying `φ`. -/

62@[simp] theorem mem_kernelOpenNormal

63 {Δ : ProfiniteFGroup.{u}} {m : ℕ}

64 {D : ProfiniteSmoothQuotientData Δ m} {x : Δ.carrier} :

65 x ∈ (D.kernelOpenNormal : Subgroup Δ.carrier) ↔ D.φ x = 1 := by

66 rfl

68/-- The `m`-th profinite derived subgroup is contained in the kernel of the quotient map. -/

69theorem topDerived_le_kernel

70 {Δ : ProfiniteFGroup.{u}} {m : ℕ}

71 (D : ProfiniteSmoothQuotientData Δ m) :

72 profiniteDerivedSeries Δ.carrier m ≤

73 (D.kernelOpenNormal : Subgroup Δ.carrier) := by

74 intro x hx

75 have hxImage :

76 D.φ x ∈ profiniteDerivedSeries D.Q m :=

77 topDerivedTop_le_comap (f := D.φ) (m := m) hx

78 have hxBot : D.φ x ∈ (⊥ : Subgroup D.Q) := by

79 simpa [D.derived_length] using hxImage

80 exact Subgroup.mem_bot.mp hxBot

82/-- The quotient by the kernel has derived length at most the quotient datum bound. -/

83theorem kernel_quotient_has_derivedLengthAtMost

84 {Δ : ProfiniteFGroup.{u}} {m : ℕ}

85 (D : ProfiniteSmoothQuotientData Δ m) :

86 ProfiniteOpenNormalQuotientHasDerivedLengthAtMost

87 Δ.carrier D.kernelOpenNormal m :=

88 ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.of_topDerived_le

89 D.kernelOpenNormal D.topDerived_le_kernel

91/-- The smooth quotient kernel avoids all nontrivial inertia powers. -/

92theorem kernel_avoidsNontrivialInertia

93 {Δ : ProfiniteFGroup.{u}} {m : ℕ}

94 (D : ProfiniteSmoothQuotientData Δ m) :

95 Δ.avoidsNontrivialInertia D.kernelOpenNormal := by

96 intro i n hn

97 have hφpow : D.φ (Δ.inertia i ^ n) = 1 := by

98 simpa using (mem_kernelOpenNormal (D := D)).1 hn

99 have hImagePow : D.φ (Δ.inertia i) ^ n = 1 := by

100 simpa [MonoidHom.map_zpow] using hφpow

101 have hdivImage : (orderOf (D.φ (Δ.inertia i)) : ℤ) ∣ n :=

102 orderOf_dvd_iff_zpow_eq_one.mpr hImagePow

103 have hdivSource : (orderOf (Δ.inertia i) : ℤ) ∣ n := by

104 rw [Δ.inertia_order i, ← D.inertia_exact i]

105 exact hdivImage

106 exact orderOf_dvd_iff_zpow_eq_one.mp hdivSource

107

108/-- The smooth quotient kernel is torsion-free. -/

109theorem kernel_torsionFree

110 {Δ : ProfiniteFGroup.{u}} {m : ℕ}

111 (D : ProfiniteSmoothQuotientData Δ m) :

112 ProfiniteOpenNormalSubgroupTorsionFree

113 Δ.carrier D.kernelOpenNormal :=

114 torsionFree_of_avoidsNontrivialInertia

115 Δ D.kernelOpenNormal D.kernel_avoidsNontrivialInertia

116

117/-- A smooth quotient datum gives a torsion-free open normal subgroup with bounded quotient. -/

118theorem has_torsionFreeOpenNormal_quotient_derivedLengthAtMost

119 {Δ : ProfiniteFGroup.{u}} {m : ℕ}

120 (D : ProfiniteSmoothQuotientData Δ m) :

121 HasTorsionFreeOpenNormalSubgroupQuotientDerivedLengthAtMost

122 Δ.carrier m :=

123 ⟨D.kernelOpenNormal, D.kernel_torsionFree,

124 D.kernel_quotient_has_derivedLengthAtMost⟩

125

126/-- The quotient derived-length bound is monotone in the target bound. -/

127theorem has_torsionFreeOpenNormal_quotient_derivedLength_le

128 {Δ : ProfiniteFGroup.{u}} {m n : ℕ}

129 (D : ProfiniteSmoothQuotientData Δ m) (hmn : m ≤ n) :

130 HasTorsionFreeOpenNormalSubgroupQuotientDerivedLengthAtMost

131 Δ.carrier n :=

132 HasTorsionFreeOpenNormalSubgroupQuotientDerivedLengthAtMost.mono

133 hmn D.has_torsionFreeOpenNormal_quotient_derivedLengthAtMost

134

135/-- Build profinite smooth quotient data from a finite target assignment satisfying the

136Fenchel-Nielsen presentation relations. -/

137noncomputable def ofPresentationLiftToFiniteOfRelations

138 (Δ : ProfiniteFGroup.{u}) {m : ℕ}

139 {A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A]

140 [IsTopologicalGroup A] [Finite A]

141 (χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)

142 (hTotal :

143 profiniteFenchelTotalRelation

144 (fun i => χ (ULift.up (ProfiniteFenchelGenerator.surfaceA i)))

145 (fun i => χ (ULift.up (ProfiniteFenchelGenerator.surfaceB i)))

146 (fun j => χ (ULift.up (ProfiniteFenchelGenerator.cusp j)))

147 (fun k => χ (ULift.up (ProfiniteFenchelGenerator.inertia k))) = 1)

148 (hPeriod :

149 ∀ k : Fin Δ.signature.numPeriods,

150 χ (ULift.up (ProfiniteFenchelGenerator.inertia k)) ^

151 Δ.signature.periods k = 1)

152 (hDerived : profiniteDerivedSeries A m = ⊥)

153 (hInertiaExact :

154 ∀ i : Fin Δ.signature.numPeriods,

155 orderOf (χ (ULift.up (ProfiniteFenchelGenerator.inertia i))) =

156 Δ.signature.periods i) :

157 ProfiniteSmoothQuotientData Δ m where

158 Q := A

159 φ := Δ.presentationLiftToFiniteOfRelations χ hTotal hPeriod

160 derived_length := hDerived

161 inertia_exact := by

162 intro i

163 simpa [presentationLiftToFiniteOfRelations] using hInertiaExact i

164

165/-- Build profinite smooth quotient data from a finite discrete target whose abstract derived

166series has the requested length. -/

167noncomputable def ofPresentationLiftToFiniteOfRelationsOfDerivedSeries

168 (Δ : ProfiniteFGroup.{u}) {m : ℕ}

169 {A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A]

170 [IsTopologicalGroup A] [Finite A]

171 (χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)

172 (hTotal :

173 profiniteFenchelTotalRelation

174 (fun i => χ (ULift.up (ProfiniteFenchelGenerator.surfaceA i)))

175 (fun i => χ (ULift.up (ProfiniteFenchelGenerator.surfaceB i)))

176 (fun j => χ (ULift.up (ProfiniteFenchelGenerator.cusp j)))

177 (fun k => χ (ULift.up (ProfiniteFenchelGenerator.inertia k))) = 1)

178 (hPeriod :

179 ∀ k : Fin Δ.signature.numPeriods,

180 χ (ULift.up (ProfiniteFenchelGenerator.inertia k)) ^

181 Δ.signature.periods k = 1)

182 (hDerived : derivedSeries A m = ⊥)

183 (hInertiaExact :

184 ∀ i : Fin Δ.signature.numPeriods,

185 orderOf (χ (ULift.up (ProfiniteFenchelGenerator.inertia i))) =

186 Δ.signature.periods i) :

187 ProfiniteSmoothQuotientData Δ m :=

188 ofPresentationLiftToFiniteOfRelations

189 Δ χ hTotal hPeriod

190 (by

191 rw [profiniteDerivedSeries_eq_derivedSeries_of_discrete]

192 exact hDerived)

193 hInertiaExact

194

195end ProfiniteSmoothQuotientData

196

197end ProfiniteFGroup

198

199end FenchelNielsen