FenchelNielsenZomorrodian.Discrete.Core.Signature
This module develops the rewriting and basis constructions behind the subgroup calculations. It tracks words and relations through the chosen transversal to obtain the required presentation or basis statements.
import
- FenchelNielsenZomorrodian.Discrete.Arithmetic.FamilyLcm
- Mathlib.Tactic.Linarith
Imported by
- FenchelNielsenZomorrodian.Discrete
- FenchelNielsenZomorrodian.Discrete.Coordinates.FenchelPeriodCoordinate
- FenchelNielsenZomorrodian.Discrete.Core
- FenchelNielsenZomorrodian.Discrete.Core.CompactFuchsianPresentation
- FenchelNielsenZomorrodian.Discrete.Singerman.KernelTransport
- FenchelNielsenZomorrodian.Profinite.FGroup
structure FenchelSignature where
orbitGenus : ℕ
numCusps : ℕ
numPeriods : ℕ
periods : Fin numPeriods → ℕ
period_ge_two : ∀ i, 2 ≤ periods iThe signature data for a Fenchel--Nielsen compact Fuchsian presentation.
def FenchelSignature.eulerCharacteristic (σ : FenchelSignature) : ℚ :=
(2 : ℚ) - 2 * σ.orbitGenus - σ.numCusps -
∑ i : Fin σ.numPeriods, (1 - ((σ.periods i : ℚ)⁻¹))Euler characteristic of a Fenchel signature.
def FenchelSignature.hyperbolicDefect (σ : FenchelSignature) : ℚ :=
-(σ.eulerCharacteristic)The hyperbolic defect associated with a Fenchel signature.
def FenchelSignature.IsHyperbolic (σ : FenchelSignature) : Prop :=
σ.eulerCharacteristic < 0Predicate asserting that a Fenchel signature is hyperbolic.
theorem FenchelSignature.isHyperbolic_iff_pos_hyperbolicDefect
{σ : FenchelSignature} :
σ.IsHyperbolic ↔ 0 < σ.hyperbolicDefectA Fenchel signature is hyperbolic exactly when its hyperbolic defect is positive.
Show proof
by
dsimp [FenchelSignature.IsHyperbolic, FenchelSignature.hyperbolicDefect]
constructor <;> intro h <;> linarithProof. 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.
□def FenchelSignature.HasCusps (σ : FenchelSignature) : Prop :=
0 < σ.numCuspsPredicate asserting that a Fenchel signature has cusps.
def FenchelSignature.IsCompact (σ : FenchelSignature) : Prop :=
σ.numCusps = 0Predicate asserting that a Fenchel signature is compact.
def otherPeriodsLcm (σ : FenchelSignature) (i : Fin σ.numPeriods) : ℕ :=
otherPeriodsLcmFamily σ.periods iThe least common multiple of the other periods is part of the finite-family period, product, and lcm data used in the Fenchel--Nielsen--Zomorrodian period reduction.
def otherPeriodsProduct (σ : FenchelSignature) (i : Fin σ.numPeriods) : ℕ :=
otherPeriodsProductFamily σ.periods iThe product of the other periods is part of the finite-family period, product, and lcm data used in the Fenchel--Nielsen--Zomorrodian period reduction.
def LCMCondition (σ : FenchelSignature) : Prop :=
LCMConditionFamily σ.periodsThe LCM condition on the periods of a Fenchel signature.
def FenchelSignature.AbelianPeriodCondition (σ : FenchelSignature) : Prop :=
LCMCondition σThe abelian period condition attached to a Fenchel signature.
theorem exists_lcm_obstruction_of_not_lcmCondition
(σ : FenchelSignature) (hNotLCM : ¬ LCMCondition σ) :
∃ i : Fin σ.numPeriods, ¬ σ.periods i ∣ otherPeriodsLcm σ iFailure of the LCM condition gives an explicit period obstruction.
Show proof
by
classical
simpa [LCMCondition, LCMConditionFamily, otherPeriodsLcm] using
not_forall.mp hNotLCMProof. 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. 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.
□