FenchelNielsenZomorrodian.Discrete.Abelianization.EllipticAbelianization
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
import
def ellipticAbelianizationHom (σ : FuchsianSignature) :
FuchsianPresentedGroup σ →* Multiplicative (PeriodAbelianization σ) :=
ellipticQuotientHom σ
(fun i => Multiplicative.ofAdd (periodClass σ i))
(by
intro i
simpa using congrArg Multiplicative.ofAdd (periodClass_nsmul_eq_zero σ i))
(by
simpa using congrArg Multiplicative.ofAdd (sum_periodClass_eq_zero σ))The elliptic abelianization homomorphism records the period class of each elliptic generator.
@[simp] theorem ellipticAbelianizationHom_elliptic
(σ : FuchsianSignature) (i : Fin σ.numPeriods) :
ellipticAbelianizationHom σ (ellipticElement σ i) =
Multiplicative.ofAdd (periodClass σ i)The elliptic abelianization homomorphism sends each elliptic generator to its prescribed abelianized class.
Show proof
by
simp only [ellipticAbelianizationHom, ellipticElement, ellipticQuotientHom_elliptic]Proof. Unfold the named transport homomorphism and the corresponding canonical word. The equality follows by evaluating the relevant generator branch and simplifying the Schreier word or block product definition.
□theorem ellipticAbelianizationHom_elliptic_order_eq_period_iff
{σ : FuchsianSignature} {i : Fin σ.numPeriods} :
orderOf (ellipticAbelianizationHom σ (ellipticElement σ i)) = σ.periods i ↔
σ.periods i ∣ otherPeriodsLcm σ.toFenchelSignature iThe image of an elliptic generator in the abelianization has order equal to its assigned period exactly under the stated divisibility condition.
Show proof
by
rw [ellipticAbelianizationHom_elliptic]
exact periodClass_orderOf_eq_period_iff (σ := σ) (i := i)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. 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. For the Fenchel--Nielsen--Zomorrodian relations, the period calculation checks that each elliptic generator has image of the prescribed order, and the product relation is verified by multiplying the images in the stated order. Divisibility, lcm, or gcd hypotheses are used precisely to make the period relators vanish in the target quotient.
□theorem ellipticAbelianizationHom_elliptic_orders_eq_periods_iff_lcmCondition
{σ : FuchsianSignature} :
(∀ i : Fin σ.numPeriods,
orderOf (ellipticAbelianizationHom σ (ellipticElement σ i)) = σ.periods i) ↔
LCMCondition σ.toFenchelSignatureThe elliptic abelianization homomorphism records the period class of each elliptic generator.
Show proof
by
constructor
· intro h i
exact (ellipticAbelianizationHom_elliptic_order_eq_period_iff (σ := σ) (i := i)).1 (h i)
· intro h i
exact (ellipticAbelianizationHom_elliptic_order_eq_period_iff (σ := σ) (i := i)).2 (h i)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. 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. For the Fenchel--Nielsen--Zomorrodian relations, the period calculation checks that each elliptic generator has image of the prescribed order, and the product relation is verified by multiplying the images in the stated order. Divisibility, lcm, or gcd hypotheses are used precisely to make the period relators vanish in the target quotient.
□theorem commHom_ellipticElement_pow_otherPeriodsLcm_eq_one
(σ : FuchsianSignature) {A : Type*} [CommGroup A]
(φ : FuchsianPresentedGroup σ →* A) (i : Fin σ.numPeriods) :
φ (ellipticElement σ i) ^ otherPeriodsLcm σ.toFenchelSignature i = 1For a homomorphism from the Fuchsian presentation to a commutative group, the image of the selected elliptic generator becomes trivial after raising it to the least common multiple of the other periods.
Show proof
by
let ξ : Fin σ.numPeriods → A := fun j => φ (ellipticElement σ j)
have hpow : ∀ j : Fin σ.numPeriods, ξ j ^ σ.periods j = 1 := by
intro j
change φ (ellipticElement σ j) ^ σ.periods j = 1
rw [← map_pow, ellipticElement_pow_period_eq_one, map_one]
have hprod : ∏ j : Fin σ.numPeriods, ξ j = 1 := by
have hrel :
(∏ j : Fin σ.numPeriods, ξ j) *
(∏ j : Fin σ.orbitGenus,
φ ⁅PresentedGroup.of (rels := relators σ) (FuchsianGenerator.surfaceA j),
PresentedGroup.of (rels := relators σ) (FuchsianGenerator.surfaceB j)⁆)
= 1 := by
simpa [ξ, totalRelation, xWord, aWord, bWord, ellipticElement,
Fin.prod_univ_def, MonoidHom.map_mul, MonoidHom.map_list_prod] using
congrArg φ
(PresentedGroup.one_of_mem (rels := relators σ)
(x := totalRelation σ) (Or.inr rfl))
have hcomm :
∏ j : Fin σ.orbitGenus,
φ ⁅PresentedGroup.of (rels := relators σ) (FuchsianGenerator.surfaceA j),
PresentedGroup.of (rels := relators σ) (FuchsianGenerator.surfaceB j)⁆
= 1 := by
refine Finset.prod_eq_one ?_
intro j hj
simpa [map_commutatorElement, commutatorElement_eq_one_iff_mul_comm] using
(mul_comm
(φ (PresentedGroup.of (rels := relators σ) (FuchsianGenerator.surfaceA j)))
(φ (PresentedGroup.of (rels := relators σ) (FuchsianGenerator.surfaceB j))))
rw [hcomm, mul_one] at hrel
exact hrel
let L := otherPeriodsLcm σ.toFenchelSignature i
have hsplit' : ((Finset.univ.erase i).prod ξ) * ξ i = 1 := by
calc
((Finset.univ.erase i).prod ξ) * ξ i = ∏ j, ξ j := by
exact Finset.prod_erase_mul (s := Finset.univ) (f := ξ) (a := i) (Finset.mem_univ i)
_ = 1 := hprod
have hsplit : ξ i * ((Finset.univ.erase i).prod ξ) = 1 := by
simpa [mul_comm] using hsplit'
have hOthers :
((Finset.univ.erase i).prod ξ) ^ L = 1 := by
rw [← Finset.prod_pow]
refine Finset.prod_eq_one ?_
intro j hj
obtain ⟨m, hm⟩ := Finset.dvd_lcm (s := Finset.univ.erase i) (f := σ.periods) hj
rw [show L = σ.periods j * m by simpa [L, otherPeriodsLcm] using hm,
pow_mul, hpow j, one_pow]
have hPow : ξ i ^ L = 1 := by
have hsplitPow := congrArg (fun a : A => a ^ L) hsplit
simp only at hsplitPow
rw [mul_pow, hOthers, mul_one] at hsplitPow
simpa [L] using hsplitPow
simpa [ξ, L] using hPowProof. 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. 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. For the Fenchel--Nielsen--Zomorrodian relations, the period calculation checks that each elliptic generator has image of the prescribed order, and the product relation is verified by multiplying the images in the stated order. Divisibility, lcm, or gcd hypotheses are used precisely to make the period relators vanish in the target quotient.
□theorem orderOf_commHom_ellipticElement_dvd_otherPeriodsLcm
(σ : FuchsianSignature) {A : Type*} [CommGroup A]
(φ : FuchsianPresentedGroup σ →* A) (i : Fin σ.numPeriods) :
orderOf (φ (ellipticElement σ i)) ∣
otherPeriodsLcm σ.toFenchelSignature iThe order of an abelianized elliptic element divides the lcm of the other periods.
Show proof
orderOf_dvd_of_pow_eq_one
(commHom_ellipticElement_pow_otherPeriodsLcm_eq_one σ φ i)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.
□theorem lcmCondition_of_commHom_elliptic_exact
(σ : FuchsianSignature) {A : Type*} [CommGroup A]
(φ : FuchsianPresentedGroup σ →* A)
(hell : ∀ i : Fin σ.numPeriods,
orderOf (φ (ellipticElement σ i)) = σ.periods i) :
LCMCondition σ.toFenchelSignatureThe LCM condition is transported through the abelianized period-coordinate homomorphism.
Show proof
by
intro i
simpa [hell i] using
orderOf_commHom_ellipticElement_dvd_otherPeriodsLcm σ φ iProof. 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. 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. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□