FenchelNielsenZomorrodian/Discrete/Coordinates/ZModFamily.lean
1import Mathlib.Data.ZMod.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Coordinates/ZModFamily.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Finite coordinate systems for Fenchel periods
14ZMod coordinate families and Fenchel period-coordinate sums used to define finite quotient maps on period generators.
15-/
17namespace FenchelNielsen
19abbrev ZModCoordinateFamily {ι : Type*} (periods : ι → ℕ) :=
20 ∀ i : ι, ZMod (periods i)
22def zmodBasisVector {ι : Type*} [DecidableEq ι] (periods : ι → ℕ) (i : ι) :
23 ZModCoordinateFamily periods :=
24 Pi.single i (1 : ZMod (periods i))
26theorem zmodBasisVector_nsmul_eq_zero
27 {ι : Type*} [DecidableEq ι] (periods : ι → ℕ) (i : ι) :
28 periods i • zmodBasisVector periods i = 0 := by
29 funext j
30 by_cases hji : j = i
31 · subst hji
32 simp only [zmodBasisVector, Pi.smul_apply, Pi.single_eq_same, nsmul_eq_mul, CharP.cast_eq_zero, mul_one,
33 Pi.zero_apply]
34 · simp only [zmodBasisVector, Pi.smul_apply, ne_eq, hji, not_false_eq_true, Pi.single_eq_of_ne, nsmul_zero,
35 Pi.zero_apply]
37theorem zmodBasisVector_addOrderOf
38 {ι : Type*} [DecidableEq ι] (periods : ι → ℕ) (i : ι) :
39 addOrderOf (zmodBasisVector periods i) = periods i := by
40 apply Nat.dvd_antisymm
41 · exact (addOrderOf_dvd_iff_nsmul_eq_zero).2
42 (zmodBasisVector_nsmul_eq_zero periods i)
43 · let π : ZModCoordinateFamily periods →+ ZMod (periods i) :=
44 { toFun := fun v => v i
45 map_zero' := rfl
46 map_add' := by
47 intro x y
48 rfl }
49 have hmap :
50 π (zmodBasisVector periods i) = (1 : ZMod (periods i)) := by
51 simp only [zmodBasisVector, AddMonoidHom.coe_mk, ZeroHom.coe_mk, Pi.single_eq_same, π]
52 have hdiv := addOrderOf_map_dvd π (zmodBasisVector periods i)
53 rw [hmap, ZMod.addOrderOf_one] at hdiv
54 exact hdiv
57 {ι : Type*} [DecidableEq ι] (periods : ι → ℕ) (i : ι) :
58 addOrderOf (zmodBasisVector periods i, -zmodBasisVector periods i) =
59 periods i := by
60 apply Nat.dvd_antisymm
61 · apply addOrderOf_dvd_iff_nsmul_eq_zero.mpr
62 ext j
63 · exact congrFun (zmodBasisVector_nsmul_eq_zero periods i) j
64 · simp only [Prod.smul_mk, smul_neg, Pi.neg_apply, congrFun (zmodBasisVector_nsmul_eq_zero periods i) j,
65 Pi.zero_apply, neg_zero, Prod.snd_zero]
66 · let π : (ZModCoordinateFamily periods × ZModCoordinateFamily periods) →+
67 ZMod (periods i) :=
68 { toFun := fun v => (v.1 : ZModCoordinateFamily periods) i
69 map_zero' := rfl
70 map_add' := by
71 intro x y
72 rfl }
73 have hmap :
74 π (zmodBasisVector periods i, -zmodBasisVector periods i) =
75 (1 : ZMod (periods i)) := by
76 simp only [zmodBasisVector, AddMonoidHom.coe_mk, ZeroHom.coe_mk, Pi.single_eq_same, π]
78 (zmodBasisVector periods i, -zmodBasisVector periods i)
79 rw [hmap, ZMod.addOrderOf_one] at hdiv
80 exact hdiv
82noncomputable def zmodCoordinateFamily_finite
83 {ι : Type*} [Fintype ι] (periods : ι → ℕ) (hpos : ∀ i, 0 < periods i) :
84 Finite (ZModCoordinateFamily periods) := by
85 classical
86 letI (i : ι) : NeZero (periods i) := ⟨ne_of_gt (hpos i)⟩
87 letI (i : ι) : Fintype (ZMod (periods i)) := ZMod.fintype (periods i)
88 exact Finite.of_fintype (ZModCoordinateFamily periods)
90end FenchelNielsen