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
- UpperHalfPlane.termℍ = Lean.ParserDescr.node `UpperHalfPlane.termℍ 1024 (Lean.ParserDescr.symbol "ℍ")
Instances For
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))
Instances For
Equations
- UpperHalfPlane.instCoeFun = { coe := fun (A : ↥(Matrix.GLPos (Fin 2) ℝ)) => ↑↑A }
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.
Instances For
Equations
- UpperHalfPlane.instCoeOutComplex = { coe := UpperHalfPlane.coe }
Equations
- UpperHalfPlane.instInhabited = { default := ⟨Complex.I, UpperHalfPlane.instInhabited.proof_1⟩ }
Extensionality lemma in terms of UpperHalfPlane.re
and UpperHalfPlane.im
.
Constructor for UpperHalfPlane
. It is useful if ⟨z, h⟩
makes Lean use a wrong
typeclass instance.
Equations
- UpperHalfPlane.mk z h = ⟨z, h⟩
Instances For
Define I := √-1 as an element on the upper half plane.
Equations
Instances For
Extension for the positivity
tactic: UpperHalfPlane.im
.
Instances For
Extension for the positivity
tactic: UpperHalfPlane.coe
.
Instances For
Numerator of the formula for a fractional linear transformation
Equations
- UpperHalfPlane.num g z = ↑(↑↑g 0 0) * ↑z + ↑(↑↑g 0 1)
Instances For
Denominator of the formula for a fractional linear transformation
Equations
- UpperHalfPlane.denom g z = ↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)
Instances For
Fractional linear transformation, also known as the Moebius transformation
Equations
- UpperHalfPlane.smulAux' g z = UpperHalfPlane.num g z / UpperHalfPlane.denom g z
Instances For
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.
Equations
- UpperHalfPlane.SLAction = MulAction.compHom UpperHalfPlane (Matrix.SpecialLinearGroup.toGLPos.comp (Matrix.SpecialLinearGroup.map (algebraMap R ℝ)))
Canonical embedding of SL(2, ℤ)
into GL(2, ℝ)⁺
.
Equations
- ↑g = Matrix.SpecialLinearGroup.toGLPos ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g)
Instances For
Alias of ModularGroup.coe
.
Canonical embedding of SL(2, ℤ)
into GL(2, ℝ)⁺
.
Equations
Instances For
Alias of ModularGroup.coe_apply_complex
.
Alias of ModularGroup.det_coe
.
Equations
- ModularGroup.SLOnGLPos = { smul := fun (s : Matrix.SpecialLinearGroup (Fin 2) ℤ) (g : ↥(Matrix.GLPos (Fin 2) ℝ)) => ↑s * g }