FenchelNielsenZomorrodian.Profinite.LowPeriodQuotient
This module develops Fenchel--Nielsen--Zomorrodian presentation reductions, period relations, reindexings, and quotient maps.
noncomputable def twoPeriodIndexZero
(Δ : ProfiniteFGroup.{u}) (hTwo : Δ.signature.numPeriods = 2) :
Fin Δ.signature.numPeriods :=
Fin.cast hTwo.symm (0 : Fin 2)The first distinguished period index in the two-period case.
noncomputable def twoPeriodIndexOne
(Δ : ProfiniteFGroup.{u}) (hTwo : Δ.signature.numPeriods = 2) :
Fin Δ.signature.numPeriods :=
Fin.cast hTwo.symm (1 : Fin 2)The second distinguished period index in the two-period case.
theorem twoPeriod_inertia_list_product
(Δ : ProfiniteFGroup.{u}) (hTwo : Δ.signature.numPeriods = 2) :
((List.finRange Δ.signature.numPeriods).map fun k => Δ.inertia k).prod =
Δ.inertia (twoPeriodIndexZero Δ hTwo) *
Δ.inertia (twoPeriodIndexOne Δ hTwo)With two periods, the inertia part of the total relation is the product of the two indexed inertia generators.
Show proof
by
cases Δ with
| mk carrier ps prof fg sig dsig surfaceA surfaceB cusp inertia rel gen
basis relators rel_eq pres presA presB presC presI inertia_order =>
cases sig with
| mk orbitGenus numCusps numPeriods periods period_ge_two =>
dsimp at hTwo ⊢
subst numPeriods
norm_num [twoPeriodIndexZero, twoPeriodIndexOne, List.finRange]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. Kernel and normal-closure claims are proved by showing that each rewritten relator lies in the generated normal subgroup and that the quotient map kills exactly those relations required by the presentation. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem twoPeriod_inertia_mul_eq_one
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hZero : Δ.signature.orbitGenus = 0)
(hTwo : Δ.signature.numPeriods = 2) :
Δ.inertia (twoPeriodIndexZero Δ hTwo) *
Δ.inertia (twoPeriodIndexOne Δ hTwo) = 1In the compact zero-genus two-period case, the two inertia generators multiply to one.
Show proof
by
have hrel := Δ.presentation_relation
have hSurface :
((List.finRange Δ.signature.orbitGenus).map fun i =>
⁅Δ.surfaceA i, Δ.surfaceB i⁆).prod = 1 := by
apply List.prod_eq_one
intro x hx
rcases List.mem_map.mp hx with ⟨j, _hj, rfl⟩
exfalso
rw [hZero] at j
exact Nat.not_lt_zero _ j.2
have hCusp :
((List.finRange Δ.signature.numCusps).map fun j => Δ.cusp j).prod = 1 := by
apply List.prod_eq_one
intro x hx
rcases List.mem_map.mp hx with ⟨j, _hj, rfl⟩
exfalso
rw [hCompact] at j
exact Nat.not_lt_zero _ j.2
rw [profiniteFenchelTotalRelation, hSurface, hCusp, one_mul, one_mul,
twoPeriod_inertia_list_product Δ hTwo] at hrel
exact hrelProof. 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. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem twoPeriod_periods_eq
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hZero : Δ.signature.orbitGenus = 0)
(hTwo : Δ.signature.numPeriods = 2) :
Δ.signature.periods (twoPeriodIndexZero Δ hTwo) =
Δ.signature.periods (twoPeriodIndexOne Δ hTwo)In the compact zero-genus two-period case, the two periods are equal.
Show proof
by
have hmul := twoPeriod_inertia_mul_eq_one Δ hCompact hZero hTwo
calc
Δ.signature.periods (twoPeriodIndexZero Δ hTwo) =
orderOf (Δ.inertia (twoPeriodIndexZero Δ hTwo)) := by
rw [Δ.inertia_order]
_ = orderOf (Δ.inertia (twoPeriodIndexOne Δ hTwo)) := by
rw [eq_inv_of_mul_eq_one_left hmul, orderOf_inv]
_ = Δ.signature.periods (twoPeriodIndexOne Δ hTwo) := by
rw [Δ.inertia_order]Proof. Unfold the named Fenchel--Nielsen reduction, cyclic-Schreier word, or total-relation definition. The equality or membership follows by evaluating the relevant generator branch, simplifying the period or product formula, and using that normal closures are closed under products, inverses, and conjugation when a relator membership is involved.
□instance instTopologicalSpaceMultiplicativeZMod (n : ℕ) :
TopologicalSpace (Multiplicative (ZMod n)) :=
⊥The multiplicative group of \(\mathrm{ZMod}\,n\) is given the discrete topology.
instance instDiscreteTopologyMultiplicativeZMod (n : ℕ) :
DiscreteTopology (Multiplicative (ZMod n)) :=
⟨rfl⟩The multiplicative group of \(\mathrm{ZMod}\,n\) is a discrete topological space.
noncomputable instance instFintypeMultiplicativeZMod (n : ℕ) [NeZero n] :
Fintype (Multiplicative (ZMod n)) :=
Fintype.ofEquiv (ZMod n) Multiplicative.toAddThe multiplicative group of \(\mathbb{Z} / n\mathbb{Z}\) has a fintype instance when \(n\) is nonzero.
noncomputable def twoPeriodCyclicGeneratorImageCore
(Δ : ProfiniteFGroup.{u}) (hTwo : Δ.signature.numPeriods = 2) :
ProfiniteFenchelGeneratorIndex.{u} Δ.signature →
Multiplicative
(ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))
| ULift.up (.inertia k) =>
if (Fin.cast hTwo k).val = 0 then
Multiplicative.ofAdd (1 :
ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))
else
(Multiplicative.ofAdd (1 :
ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo))))⁻¹
| ULift.up (.surfaceA _) => 1
| ULift.up (.surfaceB _) => 1
| ULift.up (.cusp _) => 1noncomputable def twoPeriodCyclicGeneratorImage
(Δ : ProfiniteFGroup.{u}) (hTwo : Δ.signature.numPeriods = 2) :
ProfiniteFenchelGeneratorIndex.{u} Δ.signature →
ULift.{u, 0}
(Multiplicative
(ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))) :=
fun x => ULift.up (twoPeriodCyclicGeneratorImageCore Δ hTwo x)private theorem twoPeriodCyclicGeneratorImage_total_relation
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hZero : Δ.signature.orbitGenus = 0)
(hTwo : Δ.signature.numPeriods = 2) :
profiniteFenchelTotalRelation
(fun i => twoPeriodCyclicGeneratorImageCore Δ hTwo
(ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
(fun i => twoPeriodCyclicGeneratorImageCore Δ hTwo
(ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
(fun j => twoPeriodCyclicGeneratorImageCore Δ hTwo
(ULift.up (ProfiniteFenchelGenerator.cusp j)))
(fun k => twoPeriodCyclicGeneratorImageCore Δ hTwo
(ULift.up (ProfiniteFenchelGenerator.inertia k))) = 1Show proof
by
cases Δ with
| mk carrier ps prof fg sig dsig surfaceA surfaceB cusp inertia rel gen
basis relators rel_eq pres presA presB presC presI inertia_order =>
cases sig with
| mk orbitGenus numCusps numPeriods periods period_ge_two =>
dsimp [FenchelSignature.IsCompact] at hCompact
dsimp at hZero hTwo ⊢
subst orbitGenus
subst numCusps
subst numPeriods
dsimp [profiniteFenchelTotalRelation, twoPeriodCyclicGeneratorImageCore,
twoPeriodIndexZero]
simp only [List.finRange_zero, List.map_nil, List.prod_nil, one_mul]
change
((List.finRange 2).map fun k : Fin 2 =>
if k = 0 then
Multiplicative.ofAdd (1 : ZMod (periods 0))
else
(Multiplicative.ofAdd (1 : ZMod (periods 0)))⁻¹).prod = 1
norm_num [List.finRange]Proof. Unfold the named period, generator-image, or quotient-data construction. Period relators are checked by the prescribed orders of inertia or elliptic generators; total relations are checked by multiplying the displayed generator images; and data definitions follow by reading off the corresponding period family, index, or signature field.
□private theorem twoPeriodCyclicGeneratorImage_lifted_total_relation
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hZero : Δ.signature.orbitGenus = 0)
(hTwo : Δ.signature.numPeriods = 2) :
profiniteFenchelTotalRelation
(fun i => twoPeriodCyclicGeneratorImage Δ hTwo
(ULift.up (ProfiniteFenchelGenerator.surfaceA i)))
(fun i => twoPeriodCyclicGeneratorImage Δ hTwo
(ULift.up (ProfiniteFenchelGenerator.surfaceB i)))
(fun j => twoPeriodCyclicGeneratorImage Δ hTwo
(ULift.up (ProfiniteFenchelGenerator.cusp j)))
(fun k => twoPeriodCyclicGeneratorImage Δ hTwo
(ULift.up (ProfiniteFenchelGenerator.inertia k))) = 1Show proof
by
apply
(MulEquiv.ulift :
ULift.{u, 0}
(Multiplicative
(ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))) ≃*
Multiplicative
(ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))).injective
simpa [twoPeriodCyclicGeneratorImage, profiniteFenchelTotalRelation,
map_list_prod, Function.comp_def, map_commutatorElement] using
twoPeriodCyclicGeneratorImage_total_relation Δ hCompact hZero hTwoProof. Unfold the named period, generator-image, or quotient-data construction. Period relators are checked by the prescribed orders of inertia or elliptic generators; total relations are checked by multiplying the displayed generator images; and data definitions follow by reading off the corresponding period family, index, or signature field.
□private theorem twoPeriodCyclicGeneratorImage_period_relation
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hZero : Δ.signature.orbitGenus = 0)
(hTwo : Δ.signature.numPeriods = 2)
(k : Fin Δ.signature.numPeriods) :
twoPeriodCyclicGeneratorImageCore Δ hTwo
(ULift.up (ProfiniteFenchelGenerator.inertia k)) ^
Δ.signature.periods k = 1Show proof
by
have hEq := twoPeriod_periods_eq Δ hCompact hZero hTwo
cases Δ with
| mk carrier ps prof fg sig dsig surfaceA surfaceB cusp inertia rel gen
basis relators rel_eq pres presA presB presC presI inertia_order =>
cases sig with
| mk orbitGenus numCusps numPeriods periods period_ge_two =>
dsimp at hCompact hZero hTwo hEq k ⊢
subst numPeriods
fin_cases k
· have horder :
orderOf
(Multiplicative.ofAdd (1 : ZMod (periods 0))) =
periods 0 := by
rw [orderOf_ofAdd_eq_addOrderOf, ZMod.addOrderOf_one]
simpa [twoPeriodCyclicGeneratorImageCore, twoPeriodIndexZero,
horder] using
pow_orderOf_eq_one
(Multiplicative.ofAdd (1 : ZMod (periods 0)))
· have h10 : periods 1 = periods 0 := by
simpa [twoPeriodIndexZero, twoPeriodIndexOne] using hEq.symm
have horder :
orderOf
((Multiplicative.ofAdd (1 : ZMod (periods 0)))⁻¹) =
periods 1 := by
rw [orderOf_inv, orderOf_ofAdd_eq_addOrderOf,
ZMod.addOrderOf_one, h10]
simpa [twoPeriodCyclicGeneratorImageCore, twoPeriodIndexZero,
horder] using
pow_orderOf_eq_one
((Multiplicative.ofAdd (1 : ZMod (periods 0)))⁻¹)Proof. Unfold the named period, generator-image, or quotient-data construction. Period relators are checked by the prescribed orders of inertia or elliptic generators; total relations are checked by multiplying the displayed generator images; and data definitions follow by reading off the corresponding period family, index, or signature field.
□private theorem twoPeriodCyclicGeneratorImage_lifted_period_relation
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hZero : Δ.signature.orbitGenus = 0)
(hTwo : Δ.signature.numPeriods = 2)
(k : Fin Δ.signature.numPeriods) :
twoPeriodCyclicGeneratorImage Δ hTwo
(ULift.up (ProfiniteFenchelGenerator.inertia k)) ^
Δ.signature.periods k = 1Show proof
by
apply
(MulEquiv.ulift :
ULift.{u, 0}
(Multiplicative
(ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))) ≃*
Multiplicative
(ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))).injective
simpa [twoPeriodCyclicGeneratorImage] using
twoPeriodCyclicGeneratorImage_period_relation Δ hCompact hZero hTwo kProof. Unfold the named period, generator-image, or quotient-data construction. Period relators are checked by the prescribed orders of inertia or elliptic generators; total relations are checked by multiplying the displayed generator images; and data definitions follow by reading off the corresponding period family, index, or signature field.
□private theorem twoPeriodCyclicGeneratorImage_inertia_order
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hZero : Δ.signature.orbitGenus = 0)
(hTwo : Δ.signature.numPeriods = 2)
(k : Fin Δ.signature.numPeriods) :
orderOf
(twoPeriodCyclicGeneratorImageCore Δ hTwo
(ULift.up (ProfiniteFenchelGenerator.inertia k))) =
Δ.signature.periods kShow proof
by
have hEq := twoPeriod_periods_eq Δ hCompact hZero hTwo
cases Δ with
| mk carrier ps prof fg sig dsig surfaceA surfaceB cusp inertia rel gen
basis relators rel_eq pres presA presB presC presI inertia_order =>
cases sig with
| mk orbitGenus numCusps numPeriods periods period_ge_two =>
dsimp at hCompact hZero hTwo hEq k ⊢
subst numPeriods
fin_cases k
· simp only [twoPeriodIndexZero, Fin.isValue, Fin.cast_eq_self, twoPeriodCyclicGeneratorImageCore, Fin.zero_eta,
Fin.coe_ofNat_eq_mod, Nat.zero_mod, ↓reduceIte, orderOf_ofAdd_eq_addOrderOf, ZMod.addOrderOf_one]
· have h10 : periods 1 = periods 0 := by
simpa [twoPeriodIndexZero, twoPeriodIndexOne] using hEq.symm
simp only [twoPeriodIndexZero, Fin.isValue, Fin.cast_eq_self, twoPeriodCyclicGeneratorImageCore, Fin.mk_one,
Fin.coe_ofNat_eq_mod, Nat.mod_succ, one_ne_zero, ↓reduceIte, orderOf_inv, orderOf_ofAdd_eq_addOrderOf,
ZMod.addOrderOf_one, h10]Proof. Unfold the named period, generator-image, or quotient-data construction. Period relators are checked by the prescribed orders of inertia or elliptic generators; total relations are checked by multiplying the displayed generator images; and data definitions follow by reading off the corresponding period family, index, or signature field.
□private theorem twoPeriodCyclicGeneratorImage_lifted_inertia_order
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hZero : Δ.signature.orbitGenus = 0)
(hTwo : Δ.signature.numPeriods = 2)
(k : Fin Δ.signature.numPeriods) :
orderOf
(twoPeriodCyclicGeneratorImage Δ hTwo
(ULift.up (ProfiniteFenchelGenerator.inertia k))) =
Δ.signature.periods kShow proof
by
have horder :=
orderOf_injective
((MulEquiv.ulift :
ULift.{u, 0}
(Multiplicative
(ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))) ≃*
Multiplicative
(ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))).toMonoidHom)
(MulEquiv.ulift :
ULift.{u, 0}
(Multiplicative
(ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))) ≃*
Multiplicative
(ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)))).injective
(twoPeriodCyclicGeneratorImage Δ hTwo
(ULift.up (ProfiniteFenchelGenerator.inertia k)))
rw [← horder]
exact twoPeriodCyclicGeneratorImage_inertia_order Δ hCompact hZero hTwo kProof. Unfold the named period, generator-image, or quotient-data construction. Period relators are checked by the prescribed orders of inertia or elliptic generators; total relations are checked by multiplying the displayed generator images; and data definitions follow by reading off the corresponding period family, index, or signature field.
□noncomputable def twoPeriodCyclicSmoothQuotientData
(Δ : ProfiniteFGroup.{u})
(hCompact : Δ.signature.IsCompact)
(hZero : Δ.signature.orbitGenus = 0)
(hTwo : Δ.signature.numPeriods = 2) :
ProfiniteSmoothQuotientData Δ 1 :=
have hpos :
0 < Δ.signature.periods (twoPeriodIndexZero Δ hTwo) :=
lt_of_lt_of_le (by decide : 0 < 2)
(Δ.signature.period_ge_two (twoPeriodIndexZero Δ hTwo))
letI : NeZero (Δ.signature.periods (twoPeriodIndexZero Δ hTwo)) :=
⟨Nat.pos_iff_ne_zero.mp hpos⟩
ProfiniteSmoothQuotientData.ofPresentationLiftToFiniteOfRelations
Δ (twoPeriodCyclicGeneratorImage Δ hTwo)
(twoPeriodCyclicGeneratorImage_lifted_total_relation
Δ hCompact hZero hTwo)
(twoPeriodCyclicGeneratorImage_lifted_period_relation
Δ hCompact hZero hTwo)
(profiniteDerivedSeries_one_eq_bot_of_commGroup
(ULift.{u, 0}
(Multiplicative
(ZMod (Δ.signature.periods (twoPeriodIndexZero Δ hTwo))))))
(twoPeriodCyclicGeneratorImage_lifted_inertia_order
Δ hCompact hZero hTwo)The smooth quotient data obtained from the two-period cyclic quotient.