Documentation

Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

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

Instances For

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

Denominator of the formula for a fractional linear transformation

Instances For

@[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

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.

Instances For

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

Instances For

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) :

Fractional linear transformation, also known as the Moebius transformation

Instances For

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)

@[implicit_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.

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

theorem UpperHalfPlane.denom_one (z : UpperHalfPlane) :

denom 1 ↑z = 1

@[implicit_reducible]

noncomputable instance UpperHalfPlane.SLAction {R : Type u_1} [CommRing R] [Algebra R ℝ] :

MulAction (Matrix.SpecialLinearGroup (Fin 2) R) UpperHalfPlane

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 := ⋯ }

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.

Instances For

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 τ.

Instances For

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 τ

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

↥(Matrix.GLPos (Fin 2) ℝ)

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

Instances For

@[simp]

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

↑a = ↑b ↔ a = b

@[implicit_reducible]

noncomputable instance ModularGroup.instCoeSpecialLinearGroupFinOfNatNatIntSubtypeGeneralLinearGroupRealMemSubgroupGLPos :

Coe (Matrix.SpecialLinearGroup (Fin 2) ℤ) ↥(Matrix.GLPos (Fin 2) ℝ)

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.

Instances For

@[simp]

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

coeHom g = ↑g

@[simp]

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

↑(↑↑↑g i j) = ↑(↑g i j)

@[simp]

theorem ModularGroup.det_coe {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} :

(↑↑↑g).det = 1

theorem ModularGroup.coe_one :

↑1 = 1

@[implicit_reducible]

noncomputable instance ModularGroup.SLOnGLPos :

SMul (Matrix.SpecialLinearGroup (Fin 2) ℤ) ↥(Matrix.GLPos (Fin 2) ℝ)

theorem ModularGroup.SLOnGLPos_smul_apply (s : Matrix.SpecialLinearGroup (Fin 2) ℤ) (g : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : UpperHalfPlane) :

(s • g) • z = (↑s * g) • z

instance 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