FenchelNielsenZomorrodian.Discrete.Torsion.FuchsianFiniteSubgroupFrontier
import
- FenchelNielsenZomorrodian.Discrete.Core.EllipticCompact
- Mathlib.GroupTheory.OrderOfElement
def subgroup_le_conj_ellipticStabilizer
(σ : FuchsianSignature) (K : Subgroup (FuchsianPresentedGroup σ)) : Prop :=
∃ i : Fin σ.numPeriods, ∃ c : FuchsianPresentedGroup σ,
∀ k : K, ∃ n : ℤ,
(k : FuchsianPresentedGroup σ) =
c * ellipticElement σ i ^ n * c⁻¹
/- FRONTIER `fuchsian-finite-subgroup-elliptic-stabilizer`.
This is the sole approved discrete axiom frontier in `FenchelNielsen`. It is the compact
no-cusp presentation currently consumed by the compact Fuchsian three-step route. -/A subgroup is contained in a conjugate of one elliptic stabilizer, up to powers.
axiom finiteSubgroup_le_conj_ellipticStabilizer
(σ : FuchsianSignature)
(K : Subgroup (FuchsianPresentedGroup σ)) [Finite K]
(hK : K ≠ ⊥) :
subgroup_le_conj_ellipticStabilizer σ KFinite nontrivial Fuchsian subgroups lie in conjugates of elliptic stabilizers.
theorem finiteOrder_isConj_elliptic_zpow_of_frontier
{G ι : Type*} [Group G] (elliptic : ι → G)
(frontier : ∀ K : Subgroup G, Finite K → K ≠ ⊥ →
∃ i : ι, ∃ c : G, ∀ k : K, ∃ n : ℤ,
(k : G) = c * elliptic i ^ n * c⁻¹)
(g : G) (hg : IsOfFinOrder g) (hgne : g ≠ 1) :
∃ i : ι, ∃ n : ℤ, IsConj g (elliptic i ^ n)Finite nontrivial Fuchsian subgroups lie in conjugates of elliptic stabilizers.
Show proof
by
classical
let K : Subgroup G := Subgroup.zpowers g
letI : Fintype K := Fintype.ofEquiv (Fin (orderOf g)) (finEquivZPowers hg)
let hKfinite : Finite K := Finite.of_fintype K
have hKne : K ≠ ⊥ := by
intro hK
have hgmem : g ∈ K := Subgroup.mem_zpowers g
have hgbot : g ∈ (⊥ : Subgroup G) := by
simpa [K, hK] using hgmem
exact hgne (Subgroup.mem_bot.mp hgbot)
rcases frontier K hKfinite hKne with ⟨i, c, hcontain⟩
rcases hcontain ⟨g, Subgroup.mem_zpowers g⟩ with ⟨n, hn⟩
exact ⟨i, n, (isConj_iff.2 ⟨c, hn.symm⟩).symm⟩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. 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 finiteOrder_eq_one_or_isConj_elliptic_zpow_of_frontier
{G ι : Type*} [Group G] (elliptic : ι → G)
(frontier : ∀ K : Subgroup G, Finite K → K ≠ ⊥ →
∃ i : ι, ∃ c : G, ∀ k : K, ∃ n : ℤ,
(k : G) = c * elliptic i ^ n * c⁻¹)
(g : G) (hg : IsOfFinOrder g) :
g = 1 ∨ ∃ i : ι, ∃ n : ℤ, IsConj g (elliptic i ^ n)A finite-order element is either trivial or conjugate to a power of an elliptic generator.
Show proof
by
by_cases hgne : g = 1
· exact Or.inl hgne
· exact Or.inr
(finiteOrder_isConj_elliptic_zpow_of_frontier elliptic frontier g hg hgne)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. 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.
□