FenchelNielsenZomorrodian/Discrete/Singerman/CyclicQuotientActions.lean

1import ReidemeisterSchreier.Discrete.Presentations.KernelQuotient

2import FenchelNielsenZomorrodian.Discrete.Singerman.ReidemeisterSchreier

4/-

5PUBLIC_PAGE_SNAPSHOT

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

7lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Singerman/CyclicQuotientActions.lean

8translation_root: data/translation

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

10placement: after imports, never before imports

11-/

12/-!

13# Singerman/Reidemeister-Schreier bridge

15Cyclic quotient actions, cyclic product identities, Schreier kernel computations, free-group word identities, and kernel transport for the compact Fuchsian proof.

16-/

18open scoped Pointwise

19namespace FenchelNielsen

20universe u

21noncomputable def cyclicQuotientRightRep

22 {G : Type*} [Group G] {N : ℕ}

23 (φ : G →* Multiplicative (ZMod N)) (t : G) :

24 Quotient (QuotientGroup.rightRel φ.ker) → G :=

25 Quotient.lift

26 (fun g => t ^ (Multiplicative.toAdd (φ g)).val)

27 (by

28 intro a b hab

29 have hab' : QuotientGroup.rightRel φ.ker a b := hab

30 rw [QuotientGroup.rightRel_apply] at hab'

31 have habφ : φ a = φ b := by

32 have habφ' : φ b = φ a := by

33 apply eq_of_mul_inv_eq_one

34 simpa [map_mul, map_inv] using MonoidHom.mem_ker.mp hab'

35 exact habφ'.symm

36 have hval :

37 (Multiplicative.toAdd (φ a)).val = (Multiplicative.toAdd (φ b)).val := by

38 exact congrArg ZMod.val (congrArg Multiplicative.toAdd habφ)

39 simp only [hval])

40@[simp 900] theorem cyclicQuotientRightRep_spec

41 {G : Type*} [Group G] {N : ℕ} [NeZero N]

42 (φ : G →* Multiplicative (ZMod N)) (t : G)

43 (ht : φ t = Multiplicative.ofAdd (1 : ZMod N))

44 (q : Quotient (QuotientGroup.rightRel φ.ker)) :

45 Quotient.mk'' (cyclicQuotientRightRep φ t q) = q := by

46 refine Quotient.inductionOn' q ?_

47 intro g

48 apply Quotient.sound'

49 rw [QuotientGroup.rightRel_apply]

50 rw [MonoidHom.mem_ker]

51 have hk :

52 Multiplicative.ofAdd (((Multiplicative.toAdd (φ g)).val : ℕ) : ZMod N) = φ g := by

53 exact congrArg Multiplicative.ofAdd

54 (ZMod.natCast_zmod_val (Multiplicative.toAdd (φ g)))

55 rw [show cyclicQuotientRightRep φ t (Quotient.mk'' g) =

56 t ^ (Multiplicative.toAdd (φ g)).val by rfl]

57 rw [map_mul, MonoidHom.map_inv, MonoidHom.map_pow, ← hk, ht]

58 apply (Multiplicative.toAdd : Multiplicative (ZMod N) ≃ ZMod N).injective

59 simp only [ZMod.natCast_val, ZMod.cast_id', id_eq, ofAdd_toAdd, toAdd_mul, toAdd_inv, toAdd_pow, toAdd_ofAdd,

60 nsmul_eq_mul, mul_one, add_neg_cancel, toAdd_one]

61/-- The cyclic right representative set complements the kernel. -/

62theorem ker_isComplement_range_cyclicQuotientRightRep

63 {G : Type*} [Group G] {N : ℕ} [NeZero N]

64 (φ : G →* Multiplicative (ZMod N)) (t : G)

65 (ht : φ t = Multiplicative.ofAdd (1 : ZMod N)) :

