# The upper half plane and its automorphisms #

This file defines UpperHalfPlane to be the upper half plane in .

We furthermore equip it with the structure of a GLPos 2 ℝ action by fractional linear transformations.

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

The open upper half plane

Equations
Instances For

The open upper half plane

Equations
Instances For

Canonical embedding of the upper half-plane into .

Equations
• z = z
Instances For
Equations
theorem UpperHalfPlane.ext {a : UpperHalfPlane} {b : UpperHalfPlane} (h : a = b) :
a = b
@[simp]
theorem UpperHalfPlane.ext_iff {a : UpperHalfPlane} {b : UpperHalfPlane} :
a = b a = b

Imaginary part

Equations
• = (z).im
Instances For

Real part

Equations
• = (z).re
Instances For
theorem UpperHalfPlane.ext' {a : UpperHalfPlane} {b : UpperHalfPlane} (hre : ) (him : ) :
a = b

Extensionality lemma in terms of UpperHalfPlane.re and UpperHalfPlane.im.

def UpperHalfPlane.mk (z : ) (h : 0 < z.im) :

Constructor for UpperHalfPlane. It is useful if ⟨z, h⟩ makes Lean use a wrong typeclass instance.

Equations
• = { val := z, property := h }
Instances For
@[simp]
theorem UpperHalfPlane.coe_im (z : UpperHalfPlane) :
(z).im =
@[simp]
theorem UpperHalfPlane.coe_re (z : UpperHalfPlane) :
(z).re =
@[simp]
theorem UpperHalfPlane.mk_re (z : ) (h : 0 < z.im) :
= z.re
@[simp]
theorem UpperHalfPlane.mk_im (z : ) (h : 0 < z.im) :
= z.im
@[simp]
theorem UpperHalfPlane.coe_mk (z : ) (h : 0 < z.im) :
() = z
@[simp]
theorem UpperHalfPlane.mk_coe (z : UpperHalfPlane) (h : optParam (0 < (z).im) ) :
UpperHalfPlane.mk (z) h = z

Extension for the positivity tactic: UpperHalfPlane.im.

Instances For

Extension for the positivity tactic: UpperHalfPlane.coe.

Instances For
theorem UpperHalfPlane.normSq_pos (z : UpperHalfPlane) :
0 < Complex.normSq z
theorem UpperHalfPlane.normSq_ne_zero (z : UpperHalfPlane) :
Complex.normSq z 0

Numerator of the formula for a fractional linear transformation

Equations
• = (g 0 0) * z + (g 0 1)
Instances For

Denominator of the formula for a fractional linear transformation

Equations
• = (g 1 0) * z + (g 1 1)
Instances For
theorem UpperHalfPlane.linear_ne_zero (cd : Fin 2) (z : UpperHalfPlane) (h : cd 0) :
(cd 0) * z + (cd 1) 0
theorem UpperHalfPlane.normSq_denom_pos (g : (Matrix.GLPos (Fin 2) )) (z : UpperHalfPlane) :
0 < Complex.normSq ()
theorem UpperHalfPlane.normSq_denom_ne_zero (g : (Matrix.GLPos (Fin 2) )) (z : UpperHalfPlane) :
Complex.normSq () 0

Fractional linear transformation, also known as the Moebius transformation

Equations
Instances For
theorem UpperHalfPlane.smulAux'_im (g : (Matrix.GLPos (Fin 2) )) (z : UpperHalfPlane) :
().im = / Complex.normSq ()

Fractional linear transformation, also known as the Moebius transformation

Equations
Instances For

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} [] [] :
Equations

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

Equations
• g = Matrix.SpecialLinearGroup.toGLPos
Instances For
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem UpperHalfPlane.ModularGroup.coe'_apply_complex {g : } {i : Fin 2} {j : Fin 2} :
(g i j) = (g i j)
@[simp]
Equations
theorem UpperHalfPlane.ModularGroup.SLOnGLPos_smul_apply (s : ) (g : (Matrix.GLPos (Fin 2) )) (z : UpperHalfPlane) :
(s g) z = (s * g) z
Equations
theorem UpperHalfPlane.ModularGroup.subgroup_on_glpos_smul_apply (Γ : ) (s : Γ) (g : (Matrix.GLPos (Fin 2) )) (z : UpperHalfPlane) :
(s g) z = (s * g) z
instance UpperHalfPlane.ModularGroup.subgroupSL (Γ : ) :
SMul (Γ) ()
Equations
• = { smul := fun (s : Γ) (g : ) => s * g }
theorem UpperHalfPlane.ModularGroup.subgroup_on_SL_apply (Γ : ) (s : Γ) (g : ) (z : UpperHalfPlane) :
(s g) z = (s * g) z
theorem UpperHalfPlane.specialLinearGroup_apply {R : Type u_1} [] [] (g : ) (z : UpperHalfPlane) :
g z = UpperHalfPlane.mk (((() (g 0 0)) * z + (() (g 0 1))) / ((() (g 1 0)) * z + (() (g 1 1))))
@[simp]
theorem UpperHalfPlane.coe_smul (g : (Matrix.GLPos (Fin 2) )) (z : UpperHalfPlane) :
(g z) =
@[simp]
theorem UpperHalfPlane.c_mul_im_sq_le_normSq_denom (z : UpperHalfPlane) (g : ) :
((Matrix.SpecialLinearGroup.toGLPos g) 1 0 * ) ^ 2 Complex.normSq (UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGLPos g) z)
@[simp]
theorem UpperHalfPlane.neg_smul (g : (Matrix.GLPos (Fin 2) )) (z : UpperHalfPlane) :
-g z = g z
@[simp]
theorem UpperHalfPlane.ModularGroup.subgroup_moeb (Γ : ) (A : Γ) (z : UpperHalfPlane) :
A z = A z
@[simp]
theorem UpperHalfPlane.ModularGroup.subgroup_to_sl_moeb (Γ : ) (A : Γ) (z : UpperHalfPlane) :
A z = A z
theorem UpperHalfPlane.ModularGroup.denom_apply (g : ) (z : UpperHalfPlane) :
UpperHalfPlane.denom (g) z = (g 1 0) * z + (g 1 1)
@[simp]
theorem UpperHalfPlane.coe_pos_real_smul (x : { x : // 0 < x }) (z : UpperHalfPlane) :
(x z) = x z
@[simp]
theorem UpperHalfPlane.pos_real_im (x : { x : // 0 < x }) (z : UpperHalfPlane) :
@[simp]
theorem UpperHalfPlane.pos_real_re (x : { x : // 0 < x }) (z : UpperHalfPlane) :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem UpperHalfPlane.coe_vadd (x : ) (z : UpperHalfPlane) :
(x +ᵥ z) = x + z
@[simp]
theorem UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_eq_zero (g : ) (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 : ) (hc : g 1 0 0) :
∃ (u : { x : // 0 < x }) (v : ) (w : ), (fun (x : UpperHalfPlane) => g x) = (fun (x : UpperHalfPlane) => w +ᵥ x) (fun (x : UpperHalfPlane) => ) (fun (x : UpperHalfPlane) => v +ᵥ x) fun (x : UpperHalfPlane) => u x