FenchelNielsenZomorrodian.Discrete.Core.EllipticCompact
This module studies elliptic compact for fenchel nielsen zomorrodian. An elliptic element of a compact Fuchsian signature is one of the specified elliptic generators. In the Fuchsian presented group, each elliptic element raised to its specified period is the identity.
Imported by
def ellipticElement (σ : FuchsianSignature) (i : Fin σ.numPeriods) :
FuchsianPresentedGroup σ :=
PresentedGroup.of (rels := relators σ) (FuchsianGenerator.elliptic i)An elliptic element of a compact Fuchsian signature is one of the specified elliptic generators.
@[simp] theorem ellipticElement_pow_period_eq_one
(σ : FuchsianSignature) (i : Fin σ.numPeriods) :
ellipticElement σ i ^ σ.periods i = 1In the Fuchsian presented group, each elliptic element raised to its specified period is the identity.
Show proof
by
simpa [ellipticElement, xWord] using
(PresentedGroup.one_of_mem (rels := relators σ)
(x := (xWord σ i) ^ σ.periods i) (Or.inl ⟨i, rfl⟩))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. 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.
□theorem ellipticElement_pow_eq_one_of_period_dvd
(σ : FuchsianSignature) (i : Fin σ.numPeriods) {n : ℕ}
(hdiv : σ.periods i ∣ n) :
ellipticElement σ i ^ n = 1If the elliptic period divides the exponent, the corresponding positive power is the identity.
Show proof
by
rcases hdiv with ⟨k, rfl⟩
rw [pow_mul, ellipticElement_pow_period_eq_one, one_pow]Proof. Use the defining period relation for the elliptic generator. A positive or integer exponent divisible by the period is rewritten as a multiple of the period, so the corresponding power is the identity.
□theorem ellipticElement_zpow_eq_one_of_period_int_dvd
(σ : FuchsianSignature) (i : Fin σ.numPeriods) {n : ℤ}
(hdiv : (σ.periods i : ℤ) ∣ n) :
ellipticElement σ i ^ n = 1If the elliptic period divides the integer exponent, the corresponding integer power is the identity.
Show proof
by
rcases hdiv with ⟨k, rfl⟩
rw [zpow_mul, zpow_natCast, ellipticElement_pow_period_eq_one, one_zpow]Proof. Use the defining period relation for the elliptic generator. A positive or integer exponent divisible by the period is rewritten as a multiple of the period, so the corresponding power is the identity.
□