The upper half plane and its automorphisms #

This file defines upper_half_plane to be the upper half plane in ℂ.

We furthermore equip it with the structure of an SL(2,ℝ) action by fractional linear transformations.

We define the notation ℍ for the upper half plane available in the locale upper_half_plane so as not to conflict with the quaternions.

source

def upper_half_plane :

Type

The open upper half plane

source

def upper_half_plane.im (z : ℍ) :

ℝ

Imaginary part

Equations

z.im = ↑z.im

source

def upper_half_plane.re (z : ℍ) :

ℝ

Real part

Equations

z.re = ↑z.re

source

@[simp]

theorem upper_half_plane.coe_im (z : ℍ) :

↑z.im = z.im

source

@[simp]

theorem upper_half_plane.coe_re (z : ℍ) :

↑z.re = z.re

source

theorem upper_half_plane.im_pos (z : ℍ) :

0 < z.im

source

theorem upper_half_plane.im_ne_zero (z : ℍ) :

z.im ≠ 0

source

theorem upper_half_plane.ne_zero (z : ℍ) :

↑z ≠ 0

source

theorem upper_half_plane.norm_sq_pos (z : ℍ) :

0 < ⇑complex.norm_sq ↑z

source

theorem upper_half_plane.norm_sq_ne_zero (z : ℍ) :

⇑complex.norm_sq ↑z ≠ 0

source

@[simp]

def upper_half_plane.num (g : SL(2,ℝ )) (z : ℍ) :

ℂ

Numerator of the formula for a fractional linear transformation

Equations

upper_half_plane.num g z = (↑(⇑g 0 0)) * ↑z + ↑(⇑g 0 1)

source

@[simp]

def upper_half_plane.denom (g : SL(2,ℝ )) (z : ℍ) :

ℂ

Denominator of the formula for a fractional linear transformation

Equations

upper_half_plane.denom g z = (↑(⇑g 1 0)) * ↑z + ↑(⇑g 1 1)

source

theorem upper_half_plane.linear_ne_zero (cd : fin 2 → ℝ) (z : ℍ) (h : cd ≠ 0) :

(↑(cd 0)) * ↑z + ↑(cd 1) ≠ 0

source

theorem upper_half_plane.denom_ne_zero (g : SL(2,ℝ )) (z : ℍ) :

upper_half_plane.denom g z ≠ 0

source

theorem upper_half_plane.norm_sq_denom_pos (g : SL(2,ℝ )) (z : ℍ) :

0 < ⇑complex.norm_sq (upper_half_plane.denom g z)

source

theorem upper_half_plane.norm_sq_denom_ne_zero (g : SL(2,ℝ )) (z : ℍ) :

⇑complex.norm_sq (upper_half_plane.denom g z) ≠ 0

source

noncomputable def upper_half_plane.smul_aux' (g : SL(2,ℝ )) (z : ℍ) :

ℂ

Fractional linear transformation

Equations

upper_half_plane.smul_aux' g z = upper_half_plane.num g z / upper_half_plane.denom g z

source

theorem upper_half_plane.smul_aux'_im (g : SL(2,ℝ )) (z : ℍ) :

(upper_half_plane.smul_aux' g z).im = z.im / ⇑complex.norm_sq (upper_half_plane.denom g z)

source

noncomputable def upper_half_plane.smul_aux (g : SL(2,ℝ )) (z : ℍ) :

ℍ

Fractional linear transformation

Equations

upper_half_plane.smul_aux g z = ⟨upper_half_plane.smul_aux' g z, _⟩

source

theorem upper_half_plane.denom_cocycle (x y : SL(2,ℝ )) (z : ℍ) :

upper_half_plane.denom (x * y) z = (upper_half_plane.denom x (upper_half_plane.smul_aux y z)) * upper_half_plane.denom y z

source

theorem upper_half_plane.mul_smul' (x y : SL(2,ℝ )) (z : ℍ) :

upper_half_plane.smul_aux (x * y) z = upper_half_plane.smul_aux x (upper_half_plane.smul_aux y z)

source

@[protected, instance]

noncomputable def upper_half_plane.mul_action :

mul_action SL(2,ℝ ) ℍ

The action of SL(2, ℝ) on the upper half-plane by fractional linear transformations.

Equations

upper_half_plane.mul_action = {to_has_scalar := {smul := upper_half_plane.smul_aux}, one_smul := upper_half_plane.mul_action._proof_1, mul_smul := upper_half_plane.mul_smul'}

source

@[simp]

theorem upper_half_plane.coe_smul (g : SL(2,ℝ )) (z : ℍ) :

↑(g • z) = upper_half_plane.num g z / upper_half_plane.denom g z

source

@[simp]

theorem upper_half_plane.re_smul (g : SL(2,ℝ )) (z : ℍ) :

(g • z).re = (upper_half_plane.num g z / upper_half_plane.denom g z).re

source

theorem upper_half_plane.im_smul (g : SL(2,ℝ )) (z : ℍ) :

(g • z).im = (upper_half_plane.num g z / upper_half_plane.denom g z).im

source

theorem upper_half_plane.im_smul_eq_div_norm_sq (g : SL(2,ℝ )) (z : ℍ) :

(g • z).im = z.im / ⇑complex.norm_sq (upper_half_plane.denom g z)

source

@[simp]

theorem upper_half_plane.neg_smul (g : SL(2,ℝ )) (z : ℍ) :

-g • z = g • z