ProCGroups/Presentations/SchreierTietze/Restricted.lean

1import ProCGroups.Presentations.SchreierTietze.Relators

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/ProCGroups/Presentations/SchreierTietze/Restricted.lean

7translation_root: data/translation

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

9placement: after imports, never before imports

10-/

11/-!

12# Profinite presentations

14Presentation-level API for profinite groups, finite quotients, relators, and Schreier-Tietze restrictions.

15-/

17noncomputable section

19open scoped Topology

21namespace ProCGroups.Presentations

23universe u v w

25section RestrictedPresentations

27variable {F G : Type u} [Group F] [Group G]

28variable [TopologicalSpace F] [TopologicalSpace G]

29variable [IsTopologicalGroup F] [IsTopologicalGroup G]

31/-- The inverse image in a presentation source of a subgroup of the target. -/

32def presentationSubgroupPreimage (π : F →ₜ* G) (U : Subgroup G) : Subgroup F :=

33 Subgroup.comap π.toMonoidHom U

35/-- The restricted epimorphism `π⁻¹(U) → U` attached to a presentation map `π : F → G`. -/

36def restrictPresentationHom (π : F →ₜ* G) (U : Subgroup G) :

37 presentationSubgroupPreimage π U →ₜ* U where

38 toMonoidHom :=

39 { toFun := fun x => ⟨π x.1, x.2⟩

40 map_one' := by

41 apply Subtype.ext

42 simp only [OneMemClass.coe_one, map_one]

43 map_mul' := by

44 intro x y

45 apply Subtype.ext

46 simp only [Subgroup.coe_mul, map_mul]}

47 continuous_toFun := by

48 exact Continuous.subtype_mk

49 (π.continuous_toFun.comp continuous_subtype_val)

50 (fun x => x.2)

52omit [IsTopologicalGroup F] [IsTopologicalGroup G] in

53@[simp] theorem restrictPresentationHom_apply

54 (π : F →ₜ* G) (U : Subgroup G)

55 (x : presentationSubgroupPreimage π U) :

56 restrictPresentationHom π U x = ⟨π x.1, x.2⟩ :=

57 rfl

59omit [IsTopologicalGroup F] [IsTopologicalGroup G] in

60theorem restrictPresentationHom_surjective

61 (π : F →ₜ* G) (U : Subgroup G)

62 (hπsurj : Function.Surjective π) :

63 Function.Surjective (restrictPresentationHom π U) := by

64 intro y

65 rcases hπsurj y.1 with ⟨x, hx⟩

66 refine ⟨⟨x, ?_⟩, ?_⟩

67 · change π x ∈ U

68 simp only [hx, y.2]

69 · apply Subtype.ext

70 exact hx

72omit [IsTopologicalGroup F] [IsTopologicalGroup G] in

73theorem restrictPresentationHom_ker

74 (π : F →ₜ* G) (U : Subgroup G) :

75 (restrictPresentationHom π U).toMonoidHom.ker =

76 π.toMonoidHom.ker.subgroupOf (presentationSubgroupPreimage π U) := by

77 ext x

78 constructor

79 · intro hx

80 change x.1 ∈ π.toMonoidHom.ker

81 rw [MonoidHom.mem_ker]

82 exact congrArg Subtype.val hx

83 · intro hx

84 apply Subtype.ext

85 change π x.1 = 1

86 change x.1 ∈ π.toMonoidHom.ker at hx

87 simpa [MonoidHom.mem_ker] using hx

89theorem isPresentationOf_subgroup_restrict

90 (C : ProCGroups.FiniteGroupClass.{u})

91 (π : F →ₜ* G) (U : Subgroup G)

92 (hπsurj : Function.Surjective π)

93 (hU : ProCGroups.ProC.IsProCGroup C U) :

94 IsQuotientByKernel C

95 (F := presentationSubgroupPreimage π U) (G := U)

96 (π.toMonoidHom.ker.subgroupOf (presentationSubgroupPreimage π U)) := by

97 exact ⟨hU, restrictPresentationHom π U,

98 restrictPresentationHom_surjective π U hπsurj,

99 restrictPresentationHom_ker π U⟩

100

101theorem exists_isPresentationOf_subgroup_restrict_of_isPresentationOf

102 (C : ProCGroups.FiniteGroupClass.{u})

103 {K : Subgroup F}

104 (U : Subgroup G)

105 (hU : ProCGroups.ProC.IsProCGroup C U) :

106 IsQuotientByKernel C (F := F) (G := G) K →

107 ∃ π : F →ₜ* G, Function.Surjective π ∧ π.toMonoidHom.ker = K ∧

108 IsQuotientByKernel C

109 (F := presentationSubgroupPreimage π U) (G := U)

110 (π.toMonoidHom.ker.subgroupOf (presentationSubgroupPreimage π U)) := by

111 intro hpres

112 rcases hpres with ⟨_hG, π, hπsurj, hπker⟩

113 exact ⟨π, hπsurj, hπker,

114 isPresentationOf_subgroup_restrict C π U hπsurj hU⟩

115

116theorem isPresentationOf_openSubgroup_restrict

117 (C : ProCGroups.FiniteGroupClass.{u})

118 (hC : ProCGroups.FiniteGroupClass.FullFormation C)

119 (hG : ProCGroups.ProC.IsProCGroup C G)

120 (π : F →ₜ* G) (U : OpenSubgroup G)

121 (hπsurj : Function.Surjective π) :

122 IsQuotientByKernel C

123 (F := presentationSubgroupPreimage π (U : Subgroup G)) (G := ↥(U : Subgroup G))

124 (π.toMonoidHom.ker.subgroupOf (presentationSubgroupPreimage π (U : Subgroup G))) := by

125 have hUclosed : IsClosed (((U : Subgroup G) : Set G)) :=

126 ProCGroups.openSubgroup_isClosed (G := G) U

127 have hUproC : ProCGroups.ProC.IsProCGroup C ↥(U : Subgroup G) :=

128 ProCGroups.ProC.IsProCGroup.of_isClosed_subgroup_of_fullFormation

129 hC hG (U : Subgroup G) hUclosed

130 exact isPresentationOf_subgroup_restrict C π (U : Subgroup G) hπsurj hUproC

131

132theorem exists_isPresentationOf_openSubgroup_restrict_of_isPresentationOf

133 (C : ProCGroups.FiniteGroupClass.{u})

134 (hC : ProCGroups.FiniteGroupClass.FullFormation C)

135 {K : Subgroup F} (U : OpenSubgroup G) :

136 IsQuotientByKernel C (F := F) (G := G) K →

137 ∃ π : F →ₜ* G, Function.Surjective π ∧ π.toMonoidHom.ker = K ∧

138 IsQuotientByKernel C

139 (F := presentationSubgroupPreimage π (U : Subgroup G)) (G := ↥(U : Subgroup G))

140 (π.toMonoidHom.ker.subgroupOf

141 (presentationSubgroupPreimage π (U : Subgroup G))) := by

142 intro hpres

143 rcases hpres with ⟨hG, π, hπsurj, hπker⟩

144 exact ⟨π, hπsurj, hπker,

145 isPresentationOf_openSubgroup_restrict C hC hG π U hπsurj⟩

146

147end RestrictedPresentations

148

149end ProCGroups.Presentations