FenchelNielsenZomorrodian.Profinite.FGroup
This module develops Fenchel--Nielsen--Zomorrodian presentation reductions, period relations, reindexings, and quotient maps.
import
noncomputable def liftOfSurjective
[CompactSpace F] [T2Space G]
(π : F →ₜ* G) (hπ : Function.Surjective π)
(φ : F →ₜ* A) (hker : π.toMonoidHom.ker ≤ φ.toMonoidHom.ker) :
G →ₜ* A := by
let ψ : G →* A :=
(π.toMonoidHom.liftOfSurjective hπ) ⟨φ.toMonoidHom, hker⟩
have hψcomp : ψ.comp π.toMonoidHom = φ.toMonoidHom := by
ext x
simp only [ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.liftOfSurjective, MonoidHom.coe_coe,
MonoidHom.liftOfRightInverse_comp, ψ]
have hcomp_continuous : Continuous fun x : F => ψ (π x) := by
convert φ.continuous_toFun using 1
funext x
exact MonoidHom.ext_iff.mp hψcomp x
exact
{ toMonoidHom := ψ
continuous_toFun :=
(IsQuotientMap.of_surjective_continuous
hπ π.continuous_toFun).continuous_iff.2 hcomp_continuous }Descend a continuous homomorphism along a continuous surjection, using a kernel inclusion. This is the presentation quotient bridge used for profinite F-groups: a continuous homomorphism out of the free profinite source descends to the presented group once it kills the presentation kernel.
@[simp] theorem liftOfSurjective_apply
[CompactSpace F] [T2Space G]
(π : F →ₜ* G) (hπ : Function.Surjective π)
(φ : F →ₜ* A) (hker : π.toMonoidHom.ker ≤ φ.toMonoidHom.ker)
(x : F) :
liftOfSurjective π hπ φ hker (π x) = φ xThe descended homomorphism is evaluated by applying the original homomorphism to any chosen preimage.
Show proof
by
change
((π.toMonoidHom.liftOfSurjective hπ) ⟨φ.toMonoidHom, hker⟩)
(π.toMonoidHom x) = φ.toMonoidHom x
exact
MonoidHom.liftOfRightInverse_comp_apply
(f := π.toMonoidHom) (f_inv := Function.surjInv hπ)
(Function.rightInverse_surjInv hπ) ⟨φ.toMonoidHom, hker⟩ xProof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□@[simp] theorem liftOfSurjective_comp
[CompactSpace F] [T2Space G]
(π : F →ₜ* G) (hπ : Function.Surjective π)
(φ : F →ₜ* A) (hker : π.toMonoidHom.ker ≤ φ.toMonoidHom.ker) :
(liftOfSurjective π hπ φ hker).toMonoidHom.comp π.toMonoidHom =
φ.toMonoidHomComposing the descended homomorphism with the quotient map recovers the original homomorphism.
Show proof
by
ext x
simp only [ContinuousMonoidHom.coe_toMonoidHom, MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply,
liftOfSurjective_apply]Proof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□abbrev profiniteDerivedSeries
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(m : ℕ) : Subgroup G :=
ProCGroups.FiniteStepSolvableQuotients.topDerivedTop G mThe closed derived series of a profinite group, starting from the whole group.
theorem profiniteDerivedSeries_one_eq_bot_of_commGroup
(G : Type u) [CommGroup G] [TopologicalSpace G] [T1Space G]
[IsTopologicalGroup G] :
profiniteDerivedSeries G 1 = ⊥In a commutative \(T_1\) topological group, the first closed derived subgroup is trivial.
Show proof
by
change
(⁅(⊤ : Subgroup G), (⊤ : Subgroup G)⁆).topologicalClosure =
(⊥ : Subgroup G)
have hcomm :
⁅(⊤ : Subgroup G), (⊤ : Subgroup G)⁆ = (⊥ : Subgroup G) := by
rw [Subgroup.commutator_eq_bot_iff_le_centralizer]
intro x _hx
rw [Subgroup.mem_centralizer_iff]
intro y _hy
exact mul_comm y x
rw [hcomm]
apply le_antisymm
· exact
Subgroup.topologicalClosure_minimal
(s := (⊥ : Subgroup G)) bot_le (by
change IsClosed ({1} : Set G)
exact isClosed_singleton)
· exact bot_leProof. Unfold the closed derived series. In the discrete case closures do not change the ordinary derived subgroup, and for a commutative \(T_1\) group the commutator subgroup is trivial.
□theorem profiniteDerivedSeries_eq_derivedSeries_of_discrete
(G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G]
[IsTopologicalGroup G] :
∀ m : ℕ, profiniteDerivedSeries G m = derivedSeries G mFor a discrete topological group, the closed profinite derived series agrees with the ordinary derived series.
Show proof
by
intro m
induction m with
| zero =>
rfl
| succ m ih =>
change
(⁅profiniteDerivedSeries G m, profiniteDerivedSeries G m⁆).topologicalClosure =
derivedSeries G (m + 1)
rw [ih, derivedSeries_succ]
apply le_antisymm
· exact
Subgroup.topologicalClosure_minimal
(s := ⁅derivedSeries G m, derivedSeries G m⁆) le_rfl
(isClosed_discrete _)
· exact
Subgroup.le_topologicalClosure
(s := ⁅derivedSeries G m, derivedSeries G m⁆)Proof. Unfold the closed derived series. In the discrete case closures do not change the ordinary derived subgroup, and for a commutative \(T_1\) group the commutator subgroup is trivial.
□def profiniteFenchelGeneratorSet
{G : Type u} {σ : FenchelSignature}
(surfaceA surfaceB : Fin σ.orbitGenus → G)
(cusp : Fin σ.numCusps → G)
(inertia : Fin σ.numPeriods → G) : Set G :=
Set.range surfaceA ∪ Set.range surfaceB ∪ Set.range cusp ∪ Set.range inertiaThe Fenchel--Nielsen generator set for a profinite F-group presentation.
def profiniteFenchelTotalRelation
{G : Type u} [Group G] {σ : FenchelSignature}
(surfaceA surfaceB : Fin σ.orbitGenus → G)
(cusp : Fin σ.numCusps → G)
(inertia : Fin σ.numPeriods → G) : G :=
((List.finRange σ.orbitGenus).map fun i => ⁅surfaceA i, surfaceB i⁆).prod *
((List.finRange σ.numCusps).map fun j => cusp j).prod *
((List.finRange σ.numPeriods).map fun k => inertia k).prodThe single Fenchel--Nielsen surface relation is \(\prod_i [\alpha_i,\beta_i]\,\prod_j \gamma_j\,\prod_k \delta_k=1\).
inductive ProfiniteFenchelGenerator (σ : FenchelSignature)
| surfaceA : Fin σ.orbitGenus → ProfiniteFenchelGenerator σ
| surfaceB : Fin σ.orbitGenus → ProfiniteFenchelGenerator σ
| cusp : Fin σ.numCusps → ProfiniteFenchelGenerator σ
| inertia : Fin σ.numPeriods → ProfiniteFenchelGenerator σFormal indices for the Fenchel--Nielsen profinite F-group generators.
instance instTopologicalSpaceProfiniteFenchelGenerator (σ : FenchelSignature) :
TopologicalSpace (ProfiniteFenchelGenerator σ) :=
⊥instance instDiscreteTopologyProfiniteFenchelGenerator (σ : FenchelSignature) :
DiscreteTopology (ProfiniteFenchelGenerator σ) :=
⟨rfl⟩abbrev ProfiniteFenchelGeneratorIndex (σ : FenchelSignature) : Type v :=
ULift.{v, 0} (ProfiniteFenchelGenerator σ)A universe-lifted Fenchel--Nielsen generator index, suitable as a free pro-\(C\) basis.
instance instTopologicalSpaceProfiniteFenchelGeneratorIndex (σ : FenchelSignature) :
TopologicalSpace (ProfiniteFenchelGeneratorIndex.{v} σ) :=
⊥instance instDiscreteTopologyProfiniteFenchelGeneratorIndex (σ : FenchelSignature) :
DiscreteTopology (ProfiniteFenchelGeneratorIndex.{v} σ) :=
⟨rfl⟩def profiniteFenchelRelatorSet
{F : Type u} [Group F] (σ : FenchelSignature)
(basis : ProfiniteFenchelGeneratorIndex.{u} σ → F) : Set F :=
{profiniteFenchelTotalRelation
(fun i => basis (ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
(fun i => basis (ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
(fun j => basis (ULift.up (ProfiniteFenchelGenerator.cusp j)))
(fun k => basis (ULift.up (ProfiniteFenchelGenerator.inertia k)))} ∪
Set.range fun k : Fin σ.numPeriods =>
basis (ULift.up (ProfiniteFenchelGenerator.inertia k)) ^ σ.periods kThe Fenchel--Nielsen relator set: the total surface relation and all inertia-period relations.
def ProfiniteFenchelGenerator.eval
{G : Type u} {σ : FenchelSignature}
(surfaceA surfaceB : Fin σ.orbitGenus → G)
(cusp : Fin σ.numCusps → G)
(inertia : Fin σ.numPeriods → G) :
ProfiniteFenchelGenerator σ → G
| .surfaceA i => surfaceA i
| .surfaceB i => surfaceB i
| .cusp j => cusp j
| .inertia k => inertia kA profinite Fenchel generator evaluates to its prescribed target element.
structure ProfiniteFGroup where
carrier : Type u
[group : Group carrier]
[topologicalSpace : TopologicalSpace carrier]
[isTopologicalGroup : IsTopologicalGroup carrier]
presentationSource : Type u
[presentationSourceGroup : Group presentationSource]
[presentationSourceTopologicalSpace : TopologicalSpace presentationSource]
[presentationSourceIsTopologicalGroup : IsTopologicalGroup presentationSource]
isProfinite : ProCGroups.IsProfiniteGroup carrier
topologicallyFinitelyGenerated :
ProCGroups.FiniteGeneration.TopologicallyFinitelyGenerated carrier
signature : FenchelSignature
firstDerivedSignature : FenchelSignature
surfaceA : Fin signature.orbitGenus → carrier
surfaceB : Fin signature.orbitGenus → carrier
cusp : Fin signature.numCusps → carrier
inertia : Fin signature.numPeriods → carrier
presentation_relation :
profiniteFenchelTotalRelation surfaceA surfaceB cusp inertia = 1
presentation_generates :
ProCGroups.Generation.TopologicallyGenerates
(G := carrier)
(profiniteFenchelGeneratorSet surfaceA surfaceB cusp inertia)
presentationBasis : ProfiniteFenchelGeneratorIndex.{u} signature → presentationSource
presentationRelators : Set presentationSource
presentationRelators_eq :
presentationRelators =
profiniteFenchelRelatorSet signature presentationBasis
presentation :
ProCGroups.Presentations.IsFreePresentationOfClass
(ProCGroups.FiniteGroupClass.allFinite :
ProCGroups.FiniteGroupClass.{u})
(X := ProfiniteFenchelGeneratorIndex.{u} signature)
(F := presentationSource) (G := carrier)
presentationBasis presentationRelators
presentation_π_surfaceA :
∀ i : Fin signature.orbitGenus,
ProCGroups.Presentations.IsFreePresentationOf.π presentation
(presentationBasis
(ULift.up (ProfiniteFenchelGenerator.surfaceA i))) = surfaceA i
presentation_π_surfaceB :
∀ i : Fin signature.orbitGenus,
ProCGroups.Presentations.IsFreePresentationOf.π presentation
(presentationBasis
(ULift.up (ProfiniteFenchelGenerator.surfaceB i))) = surfaceB i
presentation_π_cusp :
∀ j : Fin signature.numCusps,
ProCGroups.Presentations.IsFreePresentationOf.π presentation
(presentationBasis
(ULift.up (ProfiniteFenchelGenerator.cusp j))) = cusp j
presentation_π_inertia :
∀ k : Fin signature.numPeriods,
ProCGroups.Presentations.IsFreePresentationOf.π presentation
(presentationBasis
(ULift.up (ProfiniteFenchelGenerator.inertia k))) = inertia k
inertia_order : ∀ i, orderOf (inertia i) = signature.periods iThe profinite Fenchel--Nielsen group is the profinite group associated with the compact Fuchsian presentation.
theorem finiteOpenSubgroupsOfIndex (Δ : ProfiniteFGroup.{u}) :
ProCGroups.FiniteGeneration.HasFiniteOpenSubgroupsOfIndex Δ.carrierShow proof
by
letI : CompactSpace Δ.carrier :=
ProCGroups.IsProfiniteGroup.compactSpace Δ.isProfinite
exact
ProCGroups.FiniteGeneration.hasFiniteOpenSubgroupsOfIndex_of_topologicallyFinitelyGenerated
(G := Δ.carrier) Δ.topologicallyFinitelyGeneratedProof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. Every map between the reduced presentations is determined by the images of elliptic, handle, and boundary generators. The period and product relators are checked explicitly after applying those images. Therefore the constructed quotient or abelianized map is well defined and has the claimed effect on the named generator or class. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□noncomputable def presentationMap (Δ : ProfiniteFGroup.{u}) :
Δ.presentationSource →ₜ* Δ.carrier :=
ProCGroups.Presentations.IsFreePresentationOf.π Δ.presentationThe presentation map from the free profinite Fenchel source onto the profinite F-group.
theorem presentationMap_surjective (Δ : ProfiniteFGroup.{u}) :
Function.Surjective Δ.presentationMapThe presentation map of the profinite F-group is surjective.
Show proof
ProCGroups.Presentations.IsFreePresentationOf.π_surjective Δ.presentationProof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□theorem presentationMap_ker_eq_closedNormalClosure
(Δ : ProfiniteFGroup.{u}) :
Δ.presentationMap.toMonoidHom.ker =
ProCGroups.Presentations.closedNormalClosure Δ.presentationRelatorsThe kernel of the profinite Fuchsian presentation map is the closed normal closure of the presentation relators.
Show proof
ProCGroups.Presentations.IsFreePresentationOf.kernel_eq_closedNormalClosure
Δ.presentationProof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□theorem presentationMap_eq_one_of_mem_relators
(Δ : ProfiniteFGroup.{u}) {x : Δ.presentationSource}
(hx : x ∈ Δ.presentationRelators) :
Δ.presentationMap x = 1The profinite F-group presentation map sends every defining presentation relator to the identity.
Show proof
by
have hxClosed :
x ∈ ProCGroups.Presentations.closedNormalClosure
Δ.presentationRelators :=
ProCGroups.Presentations.subset_closedNormalClosure
(F := Δ.presentationSource) Δ.presentationRelators hx
have hxKer : x ∈ Δ.presentationMap.toMonoidHom.ker := by
rw [presentationMap_ker_eq_closedNormalClosure Δ]
exact hxClosed
exact hxKerProof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□@[simp] theorem presentationMap_surfaceA (Δ : ProfiniteFGroup.{u})
(i : Fin Δ.signature.orbitGenus) :
Δ.presentationMap
(Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.surfaceA i))) =
Δ.surfaceA iThe presentation map sends a surface \(A\)-generator to its image in the profinite F-group.
Show proof
Δ.presentation_π_surfaceA iProof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□@[simp] theorem presentationMap_surfaceB (Δ : ProfiniteFGroup.{u})
(i : Fin Δ.signature.orbitGenus) :
Δ.presentationMap
(Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.surfaceB i))) =
Δ.surfaceB iThe presentation map sends a surface \(B\)-generator to its image in the profinite F-group.
Show proof
Δ.presentation_π_surfaceB iProof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□@[simp] theorem presentationMap_cusp (Δ : ProfiniteFGroup.{u})
(j : Fin Δ.signature.numCusps) :
Δ.presentationMap
(Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.cusp j))) =
Δ.cusp jThe presentation map sends a cusp generator to its image in the profinite F-group.
Show proof
Δ.presentation_π_cusp jProof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□@[simp] theorem presentationMap_inertia (Δ : ProfiniteFGroup.{u})
(k : Fin Δ.signature.numPeriods) :
Δ.presentationMap
(Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.inertia k))) =
Δ.inertia kThe presentation map sends an inertia generator to its image in the profinite F-group.
Show proof
Δ.presentation_π_inertia kProof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□theorem presentationMap_totalRelator_eq_one
(Δ : ProfiniteFGroup.{u}) :
Δ.presentationMap
(profiniteFenchelTotalRelation
(fun i => Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
(fun i => Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
(fun j => Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.cusp j)))
(fun k => Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.inertia k)))) = 1Under the profinite F-group presentation map, the total surface relator maps to the identity.
Show proof
presentationMap_eq_one_of_mem_relators Δ (by
rw [Δ.presentationRelators_eq]
exact Or.inl rfl)Proof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□theorem presentationMap_periodRelator_eq_one
(Δ : ProfiniteFGroup.{u}) (k : Fin Δ.signature.numPeriods) :
Δ.presentationMap
(Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.inertia k)) ^
Δ.signature.periods k) = 1Under the profinite F-group presentation map, each inertia period relator maps to the identity.
Show proof
presentationMap_eq_one_of_mem_relators Δ (by
rw [Δ.presentationRelators_eq]
exact Or.inr ⟨k, rfl⟩)Proof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□noncomputable def presentationLift
(Δ : ProfiniteFGroup.{u})
{A : Type u} [Group A] [TopologicalSpace A] [T1Space A]
(φ : Δ.presentationSource →ₜ* A)
(hφ :
Δ.presentationRelators ⊆ φ.toMonoidHom.ker) :
Δ.carrier →ₜ* A := by
have hSourceProfinite :
ProCGroups.IsProfiniteGroup Δ.presentationSource :=
ProCGroups.ProC.isProfiniteGroup_of_finiteGroupClassProCPredicate
(ProCGroups.FiniteGroupClass.allFinite :
ProCGroups.FiniteGroupClass.{u})
Δ.presentation.1.isProC
letI : CompactSpace Δ.presentationSource :=
ProCGroups.IsProfiniteGroup.compactSpace hSourceProfinite
letI : T2Space Δ.carrier :=
ProCGroups.IsProfiniteGroup.t2Space Δ.isProfinite
have hClosedKer :
IsClosed ((φ.toMonoidHom.ker : Subgroup Δ.presentationSource) :
Set Δ.presentationSource) := by
change IsClosed (φ ⁻¹' ({1} : Set A))
exact isClosed_singleton.preimage φ.continuous_toFun
have hClosedNormal :
ProCGroups.Presentations.closedNormalClosure Δ.presentationRelators ≤
φ.toMonoidHom.ker :=
ProCGroups.Presentations.closedNormalClosure_le_closed_normal
(F := Δ.presentationSource) hClosedKer hφ
have hker : Δ.presentationMap.toMonoidHom.ker ≤ φ.toMonoidHom.ker := by
rw [presentationMap_ker_eq_closedNormalClosure Δ]
exact hClosedNormal
exact
ContinuousMonoidHom.liftOfSurjective
Δ.presentationMap (presentationMap_surjective Δ) φ hkerA continuous homomorphism from the presentation source whose relators vanish descends to a continuous homomorphism from the profinite F-group.
@[simp] theorem presentationLift_comp_presentationMap
(Δ : ProfiniteFGroup.{u})
{A : Type u} [Group A] [TopologicalSpace A] [T1Space A]
(φ : Δ.presentationSource →ₜ* A)
(hφ :
Δ.presentationRelators ⊆ φ.toMonoidHom.ker) :
(Δ.presentationLift φ hφ).toMonoidHom.comp
Δ.presentationMap.toMonoidHom =
φ.toMonoidHomComposing a descended presentation lift with the presentation map recovers the original source homomorphism.
Show proof
by
ext x
dsimp [presentationLift]
simp only [ContinuousMonoidHom.liftOfSurjective_apply]Proof. Unfold the finite-index transport and the chosen Schreier transversal. The forward map, quotient map, or generator equivalence is determined on the named generators, and the relator-respecting statement follows by checking the listed source relator cases after applying those generator formulas.
□@[simp] theorem presentationLift_surfaceA
(Δ : ProfiniteFGroup.{u})
{A : Type u} [Group A] [TopologicalSpace A] [T1Space A]
(φ : Δ.presentationSource →ₜ* A)
(hφ :
Δ.presentationRelators ⊆ φ.toMonoidHom.ker)
(i : Fin Δ.signature.orbitGenus) :
Δ.presentationLift φ hφ (Δ.surfaceA i) =
φ (Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.surfaceA i)))The descended presentation lift sends the surface \(A\)-generator to its prescribed image.
Show proof
by
rw [← presentationMap_surfaceA Δ i]
exact
MonoidHom.ext_iff.mp
(presentationLift_comp_presentationMap Δ φ hφ)
(Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.surfaceA i)))Proof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□@[simp] theorem presentationLift_surfaceB
(Δ : ProfiniteFGroup.{u})
{A : Type u} [Group A] [TopologicalSpace A] [T1Space A]
(φ : Δ.presentationSource →ₜ* A)
(hφ :
Δ.presentationRelators ⊆ φ.toMonoidHom.ker)
(i : Fin Δ.signature.orbitGenus) :
Δ.presentationLift φ hφ (Δ.surfaceB i) =
φ (Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.surfaceB i)))The descended presentation lift sends the surface \(B\)-generator to its prescribed image.
Show proof
by
rw [← presentationMap_surfaceB Δ i]
exact
MonoidHom.ext_iff.mp
(presentationLift_comp_presentationMap Δ φ hφ)
(Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.surfaceB i)))Proof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□@[simp] theorem presentationLift_cusp
(Δ : ProfiniteFGroup.{u})
{A : Type u} [Group A] [TopologicalSpace A] [T1Space A]
(φ : Δ.presentationSource →ₜ* A)
(hφ :
Δ.presentationRelators ⊆ φ.toMonoidHom.ker)
(j : Fin Δ.signature.numCusps) :
Δ.presentationLift φ hφ (Δ.cusp j) =
φ (Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.cusp j)))The descended presentation lift sends the cusp generator to its prescribed image.
Show proof
by
rw [← presentationMap_cusp Δ j]
exact
MonoidHom.ext_iff.mp
(presentationLift_comp_presentationMap Δ φ hφ)
(Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.cusp j)))Proof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□@[simp 900] theorem presentationLift_inertia
(Δ : ProfiniteFGroup.{u})
{A : Type u} [Group A] [TopologicalSpace A] [T1Space A]
(φ : Δ.presentationSource →ₜ* A)
(hφ :
Δ.presentationRelators ⊆ φ.toMonoidHom.ker)
(k : Fin Δ.signature.numPeriods) :
Δ.presentationLift φ hφ (Δ.inertia k) =
φ (Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.inertia k)))The descended presentation lift sends the inertia generator to its prescribed image.
Show proof
by
rw [← presentationMap_inertia Δ k]
exact
MonoidHom.ext_iff.mp
(presentationLift_comp_presentationMap Δ φ hφ)
(Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.inertia k)))Proof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□noncomputable def presentationSourceLiftToFinite
(Δ : ProfiniteFGroup.{u})
{A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
(χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A) :
Δ.presentationSource →ₜ* A := by
letI : IsTopologicalGroup A := inferInstance
have hCG :
(ProCGroups.FiniteGroupClass.allFinite :
ProCGroups.FiniteGroupClass.{u}).pred A := by
change Finite A
infer_instance
have hA :
(ProCGroups.ProC.finiteGroupClassProCPredicate
(ProCGroups.FiniteGroupClass.allFinite :
ProCGroups.FiniteGroupClass.{u})).holds (G := A) := by
exact
ProCGroups.ProC.IsProCGroup.of_finite_discrete
(C := (ProCGroups.FiniteGroupClass.allFinite :
ProCGroups.FiniteGroupClass.{u}))
ProCGroups.FiniteGroupClass.allFinite_quotientClosed hCG
have hχ : Continuous χ := continuous_of_discreteTopology
exact
{ toMonoidHom := Δ.presentation.1.lift hA χ hχ
continuous_toFun := (Δ.presentation.1.lift_spec hA χ hχ).1 }An arbitrary assignment of the Fenchel--Nielsen presentation generators to a finite discrete group lifts to the free profinite presentation source.
@[simp 900] theorem presentationSourceLiftToFinite_basis
(Δ : ProfiniteFGroup.{u})
{A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
(χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)
(x : ProfiniteFenchelGeneratorIndex.{u} Δ.signature) :
Δ.presentationSourceLiftToFinite χ (Δ.presentationBasis x) = χ xShow proof
by
letI : IsTopologicalGroup A := inferInstance
have hCG :
(ProCGroups.FiniteGroupClass.allFinite :
ProCGroups.FiniteGroupClass.{u}).pred A := by
change Finite A
infer_instance
have hA :
(ProCGroups.ProC.finiteGroupClassProCPredicate
(ProCGroups.FiniteGroupClass.allFinite :
ProCGroups.FiniteGroupClass.{u})).holds (G := A) := by
exact
ProCGroups.ProC.IsProCGroup.of_finite_discrete
(C := (ProCGroups.FiniteGroupClass.allFinite :
ProCGroups.FiniteGroupClass.{u}))
ProCGroups.FiniteGroupClass.allFinite_quotientClosed hCG
have hχ : Continuous χ := continuous_of_discreteTopology
change (Δ.presentation.1.lift hA χ hχ) (Δ.presentationBasis x) = χ x
exact (Δ.presentation.1.lift_spec hA χ hχ).2 xProof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□theorem presentationSourceLiftToFinite_totalRelator
(Δ : ProfiniteFGroup.{u})
{A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
(χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A) :
Δ.presentationSourceLiftToFinite χ
(profiniteFenchelTotalRelation
(fun i => Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
(fun i => Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
(fun j => Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.cusp j)))
(fun k => Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.inertia k)))) =
profiniteFenchelTotalRelation
(fun i => χ (ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
(fun i => χ (ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
(fun j => χ (ULift.up (ProfiniteFenchelGenerator.cusp j)))
(fun k => χ (ULift.up (ProfiniteFenchelGenerator.inertia k)))The lifted finite presentation satisfies the total relator.
Show proof
by
simp only [profiniteFenchelTotalRelation, map_mul, map_list_prod, List.map_map, Function.comp_def,
map_commutatorElement, presentationSourceLiftToFinite_basis]Proof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□theorem presentationSourceLiftToFinite_periodRelator
(Δ : ProfiniteFGroup.{u})
{A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
(χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)
(k : Fin Δ.signature.numPeriods) :
Δ.presentationSourceLiftToFinite χ
(Δ.presentationBasis
(ULift.up (ProfiniteFenchelGenerator.inertia k)) ^
Δ.signature.periods k) =
χ (ULift.up (ProfiniteFenchelGenerator.inertia k)) ^
Δ.signature.periods kThe finite lift of the profinite Fenchel presentation satisfies each period relator.
Show proof
by
simp only [map_pow, presentationSourceLiftToFinite_basis]Proof. Unfold the named period, generator-image, or quotient-data construction. Period relators are checked by the prescribed orders of inertia or elliptic generators; total relations are checked by multiplying the displayed generator images; and data definitions follow by reading off the corresponding period family, index, or signature field.
□theorem presentationSourceLiftToFinite_relators_subset_ker
(Δ : ProfiniteFGroup.{u})
{A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
(χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)
(hTotal :
profiniteFenchelTotalRelation
(fun i => χ (ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
(fun i => χ (ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
(fun j => χ (ULift.up (ProfiniteFenchelGenerator.cusp j)))
(fun k => χ (ULift.up (ProfiniteFenchelGenerator.inertia k))) = 1)
(hPeriod :
∀ k : Fin Δ.signature.numPeriods,
χ (ULift.up (ProfiniteFenchelGenerator.inertia k)) ^
Δ.signature.periods k = 1) :
Δ.presentationRelators ⊆
(Δ.presentationSourceLiftToFinite χ).toMonoidHom.kerShow proof
by
intro x hx
rw [Δ.presentationRelators_eq] at hx
rcases hx with hxTotal | ⟨k, rfl⟩
· rw [Set.mem_singleton_iff] at hxTotal
subst x
simpa [presentationSourceLiftToFinite_totalRelator] using hTotal
· simpa [presentationSourceLiftToFinite_periodRelator] using hPeriod kProof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□noncomputable def presentationLiftToFinite
(Δ : ProfiniteFGroup.{u})
{A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
(χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)
(hχ :
Δ.presentationRelators ⊆
(Δ.presentationSourceLiftToFinite χ).toMonoidHom.ker) :
Δ.carrier →ₜ* A :=
Δ.presentationLift (Δ.presentationSourceLiftToFinite χ) hχnoncomputable def presentationLiftToFiniteOfRelations
(Δ : ProfiniteFGroup.{u})
{A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
(χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)
(hTotal :
profiniteFenchelTotalRelation
(fun i => χ (ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
(fun i => χ (ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
(fun j => χ (ULift.up (ProfiniteFenchelGenerator.cusp j)))
(fun k => χ (ULift.up (ProfiniteFenchelGenerator.inertia k))) = 1)
(hPeriod :
∀ k : Fin Δ.signature.numPeriods,
χ (ULift.up (ProfiniteFenchelGenerator.inertia k)) ^
Δ.signature.periods k = 1) :
Δ.carrier →ₜ* A :=
Δ.presentationLiftToFinite χ
(presentationSourceLiftToFinite_relators_subset_ker Δ χ hTotal hPeriod)A finite target assignment satisfying exactly the Fenchel--Nielsen total and period relations descends to the profinite F-group.
@[simp] theorem presentationLiftToFinite_surfaceA
(Δ : ProfiniteFGroup.{u})
{A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
(χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)
(hχ :
Δ.presentationRelators ⊆
(Δ.presentationSourceLiftToFinite χ).toMonoidHom.ker)
(i : Fin Δ.signature.orbitGenus) :
Δ.presentationLiftToFinite χ hχ (Δ.surfaceA i) =
χ (ULift.up (ProfiniteFenchelGenerator.surfaceA i))Show proof
by
simp only [presentationLiftToFinite, presentationLift_surfaceA, presentationSourceLiftToFinite_basis]Proof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□@[simp] theorem presentationLiftToFinite_surfaceB
(Δ : ProfiniteFGroup.{u})
{A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
(χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)
(hχ :
Δ.presentationRelators ⊆
(Δ.presentationSourceLiftToFinite χ).toMonoidHom.ker)
(i : Fin Δ.signature.orbitGenus) :
Δ.presentationLiftToFinite χ hχ (Δ.surfaceB i) =
χ (ULift.up (ProfiniteFenchelGenerator.surfaceB i))Show proof
by
simp only [presentationLiftToFinite, presentationLift_surfaceB, presentationSourceLiftToFinite_basis]Proof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□@[simp] theorem presentationLiftToFinite_cusp
(Δ : ProfiniteFGroup.{u})
{A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
(χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)
(hχ :
Δ.presentationRelators ⊆
(Δ.presentationSourceLiftToFinite χ).toMonoidHom.ker)
(j : Fin Δ.signature.numCusps) :
Δ.presentationLiftToFinite χ hχ (Δ.cusp j) =
χ (ULift.up (ProfiniteFenchelGenerator.cusp j))Show proof
by
simp only [presentationLiftToFinite, presentationLift_cusp, presentationSourceLiftToFinite_basis]Proof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□@[simp] theorem presentationLiftToFinite_inertia
(Δ : ProfiniteFGroup.{u})
{A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A] [Finite A]
(χ : ProfiniteFenchelGeneratorIndex.{u} Δ.signature → A)
(hχ :
Δ.presentationRelators ⊆
(Δ.presentationSourceLiftToFinite χ).toMonoidHom.ker)
(k : Fin Δ.signature.numPeriods) :
Δ.presentationLiftToFinite χ hχ (Δ.inertia k) =
χ (ULift.up (ProfiniteFenchelGenerator.inertia k))Show proof
by
simp only [presentationLiftToFinite, presentationLift_inertia, presentationSourceLiftToFinite_basis]Proof. Use the profinite Fenchel--Nielsen presentation. A map out of the presented group is constructed by assigning images to the surface, cusp, and inertia generators and checking the total surface relator together with the inertia period relators; the universal property then gives the descended continuous homomorphism and its generator formulas.
□def IsHyperbolic (Δ : ProfiniteFGroup) : Prop :=
Δ.signature.IsHyperbolicA profinite F-group is hyperbolic when its signature is hyperbolic.
def IsPerfect (Δ : ProfiniteFGroup) : Prop :=
profiniteDerivedSeries Δ.carrier 1 = ⊤A profinite F-group is perfect when its first profinite derived subgroup is the whole carrier.
def IsNonPerfect (Δ : ProfiniteFGroup) : Prop :=
¬ Δ.IsPerfectA profinite F-group is nonperfect when it is not perfect.
def PairwiseCoprimePeriods (Δ : ProfiniteFGroup) : Prop :=
∀ i j : Fin Δ.signature.numPeriods,
i ≠ j → Nat.Coprime (Δ.signature.periods i) (Δ.signature.periods j)The profinite F-group signature has pairwise coprime periods.
def CharPerfectNumericalCondition (Δ : ProfiniteFGroup) : Prop :=
Δ.signature.orbitGenus = 0 ∧
Δ.signature.numCusps = 0 ∧
Δ.PairwiseCoprimePeriodsThe characteristic perfectness numerical condition says: orbit genus zero, no cusps, and pairwise coprime periods.
def ProfiniteOpenNormalQuotientHasDerivedLengthAtMost
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(U : OpenNormalSubgroup G) (m : ℕ) : Prop :=
profiniteDerivedSeries (G ⧸ (U : Subgroup G)) m = ⊥The selected open normal quotient has derived length bounded by the given parameter.
def ProfiniteOpenNormalSubgroupTorsionFree
(G : Type u) [Group G] [TopologicalSpace G]
(U : OpenNormalSubgroup G) : Prop :=
∀ x : G, x ∈ (U : Subgroup G) → IsOfFinOrder x → x = 1The selected open normal subgroup is torsion-free for the finite-index reduction.
def ProfiniteOpenCharacteristicSubgroup
(G : Type u) [Group G] [TopologicalSpace G] : Type u :=
{ U : OpenNormalSubgroup G //
ProCGroups.FiniteGeneration.IsTopologicallyCharacteristic (G := G) (U : Subgroup G) }The profinite open characteristic subgroup is the open normal subgroup selected by the finite-quotient data in the construction.
def ProfiniteOpenCharacteristicSubgroup.toOpenNormalSubgroup
{G : Type u} [Group G] [TopologicalSpace G]
(U : ProfiniteOpenCharacteristicSubgroup G) :
OpenNormalSubgroup G :=
U.1An open characteristic subgroup is, in particular, an open normal subgroup.
def ProfiniteOpenCharacteristicQuotientHasDerivedLengthAtMost
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(U : ProfiniteOpenCharacteristicSubgroup G) (m : ℕ) : Prop :=
ProfiniteOpenNormalQuotientHasDerivedLengthAtMost G U.toOpenNormalSubgroup mThe selected open characteristic quotient has derived length bounded by the given parameter.
def HasTorsionFreeOpenNormalSubgroupQuotientDerivedLengthAtMost
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : ℕ) : Prop :=
∃ U : OpenNormalSubgroup G,
ProfiniteOpenNormalSubgroupTorsionFree G U ∧
ProfiniteOpenNormalQuotientHasDerivedLengthAtMost G U mThe predicate records a torsion-free open normal subgroup whose quotient has derived length at most the given bound.
def HasTorsionFreeOpenCharacteristicSubgroupQuotientDerivedLengthAtMost
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : ℕ) : Prop :=
∃ U : ProfiniteOpenCharacteristicSubgroup G,
ProfiniteOpenNormalSubgroupTorsionFree G U.toOpenNormalSubgroup ∧
ProfiniteOpenCharacteristicQuotientHasDerivedLengthAtMost G U mThe predicate records a torsion-free open characteristic subgroup whose quotient has derived length at most the given bound.
theorem ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.of_topDerived_le
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(U : OpenNormalSubgroup G) {m : ℕ}
(hU : profiniteDerivedSeries G m ≤ (U : Subgroup G)) :
ProfiniteOpenNormalQuotientHasDerivedLengthAtMost G U mA containment of the top derived subgroup gives the corresponding open-normal quotient derived-length bound.
Show proof
by
let q : G →ₜ* G ⧸ (U : Subgroup G) := OpenNormalSubgroup.quotientProj U
have hclosed_comm :
∀ n : ℕ,
IsClosed
(((closedCommutator
(topDerivedTop G n) (topDerivedTop G n)).map
(q : G →* G ⧸ (U : Subgroup G)) :
Subgroup (G ⧸ (U : Subgroup G))) :
Set (G ⧸ (U : Subgroup G))) := by
intro n
exact isClosed_discrete _
have hmap :
(topDerivedTop G m).map (q : G →* G ⧸ (U : Subgroup G)) =
topDerivedTop (G ⧸ (U : Subgroup G)) m := by
exact
topDerived_map_eq_of_surj (f := q)
(OpenNormalSubgroup.quotientProj_surjective U) hclosed_comm m
rw [ProfiniteOpenNormalQuotientHasDerivedLengthAtMost, profiniteDerivedSeries,
← hmap]
apply le_bot_iff.mp
intro y hy
rcases hy with ⟨x, hx, rfl⟩
change QuotientGroup.mk' (U : Subgroup G) x = 1
exact (QuotientGroup.eq_one_iff (N := (U : Subgroup G)) x).2 (hU hx)Proof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup presentation. Kernel and normal-closure claims are proved by showing that each rewritten relator lies in the generated normal subgroup and that the quotient map kills exactly those relations required by the presentation. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.topDerived_le
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(U : OpenNormalSubgroup G) {m : ℕ}
(hU : ProfiniteOpenNormalQuotientHasDerivedLengthAtMost G U m) :
profiniteDerivedSeries G m ≤ (U : Subgroup G)A profinite open-normal quotient derived-length bound implies containment of the top derived subgroup.
Show proof
by
let q : G →ₜ* G ⧸ (U : Subgroup G) := OpenNormalSubgroup.quotientProj U
have hle := topDerivedTop_le_comap (f := q) (m := m)
intro x hx
have hxq :
q x ∈ topDerivedTop (G ⧸ (U : Subgroup G)) m :=
hle hx
have hderbot :
topDerivedTop (G ⧸ (U : Subgroup G)) m = ⊥ := by
simpa [ProfiniteOpenNormalQuotientHasDerivedLengthAtMost,
profiniteDerivedSeries] using hU
have hxqbot :
q x ∈ (⊥ : Subgroup (G ⧸ (U : Subgroup G))) := by
simpa [hderbot] using hxq
have hq1 : q x = 1 := Subgroup.mem_bot.mp hxqbot
simpa [q] using
(OpenNormalSubgroup.quotientProj_eq_one_iff (U := U) (x := x)).1 hq1Proof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup presentation. Kernel and normal-closure claims are proved by showing that each rewritten relator lies in the generated normal subgroup and that the quotient map kills exactly those relations required by the presentation. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem profiniteOpenNormalQuotientHasDerivedLengthAtMost_iff_topDerived_le
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
{U : OpenNormalSubgroup G} {m : ℕ} :
ProfiniteOpenNormalQuotientHasDerivedLengthAtMost G U m ↔
profiniteDerivedSeries G m ≤ (U : Subgroup G)A profinite open-normal quotient has derived length at most the given bound exactly when its top derived subgroup is contained in the given subgroup.
Show proof
by
constructor
· exact ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.topDerived_le U
· exact ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.of_topDerived_le UProof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup presentation. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. Every map between the reduced presentations is determined by the images of elliptic, handle, and boundary generators. The period and product relators are checked explicitly after applying those images. Therefore the constructed quotient or abelianized map is well defined and has the claimed effect on the named generator or class. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.mono
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
{U : OpenNormalSubgroup G} {m n : ℕ}
(hmn : m ≤ n)
(hU : ProfiniteOpenNormalQuotientHasDerivedLengthAtMost G U m) :
ProfiniteOpenNormalQuotientHasDerivedLengthAtMost G U nIncreasing the derived-length bound preserves the profinite open-normal quotient derived-length condition.
Show proof
by
rw [profiniteOpenNormalQuotientHasDerivedLengthAtMost_iff_topDerived_le] at hU ⊢
intro x hx
exact hU ((topDerivedTop_antitone hmn) hx)Proof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup presentation. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. Every map between the reduced presentations is determined by the images of elliptic, handle, and boundary generators. The period and product relators are checked explicitly after applying those images. Therefore the constructed quotient or abelianized map is well defined and has the claimed effect on the named generator or class. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem HasTorsionFreeOpenNormalSubgroupQuotientDerivedLengthAtMost.mono
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
{m n : ℕ} (hmn : m ≤ n)
(h :
HasTorsionFreeOpenNormalSubgroupQuotientDerivedLengthAtMost G m) :
HasTorsionFreeOpenNormalSubgroupQuotientDerivedLengthAtMost G nIncreasing the derived-length bound preserves the existence of a torsion-free open normal subgroup whose quotient has derived length at most that bound.
Show proof
by
rcases h with ⟨U, htf, hquot⟩
exact ⟨U, htf,
ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.mono hmn hquot⟩Proof. Unfold the profinite open subgroup predicate. It packages an open normal or characteristic subgroup, torsion-freeness, and a derived-length bound for the quotient; monotonicity keeps the same witness and increases only the bound.
□theorem HasTorsionFreeOpenCharacteristicSubgroupQuotientDerivedLengthAtMost.mono
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
{m n : ℕ} (hmn : m ≤ n)
(h :
HasTorsionFreeOpenCharacteristicSubgroupQuotientDerivedLengthAtMost
G m) :
HasTorsionFreeOpenCharacteristicSubgroupQuotientDerivedLengthAtMost
G nIncreasing the derived-length bound preserves the existence of a torsion-free open characteristic subgroup whose quotient has derived length at most that bound.
Show proof
by
rcases h with ⟨U, htf, hquot⟩
exact ⟨U, htf,
ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.mono hmn hquot⟩Proof. Unfold the profinite open subgroup predicate. It packages an open normal or characteristic subgroup, torsion-freeness, and a derived-length bound for the quotient; monotonicity keeps the same witness and increases only the bound.
□theorem hasTorsionFreeOpenNormal_of_characteristic
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {m : ℕ}
(h :
HasTorsionFreeOpenCharacteristicSubgroupQuotientDerivedLengthAtMost
G m) :
HasTorsionFreeOpenNormalSubgroupQuotientDerivedLengthAtMost G mA torsion-free open characteristic subgroup with a quotient derived-length bound gives the corresponding open-normal-subgroup statement.
Show proof
by
rcases h with ⟨U, htf, hquot⟩
exact ⟨U.toOpenNormalSubgroup, htf, hquot⟩Proof. Unfold the profinite open subgroup predicate. It packages an open normal or characteristic subgroup, torsion-freeness, and a derived-length bound for the quotient; monotonicity keeps the same witness and increases only the bound.
□