PSL(2) actions on the upper half-plane

The projective special linear groups PSL(2, ℤ) and PSL(2, ℝ) (quotients of SL(2, ·) by their centers {±I}) act faithfully on the upper half-plane ℍ. The PSL(2, ℝ)-action is the central-quotient descent of the SL(2, R)-action, uniformly in the coefficients; it agrees with Mathlib's PGL(2, ℝ)-action along toPGL (toPGL_smul) and with the PSL(2, ℤ)-action along the injective descent psl2zToPSL2R from TauCeti/LinearAlgebra/Matrix/ProjectiveSpecialLinearGroup.lean. The actions are measurable and preserve the invariant measure volume : Measure ℍ (inherited from Mathlib's GL(2, ℝ)-invariance).

Main results

• UpperHalfPlane.smul_eq_self_of_mem_center — the center of SL(2, R) acts trivially, for any coefficients mapping to ℝ.
• UpperHalfPlane.instMulActionPSL2 — the PSL(2, R)-action for any coefficients mapping to ℝ, descending the SL(2, R)-action along the central quotient, with the representative compatibility pslMk_smul and its pointwise-image form Matrix.SpecialLinearGroup.pslMk_smul_set.
• FaithfulSMul instances for PSL(2, ℤ) and PSL(2, ℝ) on ℍ, restricting Mathlib's faithful PGL(2, ℝ)-action along the injective toPGL and psl2zToPSL2R.
• SMulInvariantMeasure instances for SL(2, R) and PSL(2, R) (any coefficients mapping to ℝ) on (ℍ, volume).
• UpperHalfPlane.smul_eq_smul_of_coe_eq_smul — matrices differing by a nonzero scalar act identically on ℍ.
• UpperHalfPlane.glPosToPSL2R_smul — the det-normalized projective representative of a GL(2, ℝ)⁺ element (multiplicative by Real.sqrt_mul together with the centrality of positive scalars) acts on ℍ exactly as the original element.
• TauCeti.UpperHalfPlane.pslS_smul — TauCeti.pslS (the PSL(2, ℝ) image of ModularGroup.S) acts on ℍ as ModularGroup.S does; re_pslS_smul gives its effect on the real part, up to the normSq factor.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/Modularforms/PSL2Action.lean); the AINTLIB Jacobian computation of SL(2, ℤ)-invariance of the hyperbolic measure is not ported — Mathlib's SMulInvariantMeasure (GL (Fin 2) ℝ) ℍ volume subsumes it, and all invariance instances here descend from it.

References

• [DS] Diamond–Shurman, A First Course in Modular Forms, §5.4
• [Shi] Shimura, Arithmetic Theory of Automorphic Functions, §1.5
• The AINTLIB LeanModularForms project, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms (Modularforms/PSL2Action.lean)

instance UpperHalfPlane.instMeasurableConstSMulSpecialLinearGroupFinOfNatNat_tauCeti {R : Type u_1} [CommRing R] [Algebra R ℝ] : MeasurableConstSMul (Matrix.SpecialLinearGroup (Fin 2) R) UpperHalfPlane

instance UpperHalfPlane.instSMulInvariantMeasureSpecialLinearGroupFinOfNatNatVolume_tauCeti {R : Type u_1} [CommRing R] [Algebra R ℝ] : MeasureTheory.SMulInvariantMeasure (Matrix.SpecialLinearGroup (Fin 2) R) UpperHalfPlane MeasureTheory.volume

SL(2, R) preserves the invariant measure on ℍ for any coefficients mapping to ℝ; the action factors through GL(2, ℝ), whose invariance is Mathlib's.

theorem UpperHalfPlane.smul_eq_smul_of_coe_eq_smul {g h : GL (Fin 2) ℝ} {c : ℝ} (hc : c ≠ 0) (h_eq : ↑h = c • ↑g) (τ : UpperHalfPlane) : h • τ = g • τ

Nonzero-scalar action invariance for GL (Fin 2) ℝ: a matrix that is a nonzero scalar multiple of another acts identically on ℍ, through Mathlib's scalar-matrix action glScalar_smul.

@[simp]

theorem UpperHalfPlane.smul_eq_self_of_mem_center {R : Type u_1} [CommRing R] [Algebra R ℝ] (c : Matrix.SpecialLinearGroup (Fin 2) R) (hc : c ∈ Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) R)) (τ : UpperHalfPlane) : c • τ = τ

Central elements of SL(2, R) fix every point of ℍ, for any coefficients mapping to ℝ: they are the scalar matrices r • 1 with r ^ 2 = 1, and nonzero-scalar matrices act as the identity Möbius transformation.

