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

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

Denominator of the formula for a fractional linear transformation

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

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

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

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.J : GL (Fin 2) ℝ

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

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, ℝ)⁺.

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

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