FenchelNielsenZomorrodian/Discrete/Coordinates/FenchelPeriodCoordinate.lean
1import FenchelNielsenZomorrodian.Discrete.Coordinates.ZModFamily
2import FenchelNielsenZomorrodian.Discrete.Core.Signature
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Coordinates/FenchelPeriodCoordinate.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Finite coordinate systems for Fenchel periods
15ZMod coordinate families and Fenchel period-coordinate sums used to define finite quotient maps on period generators.
16-/
18open scoped BigOperators
20namespace FenchelNielsen
22abbrev FenchelPeriodCoordinate (σ : FenchelSignature) :=
23 ZModCoordinateFamily σ.periods
25def fenchelPeriodBasisVector (σ : FenchelSignature) (i : Fin σ.numPeriods) :
27 zmodBasisVector σ.periods i
29def fenchelPeriodBasisSum (σ : FenchelSignature) : FenchelPeriodCoordinate σ :=
30 ∑ i : Fin σ.numPeriods, fenchelPeriodBasisVector σ i
32end FenchelNielsen