Group action on the upper half-plane

We equip the upper half-plane with the structure of a GL (Fin 2) ℝ action by fractional linear transformations (composing with complex conjugation when needed to extend the action from the positive-determinant subgroup, so that !![-1, 0; 0, 1] acts as z ↦ -conj z.)

def UpperHalfPlane.num (g : GL (Fin 2) ℝ) (z : ℂ) : ℂ

Numerator of the formula for a fractional linear transformation

Equations

• UpperHalfPlane.num g z = ↑(↑g 0 0) * z + ↑(↑g 0 1)

def UpperHalfPlane.denom (g : GL (Fin 2) ℝ) (z : ℂ) : ℂ

Denominator of the formula for a fractional linear transformation

Equations

• UpperHalfPlane.denom g z = ↑(↑g 1 0) * z + ↑(↑g 1 1)

@[simp]

theorem UpperHalfPlane.num_neg (g : GL (Fin 2) ℝ) (z : ℂ) : num (-g) z = -num g z

@[simp]

theorem UpperHalfPlane.denom_neg (g : GL (Fin 2) ℝ) (z : ℂ) : denom (-g) z = -denom g z

theorem UpperHalfPlane.linear_ne_zero_of_im {cd : Fin 2 → ℝ} {z : ℂ} (hz : z.im ≠ 0) (h : cd ≠ 0) : ↑(cd 0) * z + ↑(cd 1) ≠ 0

theorem UpperHalfPlane.linear_ne_zero {cd : Fin 2 → ℝ} (τ : UpperHalfPlane) (h : cd ≠ 0) : ↑(cd 0) * ↑τ + ↑(cd 1) ≠ 0

theorem UpperHalfPlane.denom_ne_zero_of_im (g : GL (Fin 2) ℝ) {z : ℂ} (hz : z.im ≠ 0) : denom g z ≠ 0

@[simp]

theorem UpperHalfPlane.denom_ne_zero (g : GL (Fin 2) ℝ) (z : UpperHalfPlane) : denom g ↑z ≠ 0

theorem UpperHalfPlane.normSq_denom_pos (g : GL (Fin 2) ℝ) {z : ℂ} (hz : z.im ≠ 0) : 0 < Complex.normSq (denom g z)

theorem UpperHalfPlane.normSq_denom_ne_zero (g : GL (Fin 2) ℝ) {z : ℂ} (hz : z.im ≠ 0) : Complex.normSq (denom g z) ≠ 0

theorem UpperHalfPlane.denom_cocycle (g h : GL (Fin 2) ℝ) {z : ℂ} (hz : z.im ≠ 0) : denom (g * h) z = denom g (num h z / denom h z) * denom h z

theorem UpperHalfPlane.moebius_im (g : GL (Fin 2) ℝ) (z : ℂ) : (num g z / denom g z).im = ↑(Matrix.GeneralLinearGroup.det g) * z.im / Complex.normSq (denom g z)

noncomputable def UpperHalfPlane.σ (g : GL (Fin 2) ℝ) : ℂ ≃A[ℝ] ℂ

Automorphism of ℂ: the identity if 0 < det g and conjugation otherwise.

Equations

