FenchelNielsenZomorrodian.Discrete.Core.EllipticQuotientHom
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
- FenchelNielsenZomorrodian.Discrete.Core.CompactFuchsianPresentation
- Mathlib.Algebra.BigOperators.Fin
- Mathlib.GroupTheory.Commutator.Basic
def ellipticQuotientGeneratorImage
(σ : FuchsianSignature) {A : Type*} [CommGroup A]
(ξ : Fin σ.numPeriods → A) :
FuchsianGenerator σ → A
| .elliptic i => ξ i
| .surfaceA _ => 1
| .surfaceB _ => 1The elliptic quotient sends each generator to the prescribed elliptic image.
theorem ellipticQuotientGeneratorImage_respects_relators
(σ : FuchsianSignature) {A : Type*} [CommGroup A]
(ξ : Fin σ.numPeriods → A)
(hpow : ∀ i, ξ i ^ σ.periods i = 1)
(hprod : ∏ i : Fin σ.numPeriods, ξ i = 1) :
∀ r ∈ relators σ, FreeGroup.lift (ellipticQuotientGeneratorImage σ ξ) r = 1The elliptic quotient generator images satisfy the defining relators.
Show proof
by
intro r hr
rcases hr with ⟨i, rfl⟩ | rfl
· simpa [xWord, ellipticQuotientGeneratorImage] using hpow i
· dsimp [totalRelation]
rw [map_mul, map_list_prod, map_list_prod]
have hEll :
(List.map (⇑(FreeGroup.lift (ellipticQuotientGeneratorImage σ ξ)))
(List.map (fun i => xWord σ i) (List.finRange σ.numPeriods))).prod = 1 := by
rw [List.map_map]
have hEllMap :
(⇑(FreeGroup.lift (ellipticQuotientGeneratorImage σ ξ)) ∘
fun i : Fin σ.numPeriods => xWord σ i) = ξ := by
funext i
simp only [xWord, Function.comp_apply, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage]
rw [hEllMap]
calc
(List.map ξ (List.finRange σ.numPeriods)).prod = ∏ i : Fin σ.numPeriods, ξ i := by
simpa using (Fin.prod_univ_def (f := ξ)).symm
_ = 1 := hprod
have hComm :
(List.map (⇑(FreeGroup.lift (ellipticQuotientGeneratorImage σ ξ)))
(List.map (fun j => ⁅aWord σ j, bWord σ j⁆)
(List.finRange σ.orbitGenus))).prod = 1 := by
rw [List.map_map]
have hCommMap :
(⇑(FreeGroup.lift (ellipticQuotientGeneratorImage σ ξ)) ∘
fun j : Fin σ.orbitGenus => ⁅aWord σ j, bWord σ j⁆) =
fun _ => (1 : A) := by
funext j
dsimp
rw [map_commutatorElement]
simp only [aWord, FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage, bWord, commutatorElement_self]
rw [hCommMap]
simp only [List.map_const', List.length_finRange, List.prod_replicate, one_pow]
rw [hEll, hComm]
simp only [mul_one]Proof. Check the quotient data on the named elliptic, surface, cusp, and boundary generators. The period, power, and product relators follow from the displayed order and product calculations, so the presentation universal property supplies the quotient map; derived-length, smoothness, and profinite fields are inherited from the finite or profinite quotient construction.
□def ellipticQuotientHom
(σ : FuchsianSignature) {A : Type*} [CommGroup A]
(ξ : Fin σ.numPeriods → A)
(hpow : ∀ i, ξ i ^ σ.periods i = 1)
(hprod : ∏ i : Fin σ.numPeriods, ξ i = 1) :
FuchsianPresentedGroup σ →* A :=
PresentedGroup.toGroup (rels := relators σ)
(f := ellipticQuotientGeneratorImage σ ξ)
(ellipticQuotientGeneratorImage_respects_relators σ ξ hpow hprod)The quotient homomorphism determined by the images of the elliptic generators.
@[simp] theorem ellipticQuotientHom_elliptic
(σ : FuchsianSignature) {A : Type*} [CommGroup A]
(ξ : Fin σ.numPeriods → A)
(hpow : ∀ i, ξ i ^ σ.periods i = 1)
(hprod : ∏ i : Fin σ.numPeriods, ξ i = 1)
(i : Fin σ.numPeriods) :
ellipticQuotientHom σ ξ hpow hprod
(PresentedGroup.of (rels := relators σ) (FuchsianGenerator.elliptic i)) =
ξ iThe elliptic quotient homomorphism sends each elliptic generator to its prescribed quotient image.
Show proof
by
simp only [ellipticQuotientHom, PresentedGroup.toGroup.of, ellipticQuotientGeneratorImage]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.
□