The upper half plane and its automorphisms

This file defines the GLPos 2 ℝ action on the upper half-plane by fractional linear transformations.

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 : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : UpperHalfPlane) : ℂ

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 : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : UpperHalfPlane) : ℂ

Denominator of the formula for a fractional linear transformation

Equations

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

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

theorem UpperHalfPlane.denom_ne_zero (g : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : UpperHalfPlane) : denom g z ≠ 0

theorem UpperHalfPlane.normSq_denom_pos (g : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : UpperHalfPlane) : 0 < Complex.normSq (denom g z)

theorem UpperHalfPlane.normSq_denom_ne_zero (g : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : UpperHalfPlane) : Complex.normSq (denom g z) ≠ 0

def UpperHalfPlane.smulAux' (g : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : UpperHalfPlane) : ℂ

Fractional linear transformation, also known as the Moebius transformation

Equations

• UpperHalfPlane.smulAux' g z = UpperHalfPlane.num g z / UpperHalfPlane.denom g z

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

def UpperHalfPlane.smulAux (g : ↥(Matrix.GLPos (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 (x y : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : UpperHalfPlane) : denom (x * y) z = denom x (smulAux y z) * denom y z

theorem UpperHalfPlane.mul_smul' (x y : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : UpperHalfPlane) : smulAux (x * y) z = smulAux x (smulAux y z)

instance UpperHalfPlane.instMulActionSubtypeGeneralLinearGroupFinOfNatNatRealMemSubgroupGLPos : MulAction (↥(Matrix.GLPos (Fin 2) ℝ)) UpperHalfPlane

The action of GLPos 2 ℝ on the upper half-plane by fractional linear transformations.

Equations

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

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.toGLPos.comp (Matrix.SpecialLinearGroup.map (algebraMap R ℝ)))

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

@[simp]

theorem UpperHalfPlane.coe_smul (g : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : UpperHalfPlane) : ↑(g • z) = num g z / denom g z

@[simp]

theorem UpperHalfPlane.re_smul (g : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : UpperHalfPlane) : (g • z).re = (num g z / denom g z).re

theorem UpperHalfPlane.im_smul (g : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : UpperHalfPlane) : (g • z).im = (num g z / denom g z).im

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

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

@[simp]

theorem UpperHalfPlane.neg_smul (g : ↥(Matrix.GLPos (Fin 2) ℝ)) (z : UpperHalfPlane) : -g • z = g • z

theorem UpperHalfPlane.denom_one (z : UpperHalfPlane) : denom 1 z = 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

@[deprecated ModularGroup.coe (since := "2024-11-19")]

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

Alias of ModularGroup.coe.

---

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

Equations

• ModularGroup.coe' = ModularGroup.coe

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)

@[deprecated ModularGroup.coe_apply_complex (since := "2024-11-19")]

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

Alias of ModularGroup.coe_apply_complex.

@[simp]

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

@[deprecated ModularGroup.det_coe (since := "2024-11-19")]

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

Alias of ModularGroup.det_coe.

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 (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane) : A • z = ↑A • 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 (↑g) z)

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

@[simp]

theorem ModularGroup.denom_S (z : UpperHalfPlane) : UpperHalfPlane.denom (↑S) z = ↑z