Coarse quotients of conjugate Fuchsian groups

Let Γ ≤ PSL(2, ℝ), g ∈ PSL(2, ℝ), and let Γ' = g Γ g⁻¹, written ConjAct.toConjAct g • Γ = Γ'. The biholomorphism z ↦ g • z of the upper half-plane carries Γ-orbits onto Γ'-orbits, so it descends to a homeomorphism Subgroup.quotientConjHomeomorph of the coarse quotients Γ \ ℍ ≃ₜ Γ' \ ℍ, sending the orbit of z to the orbit of g • z. For properly discontinuous (equivalently, discrete) groups it is holomorphic, including at elliptic orbits, by holomorphic descent through the orbit projection (Subgroup.mdifferentiableAt_of_eventually_mdifferentiableAt_comp_quotientMk). Its inverse is the same construction for g⁻¹ (Subgroup.quotientConjHomeomorph_symm), so it is holomorphic in both directions. The construction is functorial: g = 1 gives the identity (Subgroup.quotientConjHomeomorph_one), and conjugating by g and then by g' is conjugating by g' * g (Subgroup.quotientConjHomeomorph_trans).

The conjugate is passed as a subgroup Γ' together with the equation ConjAct.toConjAct g • Γ = Γ', so that the inverse is again of this form and an element of the normalizer of Γ acts on Γ \ ℍ itself.

Main declarations

• Subgroup.quotientConjHomeomorph: the homeomorphism Γ \ ℍ ≃ₜ Γ' \ ℍ, with Subgroup.quotientConjHomeomorph_mk, Subgroup.quotientConjHomeomorph_symm, Subgroup.quotientConjHomeomorph_one and Subgroup.quotientConjHomeomorph_trans.
• Subgroup.mdifferentiable_quotientConjHomeomorph: it is holomorphic.

References

• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §2.2.

noncomputable def Subgroup.quotientConjHomeomorph {Γ Γ' : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (h : ConjAct.toConjAct g • Γ = Γ') : MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane ≃ₜ MulAction.orbitRel.Quotient (↥Γ') UpperHalfPlane

The coarse quotients of conjugate groups are homeomorphic. If Γ' = g Γ g⁻¹, the translation z ↦ g • z of the upper half-plane descends to a homeomorphism Γ \ ℍ ≃ₜ Γ' \ ℍ sending the orbit of z to the orbit of g • z.

Equations

• Subgroup.quotientConjHomeomorph h = Homeomorph.Quotient.congr (Homeomorph.smul g) ⋯

@[simp]

theorem Subgroup.quotientConjHomeomorph_mk {Γ Γ' : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (h : ConjAct.toConjAct g • Γ = Γ') (z : UpperHalfPlane) : (quotientConjHomeomorph h) ⟦z⟧ = ⟦g • z⟧

@[simp]

theorem Subgroup.quotientConjHomeomorph_symm {Γ Γ' : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (h : ConjAct.toConjAct g • Γ = Γ') : (quotientConjHomeomorph h).symm = quotientConjHomeomorph ⋯

The inverse of the homeomorphism of coarse quotients induced by g is the one induced by g⁻¹.

@[simp]

theorem Subgroup.quotientConjHomeomorph_one {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : ConjAct.toConjAct 1 • Γ = Γ) : quotientConjHomeomorph h = Homeomorph.refl (MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane)

Conjugation by 1 induces the identity of the coarse quotient.

@[simp]

theorem Subgroup.quotientConjHomeomorph_trans {Γ Γ' : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {Γ'' : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {g' : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (h : ConjAct.toConjAct g • Γ = Γ') (h' : ConjAct.toConjAct g' • Γ' = Γ'') : (quotientConjHomeomorph h).trans (quotientConjHomeomorph h') = quotientConjHomeomorph ⋯

Conjugating by g and then by g' induces the same homeomorphism of coarse quotients as conjugating by g' * g.

theorem Subgroup.mdifferentiable_quotientConjHomeomorph {Γ Γ' : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} [ProperlyDiscontinuousSMul (↥Γ) UpperHalfPlane] (h : ConjAct.toConjAct g • Γ = Γ') : MDiff ⇑(quotientConjHomeomorph h)

The homeomorphism of coarse quotients induced by conjugation is holomorphic, also at the elliptic orbits: its pullback to the upper half-plane is the orbit projection of Γ' composed with the biholomorphism z ↦ g • z. Proper discontinuity of Γ' follows from that of Γ.