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.

def UpperHalfPlane : Type

The open upper half plane

def UpperHalfPlane.termℍ : Lean.ParserDescr

def UpperHalfPlane.coe (z : UpperHalfPlane) : ℂ

Canonical embedding of the upper half-plane into ℂ.

instance UpperHalfPlane.instCoeOutUpperHalfPlaneComplex : CoeOut UpperHalfPlane ℂ

instance UpperHalfPlane.instInhabitedUpperHalfPlane : Inhabited UpperHalfPlane

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

instance UpperHalfPlane.canLift : CanLift ℂ UpperHalfPlane UpperHalfPlane.coe fun z => 0 < z.im

def UpperHalfPlane.im (z : UpperHalfPlane) : ℝ

Imaginary part

def UpperHalfPlane.re (z : UpperHalfPlane) : ℝ

Real part

theorem UpperHalfPlane.ext' {a : UpperHalfPlane} {b : UpperHalfPlane} (hre : UpperHalfPlane.re a = UpperHalfPlane.re b) (him : UpperHalfPlane.im a = UpperHalfPlane.im b) : a = b

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

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

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

@[simp]

theorem UpperHalfPlane.coe_im (z : UpperHalfPlane) : (↑z).im = UpperHalfPlane.im z

@[simp]

theorem UpperHalfPlane.coe_re (z : UpperHalfPlane) : (↑z).re = UpperHalfPlane.re z

@[simp]

theorem UpperHalfPlane.mk_re (z : ℂ) (h : 0 < z.im) : UpperHalfPlane.re (UpperHalfPlane.mk z h) = z.re

@[simp]

theorem UpperHalfPlane.mk_im (z : ℂ) (h : 0 < z.im) : UpperHalfPlane.im (UpperHalfPlane.mk z h) = z.im

@[simp]

theorem UpperHalfPlane.coe_mk (z : ℂ) (h : 0 < z.im) : ↑(UpperHalfPlane.mk z h) = z

@[simp]

theorem UpperHalfPlane.mk_coe (z : UpperHalfPlane) (h : optParam (0 < (↑z).im) (_ : 0 < (↑z).im)) : UpperHalfPlane.mk (↑z) h = z

theorem UpperHalfPlane.re_add_im (z : UpperHalfPlane) : ↑(UpperHalfPlane.re z) + ↑(UpperHalfPlane.im z) * Complex.I = ↑z

theorem UpperHalfPlane.im_pos (z : UpperHalfPlane) : 0 < UpperHalfPlane.im z

theorem UpperHalfPlane.im_ne_zero (z : UpperHalfPlane) : UpperHalfPlane.im z ≠ 0

theorem UpperHalfPlane.ne_zero (z : UpperHalfPlane) : ↑z ≠ 0

theorem UpperHalfPlane.normSq_pos (z : UpperHalfPlane) : 0 < ↑Complex.normSq ↑z

theorem UpperHalfPlane.normSq_ne_zero (z : UpperHalfPlane) : ↑Complex.normSq ↑z ≠ 0

theorem UpperHalfPlane.im_inv_neg_coe_pos (z : UpperHalfPlane) : 0 < (-↑z)⁻¹.im

