FenchelNielsenZomorrodian.Discrete.Abelianization.PeriodCoordinate
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.Coordinates.ZModFamily
- FenchelNielsenZomorrodian.Discrete.Core.CompactFuchsianPresentation
- Mathlib.Algebra.BigOperators.Pi
abbrev PeriodCoordinate (σ : FuchsianSignature) :=
ZModCoordinateFamily σ.periodsCoordinate data for a single period in the abelianized Fenchel presentation.
def periodDiagonal (σ : FuchsianSignature) : PeriodCoordinate σ :=
fun _ => 1The diagonal period vector formed from the family of period basis vectors.
def periodRelation (σ : FuchsianSignature) : AddSubgroup (PeriodCoordinate σ) :=
AddSubgroup.zmultiples (periodDiagonal σ)The linear period relation imposed by the corresponding elliptic period.
abbrev PeriodAbelianization (σ : FuchsianSignature) :=
PeriodCoordinate σ ⧸ periodRelation σAbelian period data for a Fenchel signature.
def periodBasisVector (σ : FuchsianSignature) (i : Fin σ.numPeriods) : PeriodCoordinate σ :=
zmodBasisVector σ.periods iThe basis vector used for the selected period coordinate in the abelianized period module.
def periodClass (σ : FuchsianSignature) (i : Fin σ.numPeriods) : PeriodAbelianization σ :=
(periodBasisVector σ i : PeriodCoordinate σ)The abelianized class associated with a selected period generator.
theorem sum_periodBasisVector_eq_periodDiagonal (σ : FuchsianSignature) :
(∑ i : Fin σ.numPeriods, periodBasisVector σ i) = periodDiagonal σThe sum of the period basis vectors is the diagonal period vector.
Show proof
by
simpa [periodBasisVector, zmodBasisVector, periodDiagonal] using
(Finset.univ_sum_single (fun i : Fin σ.numPeriods => (1 : ZMod (σ.periods i))))Proof. Unfold the period-coordinate basis and diagonal definitions. Each coordinate statement is a componentwise calculation in the abelianized period module, and the period relation is the corresponding linear relation for the elliptic generator.
□theorem sum_periodClass_eq_zero (σ : FuchsianSignature) :
(∑ i : Fin σ.numPeriods, periodClass σ i) = 0The sum of the period classes is zero in the abelianized presentation module.
Show proof
by
have hsum :
(((∑ i : Fin σ.numPeriods, periodBasisVector σ i) : PeriodCoordinate σ) :
PeriodAbelianization σ) = (periodDiagonal σ : PeriodAbelianization σ) := by
exact congrArg (fun v : PeriodCoordinate σ => (v : PeriodAbelianization σ))
(sum_periodBasisVector_eq_periodDiagonal σ)
have hdiag : (periodDiagonal σ : PeriodAbelianization σ) = 0 := by
have hmem : periodDiagonal σ ∈ periodRelation σ := by
change periodDiagonal σ ∈ AddSubgroup.zmultiples (periodDiagonal σ)
exact ⟨1, by simp only [one_smul]⟩
exact (QuotientAddGroup.eq_iff_sub_mem (N := periodRelation σ)
(x := periodDiagonal σ) (y := 0)).2 <| by simpa using hmem
simpa [periodClass] using hsum.trans hdiagProof. 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_nsmul_eq_zero (σ : FuchsianSignature) (i : Fin σ.numPeriods) :
σ.periods i • periodClass σ i = 0The assigned period annihilates its period class in the abelianized presentation module.
Show proof
by
have hvec : σ.periods i • periodBasisVector σ i = 0 :=
zmodBasisVector_nsmul_eq_zero σ.periods i
simpa [periodClass] using
congrArg (fun v : PeriodCoordinate σ => (v : PeriodAbelianization σ)) hvecProof. 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 otherPeriodsLcm_nsmul_periodClass_eq_zero
(σ : FuchsianSignature) (i : Fin σ.numPeriods) :
otherPeriodsLcm σ.toFenchelSignature i • periodClass σ i = 0The least common multiple of the other periods annihilates the chosen period class in the abelianized presentation module.
Show proof
by
classical
let L := otherPeriodsLcm σ.toFenchelSignature i
have hmem : L • periodBasisVector σ i ∈ periodRelation σ := by
change L • periodBasisVector σ i ∈ AddSubgroup.zmultiples (periodDiagonal σ)
refine ⟨(L : ℤ), ?_⟩
funext j
by_cases hji : j = i
· subst hji
simp only [Pi.smul_apply, periodDiagonal, zsmul_eq_mul, Int.cast_natCast, mul_one, periodBasisVector,
zmodBasisVector, Pi.single_eq_same, nsmul_eq_mul, L]
· have hjmem : j ∈ (Finset.univ.erase i : Finset (Fin σ.numPeriods)) := by
exact Finset.mem_erase.mpr ⟨hji, Finset.mem_univ j⟩
have hjdvd : σ.periods j ∣ L := by
exact Finset.dvd_lcm (s := Finset.univ.erase i) (f := σ.periods) hjmem
have hLzero : (L : ZMod (σ.periods j)) = 0 :=
(ZMod.natCast_eq_zero_iff L (σ.periods j)).2 hjdvd
simp only [Pi.smul_apply, periodDiagonal, zsmul_eq_mul, Int.cast_natCast, hLzero, mul_one, periodBasisVector,
zmodBasisVector, ne_eq, hji, not_false_eq_true, Pi.single_eq_of_ne, nsmul_zero, L]
exact
(QuotientAddGroup.eq_iff_sub_mem
(N := periodRelation σ)
(x := otherPeriodsLcm σ.toFenchelSignature i • periodBasisVector σ i)
(y := 0)).2 (by
simpa [periodClass, L] using hmem)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. 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.
□