FenchelNielsenZomorrodian.Discrete.CompactFuchsian.ZeroGenus.Perfectness
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
private theorem hom_trivial_of_zeroGenus_pairwiseCoprime
(σ : FuchsianSignature) (hZero : σ.orbitGenus = 0)
(hPair :
∀ i j : Fin σ.numPeriods, i ≠ j → Nat.Coprime (σ.periods i) (σ.periods j))
{A : Type*} [CommGroup A] (φ : FuchsianPresentedGroup σ →* A) :
φ = 1In zero genus with pairwise coprime periods, the displayed homomorphism is trivial.
Show proof
by
apply PresentedGroup.ext
intro x
cases x with
| elliptic i =>
let ξ : Fin σ.numPeriods → A := fun j => φ (ellipticElement σ j)
have hpow : ∀ j : Fin σ.numPeriods, ξ j ^ σ.periods j = 1 := by
intro j
simpa [ξ, ellipticElement, xWord, MonoidHom.map_pow] using
congrArg φ
(PresentedGroup.one_of_mem (rels := relators σ)
(x := (xWord σ j) ^ σ.periods j) (Or.inl ⟨j, rfl⟩))
let L := otherPeriodsLcm σ.toFenchelSignature i
have hPow : ξ i ^ L = 1 := by
simpa [ξ, L] using
commHom_ellipticElement_pow_otherPeriodsLcm_eq_one σ φ i
have hCoprimeProd :
Nat.Coprime (σ.periods i)
((Finset.univ.erase i : Finset (Fin σ.numPeriods)).prod σ.periods) := by
rw [Nat.coprime_prod_right_iff]
intro j hj
exact hPair i j (Finset.mem_erase.mp hj).1.symm
have hLDiv :
L ∣ (Finset.univ.erase i : Finset (Fin σ.numPeriods)).prod σ.periods := by
dsimp [L, otherPeriodsLcm]
exact Finset.lcm_dvd (fun j hj => Finset.dvd_prod_of_mem _ hj)
have hCoprime : Nat.Coprime (σ.periods i) L := hCoprimeProd.of_dvd_right hLDiv
have hOrder :
orderOf (ξ i) = 1 := by
exact Nat.eq_one_of_dvd_coprimes hCoprime
(orderOf_dvd_of_pow_eq_one (hpow i))
(orderOf_dvd_of_pow_eq_one hPow)
exact orderOf_eq_one_iff.mp hOrder
| surfaceA j =>
exfalso
rw [hZero] at j
exact Nat.not_lt_zero _ j.2
| surfaceB j =>
exfalso
rw [hZero] at j
exact Nat.not_lt_zero _ j.2theorem FuchsianSignature.isPerfect_of_zeroGenus_pairwiseCoprime
(σ : FuchsianSignature) (hZero : σ.orbitGenus = 0)
(hPair :
∀ i j : Fin σ.numPeriods, i ≠ j → Nat.Coprime (σ.periods i) (σ.periods j)) :
IsPerfectGroup (FuchsianPresentedGroup σ)A zero-genus Fuchsian signature with pairwise coprime periods gives a perfect presented group.
Show proof
by
rw [IsPerfectGroup, derivedSeries_one]
apply top_le_iff.mp
intro g hg
rw [← Abelianization.ker_of (G := FuchsianPresentedGroup σ), MonoidHom.mem_ker]
have htriv :
(Abelianization.of :
FuchsianPresentedGroup σ →* Abelianization (FuchsianPresentedGroup σ)) = 1 :=
hom_trivial_of_zeroGenus_pairwiseCoprime σ hZero hPair Abelianization.of
simpa using congrArg
(fun f : FuchsianPresentedGroup σ →* Abelianization (FuchsianPresentedGroup σ) => f g) htrivProof. 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. 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. 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.
□theorem exists_prime_dvd_two_periods_of_zeroGenus_notPerfect
(σ : FuchsianSignature) (hZero : σ.orbitGenus = 0)
(hNonperfect : ¬ IsPerfectGroup (FuchsianPresentedGroup σ)) :
∃ p : ℕ, p.Prime ∧
∃ i j : Fin σ.numPeriods, i ≠ j ∧ p ∣ σ.periods i ∧ p ∣ σ.periods jIn the non-perfect zero-genus case, some prime divides two of the periods.
Show proof
by
exact (not_pairwiseCoprimeFamily_iff_exists_prime_dvd_two (periods := σ.periods)).mp <| by
intro hPair
exact hNonperfect (FuchsianSignature.isPerfect_of_zeroGenus_pairwiseCoprime σ hZero hPair)Proof. Use the zero-genus non-perfectness criterion to extract the two period entries with a common prime divisor.
□