def UpperHalfPlane.num (g : { x // x ∈ Matrix.GLPos (Fin 2) ℝ }) (z : UpperHalfPlane) : ℂ

Numerator of the formula for a fractional linear transformation

def UpperHalfPlane.denom (g : { x // x ∈ Matrix.GLPos (Fin 2) ℝ }) (z : UpperHalfPlane) : ℂ

Denominator of the formula for a fractional linear transformation

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 : { x // x ∈ Matrix.GLPos (Fin 2) ℝ }) (z : UpperHalfPlane) : UpperHalfPlane.denom g z ≠ 0

theorem UpperHalfPlane.normSq_denom_pos (g : { x // x ∈ Matrix.GLPos (Fin 2) ℝ }) (z : UpperHalfPlane) : 0 < ↑Complex.normSq (UpperHalfPlane.denom g z)

theorem UpperHalfPlane.normSq_denom_ne_zero (g : { x // x ∈ Matrix.GLPos (Fin 2) ℝ }) (z : UpperHalfPlane) : ↑Complex.normSq (UpperHalfPlane.denom g z) ≠ 0

def UpperHalfPlane.smulAux' (g : { x // x ∈ Matrix.GLPos (Fin 2) ℝ }) (z : UpperHalfPlane) : ℂ

Fractional linear transformation, also known as the Moebius transformation

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

def UpperHalfPlane.smulAux (g : { x // x ∈ Matrix.GLPos (Fin 2) ℝ }) (z : UpperHalfPlane) : UpperHalfPlane

Fractional linear transformation, also known as the Moebius transformation

theorem UpperHalfPlane.denom_cocycle (x : { x // x ∈ Matrix.GLPos (Fin 2) ℝ }) (y : { x // x ∈ Matrix.GLPos (Fin 2) ℝ }) (z : UpperHalfPlane) : UpperHalfPlane.denom (x * y) z = UpperHalfPlane.denom x (UpperHalfPlane.smulAux y z) * UpperHalfPlane.denom y z

theorem UpperHalfPlane.mul_smul' (x : { x // x ∈ Matrix.GLPos (Fin 2) ℝ }) (y : { x // x ∈ Matrix.GLPos (Fin 2) ℝ }) (z : UpperHalfPlane) : UpperHalfPlane.smulAux (x * y) z = UpperHalfPlane.smulAux x (UpperHalfPlane.smulAux y z)

instance UpperHalfPlane.instMulActionSubtypeGeneralLinearGroupFinOfNatNatInstOfNatNatRealInstDecidableEqFinFintypeToCommRingToStrictOrderedCommRingLinearOrderedCommRingMemSubgroupInstGroupUnitsMatrixToMonoidToMonoidWithZeroSemiringToSemiringToCommSemiringInstMembershipInstSetLikeSubgroupGLPosUpperHalfPlaneToMonoidToMonoidToDivInvMonoidToSubmonoid : MulAction { x // x ∈ Matrix.GLPos (Fin 2) ℝ } UpperHalfPlane

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

instance UpperHalfPlane.SLAction {R : Type u_1} [CommRing R] [Algebra R ℝ] : MulAction (Matrix.SpecialLinearGroup (Fin 2) R) UpperHalfPlane

def UpperHalfPlane.coe' : Matrix.SpecialLinearGroup (Fin 2) ℤ → { x // x ∈ Matrix.GLPos (Fin 2) ℝ }

instance UpperHalfPlane.instCoeSpecialLinearGroupFinOfNatNatInstOfNatNatInstDecidableEqFinFintypeIntInstCommRingIntSubtypeGeneralLinearGroupRealToCommRingToStrictOrderedCommRingLinearOrderedCommRingMemSubgroupInstGroupUnitsMatrixToMonoidToMonoidWithZeroSemiringToSemiringToCommSemiringInstMembershipInstSetLikeSubgroupGLPos : Coe (Matrix.SpecialLinearGroup (Fin 2) ℤ) { x // x ∈ Matrix.GLPos (Fin 2) ℝ }

@[simp]

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

@[simp]

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

instance UpperHalfPlane.SLOnGLPos : SMul (Matrix.SpecialLinearGroup (Fin 2) ℤ) { x // x ∈ Matrix.GLPos (Fin 2) ℝ }

theorem UpperHalfPlane.SLOnGLPos_smul_apply (s : Matrix.SpecialLinearGroup (Fin 2) ℤ) (g : { x // x ∈ Matrix.GLPos (Fin 2) ℝ }) (z : UpperHalfPlane) : (s • g) • z = (↑s * g) • z

instance UpperHalfPlane.SL_to_GL_tower : IsScalarTower (Matrix.SpecialLinearGroup (Fin 2) ℤ) { x // x ∈ Matrix.GLPos (Fin 2) ℝ } UpperHalfPlane

instance UpperHalfPlane.subgroupGLPos (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : SMul { x // x ∈ Γ } { x // x ∈ Matrix.GLPos (Fin 2) ℝ }

theorem UpperHalfPlane.subgroup_on_glpos_smul_apply (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (s : { x // x ∈ Γ }) (g : { x // x ∈ Matrix.GLPos (Fin 2) ℝ }) (z : UpperHalfPlane) : (s • g) • z = (↑↑s * g) • z

instance UpperHalfPlane.subgroup_on_glpos (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : IsScalarTower { x // x ∈ Γ } { x // x ∈ Matrix.GLPos (Fin 2) ℝ } UpperHalfPlane

instance UpperHalfPlane.subgroupSL (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : SMul { x // x ∈ Γ } (Matrix.SpecialLinearGroup (Fin 2) ℤ)

theorem UpperHalfPlane.subgroup_on_SL_apply (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (s : { x // x ∈ Γ }) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane) : (s • g) • z = (↑s * g) • z

instance UpperHalfPlane.subgroup_to_SL_tower (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : IsScalarTower { x // x ∈ Γ } (Matrix.SpecialLinearGroup (Fin 2) ℤ) UpperHalfPlane

theorem UpperHalfPlane.specialLinearGroup_apply {R : Type u_1} [CommRing R] [Algebra R ℝ] (g : Matrix.SpecialLinearGroup (Fin 2) R) (z : UpperHalfPlane) : g • z = UpperHalfPlane.mk ((↑(↑(algebraMap R ℝ) (↑↑g 0 0)) * ↑z + ↑(↑(algebraMap R ℝ) (↑↑g 0 1))) / (↑(↑(algebraMap R ℝ) (↑↑g 1 0)) * ↑z + ↑(↑(algebraMap R ℝ) (↑↑g 1 1)))) (_ : 0 < (↑(g • z)).im)

@[simp]

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

@[simp]

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

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

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

instance UpperHalfPlane.instFactEvenNatInstAddNatCardFinOfNatInstOfNatNatFintype : Fact (Even (Fintype.card (Fin 2)))

@[simp]

theorem UpperHalfPlane.neg_smul (g : { x // x ∈ Matrix.GLPos (Fin 2) ℝ }) (z : UpperHalfPlane) : -g • z = g • z

@[simp]

theorem UpperHalfPlane.sl_moeb (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane) : A • z = ↑A • z

theorem UpperHalfPlane.subgroup_moeb (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (A : { x // x ∈ Γ }) (z : UpperHalfPlane) : A • z = ↑↑A • z

@[simp]

theorem UpperHalfPlane.subgroup_to_sl_moeb (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (A : { x // x ∈ Γ }) (z : UpperHalfPlane) : A • z = ↑A • z

@[simp]

theorem UpperHalfPlane.SL_neg_smul (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane) : -g • z = g • z

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

theorem UpperHalfPlane.SpecialLinearGroup.im_smul_eq_div_normSq (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane) : UpperHalfPlane.im (g • z) = UpperHalfPlane.im z / ↑Complex.normSq (UpperHalfPlane.denom (↑g) z)

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

instance UpperHalfPlane.posRealAction : MulAction { x // 0 < x } UpperHalfPlane

@[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) : UpperHalfPlane.im (x • z) = ↑x * UpperHalfPlane.im z

@[simp]

theorem UpperHalfPlane.pos_real_re (x : { x // 0 < x }) (z : UpperHalfPlane) : UpperHalfPlane.re (x • z) = ↑x * UpperHalfPlane.re z

instance UpperHalfPlane.instAddActionRealUpperHalfPlaneInstAddMonoidReal : AddAction ℝ UpperHalfPlane

@[simp]

theorem UpperHalfPlane.coe_vadd (x : ℝ) (z : UpperHalfPlane) : ↑(x +ᵥ z) = ↑x + ↑z

@[simp]

theorem UpperHalfPlane.vadd_re (x : ℝ) (z : UpperHalfPlane) : UpperHalfPlane.re (x +ᵥ z) = x + UpperHalfPlane.re z

@[simp]

theorem UpperHalfPlane.vadd_im (x : ℝ) (z : UpperHalfPlane) : UpperHalfPlane.im (x +ᵥ z) = UpperHalfPlane.im z

theorem UpperHalfPlane.modular_S_smul (z : UpperHalfPlane) : ModularGroup.S • z = UpperHalfPlane.mk (-↑z)⁻¹ (_ : 0 < (-↑z)⁻¹.im)

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 v, (fun x x_1 => x • x_1) g = (fun z => v +ᵥ z) ∘ fun z => u • z

theorem UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_ne_zero (g : Matrix.SpecialLinearGroup (Fin 2) ℝ) (hc : ↑↑g 1 0 ≠ 0) : ∃ u v w, (fun x x_1 => x • x_1) g = (fun x x_1 => x +ᵥ x_1) w ∘ (fun x x_1 => x • x_1) ModularGroup.S ∘ (fun x x_1 => x +ᵥ x_1) v ∘ (fun x x_1 => x • x_1) u