FenchelNielsenZomorrodian.Discrete.FiniteIndex.Smooth
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
structure SmoothQuotientData
(G : Type*) [Group G]
(ι : Type*) (periods : ι → ℕ) (elliptic : ι → G)
(m : ℕ) where
Q : Type
[group : Group Q]
[finite : Finite Q]
φ : G →* Q
derived_length : derivedSeries Q m = ⊥
elliptic_exact : ∀ i : ι, orderOf (φ (elliptic i)) = periods iData for a smooth quotient of a Fenchel--Nielsen--Zomorrodian group.
def kernel {G : Type*} [Group G] {ι : Type*} {periods : ι → ℕ}
{elliptic : ι → G} {m : ℕ}
(D : SmoothQuotientData G ι periods elliptic m) : Subgroup G := by
letI : Group D.Q := D.group
exact D.φ.kerThe kernel subgroup of the finite smooth quotient map.
theorem kernel_quotient_has_derivedLengthAtMost
{G : Type*} [Group G] {ι : Type*} {periods : ι → ℕ}
{elliptic : ι → G} {m : ℕ}
(D : SmoothQuotientData G ι periods elliptic m) :
SubgroupQuotientHasDerivedLengthAtMost D.kernel mThe quotient by the kernel has derived length at most the quotient datum bound.
Show proof
by
intro g hg
letI : Group D.Q := D.group
change g ∈ D.φ.ker
rw [MonoidHom.mem_ker]
have hmap : D.φ g ∈ (derivedSeries G m).map D.φ := by
exact ⟨g, hg, rfl⟩
have hle : (derivedSeries G m).map D.φ ≤ derivedSeries D.Q m :=
map_derivedSeries_le_derivedSeries D.φ m
have hderived : D.φ g ∈ derivedSeries D.Q m := hle hmap
rw [D.derived_length] at hderived
simpa using hderivedProof. 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. 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. For the Fenchel--Nielsen--Zomorrodian relations, the period calculation checks that each elliptic generator has image of the prescribed order, and the product relation is verified by multiplying the images in the stated order. Divisibility, lcm, or gcd hypotheses are used precisely to make the period relators vanish in the target quotient.
□theorem source_element_eq_one_of_kernel_conjugate_elliptic_zpow
{G : Type*} [Group G] {ι : Type*} {periods : ι → ℕ}
{elliptic : ι → G} {m : ℕ}
(D : SmoothQuotientData G ι periods elliptic m)
(hEllipticZPow :
∀ i : ι, ∀ n : ℤ, (periods i : ℤ) ∣ n → elliptic i ^ n = 1)
(g : G)
(hgKernel : g ∈ D.kernel)
(hConj : ∃ i : ι, ∃ n : ℤ, IsConj g (elliptic i ^ n)) :
g = 1A kernel element conjugate to an elliptic power is trivial when the finite quotient detects the elliptic order and elliptic powers vanish exactly at multiples of the period.
Show proof
by
letI : Group D.Q := D.group
have hgKernel_eq : D.φ g = 1 := by
change g ∈ D.φ.ker at hgKernel
exact MonoidHom.mem_ker.mp hgKernel
rcases hConj with ⟨i, n, hconj⟩
have hφconj : IsConj (D.φ g) (D.φ (elliptic i ^ n)) :=
D.φ.map_isConj hconj
have hφtarget : D.φ (elliptic i ^ n) = 1 := by
exact isConj_one_right.mp <| by simpa [hgKernel_eq] using hφconj
have hdiv : (periods i : ℤ) ∣ n := by
rw [← D.elliptic_exact i]
exact orderOf_dvd_iff_zpow_eq_one.mpr (by
simpa [MonoidHom.map_zpow] using hφtarget)
have htargetOne : elliptic i ^ n = 1 :=
hEllipticZPow i n hdiv
exact isConj_one_left.mp <| by simpa [htargetOne] using hconjProof. 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. 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_of_finiteOrderClassification
{G : Type*} [Group G] {ι : Type*} {periods : ι → ℕ}
{elliptic : ι → G} {m : ℕ}
(D : SmoothQuotientData G ι periods elliptic m)
(hEllipticZPow :
∀ i : ι, ∀ n : ℤ, (periods i : ℤ) ∣ n → elliptic i ^ n = 1)
(hFiniteOrder :
∀ g : G, IsOfFinOrder g →
g = 1 ∨ ∃ i : ι, ∃ n : ℤ, IsConj g (elliptic i ^ n)) :
IsTorsionFreeGroup D.kernelThe smooth quotient kernel is torsion-free when every finite-order source element is either trivial or conjugate to an elliptic power.
Show proof
by
intro g hgfin
have hgfinSource : IsOfFinOrder (g : G) := by
simpa using
(Submonoid.isOfFinOrder_coe
(H := D.kernel.toSubmonoid) (x := g)).2 hgfin
rcases hFiniteOrder (g : G) hgfinSource with hgOne | hConj
· exact Subtype.ext hgOne
· exact Subtype.ext
(D.source_element_eq_one_of_kernel_conjugate_elliptic_zpow
hEllipticZPow (g : G) g.2 hConj)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. 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 sourceSubgroup_exists_of_finiteOrderClassification
{G : Type*} [Group G] {ι : Type*} {periods : ι → ℕ}
{elliptic : ι → G} {m : ℕ}
(D : SmoothQuotientData G ι periods elliptic m)
(hEllipticZPow :
∀ i : ι, ∀ n : ℤ, (periods i : ℤ) ∣ n → elliptic i ^ n = 1)
(hFiniteOrder :
∀ g : G, IsOfFinOrder g →
g = 1 ∨ ∃ i : ι, ∃ n : ℤ, IsConj g (elliptic i ^ n)) :
∃ L : Subgroup G,
L.FiniteIndex ∧ IsTorsionFreeGroup L ∧
SubgroupQuotientHasDerivedLengthAtMost L mThe source subgroup associated with the smooth quotient exists under the finite-order classification hypothesis.
Show proof
by
have hfinite : D.kernel.FiniteIndex := by
letI : Group D.Q := D.group
letI : Finite D.Q := D.finite
change D.φ.ker.FiniteIndex
exact Subgroup.finiteIndex_of_finite_quotient
exact ⟨D.kernel, hfinite,
D.kernel_torsionFree_of_finiteOrderClassification
hEllipticZPow hFiniteOrder,
D.kernel_quotient_has_derivedLengthAtMost⟩Proof. Check the quotient data on the named elliptic, surface, cusp, and boundary generators. The period, power, and product relators follow from the displayed order and product calculations, so the presentation universal property supplies the quotient map; derived-length, smoothness, and profinite fields are inherited from the finite or profinite quotient construction.
□