FenchelNielsenZomorrodian/Discrete/Abelianization/PeriodCoordinate.lean
1import FenchelNielsenZomorrodian.Discrete.Coordinates.ZModFamily
2import FenchelNielsenZomorrodian.Discrete.Core.CompactFuchsianPresentation
3import Mathlib.Algebra.BigOperators.Pi
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Abelianization/PeriodCoordinate.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Abelianization of compact Fuchsian presentations
16Finite cyclic coordinate calculations for elliptic generators, period classes, period quotients, and order formulas in compact Fuchsian abelianizations.
17-/
19open scoped BigOperators
21namespace FenchelNielsen
23abbrev PeriodCoordinate (σ : FuchsianSignature) :=
24 ZModCoordinateFamily σ.periods
26def periodDiagonal (σ : FuchsianSignature) : PeriodCoordinate σ :=
27 fun _ => 1
29def periodRelation (σ : FuchsianSignature) : AddSubgroup (PeriodCoordinate σ) :=
30 AddSubgroup.zmultiples (periodDiagonal σ)
32abbrev PeriodAbelianization (σ : FuchsianSignature) :=
33 PeriodCoordinate σ ⧸ periodRelation σ
35def periodBasisVector (σ : FuchsianSignature) (i : Fin σ.numPeriods) : PeriodCoordinate σ :=
36 zmodBasisVector σ.periods i
38def periodClass (σ : FuchsianSignature) (i : Fin σ.numPeriods) : PeriodAbelianization σ :=
39 (periodBasisVector σ i : PeriodCoordinate σ)
41theorem sum_periodBasisVector_eq_periodDiagonal (σ : FuchsianSignature) :
42 (∑ i : Fin σ.numPeriods, periodBasisVector σ i) = periodDiagonal σ := by
43 simpa [periodBasisVector, zmodBasisVector, periodDiagonal] using
44 (Finset.univ_sum_single (fun i : Fin σ.numPeriods => (1 : ZMod (σ.periods i))))
46theorem sum_periodClass_eq_zero (σ : FuchsianSignature) :
47 (∑ i : Fin σ.numPeriods, periodClass σ i) = 0 := by
48 have hsum :
49 (((∑ i : Fin σ.numPeriods, periodBasisVector σ i) : PeriodCoordinate σ) :
50 PeriodAbelianization σ) = (periodDiagonal σ : PeriodAbelianization σ) := by
51 exact congrArg (fun v : PeriodCoordinate σ => (v : PeriodAbelianization σ))
53 have hdiag : (periodDiagonal σ : PeriodAbelianization σ) = 0 := by
54 have hmem : periodDiagonal σ ∈ periodRelation σ := by
55 change periodDiagonal σ ∈ AddSubgroup.zmultiples (periodDiagonal σ)
56 exact ⟨1, by simp only [one_smul]⟩
57 exact (QuotientAddGroup.eq_iff_sub_mem (N := periodRelation σ)
58 (x := periodDiagonal σ) (y := 0)).2 <| by simpa using hmem
59 simpa [periodClass] using hsum.trans hdiag
61theorem periodClass_nsmul_eq_zero (σ : FuchsianSignature) (i : Fin σ.numPeriods) :
62 σ.periods i • periodClass σ i = 0 := by
63 have hvec : σ.periods i • periodBasisVector σ i = 0 :=
64 zmodBasisVector_nsmul_eq_zero σ.periods i
65 simpa [periodClass] using
66 congrArg (fun v : PeriodCoordinate σ => (v : PeriodAbelianization σ)) hvec
69 (σ : FuchsianSignature) (i : Fin σ.numPeriods) :
70 otherPeriodsLcm σ.toFenchelSignature i • periodClass σ i = 0 := by
71 classical
72 let L := otherPeriodsLcm σ.toFenchelSignature i
73 have hmem : L • periodBasisVector σ i ∈ periodRelation σ := by
74 change L • periodBasisVector σ i ∈ AddSubgroup.zmultiples (periodDiagonal σ)
75 refine ⟨(L : ℤ), ?_⟩
76 funext j
77 by_cases hji : j = i
78 · subst hji
79 simp only [Pi.smul_apply, periodDiagonal, zsmul_eq_mul, Int.cast_natCast, mul_one, periodBasisVector,
80 zmodBasisVector, Pi.single_eq_same, nsmul_eq_mul, L]
81 · have hjmem : j ∈ (Finset.univ.erase i : Finset (Fin σ.numPeriods)) := by
82 exact Finset.mem_erase.mpr ⟨hji, Finset.mem_univ j⟩
83 have hjdvd : σ.periods j ∣ L := by
84 exact Finset.dvd_lcm (s := Finset.univ.erase i) (f := σ.periods) hjmem
85 have hLzero : (L : ZMod (σ.periods j)) = 0 :=
86 (ZMod.natCast_eq_zero_iff L (σ.periods j)).2 hjdvd
87 simp only [Pi.smul_apply, periodDiagonal, zsmul_eq_mul, Int.cast_natCast, hLzero, mul_one, periodBasisVector,
88 zmodBasisVector, ne_eq, hji, not_false_eq_true, Pi.single_eq_of_ne, nsmul_zero, L]
89 exact
90 (QuotientAddGroup.eq_iff_sub_mem
91 (N := periodRelation σ)
92 (x := otherPeriodsLcm σ.toFenchelSignature i • periodBasisVector σ i)
93 (y := 0)).2 (by
94 simpa [periodClass, L] using hmem)
96end FenchelNielsen