66 Subgroup.IsComplement (φ.ker : Set G) (Set.range (cyclicQuotientRightRep φ t)) :=

67 Subgroup.isComplement_range_right (cyclicQuotientRightRep_spec φ t ht)

68/-- The representative set of `cyclicQuotientRightRep` contains the identity. -/

69theorem one_mem_range_cyclicQuotientRightRep

70 {G : Type*} [Group G] {N : ℕ}

71 (φ : G →* Multiplicative (ZMod N)) (t : G) :

72 (1 : G) ∈ Set.range (cyclicQuotientRightRep φ t) := by

73 refine ⟨Quotient.mk'' (1 : G), ?_⟩

74 simp only [cyclicQuotientRightRep, Quotient.lift_mk, map_one, toAdd_one, ZMod.val_zero, pow_zero]

75/-- Powers below the modulus of the distinguished free generator lie in the representative set. -/

76theorem generatorPower_mem_range_cyclicQuotientRightRep

77 {X : Type*} {N : ℕ} [NeZero N]

78 (φ : FreeGroup X →* Multiplicative (ZMod N)) (x : X)

79 (hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N))

80 {m : ℕ} (hm : m < N) :

81 (FreeGroup.of x) ^ m ∈ Set.range (cyclicQuotientRightRep φ (FreeGroup.of x)) := by

82 classical

83 refine ⟨Quotient.mk'' ((FreeGroup.of x) ^ m), ?_⟩

84 have hφm : φ ((FreeGroup.of x) ^ m) = Multiplicative.ofAdd ((m : ℕ) : ZMod N) := by

85 rw [map_pow, hx]

86 apply (Multiplicative.toAdd : Multiplicative (ZMod N) ≃ ZMod N).injective

87 simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, mul_one]

88 have hval : (Multiplicative.toAdd (φ ((FreeGroup.of x) ^ m))).val = m := by

89 rw [hφm]

90 simpa using (ZMod.val_natCast_of_lt hm)

91 change (FreeGroup.of x) ^ (Multiplicative.toAdd (φ ((FreeGroup.of x) ^ m))).val =

92 (FreeGroup.of x) ^ m

93 rw [hval]

94theorem mem_range_cyclicQuotientRightRep_iff_generatorPower

95 {X : Type*} {N : ℕ} [NeZero N]

96 (φ : FreeGroup X →* Multiplicative (ZMod N)) {x : X}

97 (hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N))

98 {t : FreeGroup X} :

99 t ∈ Set.range (cyclicQuotientRightRep φ (FreeGroup.of x)) ↔

100 ∃ k : Fin N, t = (FreeGroup.of x) ^ k.val := by

101 constructor

102 · intro ht

103 rcases ht with ⟨q, rfl⟩

104 refine Quotient.inductionOn' q ?_

105 intro g

106 exact

107 ⟨⟨(Multiplicative.toAdd (φ g)).val,

108 ZMod.val_lt (Multiplicative.toAdd (φ g))⟩, rfl⟩

109 · rintro ⟨k, rfl⟩

110 exact generatorPower_mem_range_cyclicQuotientRightRep φ x hx k.isLt

111theorem cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator

112 {X : Type*} [DecidableEq X] {N : ℕ} [NeZero N]

113 (φ : FreeGroup X →* Multiplicative (ZMod N)) (x : X)

114 (hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N)) :

115 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))

116 IsRightSchreierTransversal φ.ker T := by

117 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))

118 refine ⟨?_, ?_, ?_⟩

119 · simpa [T] using

120 ker_isComplement_range_cyclicQuotientRightRep φ (FreeGroup.of x) hx

121 · simpa [T] using

122 one_mem_range_cyclicQuotientRightRep φ (FreeGroup.of x)

123 · intro t ht

124 rcases ht with ⟨q, rfl⟩

125 refine Quotient.inductionOn' q ?_

126 intro g u hu

127 have hrep :

