FenchelNielsenZomorrodian.Profinite.DiscreteBridge
This module develops Fenchel--Nielsen--Zomorrodian presentation reductions, period relations, reindexings, and quotient maps.
import
theorem mul_swap_eq_one_of_mul_eq_one
{G : Type*} [Group G] {a b : G} (h : a * b = 1) :
b * a = 1If \(a b = 1\), then the swapped product \(b a\) is also \(1\).
Show proof
by
have ha : a = b⁻¹ := by
calc
a = a * 1 := by simp only [mul_one]
_ = a * (b * b⁻¹) := by simp only [mul_one, mul_inv_cancel]
_ = (a * b) * b⁻¹ := by group
_ = b⁻¹ := by simp only [h, one_mul]
simp only [ha, mul_inv_cancel]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.
□noncomputable def compactPresentationHomToProfinite
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hPeriods : 3 ≤ Δ.signature.numPeriods) :
FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods) →*
Δ.carrier := by
let σ := compactFuchsianSignature Δ.signature hCompact hPeriods
let f : FuchsianGenerator σ → Δ.carrier
| .elliptic i => Δ.inertia i
| .surfaceA i => Δ.surfaceA i
| .surfaceB i => Δ.surfaceB i
refine PresentedGroup.toGroup (rels := relators σ) (f := f) ?_
intro r hr
rcases hr with ⟨i, rfl⟩ | rfl
· have hpow : Δ.inertia i ^ Δ.signature.periods i = 1 := by
rw [← Δ.inertia_order i]
exact pow_orderOf_eq_one (Δ.inertia i)
simpa [σ, f, xWord, compactFuchsianSignature] using hpow
· have hCusp :
((List.finRange Δ.signature.numCusps).map fun j => Δ.cusp j).prod = 1 := by
apply List.prod_eq_one
intro x hx
rcases List.mem_map.mp hx with ⟨j, _hj, rfl⟩
exfalso
rw [hCompact] at j
exact Nat.not_lt_zero _ j.2
have hRel :
((List.finRange Δ.signature.orbitGenus).map fun i =>
⁅Δ.surfaceA i, Δ.surfaceB i⁆).prod *
((List.finRange Δ.signature.numPeriods).map fun k => Δ.inertia k).prod =
1 := by
simpa [profiniteFenchelTotalRelation, hCusp, mul_assoc] using
Δ.presentation_relation
have hRel' :
((List.finRange Δ.signature.numPeriods).map fun k => Δ.inertia k).prod *
((List.finRange Δ.signature.orbitGenus).map fun i =>
⁅Δ.surfaceA i, Δ.surfaceB i⁆).prod =
1 :=
mul_swap_eq_one_of_mul_eq_one hRel
simpa [σ, f, totalRelation, xWord, aWord, bWord, compactFuchsianSignature,
map_list_prod, Function.comp_def, map_commutatorElement] using hRel'
@[local simp]The abstract compact Fuchsian presentation maps to a compact profinite F-group by sending the paper generators to the corresponding profinite presentation generators.
theorem compactPresentationHomToProfinite_elliptic
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hPeriods : 3 ≤ Δ.signature.numPeriods)
(i : Fin Δ.signature.numPeriods) :
compactPresentationHomToProfinite Δ hCompact hPeriods
(ellipticElement
(compactFuchsianSignature Δ.signature hCompact hPeriods) i) =
Δ.inertia iThe compact-presentation homomorphism sends each elliptic generator to the corresponding profinite elliptic element.
Show proof
by
simp only [compactPresentationHomToProfinite, ellipticElement, PresentedGroup.toGroup.of]
@[local simp]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. 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 compactPresentationHomToProfinite_surfaceA
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hPeriods : 3 ≤ Δ.signature.numPeriods)
(i : Fin Δ.signature.orbitGenus) :
compactPresentationHomToProfinite Δ hCompact hPeriods
(PresentedGroup.of
(rels := relators
(compactFuchsianSignature Δ.signature hCompact hPeriods))
(FuchsianGenerator.surfaceA i)) =
Δ.surfaceA iThe compact-presentation homomorphism sends each surface A-generator to its prescribed profinite image.
Show proof
by
simp only [compactPresentationHomToProfinite, PresentedGroup.toGroup.of]
@[local simp]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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem compactPresentationHomToProfinite_surfaceB
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hPeriods : 3 ≤ Δ.signature.numPeriods)
(i : Fin Δ.signature.orbitGenus) :
compactPresentationHomToProfinite Δ hCompact hPeriods
(PresentedGroup.of
(rels := relators
(compactFuchsianSignature Δ.signature hCompact hPeriods))
(FuchsianGenerator.surfaceB i)) =
Δ.surfaceB iThe compact-presentation homomorphism sends each surface B-generator to its prescribed profinite image.
Show proof
by
simp only [compactPresentationHomToProfinite, PresentedGroup.toGroup.of]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. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□private theorem compactPresentationHomToProfinite_elliptic_order
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hPeriods : 3 ≤ Δ.signature.numPeriods)
(i : Fin Δ.signature.numPeriods) :
orderOf
(ellipticElement
(compactFuchsianSignature Δ.signature hCompact hPeriods) i) =
Δ.signature.periods iShow proof
by
apply Nat.dvd_antisymm
· simpa [compactFuchsianSignature] using
orderOf_dvd_of_pow_eq_one
(ellipticElement_pow_period_eq_one
(compactFuchsianSignature Δ.signature hCompact hPeriods) i)
· have hdiv :=
orderOf_map_dvd
(compactPresentationHomToProfinite Δ hCompact hPeriods)
(ellipticElement
(compactFuchsianSignature Δ.signature hCompact hPeriods) i)
simpa [compactPresentationHomToProfinite_elliptic,
Δ.inertia_order i] using hdivProof. 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. 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.
□private noncomputable def compactDiscreteNormalQuotientGeneratorImageCore
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hPeriods : 3 ≤ Δ.signature.numPeriods)
(H : Subgroup
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods)))
[H.Normal] :
ProfiniteFenchelGeneratorIndex.{u} Δ.signature →
FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H
| ULift.up (.surfaceA i) =>
QuotientGroup.mk' H
(PresentedGroup.of
(rels := relators
(compactFuchsianSignature Δ.signature hCompact hPeriods))
(FuchsianGenerator.surfaceA i))
| ULift.up (.surfaceB i) =>
QuotientGroup.mk' H
(PresentedGroup.of
(rels := relators
(compactFuchsianSignature Δ.signature hCompact hPeriods))
(FuchsianGenerator.surfaceB i))
| ULift.up (.cusp _) => 1
| ULift.up (.inertia i) =>
QuotientGroup.mk' H
(ellipticElement
(compactFuchsianSignature Δ.signature hCompact hPeriods) i)Core generator-image data for the compact discrete normal quotient.
private noncomputable def compactDiscreteNormalQuotientGeneratorImage
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hPeriods : 3 ≤ Δ.signature.numPeriods)
(H : Subgroup
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods)))
[H.Normal] :
ProfiniteFenchelGeneratorIndex.{u} Δ.signature →
ULift.{u, 0}
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H) :=
fun x =>
ULift.up
(compactDiscreteNormalQuotientGeneratorImageCore Δ hCompact hPeriods H x)Generator-image data for the compact discrete normal quotient.
private theorem compactDiscreteNormalQuotientGeneratorImage_total_relation
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hPeriods : 3 ≤ Δ.signature.numPeriods)
(H : Subgroup
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods)))
[H.Normal] :
profiniteFenchelTotalRelation
(fun i => compactDiscreteNormalQuotientGeneratorImageCore
Δ hCompact hPeriods H
(ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
(fun i => compactDiscreteNormalQuotientGeneratorImageCore
Δ hCompact hPeriods H
(ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
(fun j => compactDiscreteNormalQuotientGeneratorImageCore
Δ hCompact hPeriods H
(ULift.up (ProfiniteFenchelGenerator.cusp j)))
(fun k => compactDiscreteNormalQuotientGeneratorImageCore
Δ hCompact hPeriods H
(ULift.up (ProfiniteFenchelGenerator.inertia k))) = 1The compact discrete normal quotient satisfies the total Fenchel--Nielsen relation.
Show proof
by
let σ := compactFuchsianSignature Δ.signature hCompact hPeriods
let q : FuchsianPresentedGroup σ →*
FuchsianPresentedGroup σ ⧸ H :=
QuotientGroup.mk' H
have hPresented :
q (PresentedGroup.mk (relators σ) (totalRelation σ)) = 1 := by
simpa using congrArg q
(PresentedGroup.one_of_mem (rels := relators σ)
(x := totalRelation σ) (Or.inr rfl))
have hPresented' :
q (PresentedGroup.mk (relators σ)
(((List.finRange Δ.signature.numPeriods).map fun i =>
xWord σ i).prod)) *
q (PresentedGroup.mk (relators σ)
(((List.finRange Δ.signature.orbitGenus).map fun j =>
⁅aWord σ j, bWord σ j⁆).prod)) =
1 := by
simpa [σ, q, totalRelation, xWord, aWord, bWord, ellipticElement,
Function.comp_def, map_commutatorElement, compactFuchsianSignature] using hPresented
have hDiscreteTotal :
((List.finRange Δ.signature.numPeriods).map fun i =>
q (PresentedGroup.mk (relators σ) (xWord σ i))).prod *
((List.finRange Δ.signature.orbitGenus).map fun j =>
⁅q (PresentedGroup.mk (relators σ) (aWord σ j)),
q (PresentedGroup.mk (relators σ) (bWord σ j))⁆).prod =
1 := by
simpa [map_list_prod, Function.comp_def, map_commutatorElement] using hPresented'
have hSwapped :
((List.finRange Δ.signature.orbitGenus).map fun j =>
⁅q (PresentedGroup.mk (relators σ) (aWord σ j)),
q (PresentedGroup.mk (relators σ) (bWord σ j))⁆).prod *
((List.finRange Δ.signature.numPeriods).map fun i =>
q (PresentedGroup.mk (relators σ) (xWord σ i))).prod =
1 :=
mul_swap_eq_one_of_mul_eq_one hDiscreteTotal
have hCusp :
((List.finRange Δ.signature.numCusps).map fun _j =>
(1 :
FuchsianPresentedGroup σ ⧸ H)).prod = 1 := by
rw [hCompact]
simp only [List.finRange_zero, List.map_nil, List.prod_nil]
simpa [profiniteFenchelTotalRelation,
compactDiscreteNormalQuotientGeneratorImageCore, σ, q, hCusp,
compactFuchsianSignature, mul_assoc] using hSwappedProof. Use the discrete smooth quotient data and lift it through the profinite Fenchel presentation. Generator-image statements are checked on surface, cusp, and inertia generators; inertia-order and total-relation conditions are inherited from the discrete quotient, and the derived-length and smooth-data fields are transported through the normal quotient.
□private theorem compactDiscreteNormalQuotientGeneratorImage_lifted_total_relation
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hPeriods : 3 ≤ Δ.signature.numPeriods)
(H : Subgroup
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods)))
[H.Normal] :
profiniteFenchelTotalRelation
(fun i => compactDiscreteNormalQuotientGeneratorImage
Δ hCompact hPeriods H
(ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
(fun i => compactDiscreteNormalQuotientGeneratorImage
Δ hCompact hPeriods H
(ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
(fun j => compactDiscreteNormalQuotientGeneratorImage
Δ hCompact hPeriods H
(ULift.up (ProfiniteFenchelGenerator.cusp j)))
(fun k => compactDiscreteNormalQuotientGeneratorImage
Δ hCompact hPeriods H
(ULift.up (ProfiniteFenchelGenerator.inertia k))) = 1The lifted compact discrete normal quotient satisfies the total Fenchel--Nielsen relation.
Show proof
by
apply
(MulEquiv.ulift :
ULift.{u, 0}
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H) ≃*
FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H).injective
simpa [compactDiscreteNormalQuotientGeneratorImage, profiniteFenchelTotalRelation,
map_list_prod, Function.comp_def, map_commutatorElement] using
compactDiscreteNormalQuotientGeneratorImage_total_relation
Δ hCompact hPeriods HProof. Use the discrete smooth quotient data and lift it through the profinite Fenchel presentation. Generator-image statements are checked on surface, cusp, and inertia generators; inertia-order and total-relation conditions are inherited from the discrete quotient, and the derived-length and smooth-data fields are transported through the normal quotient.
□private theorem compactDiscreteNormalQuotientGeneratorImage_period_relation
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hPeriods : 3 ≤ Δ.signature.numPeriods)
(H : Subgroup
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods)))
[H.Normal]
(k : Fin Δ.signature.numPeriods) :
compactDiscreteNormalQuotientGeneratorImageCore
Δ hCompact hPeriods H
(ULift.up (ProfiniteFenchelGenerator.inertia k)) ^
Δ.signature.periods k = 1The compact discrete normal quotient generator image satisfies each prescribed period relation.
Show proof
by
change
(QuotientGroup.mk' H
(ellipticElement
(compactFuchsianSignature Δ.signature hCompact hPeriods) k)) ^
(compactFuchsianSignature Δ.signature hCompact hPeriods).periods k = 1
rw [← map_pow, ellipticElement_pow_period_eq_one, map_one]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.
□private theorem compactDiscreteNormalQuotientGeneratorImage_lifted_period_relation
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hPeriods : 3 ≤ Δ.signature.numPeriods)
(H : Subgroup
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods)))
[H.Normal]
(k : Fin Δ.signature.numPeriods) :
compactDiscreteNormalQuotientGeneratorImage
Δ hCompact hPeriods H
(ULift.up (ProfiniteFenchelGenerator.inertia k)) ^
Δ.signature.periods k = 1The lifted compact discrete normal quotient generator image satisfies each prescribed period relation.
Show proof
by
apply
(MulEquiv.ulift :
ULift.{u, 0}
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H) ≃*
FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H).injective
simpa [compactDiscreteNormalQuotientGeneratorImage] using
compactDiscreteNormalQuotientGeneratorImage_period_relation
Δ hCompact hPeriods H kProof. 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.
□private theorem compactDiscreteNormalQuotient_derivedLength
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hPeriods : 3 ≤ Δ.signature.numPeriods)
(H : Subgroup
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods)))
[H.Normal]
(hHQuot :
SubgroupQuotientHasDerivedLengthAtMost H 3) :
derivedSeries
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H) 3 =
⊥The compact discrete normal quotient has derived length bounded by the given parameter.
Show proof
by
let σ := compactFuchsianSignature Δ.signature hCompact hPeriods
let q : FuchsianPresentedGroup σ →*
FuchsianPresentedGroup σ ⧸ H :=
QuotientGroup.mk' H
have hmap :
Subgroup.map q (derivedSeries (FuchsianPresentedGroup σ) 3) =
derivedSeries (FuchsianPresentedGroup σ ⧸ H) 3 :=
derivedSeries_map_surjective q (QuotientGroup.mk'_surjective H) 3
apply le_antisymm
· intro y hy
rw [← hmap] at hy
rcases hy with ⟨x, hx, rfl⟩
exact Subgroup.mem_bot.mpr
((QuotientGroup.eq_one_iff x).2 (hHQuot hx))
· exact bot_leProof. Use the discrete smooth quotient data and lift it through the profinite Fenchel presentation. Generator-image statements are checked on surface, cusp, and inertia generators; inertia-order and total-relation conditions are inherited from the discrete quotient, and the derived-length and smooth-data fields are transported through the normal quotient.
□private theorem compactDiscreteNormalQuotientGeneratorImage_inertia_order
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hPeriods : 3 ≤ Δ.signature.numPeriods)
(H : Subgroup
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods)))
[H.Normal]
(hHTF : IsTorsionFreeGroup H)
(k : Fin Δ.signature.numPeriods) :
orderOf
(compactDiscreteNormalQuotientGeneratorImageCore
Δ hCompact hPeriods H
(ULift.up (ProfiniteFenchelGenerator.inertia k))) =
Δ.signature.periods kThe compact discrete normal quotient sends each inertia generator to an element of the prescribed order.
Show proof
by
let σ := compactFuchsianSignature Δ.signature hCompact hPeriods
let q : FuchsianPresentedGroup σ →*
FuchsianPresentedGroup σ ⧸ H :=
QuotientGroup.mk' H
have hKerTF : IsTorsionFreeGroup q.ker := by
change IsTorsionFreeGroup (QuotientGroup.mk' H).ker
rw [QuotientGroup.ker_mk']
exact hHTF
have hFinite : IsOfFinOrder (ellipticElement σ k) := by
rw [← orderOf_pos_iff]
rw [compactPresentationHomToProfinite_elliptic_order Δ hCompact hPeriods k]
exact lt_of_lt_of_le (by decide : 0 < 2) (Δ.signature.period_ge_two k)
calc
orderOf
(compactDiscreteNormalQuotientGeneratorImageCore
Δ hCompact hPeriods H
(ULift.up (ProfiniteFenchelGenerator.inertia k))) =
orderOf (q (ellipticElement σ k)) := by
rfl
_ = orderOf (ellipticElement σ k) :=
orderOf_map_eq_of_torsionFree_ker q hKerTF hFinite
_ = Δ.signature.periods k :=
compactPresentationHomToProfinite_elliptic_order Δ hCompact hPeriods kProof. Use the discrete smooth quotient data and lift it through the profinite Fenchel presentation. Generator-image statements are checked on surface, cusp, and inertia generators; inertia-order and total-relation conditions are inherited from the discrete quotient, and the derived-length and smooth-data fields are transported through the normal quotient.
□private theorem compactDiscreteNormalQuotientGeneratorImage_lifted_inertia_order
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hPeriods : 3 ≤ Δ.signature.numPeriods)
(H : Subgroup
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods)))
[H.Normal]
(hHTF : IsTorsionFreeGroup H)
(k : Fin Δ.signature.numPeriods) :
orderOf
(compactDiscreteNormalQuotientGeneratorImage
Δ hCompact hPeriods H
(ULift.up (ProfiniteFenchelGenerator.inertia k))) =
Δ.signature.periods kThe lifted compact discrete normal quotient preserves the prescribed inertia-generator orders.
Show proof
by
have horder :=
orderOf_injective
((MulEquiv.ulift :
ULift.{u, 0}
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H) ≃*
FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H).toMonoidHom)
(MulEquiv.ulift :
ULift.{u, 0}
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H) ≃*
FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H).injective
(compactDiscreteNormalQuotientGeneratorImage Δ hCompact hPeriods H
(ULift.up (ProfiniteFenchelGenerator.inertia k)))
rw [← horder]
exact
compactDiscreteNormalQuotientGeneratorImage_inertia_order
Δ hCompact hPeriods H hHTF kProof. Use the discrete smooth quotient data and lift it through the profinite Fenchel presentation. Generator-image statements are checked on surface, cusp, and inertia generators; inertia-order and total-relation conditions are inherited from the discrete quotient, and the derived-length and smooth-data fields are transported through the normal quotient.
□private noncomputable def compactDiscreteNormalQuotientSmoothData
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hPeriods : 3 ≤ Δ.signature.numPeriods)
(H : Subgroup
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods)))
(hHFiniteIndex : H.FiniteIndex)
(hHNormal : H.Normal)
(hHTF : IsTorsionFreeGroup H)
(hHQuot : SubgroupQuotientHasDerivedLengthAtMost H 3) :
ProfiniteSmoothQuotientData Δ 3 := by
letI : H.Normal := hHNormal
letI : H.FiniteIndex := hHFiniteIndex
letI :
TopologicalSpace
(ULift.{u, 0}
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H)) :=
⊥
letI :
DiscreteTopology
(ULift.{u, 0}
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H)) :=
⟨rfl⟩
letI :
Finite
(ULift.{u, 0}
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods) ⧸ H)) := by
infer_instance
exact
ProfiniteSmoothQuotientData.ofPresentationLiftToFiniteOfRelationsOfDerivedSeries
Δ (compactDiscreteNormalQuotientGeneratorImage Δ hCompact hPeriods H)
(compactDiscreteNormalQuotientGeneratorImage_lifted_total_relation
Δ hCompact hPeriods H)
(compactDiscreteNormalQuotientGeneratorImage_lifted_period_relation
Δ hCompact hPeriods H)
(derivedSeries_ulift_eq_bot_of
(compactDiscreteNormalQuotient_derivedLength
Δ hCompact hPeriods H hHQuot))
(compactDiscreteNormalQuotientGeneratorImage_lifted_inertia_order
Δ hCompact hPeriods H hHTF)The smooth quotient data obtained from the compact discrete normal quotient.
private theorem compactDiscrete_sourceSubgroup_exists_of_isNonPerfect_zeroGenus
(Δ : ProfiniteFGroup.{u})
(hNonPerfect : Δ.IsNonPerfect)
(hCompact : Δ.signature.IsCompact)
(hZero : Δ.signature.orbitGenus = 0)
(hPeriods : 3 ≤ Δ.signature.numPeriods) :
∃ H : Subgroup
(FuchsianPresentedGroup
(compactFuchsianSignature Δ.signature hCompact hPeriods)),
H.FiniteIndex ∧ IsTorsionFreeGroup H ∧
SubgroupQuotientHasDerivedLengthAtMost H 3Show proof
by
classical
let σ := compactFuchsianSignature Δ.signature hCompact hPeriods
have hZeroσ : σ.orbitGenus = 0 := by
simpa [σ, compactFuchsianSignature] using hZero
rcases
exists_prime_dvd_two_periods_of_isNonPerfect_zeroGenus_noCusps
Δ hNonPerfect hZero hCompact with
⟨p, hpPrime, i, j, hij, hpi, hpj⟩
let D : FirstReductionPeriodData σ :=
firstReductionPeriodDataOfPrimePair σ hpPrime hij
(by simpa [σ, compactFuchsianSignature] using hpi)
(by simpa [σ, compactFuchsianSignature] using hpj)
exact threeStep_sourceSubgroup_exists_of_zeroGenus_periodData σ hZeroσ DProof. 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 compactDiscreteBridge_threeStep_normal_of_isNonPerfect
(Δ : ProfiniteFGroup.{u})
(hNonPerfect : Δ.IsNonPerfect)
(hCompact : Δ.signature.IsCompact)
(hZero : Δ.signature.orbitGenus = 0)
(hPeriods : 3 ≤ Δ.signature.numPeriods) :
HasTorsionFreeOpenNormalSubgroupQuotientDerivedLengthAtMost
Δ.carrier 3Show proof
by
classical
let σ := compactFuchsianSignature Δ.signature hCompact hPeriods
rcases compactDiscrete_sourceSubgroup_exists_of_isNonPerfect_zeroGenus
Δ hNonPerfect hCompact hZero hPeriods with
⟨Hsource, hHsourceFiniteIndex, hHsourceTF, hHsourceQuot⟩
haveI : Hsource.FiniteIndex := hHsourceFiniteIndex
rcases
hasFiniteIndexTorsionFreeNormalSubgroupWithDerivedLengthAtMost_of_subgroup
Hsource hHsourceTF hHsourceQuot with
⟨H, hHFiniteIndex, hHNormal, hHTF, hHQuot⟩
exact
(compactDiscreteNormalQuotientSmoothData
Δ hCompact hPeriods H hHFiniteIndex hHNormal hHTF hHQuot
).has_torsionFreeOpenNormal_quotient_derivedLengthAtMostProof. Use the discrete smooth quotient data and lift it through the profinite Fenchel presentation. Generator-image statements are checked on surface, cusp, and inertia generators; inertia-order and total-relation conditions are inherited from the discrete quotient, and the derived-length and smooth-data fields are transported through the normal quotient.
□