• UpperHalfPlane.σ g = if 0 < ↑(Matrix.GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE

theorem UpperHalfPlane.σ_conj (g : GL (Fin 2) ℝ) (z : ℂ) : (σ g) ((starRingEnd ℂ) z) = (starRingEnd ℂ) ((σ g) z)

@[simp]

theorem UpperHalfPlane.σ_ofReal (g : GL (Fin 2) ℝ) (y : ℝ) : (σ g) ↑y = ↑y

theorem UpperHalfPlane.σ_num (g h : GL (Fin 2) ℝ) (z : ℂ) : (σ g) (num h z) = num h ((σ g) z)

theorem UpperHalfPlane.σ_denom (g h : GL (Fin 2) ℝ) (z : ℂ) : (σ g) (denom h z) = denom h ((σ g) z)

@[simp]

theorem UpperHalfPlane.σ_neg (g : GL (Fin 2) ℝ) : σ (-g) = σ g

@[simp]

theorem UpperHalfPlane.σ_sq (g : GL (Fin 2) ℝ) (z : ℂ) : (σ g) ((σ g) z) = z

theorem UpperHalfPlane.σ_im_ne_zero {g : GL (Fin 2) ℝ} {z : ℂ} : ((σ g) z).im ≠ 0 ↔ z.im ≠ 0

theorem UpperHalfPlane.σ_mul (g g' : GL (Fin 2) ℝ) (z : ℂ) : (σ (g * g')) z = (σ g) ((σ g') z)

theorem UpperHalfPlane.σ_mul_comm (g h : GL (Fin 2) ℝ) (z : ℂ) : (σ g) ((σ h) z) = (σ h) ((σ g) z)

@[simp]

theorem UpperHalfPlane.norm_σ (g : GL (Fin 2) ℝ) (z : ℂ) : ‖(σ g) z‖ = ‖z‖

noncomputable def UpperHalfPlane.smulAux' (g : GL (Fin 2) ℝ) (z : ℂ) : ℂ

Fractional linear transformation, also known as the Moebius transformation

Equations

• UpperHalfPlane.smulAux' g z = (UpperHalfPlane.σ g) (UpperHalfPlane.num g z / UpperHalfPlane.denom g z)

theorem UpperHalfPlane.smulAux'_im (g : GL (Fin 2) ℝ) (z : ℂ) : (smulAux' g z).im = |↑(Matrix.GeneralLinearGroup.det g)| * z.im / Complex.normSq (denom g z)

noncomputable def UpperHalfPlane.smulAux (g : GL (Fin 2) ℝ) (z : UpperHalfPlane) : UpperHalfPlane

Fractional linear transformation, also known as the Moebius transformation

Equations

• UpperHalfPlane.smulAux g z = { coe := UpperHalfPlane.smulAux' g ↑z, coe_im_pos := ⋯ }

theorem UpperHalfPlane.denom_cocycle' (g h : GL (Fin 2) ℝ) (z : UpperHalfPlane) : denom (g * h) ↑z = (σ h) (denom g ↑(smulAux h z)) * denom h ↑z

theorem UpperHalfPlane.mul_smul' (g h : GL (Fin 2) ℝ) (z : UpperHalfPlane) : smulAux (g * h) z = smulAux g (smulAux h z)

@[instance_reducible]

noncomputable instance UpperHalfPlane.glAction : MulAction (GL (Fin 2) ℝ) UpperHalfPlane

Action of GL (Fin 2) ℝ on the upper half-plane, with GL(2, ℝ)⁺ acting by Moebius transformations in the usual way, extended to all of GL (Fin 2) ℝ using complex conjugation.

Equations

• UpperHalfPlane.glAction = { smul := UpperHalfPlane.smulAux, mul_smul := UpperHalfPlane.mul_smul', one_smul := ⋯ }

theorem UpperHalfPlane.coe_smul (g : GL (Fin 2) ℝ) (z : UpperHalfPlane) : ↑(g • z) = (σ g) (num g ↑z / denom g ↑z)

theorem UpperHalfPlane.coe_smul_of_det_pos {g : GL (Fin 2) ℝ} (hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)) (z : UpperHalfPlane) : ↑(g • z) = num g ↑z / denom g ↑z

theorem UpperHalfPlane.denom_cocycle_σ (g h : GL (Fin 2) ℝ) (z : UpperHalfPlane) : denom (g * h) ↑z = (σ h) (denom g ↑(h • z)) * denom h ↑z

theorem UpperHalfPlane.glPos_smul_def {g : GL (Fin 2) ℝ} (hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)) (z : UpperHalfPlane) : g • z = { coe := num g ↑z / denom g ↑z, coe_im_pos := ⋯ }

theorem UpperHalfPlane.re_smul (g : GL (Fin 2) ℝ) (z : UpperHalfPlane) : (g • z).re = (num g ↑z / denom g ↑z).re

theorem UpperHalfPlane.im_smul (g : GL (Fin 2) ℝ) (z : UpperHalfPlane) : (g • z).im = |(num g ↑z / denom g ↑z).im|

theorem UpperHalfPlane.im_smul_eq_div_normSq (g : GL (Fin 2) ℝ) (z : UpperHalfPlane) : (g • z).im = |↑(Matrix.GeneralLinearGroup.det g)| * z.im / Complex.normSq (denom g ↑z)

theorem UpperHalfPlane.c_mul_im_sq_le_normSq_denom (g : GL (Fin 2) ℝ) (z : UpperHalfPlane) : (↑g 1 0 * z.im) ^ 2 ≤ Complex.normSq (denom g ↑z)

@[simp]

theorem UpperHalfPlane.neg_smul (g : GL (Fin 2) ℝ) (z : UpperHalfPlane) : -g • z = g • z

@[simp]

theorem UpperHalfPlane.num_one (z : UpperHalfPlane) : num 1 ↑z = ↑z

@[simp]

theorem UpperHalfPlane.denom_one (z : UpperHalfPlane) : denom 1 ↑z = 1

@[simp]

theorem UpperHalfPlane.num_scalar (u : ℝˣ) (z : UpperHalfPlane) : num ((Matrix.GeneralLinearGroup.scalar (Fin 2)) u) ↑z = ↑↑u * ↑z

@[simp]

theorem UpperHalfPlane.denom_scalar (u : ℝˣ) (z : UpperHalfPlane) : denom ((Matrix.GeneralLinearGroup.scalar (Fin 2)) u) ↑z = ↑↑u

@[simp]

theorem UpperHalfPlane.glScalar_smul (u : ℝˣ) (z : UpperHalfPlane) : (Matrix.GeneralLinearGroup.scalar (Fin 2)) u • z = z

instance UpperHalfPlane.instIsPretransitiveGeneralLinearGroupFinOfNatNatReal : MulAction.IsPretransitive (GL (Fin 2) ℝ) UpperHalfPlane

@[instance_reducible]

noncomputable instance UpperHalfPlane.instMulActionProjGenLinGroupFinOfNatNatReal : MulAction (Matrix.ProjGenLinGroup (Fin 2) ℝ) UpperHalfPlane

Equations

• UpperHalfPlane.instMulActionProjGenLinGroupFinOfNatNatReal = Matrix.ProjGenLinGroup.mulActionOfGL UpperHalfPlane.glScalar_smul

@[simp]

theorem UpperHalfPlane.pglMk_smul (g : GL (Fin 2) ℝ) (z : UpperHalfPlane) : Matrix.ProjGenLinGroup.mk g • z = g • z

instance UpperHalfPlane.instIsPretransitiveProjGenLinGroupFinOfNatNatReal : MulAction.IsPretransitive (Matrix.ProjGenLinGroup (Fin 2) ℝ) UpperHalfPlane

@[instance_reducible]

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

Equations

• UpperHalfPlane.SLAction = MulAction.compHom UpperHalfPlane (Matrix.SpecialLinearGroup.mapGL ℝ)

theorem UpperHalfPlane.coe_specialLinearGroup_apply {R : Type u_1} [CommRing R] [Algebra R ℝ] (g : Matrix.SpecialLinearGroup (Fin 2) R) (z : UpperHalfPlane) : ↑(g • z) = (↑((algebraMap R ℝ) (↑g 0 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 0 1))) / (↑((algebraMap R ℝ) (↑g 1 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 1 1)))

theorem UpperHalfPlane.specialLinearGroup_apply {R : Type u_1} [CommRing R] [Algebra R ℝ] (g : Matrix.SpecialLinearGroup (Fin 2) R) (z : UpperHalfPlane) : g • z = { coe := (↑((algebraMap R ℝ) (↑g 0 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 0 1))) / (↑((algebraMap R ℝ) (↑g 1 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 1 1))), coe_im_pos := ⋯ }

these next few lemmas are not flagged @simp because of the constructors on the RHS; instead we use the versions with coercions to ℂ as simp lemmas instead.

theorem UpperHalfPlane.modular_S_smul (z : UpperHalfPlane) : ModularGroup.S • z = { coe := (-↑z)⁻¹, coe_im_pos := ⋯ }

theorem UpperHalfPlane.modular_T_zpow_smul (z : UpperHalfPlane) (n : ℤ) : ModularGroup.T ^ n • z = ↑n +ᵥ z

theorem UpperHalfPlane.modular_T_smul (z : UpperHalfPlane) : ModularGroup.T • z = 1 +ᵥ z

theorem UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_eq_zero (g : Matrix.SpecialLinearGroup (Fin 2) ℝ) (hc : ↑g 1 0 = 0) : ∃ (u : { x : ℝ // 0 < x }) (v : ℝ), (fun (x : UpperHalfPlane) => g • x) = (fun (x : UpperHalfPlane) => v +ᵥ x) ∘ fun (x : UpperHalfPlane) => u • x

theorem UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_ne_zero (g : Matrix.SpecialLinearGroup (Fin 2) ℝ) (hc : ↑g 1 0 ≠ 0) : ∃ (u : { x : ℝ // 0 < x }) (v : ℝ) (w : ℝ), (fun (x : UpperHalfPlane) => g • x) = (fun (x : UpperHalfPlane) => w +ᵥ x) ∘ (fun (x : UpperHalfPlane) => ModularGroup.S • x) ∘ (fun (x : UpperHalfPlane) => v +ᵥ x) ∘ fun (x : UpperHalfPlane) => u • x

noncomputable def UpperHalfPlane.toSL2R (z : UpperHalfPlane) : Matrix.SpecialLinearGroup (Fin 2) ℝ

Map from ℍ to SL(2, ℝ), giving a continuous section of the map g ↦ g • I.

Equations

• z.toSL2R = ⟨!![√z.im, z.re / √z.im; 0, 1 / √z.im], ⋯⟩

theorem UpperHalfPlane.toSL2R_apply (z : UpperHalfPlane) : z.toSL2R = ⟨!![√z.im, z.re / √z.im; 0, 1 / √z.im], ⋯⟩

@[simp]

theorem UpperHalfPlane.coe_toSL2R (z : UpperHalfPlane) : ↑z.toSL2R = !![√z.im, z.re / √z.im; 0, 1 / √z.im]

@[simp]

theorem UpperHalfPlane.toSL2R_smul_I (z : UpperHalfPlane) : z.toSL2R • I = z

instance UpperHalfPlane.isPretransitiveSL2R : MulAction.IsPretransitive (Matrix.SpecialLinearGroup (Fin 2) ℝ) UpperHalfPlane

SL(2, ℝ) acts transitively on the upper half-plane.

instance UpperHalfPlane.isPretransitiveGL2R : MulAction.IsPretransitive (GL (Fin 2) ℝ) UpperHalfPlane

GL(2, ℝ) acts transitively on the upper half-plane.

noncomputable def UpperHalfPlane.J : GL (Fin 2) ℝ

The matrix [-1, 0; 0, 1], which defines an anti-holomorphic involution of ℍ via τ ↦ -conj τ.

Equations

• UpperHalfPlane.J = Matrix.GeneralLinearGroup.mkOfDetNeZero !![-1, 0; 0, 1] UpperHalfPlane.J._proof_1

theorem UpperHalfPlane.coe_J_smul (τ : UpperHalfPlane) : ↑(J • τ) = -(starRingEnd ℂ) ↑τ

@[simp]

theorem UpperHalfPlane.val_J : ↑J = !![-1, 0; 0, 1]

@[simp]

theorem UpperHalfPlane.J_sq : J ^ 2 = 1

@[simp]

theorem UpperHalfPlane.det_J : Matrix.GeneralLinearGroup.det J = -1

@[simp]

theorem UpperHalfPlane.sigma_J : σ J = Complex.conjCAE

@[simp]

theorem UpperHalfPlane.denom_J (τ : ℂ) : denom J τ = 1

@[simp]

theorem UpperHalfPlane.denom_J_mul (g : GL (Fin 2) ℝ) (τ : ℂ) : denom (J * g) τ = denom g τ

@[deprecated "use GL(2, ℝ)" (since := "2026-04-29")]

noncomputable def ModularGroup.coe (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) : ↥(Matrix.GLPos (Fin 2) ℝ)

Canonical embedding of SL(2, ℤ) into GL(2, ℝ)⁺.

Equations

• ModularGroup.coe g = Matrix.SpecialLinearGroup.toGLPos ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g)

@[deprecated "use GL(2, ℝ)" (since := "2026-04-29")]

theorem ModularGroup.coe_inj (a b : Matrix.SpecialLinearGroup (Fin 2) ℤ) : coe a = coe b ↔ a = b

@[deprecated "use GL(2, ℝ)" (since := "2026-04-29")]

noncomputable def ModularGroup.coeHom : Matrix.SpecialLinearGroup (Fin 2) ℤ →* ↥(Matrix.GLPos (Fin 2) ℝ)

Canonical embedding of SL(2, ℤ) into GL(2, ℝ)⁺, bundled as a group hom.

Equations

• ModularGroup.coeHom = Matrix.SpecialLinearGroup.toGLPos.comp (Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ))

@[deprecated "use GL(2, ℝ)" (since := "2026-04-29")]

theorem ModularGroup.coeHom_apply (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) : coeHom g = coe g

@[deprecated "use GL(2, ℝ)" (since := "2026-04-29")]

theorem ModularGroup.coe_apply_complex {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} {i j : Fin 2} : ↑(↑↑(coe g) i j) = ↑(↑g i j)

@[deprecated "use GL(2, ℝ)" (since := "2026-04-29")]

theorem ModularGroup.det_coe {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} : (↑↑(coe g)).det = 1

@[deprecated "use GL(2, ℝ)" (since := "2026-04-29")]

theorem ModularGroup.coe_one : coe 1 = 1

@[reducible, deprecated "use GL(2, ℝ)" (since := "2026-04-29")]

noncomputable def ModularGroup.SLOnGLPos : SMul (Matrix.SpecialLinearGroup (Fin 2) ℤ) ↥(Matrix.GLPos (Fin 2) ℝ)

Multiplication action of SL(2, ℤ) on GL(2, ℝ)⁺.

Equations

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

@[deprecated "use GL(2, ℝ)" (since := "2026-04-29")]

theorem ModularGroup.SLOnGLPos_smul_apply (s : Matrix.SpecialLinearGroup (Fin 2) ℤ) (g : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : UpperHalfPlane) : (s • g) • z = (Matrix.SpecialLinearGroup.toGLPos ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) s) * g) • z

@[deprecated "use GL(2, ℝ)" (since := "2026-04-29")]

theorem ModularGroup.SL_to_GL_tower : IsScalarTower (Matrix.SpecialLinearGroup (Fin 2) ℤ) (↥(Matrix.GLPos (Fin 2) ℝ)) UpperHalfPlane

@[simp]

theorem ModularGroup.sl_moeb (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane) : g • z = Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g) • z

@[simp]

theorem ModularGroup.SL_neg_smul (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane) : -g • z = g • z

theorem ModularGroup.im_smul_eq_div_normSq (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane) : (g • z).im = z.im / Complex.normSq (UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z)

theorem ModularGroup.denom_apply (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane) : UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z = ↑(↑g 1 0) * ↑z + ↑(↑g 1 1)

@[simp]

theorem ModularGroup.denom_S (z : UpperHalfPlane) : UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S)) ↑z = ↑z