Documentation

Mathlib.Analysis.Complex.UpperHalfPlane.Basic

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

      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 2Fin 2
        Equations

        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

          Canonical embedding of the upper half-plane into .

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

            Imaginary part

            Equations
            • z.im = (↑z).im
            Instances For

              Real part

              Equations
              • z.re = (↑z).re
              Instances For
                theorem UpperHalfPlane.ext' {a b : UpperHalfPlane} (hre : a.re = b.re) (him : a.im = b.im) :
                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
                Instances For
                  @[simp]
                  theorem UpperHalfPlane.coe_im (z : UpperHalfPlane) :
                  (↑z).im = z.im
                  @[simp]
                  theorem UpperHalfPlane.coe_re (z : UpperHalfPlane) :
                  (↑z).re = z.re
                  @[simp]
                  theorem UpperHalfPlane.mk_re (z : ) (h : 0 < z.im) :
                  (UpperHalfPlane.mk z h).re = z.re
                  @[simp]
                  theorem UpperHalfPlane.mk_im (z : ) (h : 0 < z.im) :
                  (UpperHalfPlane.mk z h).im = z.im
                  @[simp]
                  theorem UpperHalfPlane.coe_mk (z : ) (h : 0 < z.im) :
                  (UpperHalfPlane.mk z h) = z
                  @[simp]
                  theorem UpperHalfPlane.coe_mk_subtype {z : } (hz : 0 < z.im) :
                  z, hz = z
                  @[simp]
                  theorem UpperHalfPlane.mk_coe (z : UpperHalfPlane) (h : 0 < (↑z).im := ) :
                  UpperHalfPlane.mk (↑z) h = z
                  theorem UpperHalfPlane.re_add_im (z : UpperHalfPlane) :
                  z.re + z.im * Complex.I = z

                  Define I := √-1 as an element on the upper half plane.

                  Equations
                  Instances For
                    theorem UpperHalfPlane.ne_nat (z : UpperHalfPlane) (n : ) :
                    z n
                    theorem UpperHalfPlane.ne_int (z : UpperHalfPlane) (n : ) :
                    z n

                    Numerator of the formula for a fractional linear transformation

                    Equations
                    Instances For

                      Denominator of the formula for a fractional linear transformation

                      Equations
                      Instances For
                        theorem UpperHalfPlane.linear_ne_zero (cd : Fin 2) (z : UpperHalfPlane) (h : cd 0) :
                        (cd 0) * z + (cd 1) 0

                        Fractional linear transformation, also known as the Moebius transformation

                        Equations
                        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
                            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))))
                            @[simp]
                            @[simp]
                            theorem UpperHalfPlane.neg_smul (g : (Matrix.GLPos (Fin 2) )) (z : UpperHalfPlane) :
                            -g z = g z
                            @[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) :
                            (x z).im = x * z.im
                            @[simp]
                            theorem UpperHalfPlane.pos_real_re (x : { x : // 0 < x }) (z : UpperHalfPlane) :
                            (x z).re = x * z.re
                            @[simp]
                            theorem UpperHalfPlane.coe_vadd (x : ) (z : UpperHalfPlane) :
                            (x +ᵥ z) = x + z
                            @[simp]
                            theorem UpperHalfPlane.vadd_re (x : ) (z : UpperHalfPlane) :
                            (x +ᵥ z).re = x + z.re
                            @[simp]
                            theorem UpperHalfPlane.vadd_im (x : ) (z : UpperHalfPlane) :
                            (x +ᵥ z).im = z.im
                            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

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

                            Equations
                            Instances For
                              @[deprecated ModularGroup.coe]

                              Alias of ModularGroup.coe.


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

                              Equations
                              Instances For
                                @[simp]
                                theorem ModularGroup.coe_apply_complex {g : Matrix.SpecialLinearGroup (Fin 2) } {i j : Fin 2} :
                                (g i j) = (g i j)
                                @[deprecated ModularGroup.coe_apply_complex]
                                theorem ModularGroup.coe'_apply_complex {g : Matrix.SpecialLinearGroup (Fin 2) } {i j : Fin 2} :
                                (g i j) = (g i j)

                                Alias of ModularGroup.coe_apply_complex.

                                @[simp]
                                theorem ModularGroup.det_coe {g : Matrix.SpecialLinearGroup (Fin 2) } :
                                (↑g).det = 1
                                @[deprecated ModularGroup.det_coe]
                                theorem ModularGroup.det_coe' {g : Matrix.SpecialLinearGroup (Fin 2) } :
                                (↑g).det = 1

                                Alias of ModularGroup.det_coe.

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