ProCGroups.Presentations.SchreierTietze.Restricted
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
def presentationSubgroupPreimage (π : F →ₜ* G) (U : Subgroup G) : Subgroup F :=
Subgroup.comap π.toMonoidHom UThe inverse image in a presentation source of a subgroup of the target.
def restrictPresentationHom (π : F →ₜ* G) (U : Subgroup G) :
presentationSubgroupPreimage π U →ₜ* U where
toMonoidHom :=
{ toFun := fun x => ⟨π x.1, x.2⟩
map_one' := by
apply Subtype.ext
simp only [OneMemClass.coe_one, map_one]
map_mul' := by
intro x y
apply Subtype.ext
simp only [Subgroup.coe_mul, map_mul]}
continuous_toFun := by
exact Continuous.subtype_mk
(π.continuous_toFun.comp continuous_subtype_val)
(fun x => x.2)The restricted epimorphism \(\pi^{-1}(U) \to U\) attached to a presentation map \(\pi:F\to G\).
@[simp] theorem restrictPresentationHom_apply
(π : F →ₜ* G) (U : Subgroup G)
(x : presentationSubgroupPreimage π U) :
restrictPresentationHom π U x = ⟨π x.1, x.2⟩The restricted presentation homomorphism evaluates by applying the original presentation homomorphism to the underlying generator.
Show proof
rflProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem restrictPresentationHom_surjective
(π : F →ₜ* G) (U : Subgroup G)
(hπsurj : Function.Surjective π) :
Function.Surjective (restrictPresentationHom π U)The restricted presentation homomorphism is surjective.
Show proof
by
intro y
rcases hπsurj y.1 with ⟨x, hx⟩
refine ⟨⟨x, ?_⟩, ?_⟩
· change π x ∈ U
simp only [hx, y.2]
· apply Subtype.ext
exact hxProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem restrictPresentationHom_ker
(π : F →ₜ* G) (U : Subgroup G) :
(restrictPresentationHom π U).toMonoidHom.ker =
π.toMonoidHom.ker.subgroupOf (presentationSubgroupPreimage π U)Show proof
by
ext x
constructor
· intro hx
change x.1 ∈ π.toMonoidHom.ker
rw [MonoidHom.mem_ker]
exact congrArg Subtype.val hx
· intro hx
apply Subtype.ext
change π x.1 = 1
change x.1 ∈ π.toMonoidHom.ker at hx
simpa [MonoidHom.mem_ker] using hxProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem isPresentationOf_subgroup_restrict
(C : ProCGroups.FiniteGroupClass.{u})
(π : F →ₜ* G) (U : Subgroup G)
(hπsurj : Function.Surjective π)
(hU : ProCGroups.ProC.IsProCGroup C U) :
IsQuotientByKernel C
(F := presentationSubgroupPreimage π U) (G := U)
(π.toMonoidHom.ker.subgroupOf (presentationSubgroupPreimage π U))The Tietze presentation identity follows from the prescribed generator and relator replacement maps.
Show proof
by
exact ⟨hU, restrictPresentationHom π U,
restrictPresentationHom_surjective π U hπsurj,
restrictPresentationHom_ker π U⟩Proof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem exists_isPresentationOf_subgroup_restrict_of_isPresentationOf
(C : ProCGroups.FiniteGroupClass.{u})
{K : Subgroup F}
(U : Subgroup G)
(hU : ProCGroups.ProC.IsProCGroup C U) :
IsQuotientByKernel C (F := F) (G := G) K →
∃ π : F →ₜ* G, Function.Surjective π ∧ π.toMonoidHom.ker = K ∧
IsQuotientByKernel C
(F := presentationSubgroupPreimage π U) (G := U)
(π.toMonoidHom.ker.subgroupOf (presentationSubgroupPreimage π U))The Tietze presentation identity follows from the prescribed generator and relator replacement maps.
Show proof
by
intro hpres
rcases hpres with ⟨_hG, π, hπsurj, hπker⟩
exact ⟨π, hπsurj, hπker,
isPresentationOf_subgroup_restrict C π U hπsurj hU⟩Proof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem isPresentationOf_openSubgroup_restrict
(C : ProCGroups.FiniteGroupClass.{u})
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
(hG : ProCGroups.ProC.IsProCGroup C G)
(π : F →ₜ* G) (U : OpenSubgroup G)
(hπsurj : Function.Surjective π) :
IsQuotientByKernel C
(F := presentationSubgroupPreimage π (U : Subgroup G)) (G := ↥(U : Subgroup G))
(π.toMonoidHom.ker.subgroupOf (presentationSubgroupPreimage π (U : Subgroup G)))The Tietze presentation identity follows from the prescribed generator and relator replacement maps.
Show proof
by
have hUclosed : IsClosed (((U : Subgroup G) : Set G)) :=
ProCGroups.openSubgroup_isClosed (G := G) U
have hUproC : ProCGroups.ProC.IsProCGroup C ↥(U : Subgroup G) :=
ProCGroups.ProC.IsProCGroup.of_isClosed_subgroup_of_fullFormation
hC hG (U : Subgroup G) hUclosed
exact isPresentationOf_subgroup_restrict C π (U : Subgroup G) hπsurj hUproCProof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□theorem exists_isPresentationOf_openSubgroup_restrict_of_isPresentationOf
(C : ProCGroups.FiniteGroupClass.{u})
(hC : ProCGroups.FiniteGroupClass.FullFormation C)
{K : Subgroup F} (U : OpenSubgroup G) :
IsQuotientByKernel C (F := F) (G := G) K →
∃ π : F →ₜ* G, Function.Surjective π ∧ π.toMonoidHom.ker = K ∧
IsQuotientByKernel C
(F := presentationSubgroupPreimage π (U : Subgroup G)) (G := ↥(U : Subgroup G))
(π.toMonoidHom.ker.subgroupOf
(presentationSubgroupPreimage π (U : Subgroup G)))The Tietze presentation identity follows from the prescribed generator and relator replacement maps.
Show proof
by
intro hpres
rcases hpres with ⟨hG, π, hπsurj, hπker⟩
exact ⟨π, hπsurj, hπker,
isPresentationOf_openSubgroup_restrict C hC hG π U hπsurj⟩Proof. Unfold the pro-\(C\) presentation data together with the Reidemeister--Schreier and Tietze constructions. The restricted source map is checked on generators, and the kernel condition is expressed as equality of the closed normal closures generated by the rewritten relators. Redundant or degenerate relators are removed by Tietze equivalence, while generator and relator replacement maps descend by the universal property of the presented pro-\(C\) group. Open-subgroup and class-membership assertions use permanence of pro-\(C\) groups under closed subgroups and finite quotients.
□