FenchelNielsenZomorrodian.Profinite.MainTheorem
This module develops Fenchel--Nielsen--Zomorrodian presentation reductions, period relations, reindexings, and quotient maps.
import
- FenchelNielsenZomorrodian.Profinite.CharacteristicClosure
- FenchelNielsenZomorrodian.Profinite.CuspedQuotient
- FenchelNielsenZomorrodian.Profinite.DiscreteBridge
- FenchelNielsenZomorrodian.Profinite.LowPeriodQuotient
- FenchelNielsenZomorrodian.Profinite.PositiveGenusQuotient
- FenchelNielsenZomorrodian.Profinite.TorsionFrontier
theorem exists_torsionFree_openNormalSubgroup
(Δ : ProfiniteFGroup.{u}) :
∃ U : OpenNormalSubgroup Δ.carrier,
ProfiniteOpenNormalSubgroupTorsionFree Δ.carrier UProfinite Fenchel--Nielsen existence theorem, normal-subgroup form. Every profinite Fenchel group has a torsion-free open normal subgroup. The result is not restricted to non-perfect groups.
Show proof
exists_torsionFreeOpenNormalSubgroup Δ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. 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.
□theorem exists_torsionFree_openCharacteristicSubgroup
(Δ : ProfiniteFGroup.{u}) :
∃ U : ProfiniteOpenCharacteristicSubgroup Δ.carrier,
ProfiniteOpenNormalSubgroupTorsionFree Δ.carrier U.toOpenNormalSubgroupProfinite Fenchel--Nielsen existence theorem, characteristic-subgroup form. Every profinite Fenchel group has a torsion-free open characteristic subgroup. This is the existence-only theorem and does not assume non-perfectness.
Show proof
by
letI : CompactSpace Δ.carrier := Δ.isProfinite.compactSpace
exact
exists_torsionFree_openCharacteristicSubgroup_of_exists_torsionFree_openNormalSubgroup
(G := Δ.carrier) Δ.finiteOpenSubgroupsOfIndex
(exists_torsionFree_openNormalSubgroup Δ)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. 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.
□private theorem threeStep_normal_of_isNonPerfect
(Δ : ProfiniteFGroup.{u}) :
Δ.IsNonPerfect →
HasTorsionFreeOpenNormalSubgroupQuotientDerivedLengthAtMost
Δ.carrier 3A non-perfect profinite F-group has a torsion-free open normal subgroup whose quotient has derived length at most three.
Show proof
by
intro hNonPerfect
by_cases hCusps : Δ.signature.HasCusps
· exact
ProfiniteSmoothQuotientData.has_torsionFreeOpenNormal_quotient_derivedLength_le
(cuspedSmoothQuotientData Δ hCusps) (by decide : 1 ≤ 3)
· have hCompact : Δ.signature.IsCompact := by
dsimp [FenchelSignature.HasCusps, FenchelSignature.IsCompact] at hCusps ⊢
omega
by_cases hGenus : 1 ≤ Δ.signature.orbitGenus
· exact
ProfiniteSmoothQuotientData.has_torsionFreeOpenNormal_quotient_derivedLength_le
(positiveGenusSmoothQuotientData Δ hGenus) (by decide : 2 ≤ 3)
· have hZero : Δ.signature.orbitGenus = 0 := by omega
by_cases hPeriods : 3 ≤ Δ.signature.numPeriods
· exact
compactDiscreteBridge_threeStep_normal_of_isNonPerfect
Δ hNonPerfect hCompact hZero hPeriods
· have hTwo :
Δ.signature.numPeriods = 2 :=
numPeriods_eq_two_of_isNonPerfect_zeroGenus_noCusps_not_three
Δ hNonPerfect hZero hCompact hPeriods
exact
ProfiniteSmoothQuotientData.has_torsionFreeOpenNormal_quotient_derivedLength_le
(twoPeriodCyclicSmoothQuotientData Δ hCompact hZero hTwo) (by decide : 1 ≤ 3)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. For period-class statements, the relevant lcm or gcd divisibility is converted into a scalar multiple of the abelianized elliptic generator, and the defining period relation makes that multiple vanish. 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. 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 exists_openNormal_torsionFree_dl_le_three_of_nonperfect
(Δ : ProfiniteFGroup.{u}) :
Δ.IsNonPerfect →
HasTorsionFreeOpenNormalSubgroupQuotientDerivedLengthAtMost
Δ.carrier 3Normal-subgroup form of the non-perfect three-step Fenchel--Nielsen theorem.
Show proof
threeStep_normal_of_isNonPerfect Δ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 exists_openChar_torsionFree_dl_le_three_of_nonperfect
(Δ : ProfiniteFGroup.{u}) :
Δ.IsNonPerfect →
HasTorsionFreeOpenCharacteristicSubgroupQuotientDerivedLengthAtMost
Δ.carrier 3Characteristic-subgroup form of the non-perfect three-step Fenchel--Nielsen theorem.
Show proof
by
intro hNonPerfect
letI : CompactSpace Δ.carrier := Δ.isProfinite.compactSpace
exact
hasTorsionFreeOpenCharacteristicSubgroupQuotientDerivedLengthAtMost_of_normal
(G := Δ.carrier) Δ.finiteOpenSubgroupsOfIndex
(threeStep_normal_of_isNonPerfect Δ hNonPerfect)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.
□