@[instance_reducible]

noncomputable instance UpperHalfPlane.instMulActionPSL2 {R : Type u_1} [CommRing R] [Algebra R ℝ] : MulAction (Matrix.ProjectiveSpecialLinearGroup (Fin 2) R) UpperHalfPlane

The PSL(2, R)-action on ℍ for any coefficients mapping to ℝ: the descent of the SL(2, R)-action along the central quotient, well-defined since central elements fix every point (smul_eq_self_of_mem_center). The underlying permutation homomorphism is recoverable as MulAction.toPermHom.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem UpperHalfPlane.pslMk_smul {R : Type u_1} [CommRing R] [Algebra R ℝ] (g : Matrix.SpecialLinearGroup (Fin 2) R) (τ : UpperHalfPlane) : ↑g • τ = g • τ

The PSL(2, R) action of a representative coincides with the SL(2, R) action.

@[simp]

theorem Matrix.SpecialLinearGroup.pslMk_smul_set {R : Type u_1} [CommRing R] [Algebra R ℝ] (g : SpecialLinearGroup (Fin 2) R) (S : Set UpperHalfPlane) : ↑g • S = g • S

The PSL(2, R)-action on subsets of ℍ is the SL(2, R)-action of any representative, the pointwise-image counterpart of UpperHalfPlane.pslMk_smul.

instance UpperHalfPlane.instMeasurableConstSMulProjectiveSpecialLinearGroupFinOfNatNat_tauCeti {R : Type u_1} [CommRing R] [Algebra R ℝ] : MeasurableConstSMul (Matrix.ProjectiveSpecialLinearGroup (Fin 2) R) UpperHalfPlane

instance UpperHalfPlane.instSMulInvariantMeasureProjectiveSpecialLinearGroupFinOfNatNatVolume_tauCeti {R : Type u_1} [CommRing R] [Algebra R ℝ] : MeasureTheory.SMulInvariantMeasure (Matrix.ProjectiveSpecialLinearGroup (Fin 2) R) UpperHalfPlane MeasureTheory.volume

PSL(2, R) preserves the invariant measure on ℍ, descending the SL(2, R) invariance.

@[simp]

theorem UpperHalfPlane.toPGL_smul (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (τ : UpperHalfPlane) : Matrix.ProjectiveSpecialLinearGroup.toPGL g • τ = g • τ

Mathlib's PGL(2, ℝ)-action along toPGL agrees with the PSL(2, ℝ)-action.

instance UpperHalfPlane.instFaithfulSMulProjectiveSpecialLinearGroupFinOfNatNatReal_tauCeti : FaithfulSMul (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) UpperHalfPlane

The PSL(2, ℝ)-action on ℍ is faithful, through the faithful PGL(2, ℝ)-action and the injective toPGL.

@[simp]

theorem UpperHalfPlane.psl2zToPSL2R_smul (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane) : psl2zToPSL2R g • τ = g • τ

The PSL(2, ℤ)-action factors through the PSL(2, ℝ)-action along the descent psl2zToPSL2R.

instance UpperHalfPlane.instFaithfulSMulProjectiveSpecialLinearGroupFinOfNatNatInt_tauCeti : FaithfulSMul (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) UpperHalfPlane

The PSL(2, ℤ)-action on ℍ is faithful, through the injective descent psl2zToPSL2R and the faithfulness of the PSL(2, ℝ)-action.

theorem UpperHalfPlane.glPosToPSL2R_smul (g : ↥(Matrix.GLPos (Fin 2) ℝ)) (τ : UpperHalfPlane) : glPosToPSL2R g • τ = g • τ

Action equivariance: the projective representative glPosToPSL2R g acts on ℍ exactly as g does, even though det g need not be 1.

theorem TauCeti.UpperHalfPlane.pslS_smul (τ : UpperHalfPlane) : pslS • τ = ModularGroup.S • τ

pslS acts on ℍ as ModularGroup.S does, i.e. as z ↦ -1/z.

theorem TauCeti.UpperHalfPlane.re_pslS_smul (τ : UpperHalfPlane) : (pslS • τ).re = -τ.re / Complex.normSq ↑τ

pslS reverses the sign of the real part, up to the norm-square factor.

theorem TauCeti.UpperHalfPlane.re_mul_pslS_inv_smul (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) : ((g * pslS)⁻¹ • z).re = -(g⁻¹ • z).re / Complex.normSq ↑(g⁻¹ • z)

Translating by (g * pslS)⁻¹ negates the real part of the g⁻¹-translate w = g⁻¹ • z and divides it by normSq w: ((g * pslS)⁻¹ • z).re = -w.re / normSq w.