FenchelNielsenZomorrodian.Discrete.Coordinates.ZModFamily
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
- Mathlib.Data.ZMod.Basic
abbrev ZModCoordinateFamily {ι : Type*} (periods : ι → ℕ) :=
∀ i : ι, ZMod (periods i)The family of cyclic coordinates used to record period data modulo each period.
def zmodBasisVector {ι : Type*} [DecidableEq ι] (periods : ι → ℕ) (i : ι) :
ZModCoordinateFamily periods :=
Pi.single i (1 : ZMod (periods i))The standard basis vector in the corresponding cyclic-coordinate family.
theorem zmodBasisVector_nsmul_eq_zero
{ι : Type*} [DecidableEq ι] (periods : ι → ℕ) (i : ι) :
periods i • zmodBasisVector periods i = 0A basis vector in the cyclic-coordinate family is killed by its period scalar.
Show proof
by
funext j
by_cases hji : j = i
· subst hji
simp only [zmodBasisVector, Pi.smul_apply, Pi.single_eq_same, nsmul_eq_mul, CharP.cast_eq_zero, mul_one,
Pi.zero_apply]
· simp only [zmodBasisVector, Pi.smul_apply, ne_eq, hji, not_false_eq_true, Pi.single_eq_of_ne, nsmul_zero,
Pi.zero_apply]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. 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. 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.
□theorem zmodBasisVector_addOrderOf
{ι : Type*} [DecidableEq ι] (periods : ι → ℕ) (i : ι) :
addOrderOf (zmodBasisVector periods i) = periods iAdding the coordinate order does not change the corresponding \(\mathbb{Z}/n\mathbb{Z}\) basis vector.
Show proof
by
apply Nat.dvd_antisymm
· exact (addOrderOf_dvd_iff_nsmul_eq_zero).2
(zmodBasisVector_nsmul_eq_zero periods i)
· let π : ZModCoordinateFamily periods →+ ZMod (periods i) :=
{ toFun := fun v => v i
map_zero' := rfl
map_add' := by
intro x y
rfl }
have hmap :
π (zmodBasisVector periods i) = (1 : ZMod (periods i)) := by
simp only [zmodBasisVector, AddMonoidHom.coe_mk, ZeroHom.coe_mk, Pi.single_eq_same, π]
have hdiv := addOrderOf_map_dvd π (zmodBasisVector periods i)
rw [hmap, ZMod.addOrderOf_one] at hdiv
exact hdivProof. Unfold the ZMod coordinate basis vector. Adding the modulus changes the coordinate by a multiple of the order, so the class in ZMod and the corresponding basis vector are unchanged.
□theorem zmodBasisVector_pair_neg_addOrderOf
{ι : Type*} [DecidableEq ι] (periods : ι → ℕ) (i : ι) :
addOrderOf (zmodBasisVector periods i, -zmodBasisVector periods i) =
periods iAdding the coordinate order to the negative paired \(\mathbb{Z}/n\mathbb{Z}\) basis vector leaves the class unchanged.
Show proof
by
apply Nat.dvd_antisymm
· apply addOrderOf_dvd_iff_nsmul_eq_zero.mpr
ext j
· exact congrFun (zmodBasisVector_nsmul_eq_zero periods i) j
· simp only [Prod.smul_mk, smul_neg, Pi.neg_apply, congrFun (zmodBasisVector_nsmul_eq_zero periods i) j,
Pi.zero_apply, neg_zero, Prod.snd_zero]
· let π : (ZModCoordinateFamily periods × ZModCoordinateFamily periods) →+
ZMod (periods i) :=
{ toFun := fun v => (v.1 : ZModCoordinateFamily periods) i
map_zero' := rfl
map_add' := by
intro x y
rfl }
have hmap :
π (zmodBasisVector periods i, -zmodBasisVector periods i) =
(1 : ZMod (periods i)) := by
simp only [zmodBasisVector, AddMonoidHom.coe_mk, ZeroHom.coe_mk, Pi.single_eq_same, π]
have hdiv := addOrderOf_map_dvd π
(zmodBasisVector periods i, -zmodBasisVector periods i)
rw [hmap, ZMod.addOrderOf_one] at hdiv
exact hdivProof. Unfold the ZMod coordinate basis vector. Adding the modulus changes the coordinate by a multiple of the order, so the class in ZMod and the corresponding basis vector are unchanged.
□noncomputable def zmodCoordinateFamily_finite
{ι : Type*} [Fintype ι] (periods : ι → ℕ) (hpos : ∀ i, 0 < periods i) :
Finite (ZModCoordinateFamily periods) := by
classical
letI (i : ι) : NeZero (periods i) := ⟨ne_of_gt (hpos i)⟩
letI (i : ι) : Fintype (ZMod (periods i)) := ZMod.fintype (periods i)
exact Finite.of_fintype (ZModCoordinateFamily periods)The integer-coordinate family used by the presentation reduction is finite.