Maps into `PSL(2, ℝ)` #

The algebraic maps connecting the matrix groups of the modular theory to PSL(2, ℝ):

sl2zToPSL2R : SL(2, ℤ) →* PSL(2, ℝ) — cast entries to ℝ, then project; its kernel is the center of SL(2, ℤ) (sl2zToPSL2R_ker), since an integer matrix casts to a real scalar matrix iff it is itself scalar.
psl2zToPSL2R : PSL(2, ℤ) →* PSL(2, ℝ) — the injective descent (psl2zToPSL2R_injective).
glPosToSL2R : GL(2, ℝ)⁺ →* SL(2, ℝ) — the det-normalized representative (√det g)⁻¹ • g, a monoid homomorphism since positive scalars are central and √ is multiplicative on them; glPosToPSL2R is its projectivization.
Matrix.ProjectiveSpecialLinearGroup.mk_neg — negating a matrix of SL(2, S) does not change its class in PSL(2, S).
TauCeti.pslS : PSL(2, ℝ) — the image of ModularGroup.S, squaring to the identity (pslS_mul_self, pslS_inv).

The actions of these groups on the upper half-plane, and the compatibility of these maps with them, are in TauCeti/Analysis/Complex/UpperHalfPlane/PSL/Action.lean.

sl2zToPSL2R, psl2zToPSL2R, and glPosToSL2R/glPosToPSL2R are split out of the AINTLIB LeanModularForms port (LeanModularForms/Modularforms/PSL2Action.lean, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms); pslS is not part of that port. All are pure matrix-group algebra with no dependence on ℍ.

source

def sl2zToPSL2R :

Matrix.SpecialLinearGroup (Fin 2) ℤ →* Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ

The lift SL(2, ℤ) →* PSL(2, ℝ): cast SL(2, ℤ) entries to ℝ via SpecialLinearGroup.map (Int.castRingHom ℝ), then project to the ±I-quotient.

Equations

sl2zToPSL2R = (QuotientGroup.mk' (Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) ℝ))).comp (Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ))

Instances For

source

@[simp]

theorem sl2zToPSL2R_apply (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) :

sl2zToPSL2R g = ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g)

source

theorem sl2zToPSL2R_ker :

sl2zToPSL2R.ker = Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) ℤ)

The kernel of sl2zToPSL2R is the center of SL(2, ℤ): an integer matrix casts to a real scalar matrix iff it is itself a scalar matrix.

source

def psl2zToPSL2R :

Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ →* Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ

The descended hom PSL(2, ℤ) →* PSL(2, ℝ). sl2zToPSL2R factors through PSL(2, ℤ) = SL(2, ℤ) ⧸ center SL(2, ℤ) since integer scalar matrices map into center SL(2, ℝ).

Equations

psl2zToPSL2R = QuotientGroup.lift (Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) ℤ)) sl2zToPSL2R psl2zToPSL2R._proof_2✝

Instances For

source

@[simp]

theorem psl2zToPSL2R_mk (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) :

psl2zToPSL2R ↑g = sl2zToPSL2R g

source

theorem psl2zToPSL2R_injective :

Function.Injective ⇑psl2zToPSL2R

psl2zToPSL2R is injective: its kernel is the image of sl2zToPSL2R.ker = center SL(2, ℤ) under the PSL(2, ℤ)-projection, which is ⊥.

source

@[simp]

theorem Matrix.ProjectiveSpecialLinearGroup.mk_neg {S : Type u_1} [CommRing S] (A : SpecialLinearGroup (Fin 2) S) :

↑(-A) = ↑A

Negating a special linear matrix does not change its class in PSL(2, S).

source

theorem ModularGroup.S_inv_PSL2Z :

(↑S)⁻¹ = ↑S

ModularGroup.S is its own inverse in PSL(2, ℤ).

source

@[simp]

theorem ModularGroup.S_mul_S_PSL2Z :

↑S * ↑S = 1

ModularGroup.S squares to the identity in PSL(2, ℤ).

source

noncomputable def TauCeti.pslS :

Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ

The image of ModularGroup.S (the matrix !![0, -1; 1, 0], representing the Möbius map z ↦ -1/z) in PSL(2, ℝ).

Equations

TauCeti.pslS = psl2zToPSL2R ↑ModularGroup.S

Instances For

source

theorem TauCeti.pslS_def :

pslS = psl2zToPSL2R ↑ModularGroup.S

pslS is the image of ModularGroup.S under psl2zToPSL2R.

source

@[simp]

theorem TauCeti.pslS_mul_self :

pslS * pslS = 1

pslS squares to the identity of PSL(2, ℝ).

source

@[simp]

theorem TauCeti.pslS_inv :

pslS ⁻¹ = pslS

pslS is its own inverse.

source

noncomputable def glPosToSL2R :

↥(Matrix.GLPos (Fin 2) ℝ) →* Matrix.SpecialLinearGroup (Fin 2) ℝ

The det-normalized SL(2, ℝ) representative of a GL(2, ℝ)⁺ element, as a monoid homomorphism: the matrix (√ det g)⁻¹ • g has determinant 1, and normalization is multiplicative because positive scalars are central and √ is multiplicative on them.

Equations