128 cyclicQuotientRightRep φ (FreeGroup.of x) (Quotient.mk'' g) =

129 (FreeGroup.of x) ^ (Multiplicative.toAdd (φ g)).val := rfl

130 rw [hrep] at hu

131 rcases hu with ⟨m, hm, rfl⟩

132 have hm' : m ≤ (Multiplicative.toAdd (φ g)).val := by

133 simpa [FreeGroup.toWord_of_pow, List.length_replicate] using hm

134 have hmlt : m < N := lt_of_le_of_lt hm' (ZMod.val_lt (Multiplicative.toAdd (φ g)))

135 rw [FreeGroup.toWord_of_pow, List.take_replicate, min_eq_left hm',

136 ← FreeGroup.toWord_of_pow, FreeGroup.mk_toWord]

137 exact generatorPower_mem_range_cyclicQuotientRightRep φ x hx hmlt

138noncomputable def freeGroupKernelSchreierBasisEquivOfCyclicQuotientGenerator

139 {X : Type*} [DecidableEq X] {N : ℕ} [NeZero N]

140 (φ : FreeGroup X →* Multiplicative (ZMod N)) (x : X)

141 (hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N)) :

142 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))

143 let hT : IsRightSchreierTransversal φ.ker T :=

144 cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx

145 FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker := by

146 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))

147 let hT : IsRightSchreierTransversal φ.ker T :=

148 cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx

149 exact schreierGeneratorInverseBasisEquiv (X := X) hT

150@[simp 900] theorem freeGroupKernelSchreierBasisEquivOfCyclicQuotientGenerator_of

151 {X : Type*} [DecidableEq X] {N : ℕ} [NeZero N]

152 (φ : FreeGroup X →* Multiplicative (ZMod N)) (x : X)

153 (hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N)) :

154 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))

155 let hT : IsRightSchreierTransversal φ.ker T :=

156 cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx

157 ∀ z : ↥(schreierGeneratorSet hT),

158 freeGroupKernelSchreierBasisEquivOfCyclicQuotientGenerator φ x hx (FreeGroup.of z) =

159 (z : φ.ker)⁻¹ := by

160 classical

161 dsimp

162 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))

163 let hT : IsRightSchreierTransversal φ.ker T :=

164 cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx

165 intro z

166 exact schreierGeneratorInverseBasisEquiv_of (X := X) hT z

167noncomputable def presentedFreeKernelCyclicSchreierRelatorQuotientEquivPresentedKernel

168 {X : Type*} [DecidableEq X] {N : ℕ} [NeZero N] {rels : Set (FreeGroup X)}

169 {f : X → Multiplicative (ZMod N)}

170 (hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1)

171 (x : X)

172 (hx : FreeGroup.lift f (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N)) :

173 let φ := FreeGroup.lift f

174 let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))

175 let hT : IsRightSchreierTransversal φ.ker T :=

176 cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx

177 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=

178 freeGroupKernelSchreierBasisEquivOfCyclicQuotientGenerator φ x hx

179 FreeGroup ↥(schreierGeneratorSet hT) ⧸

180 Subgroup.normalClosure

181 (ReidemeisterSchreier.Discrete.Presentations.freeGroupPullbackRelatorSet e

182 (ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet (f := f) (rels := rels) T)) ≃*

183 (PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker := by

184 classical

185 let φ : FreeGroup X →* Multiplicative (ZMod N) := FreeGroup.lift f

186 let T : Set (FreeGroup X) := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))

187 let hT : IsRightSchreierTransversal φ.ker T :=

188 cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx

189 let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=

190 freeGroupKernelSchreierBasisEquivOfCyclicQuotientGenerator φ x hx

191 simpa [φ, T, hT, e] using

192 ReidemeisterSchreier.Discrete.Presentations.presentedFreeKernelSchreierRelatorQuotientEquivPresentedKernel hrels hT.1 e

193end FenchelNielsen