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

Instances For

instance UpperHalfPlane.instCoeFun :

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

Equations

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

Instances For

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

Numerator of the formula for a fractional linear transformation

Equations

Instances For

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

Denominator of the formula for a fractional linear transformation

Equations

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)

def UpperHalfPlane.σ (g : GL (Fin 2) ℝ) :

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

Equations

Instances For

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

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

Fractional linear transformation, also known as the Moebius transformation

Equations

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)

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

Fractional linear transformation, also known as the Moebius transformation

Equations

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)

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

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

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

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

Equations

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

Instances For

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

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

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

instance ModularGroup.SLOnGLPos :

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

Equations

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