FenchelNielsenZomorrodian.Discrete.Abelianization.PeriodClassOrder
This module studies period class order for fenchel nielsen zomorrodian. If a multiple kills a period class, then the gcd of that period with the lcm of the other periods divides the multiple. The additive order of the elliptic period class is \(\gcd(n_i,\operatorname{lcm}_{j\ne i} n_j)\).
theorem gcd_period_otherLcm_dvd_of_nsmul_periodClass_eq_zero
(σ : FuchsianSignature) (i : Fin σ.numPeriods) {n : ℕ}
(hzero : n • periodClass σ i = 0) :
Nat.gcd (σ.periods i) (otherPeriodsLcm σ.toFenchelSignature i) ∣ nIf a multiple kills a period class, then the gcd of that period with the lcm of the other periods divides the multiple.
Show proof
by
classical
let L := otherPeriodsLcm σ.toFenchelSignature i
let d := Nat.gcd (σ.periods i) L
have hmem : n • periodBasisVector σ i ∈ periodRelation σ := by
simpa using
(QuotientAddGroup.eq_iff_sub_mem (N := periodRelation σ)
(x := n • periodBasisVector σ i) (y := 0)).1 <| by
simpa [periodClass] using hzero
change n • periodBasisVector σ i ∈ AddSubgroup.zmultiples (periodDiagonal σ) at hmem
rcases hmem with ⟨z, hz⟩
have hOthers :
∀ j ∈ (Finset.univ.erase i : Finset (Fin σ.numPeriods)),
σ.periods j ∣ Int.natAbs z := by
intro j hj
have hji : j ≠ i := (Finset.mem_erase.mp hj).1
have hcoord : (z : ZMod (σ.periods j)) = 0 := by
have := congrArg (fun v : PeriodCoordinate σ => v j) hz
simpa [periodDiagonal, periodBasisVector, zmodBasisVector, hji] using this
have hzdiv : (σ.periods j : ℤ) ∣ z := by
exact (ZMod.intCast_zmod_eq_zero_iff_dvd z (σ.periods j)).mp hcoord
exact Int.natCast_dvd.mp hzdiv
have hLzNat : L ∣ Int.natAbs z := by
exact Finset.lcm_dvd hOthers
have hdzNat : d ∣ Int.natAbs z :=
(Nat.gcd_dvd_right (σ.periods i) L).trans hLzNat
have hdzInt : (d : ℤ) ∣ z := by
exact Int.natCast_dvd.mpr hdzNat
have hdaNat : d ∣ σ.periods i := Nat.gcd_dvd_left (σ.periods i) L
have hdaInt : (d : ℤ) ∣ (σ.periods i : ℤ) := by
exact Int.natCast_dvd_natCast.mpr hdaNat
have hcoordi :
((n : ℤ) : ZMod (σ.periods i)) = (z : ZMod (σ.periods i)) := by
have := congrArg (fun v : PeriodCoordinate σ => v i) hz
simpa [periodDiagonal, periodBasisVector, zmodBasisVector] using this.symm
have hdiff : (σ.periods i : ℤ) ∣ z - (n : ℤ) := by
exact
(ZMod.intCast_eq_intCast_iff_dvd_sub (n : ℤ) z (σ.periods i)).mp hcoordi
have hdDiff : (d : ℤ) ∣ z - (n : ℤ) := hdaInt.trans hdiff
have hdNInt : (d : ℤ) ∣ (n : ℤ) := by
have hsub : (d : ℤ) ∣ z - (z - (n : ℤ)) := dvd_sub hdzInt hdDiff
simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using hsub
exact Int.natCast_dvd_natCast.mp hdNIntProof. 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. 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. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums. 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 periodClass_addOrderOf_eq_gcd
(σ : FuchsianSignature) (i : Fin σ.numPeriods) :
addOrderOf (periodClass σ i) =
Nat.gcd (σ.periods i) (otherPeriodsLcm σ.toFenchelSignature i)The additive order of the elliptic period class is \(\gcd(n_i,\operatorname{lcm}_{j\ne i} n_j)\).
Show proof
by
apply Nat.dvd_antisymm
· exact Nat.dvd_gcd
((addOrderOf_dvd_iff_nsmul_eq_zero).2 (periodClass_nsmul_eq_zero σ i))
((addOrderOf_dvd_iff_nsmul_eq_zero).2
(otherPeriodsLcm_nsmul_periodClass_eq_zero σ i))
· exact gcd_period_otherLcm_dvd_of_nsmul_periodClass_eq_zero σ i (by simp only [addOrderOf_nsmul_eq_zero])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. 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 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 periodClass_addOrderOf_eq_period_iff
{σ : FuchsianSignature} {i : Fin σ.numPeriods} :
addOrderOf (periodClass σ i) = σ.periods i ↔
σ.periods i ∣ otherPeriodsLcm σ.toFenchelSignature iThe additive order of a period class equals its assigned period exactly under the stated divisibility condition.
Show proof
by
rw [periodClass_addOrderOf_eq_gcd]
exact Nat.gcd_eq_left_iff_dvdProof. 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. 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 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 periodClass_orderOf_eq_period_iff
{σ : FuchsianSignature} {i : Fin σ.numPeriods} :
orderOf (Multiplicative.ofAdd (periodClass σ i)) = σ.periods i ↔
σ.periods i ∣ otherPeriodsLcm σ.toFenchelSignature iThe two defining conditions are equivalent after unfolding.
Show proof
by
rw [orderOf_ofAdd_eq_addOrderOf]
exact periodClass_addOrderOf_eq_period_iff (σ := σ) (i := i)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. 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 equivalence and homeomorphism statements, the two comparison maps are composed in both orders and evaluated on the coordinates that determine the source. Each composite reduces to the identity transition or to the chosen representative identity on finite stages, so the algebraic inverse laws and the topological inverse laws follow simultaneously. 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 periodClass_addOrderOf_eq_period
(σ : FuchsianSignature) (hLCM : LCMCondition σ.toFenchelSignature)
(i : Fin σ.numPeriods) :
addOrderOf (periodClass σ i) = σ.periods iUnder the LCM condition, the additive order of each elliptic period class is exactly the prescribed period.
Show proof
(periodClass_addOrderOf_eq_period_iff (σ := σ) (i := i)).2 (hLCM i)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. 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. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem periodClass_orderOf_eq_period
(σ : FuchsianSignature) (hLCM : LCMCondition σ.toFenchelSignature)
(i : Fin σ.numPeriods) :
orderOf (Multiplicative.ofAdd (periodClass σ i)) = σ.periods iUnder the LCM condition, the multiplicative order of each elliptic period class is exactly the prescribed period.
Show proof
(periodClass_orderOf_eq_period_iff (σ := σ) (i := i)).2 (hLCM i)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. 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. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□