FenchelNielsenZomorrodian.Profinite.SmoothQuotient
This module develops Fenchel--Nielsen--Zomorrodian presentation reductions, period relations, reindexings, and quotient maps.
structure ProfiniteSmoothQuotientData
(Δ : ProfiniteFGroup.{u}) (m : ℕ) where
Q : Type u
[group : Group Q]
[topologicalSpace : TopologicalSpace Q]
[discreteTopology : DiscreteTopology Q]
[isTopologicalGroup : IsTopologicalGroup Q]
[finite : Finite Q]
φ : Δ.carrier →ₜ* Q
derived_length : profiniteDerivedSeries Q m = ⊥
inertia_exact :
∀ i : Fin Δ.signature.numPeriods,
orderOf (φ (Δ.inertia i)) = Δ.signature.periods iA finite smooth quotient of a profinite F-group. The datum is the profinite analogue of the finite smooth quotient data used on the discrete side: the target is finite and discrete, the quotient has derived length at most m, and each inertia generator maps to an element of exactly the prescribed period.
def kernelOpenNormal {Δ : ProfiniteFGroup.{u}} {m : ℕ}
(D : ProfiniteSmoothQuotientData Δ m) :
OpenNormalSubgroup Δ.carrier :=
OpenNormalSubgroup.ker D.φThe open normal kernel attached to a finite smooth quotient.
@[simp] theorem mem_kernelOpenNormal
{Δ : ProfiniteFGroup.{u}} {m : ℕ}
{D : ProfiniteSmoothQuotientData Δ m} {x : Δ.carrier} :
x ∈ (D.kernelOpenNormal : Subgroup Δ.carrier) ↔ D.φ x = 1Membership in the kernel open normal subgroup is equality to \(1\) after applying \(\varphi\).
Show proof
by
rflProof. 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 topDerived_le_kernel
{Δ : ProfiniteFGroup.{u}} {m : ℕ}
(D : ProfiniteSmoothQuotientData Δ m) :
profiniteDerivedSeries Δ.carrier m ≤
(D.kernelOpenNormal : Subgroup Δ.carrier)The \(m\)-th profinite derived subgroup is contained in the kernel of the quotient map.
Show proof
by
intro x hx
have hxImage :
D.φ x ∈ profiniteDerivedSeries D.Q m :=
topDerivedTop_le_comap (f := D.φ) (m := m) hx
have hxBot : D.φ x ∈ (⊥ : Subgroup D.Q) := by
simpa [D.derived_length] using hxImage
exact Subgroup.mem_bot.mp hxBotProof. 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 kernel_quotient_has_derivedLengthAtMost
{Δ : ProfiniteFGroup.{u}} {m : ℕ}
(D : ProfiniteSmoothQuotientData Δ m) :
ProfiniteOpenNormalQuotientHasDerivedLengthAtMost
Δ.carrier D.kernelOpenNormal mThe quotient by the kernel has derived length at most the quotient datum bound.
Show proof
ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.of_topDerived_le
D.kernelOpenNormal D.topDerived_le_kernelProof. 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 kernel_avoidsNontrivialInertia
{Δ : ProfiniteFGroup.{u}} {m : ℕ}
(D : ProfiniteSmoothQuotientData Δ m) :
Δ.avoidsNontrivialInertia D.kernelOpenNormalThe smooth quotient kernel avoids all nontrivial inertia powers.
Show proof
by
intro i n hn
have hφpow : D.φ (Δ.inertia i ^ n) = 1 := by
simpa using (mem_kernelOpenNormal (D := D)).1 hn
have hImagePow : D.φ (Δ.inertia i) ^ n = 1 := by
simpa [MonoidHom.map_zpow] using hφpow
have hdivImage : (orderOf (D.φ (Δ.inertia i)) : ℤ) ∣ n :=
orderOf_dvd_iff_zpow_eq_one.mpr hImagePow
have hdivSource : (orderOf (Δ.inertia i) : ℤ) ∣ n := by
rw [Δ.inertia_order i, ← D.inertia_exact i]
exact hdivImage
exact orderOf_dvd_iff_zpow_eq_one.mp hdivSourceProof. 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 kernel_torsionFree
{Δ : ProfiniteFGroup.{u}} {m : ℕ}
(D : ProfiniteSmoothQuotientData Δ m) :
ProfiniteOpenNormalSubgroupTorsionFree
Δ.carrier D.kernelOpenNormalThe kernel attached to profinite smooth quotient data is torsion-free.
Show proof
torsionFree_of_avoidsNontrivialInertia
Δ D.kernelOpenNormal D.kernel_avoidsNontrivialInertiaProof. Unfold the arithmetic, signature, quotient, or subgroup definition named in the statement. The result is a direct numerical, topological, or kernel-property calculation rather than a generic presentation-relator check.
□theorem has_torsionFreeOpenNormal_quotient_derivedLengthAtMost
{Δ : ProfiniteFGroup.{u}} {m : ℕ}
(D : ProfiniteSmoothQuotientData Δ m) :
HasTorsionFreeOpenNormalSubgroupQuotientDerivedLengthAtMost
Δ.carrier mA smooth quotient datum gives a torsion-free open normal subgroup with bounded quotient.
Show proof
⟨D.kernelOpenNormal, D.kernel_torsionFree,
D.kernel_quotient_has_derivedLengthAtMost⟩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 has_torsionFreeOpenNormal_quotient_derivedLength_le
{Δ : ProfiniteFGroup.{u}} {m n : ℕ}
(D : ProfiniteSmoothQuotientData Δ m) (hmn : m ≤ n) :
HasTorsionFreeOpenNormalSubgroupQuotientDerivedLengthAtMost
Δ.carrier nThe quotient derived-length bound is monotone in the target bound.
Show proof
HasTorsionFreeOpenNormalSubgroupQuotientDerivedLengthAtMost.mono
hmn D.has_torsionFreeOpenNormal_quotient_derivedLengthAtMostProof. 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.
□noncomputable def ofPresentationLiftToFiniteOfRelations
(Δ : ProfiniteFGroup.{u}) {m : ℕ}
{A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A]
[IsTopologicalGroup 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)
(hDerived : profiniteDerivedSeries A m = ⊥)
(hInertiaExact :
∀ i : Fin Δ.signature.numPeriods,
orderOf (χ (ULift.up (ProfiniteFenchelGenerator.inertia i))) =
Δ.signature.periods i) :
ProfiniteSmoothQuotientData Δ m where
Q := A
φ := Δ.presentationLiftToFiniteOfRelations χ hTotal hPeriod
derived_length := hDerived
inertia_exact := by
intro i
simpa [presentationLiftToFiniteOfRelations] using hInertiaExact iBuild profinite smooth quotient data from a finite target assignment satisfying the Fenchel--Nielsen presentation relations.
noncomputable def ofPresentationLiftToFiniteOfRelationsOfDerivedSeries
(Δ : ProfiniteFGroup.{u}) {m : ℕ}
{A : Type u} [Group A] [TopologicalSpace A] [DiscreteTopology A]
[IsTopologicalGroup 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)
(hDerived : derivedSeries A m = ⊥)
(hInertiaExact :
∀ i : Fin Δ.signature.numPeriods,
orderOf (χ (ULift.up (ProfiniteFenchelGenerator.inertia i))) =
Δ.signature.periods i) :
ProfiniteSmoothQuotientData Δ m :=
ofPresentationLiftToFiniteOfRelations
Δ χ hTotal hPeriod
(by
rw [profiniteDerivedSeries_eq_derivedSeries_of_discrete]
exact hDerived)
hInertiaExactBuild profinite smooth quotient data from a finite discrete target whose abstract derived series has the requested length.