FenchelNielsenZomorrodian.Profinite.CuspedQuotient
This module develops Fenchel--Nielsen--Zomorrodian presentation reductions, period relations, reindexings, and quotient maps.
import
private theorem ulift_list_prod_down {α : Type v} [Monoid α]
(xs : List (ULift.{u, v} α)) :
xs.prod.down = (xs.map (fun x => x.down)).prodThe lifted list product descends to the corresponding profinite product.
Show proof
by
induction xs with
| nil =>
rfl
| cons x xs ih =>
simp only [List.prod_cons, ULift.mul_down, ih, List.map_cons]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.
□private def firstCusp (σ : FenchelSignature) (hCusps : σ.HasCusps) : Fin σ.numCusps :=
⟨0, hCusps⟩The distinguished cusp used to cancel the total relation in the direct cusped quotient.
abbrev CuspedSmoothQuotient (σ : FenchelSignature) :=
Multiplicative (FenchelPeriodCoordinate σ)instance instTopologicalSpaceCuspedSmoothQuotient (σ : FenchelSignature) :
TopologicalSpace (CuspedSmoothQuotient σ) :=
⊥The cusped smooth quotient carries the topology induced by its finite quotient construction.
instance instDiscreteTopologyCuspedSmoothQuotient (σ : FenchelSignature) :
DiscreteTopology (CuspedSmoothQuotient σ) :=
⟨rfl⟩The cusped smooth quotient carries the discrete topology at the finite quotient stage.
noncomputable instance instFiniteULiftCuspedSmoothQuotient (σ : FenchelSignature) :
Finite (ULift.{u, 0} (CuspedSmoothQuotient σ)) := by
letI : Finite (FenchelPeriodCoordinate σ) :=
zmodCoordinateFamily_finite σ.periods
(fun i => lt_of_lt_of_le (by decide : 0 < 2) (σ.period_ge_two i))
infer_instanceThe lifted cusped smooth quotient type is finite.
def cuspedSmoothGeneratorImageCore
(σ : FenchelSignature) (hCusps : σ.HasCusps) :
ProfiniteFenchelGeneratorIndex.{u} σ → CuspedSmoothQuotient σ
| ULift.up (.surfaceA _) => 1
| ULift.up (.surfaceB _) => 1
| ULift.up (.cusp j) =>
if j = firstCusp σ hCusps then
Multiplicative.ofAdd (-(fenchelPeriodBasisSum σ))
else
1
| ULift.up (.inertia k) =>
Multiplicative.ofAdd (fenchelPeriodBasisVector σ k)def cuspedSmoothGeneratorImage
(Δ : ProfiniteFGroup.{u}) (hCusps : Δ.signature.HasCusps) :
ProfiniteFenchelGeneratorIndex.{u} Δ.signature →
ULift.{u, 0} (CuspedSmoothQuotient Δ.signature) :=
fun x => ULift.up (cuspedSmoothGeneratorImageCore Δ.signature hCusps x)The cusped smooth generator image is the direct cusped quotient, universe-lifted to match the carrier of \(\Delta\).
private theorem cuspedSmooth_inertia_list_product
(σ : FenchelSignature) (hCusps : σ.HasCusps) :
(List.map
(fun k : Fin σ.numPeriods =>
cuspedSmoothGeneratorImageCore (σ := σ) hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k)))
(List.finRange σ.numPeriods)).prod =
Multiplicative.ofAdd (fenchelPeriodBasisSum σ)The cusped smooth generator list product gives the required relation.
Show proof
by
rw [show
(fun k : Fin σ.numPeriods =>
cuspedSmoothGeneratorImageCore (σ := σ) hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k))) =
fun k : Fin σ.numPeriods =>
Multiplicative.ofAdd (fenchelPeriodBasisVector σ k) by
funext k
simp only [cuspedSmoothGeneratorImageCore]]
calc
(List.map
(fun k : Fin σ.numPeriods =>
Multiplicative.ofAdd (fenchelPeriodBasisVector σ k))
(List.finRange σ.numPeriods)).prod =
∏ k : Fin σ.numPeriods,
Multiplicative.ofAdd (fenchelPeriodBasisVector σ k) := by
simpa using
(Fin.prod_univ_def
(f := fun k : Fin σ.numPeriods =>
Multiplicative.ofAdd (fenchelPeriodBasisVector σ k))).symm
_ = Multiplicative.ofAdd (fenchelPeriodBasisSum σ) := by
symm
exact ofAdd_sum
(s := Finset.univ)
(f := fun k : Fin σ.numPeriods => fenchelPeriodBasisVector σ k)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.
□private theorem cuspedSmooth_cusp_list_product
(σ : FenchelSignature) (hCusps : σ.HasCusps) :
(List.map
(fun j : Fin σ.numCusps =>
cuspedSmoothGeneratorImageCore (σ := σ) hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.cusp j)))
(List.finRange σ.numCusps)).prod =
Multiplicative.ofAdd (-(fenchelPeriodBasisSum σ))The cusped smooth generator list product gives the required relation.
Show proof
by
classical
calc
(List.map
(fun j : Fin σ.numCusps =>
cuspedSmoothGeneratorImageCore (σ := σ) hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.cusp j)))
(List.finRange σ.numCusps)).prod =
∏ j : Fin σ.numCusps,
cuspedSmoothGeneratorImageCore (σ := σ) hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.cusp j)) := by
simpa using
(Fin.prod_univ_def
(f := fun j : Fin σ.numCusps =>
cuspedSmoothGeneratorImageCore (σ := σ) hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.cusp j)))).symm
_ = Multiplicative.ofAdd (-(fenchelPeriodBasisSum σ)) := by
rw [Finset.prod_eq_single (firstCusp σ hCusps)]
· simp only [cuspedSmoothGeneratorImageCore, ↓reduceIte, ofAdd_neg]
· intro j _hj hj
simp only [cuspedSmoothGeneratorImageCore, hj, ↓reduceIte]
· intro hnot
exact False.elim (hnot (Finset.mem_univ _))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.
□private theorem cuspedSmoothGeneratorImage_total_relation
(Δ : ProfiniteFGroup.{u}) (hCusps : Δ.signature.HasCusps) :
profiniteFenchelTotalRelation
(fun i => cuspedSmoothGeneratorImageCore Δ.signature hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.surfaceA i)))
(fun i => cuspedSmoothGeneratorImageCore Δ.signature hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.surfaceB i)))
(fun j => cuspedSmoothGeneratorImageCore Δ.signature hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.cusp j)))
(fun k => cuspedSmoothGeneratorImageCore Δ.signature hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k))) = 1The cusped smooth generator images satisfy the total relation.
Show proof
by
dsimp [profiniteFenchelTotalRelation]
rw [cuspedSmooth_cusp_list_product, cuspedSmooth_inertia_list_product]
simp only [cuspedSmoothGeneratorImageCore, commutatorElement_self, List.map_const', List.length_finRange,
List.prod_replicate, one_pow, ofAdd_neg, one_mul, inv_mul_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. 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.
□private theorem cuspedSmoothGeneratorImage_lifted_total_relation
(Δ : ProfiniteFGroup.{u}) (hCusps : Δ.signature.HasCusps) :
profiniteFenchelTotalRelation
(fun i => cuspedSmoothGeneratorImage Δ hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.surfaceA i)))
(fun i => cuspedSmoothGeneratorImage Δ hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.surfaceB i)))
(fun j => cuspedSmoothGeneratorImage Δ hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.cusp j)))
(fun k => cuspedSmoothGeneratorImage Δ hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k))) = 1The cusped smooth generator images satisfy the total relation.
Show proof
by
let e :
ULift.{u, 0} (CuspedSmoothQuotient Δ.signature) ≃*
CuspedSmoothQuotient Δ.signature :=
MulEquiv.ulift
apply e.injective
simp only [MulEquiv.ulift, profiniteFenchelTotalRelation, cuspedSmoothGeneratorImage, MulEquiv.coe_mk,
Equiv.ulift_apply, ULift.mul_down, ULift.one_down, e]
rw [ulift_list_prod_down, ulift_list_prod_down, ulift_list_prod_down]
have h := cuspedSmoothGeneratorImage_total_relation Δ hCusps
dsimp [profiniteFenchelTotalRelation] at h
simpa [List.map_map, Function.comp_def, commutatorElement,
cuspedSmoothGeneratorImageCore] using hProof. 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. 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.
□private theorem cuspedSmoothGeneratorImage_period_relation
(Δ : ProfiniteFGroup.{u}) (hCusps : Δ.signature.HasCusps)
(k : Fin Δ.signature.numPeriods) :
cuspedSmoothGeneratorImageCore Δ.signature hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k)) ^
Δ.signature.periods k = 1The cusped smooth generator image satisfies each prescribed period relation.
Show proof
by
change
Multiplicative.ofAdd (fenchelPeriodBasisVector Δ.signature k) ^
Δ.signature.periods k = 1
rw [← ofAdd_nsmul]
rw [show
Δ.signature.periods k • fenchelPeriodBasisVector Δ.signature k = 0 by
simpa [fenchelPeriodBasisVector] using
zmodBasisVector_nsmul_eq_zero Δ.signature.periods k]
rflProof. 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 cuspedSmoothGeneratorImage_lifted_period_relation
(Δ : ProfiniteFGroup.{u}) (hCusps : Δ.signature.HasCusps)
(k : Fin Δ.signature.numPeriods) :
cuspedSmoothGeneratorImage Δ hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k)) ^
Δ.signature.periods k = 1The lifted cusped smooth generator image satisfies each prescribed period relation.
Show proof
by
let e :
ULift.{u, 0} (CuspedSmoothQuotient Δ.signature) ≃*
CuspedSmoothQuotient Δ.signature :=
MulEquiv.ulift
apply e.injective
simp only [MulEquiv.ulift, cuspedSmoothGeneratorImage, MulEquiv.coe_mk, Equiv.ulift_apply, ULift.pow_down,
ULift.one_down, e]
exact cuspedSmoothGeneratorImage_period_relation Δ hCusps 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 cuspedSmoothGeneratorImage_inertia_order
(Δ : ProfiniteFGroup.{u}) (hCusps : Δ.signature.HasCusps)
(k : Fin Δ.signature.numPeriods) :
orderOf
(cuspedSmoothGeneratorImageCore Δ.signature hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k))) =
Δ.signature.periods kThe image of a cusped smooth generator has the prescribed inertia order.
Show proof
by
rw [cuspedSmoothGeneratorImageCore, orderOf_ofAdd_eq_addOrderOf]
exact zmodBasisVector_addOrderOf Δ.signature.periods kProof. 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.
□private theorem cuspedSmoothGeneratorImage_lifted_inertia_order
(Δ : ProfiniteFGroup.{u}) (hCusps : Δ.signature.HasCusps)
(k : Fin Δ.signature.numPeriods) :
orderOf
(cuspedSmoothGeneratorImage Δ hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k))) =
Δ.signature.periods kThe image of a cusped smooth generator has the prescribed inertia order.
Show proof
by
let e :
ULift.{u, 0} (CuspedSmoothQuotient Δ.signature) ≃*
CuspedSmoothQuotient Δ.signature :=
MulEquiv.ulift
have horder :=
orderOf_injective
e.toMonoidHom
e.injective
(cuspedSmoothGeneratorImage Δ hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k)))
have hcore :
orderOf
(e.toMonoidHom (cuspedSmoothGeneratorImage Δ hCusps
(ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k)))) =
Δ.signature.periods k := by
exact cuspedSmoothGeneratorImage_inertia_order Δ hCusps k
exact horder.symm.trans hcoreProof. 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 cuspedSmoothQuotientData
(Δ : ProfiniteFGroup.{u}) (hCusps : Δ.signature.HasCusps) :
ProfiniteSmoothQuotientData Δ 1 :=
ProfiniteSmoothQuotientData.ofPresentationLiftToFiniteOfRelations
Δ (cuspedSmoothGeneratorImage Δ hCusps)
(cuspedSmoothGeneratorImage_lifted_total_relation Δ hCusps)
(cuspedSmoothGeneratorImage_lifted_period_relation Δ hCusps)
(profiniteDerivedSeries_one_eq_bot_of_commGroup
(ULift.{u, 0} (CuspedSmoothQuotient Δ.signature)))
(cuspedSmoothGeneratorImage_lifted_inertia_order Δ hCusps)The smooth quotient data for the cusped profinite F-group quotient.