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.«term↑ₘ_» : Lean.ParserDescr

The coercion first into an element of GL(2, ℝ)⁺, then GL(2, ℝ) and finally a 2 × 2 matrix.

This notation is scoped in namespace UpperHalfPlane.

Equations

• UpperHalfPlane.«term↑ₘ_» = Lean.ParserDescr.node `UpperHalfPlane.«term↑ₘ_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↑ₘ") (Lean.ParserDescr.cat `term 1024))

instance UpperHalfPlane.instCoeFun : CoeFun ↥(Matrix.GLPos (Fin 2) ℝ) fun (x : ↥(Matrix.GLPos (Fin 2) ℝ)) => Fin 2 → Fin 2 → ℝ

Equations

• UpperHalfPlane.instCoeFun = { coe := fun (A : ↥(Matrix.GLPos (Fin 2) ℝ)) => ↑↑A }

def UpperHalfPlane.«term↑ₘ[_]_» : Lean.ParserDescr

The coercion into an element of GL(2, R) and finally a 2 × 2 matrix over R. This is similar to ↑ₘ, but without positivity requirements, and allows the user to specify the ring R, which can be useful to help Lean elaborate correctly.

This notation is scoped in namespace UpperHalfPlane.

Equations

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

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

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) ℝ) : ℂ →+* ℂ

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

Equations

• UpperHalfPlane.σ g = if 0 < ↑(Matrix.GeneralLinearGroup.det g) then RingHom.id ℂ else starRingEnd ℂ

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‖

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)

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

Fractional linear transformation, also known as the Moebius transformation

Equations

• UpperHalfPlane.smulAux g z = UpperHalfPlane.mk (UpperHalfPlane.smulAux' g ↑z) ⋯

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 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 := UpperHalfPlane.glAction._proof_1 }

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 = mk (num g ↑z / denom g ↑z) ⋯

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

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 = mk ((↑((algebraMap R ℝ) (↑g 0 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 0 1))) / (↑((algebraMap R ℝ) (↑g 1 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 1 1)))) ⋯

theorem UpperHalfPlane.modular_S_smul (z : UpperHalfPlane) : ModularGroup.S • z = mk (-↑z)⁻¹ ⋯

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

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

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

Equations

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

@[simp]

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

instance ModularGroup.instCoeSpecialLinearGroupFinOfNatNatIntSubtypeGeneralLinearGroupRealMemSubgroupGLPos : Coe (Matrix.SpecialLinearGroup (Fin 2) ℤ) ↥(Matrix.GLPos (Fin 2) ℝ)

Equations

• ModularGroup.instCoeSpecialLinearGroupFinOfNatNatIntSubtypeGeneralLinearGroupRealMemSubgroupGLPos = { coe := ModularGroup.coe }

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

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

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

Equations

• ModularGroup.SLOnGLPos = { smul := fun (s : Matrix.SpecialLinearGroup (Fin 2) ℤ) (g : ↥(Matrix.GLPos (Fin 2) ℝ)) => ↑s * g }

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