Documentation

TauCeti.Analysis.Complex.UpperHalfPlane.SmulDeriv

The derivative of the PSL(2, ℝ)-action on the upper half-plane #

A Möbius transformation of the upper half-plane is holomorphic, with derivative det g / denom g z ^ 2 at z, where denom g z = c * z + d is Mathlib's automorphy factor (UpperHalfPlane.hasStrictDerivAt_smul). A representative in SL(2, ℝ) has determinant 1, so the derivative is (denom g z ^ 2)⁻¹; squaring the automorphy factor cancels the sign ambiguity of the representative, so this depends only on the class in PSL(2, ℝ). That well-defined derivative is Matrix.ProjectiveSpecialLinearGroup.smulDeriv, the quantity the effective projective action attaches to a point.

By the chain rule the derivative is a cocycle for the action (Matrix.ProjectiveSpecialLinearGroup.smulDeriv_mul); restricted to the stabilizer of a point it therefore becomes a character, which is what governs the stabilizers of a discrete subgroup.

Main declarations #

References #

source
theorem Matrix.SpecialLinearGroup.denom_mapGL_neg (g : SpecialLinearGroup (Fin 2) ℝ) (z : ℂ) :
UpperHalfPlane.denom ((mapGL ℝ) (-g)) z = -UpperHalfPlane.denom ((mapGL ℝ) g) z

The automorphy factor changes sign along with its matrix, so squaring it gives a function of the class in PSL(2, ℝ).

source
theorem Matrix.SpecialLinearGroup.normSq_denom_eq_one_of_smul_eq_self {g : SpecialLinearGroup (Fin 2) ℝ} {z : UpperHalfPlane} (hz : g • z = z) :
Complex.normSq (UpperHalfPlane.denom ((mapGL ℝ) g) ↑z) = 1

The automorphy factor at a fixed point is unimodular. The imaginary part of g • z is im z divided by the squared modulus of the automorphy factor, so fixing z forces that modulus to be 1.

source
noncomputable def Matrix.ProjectiveSpecialLinearGroup.smulDeriv (q : ProjectiveSpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) :
ℂ

The derivative at z : ℍ of the Möbius transformation of the upper half-plane attached to q : PSL(2, ℝ); see Matrix.ProjectiveSpecialLinearGroup.deriv_coe_smul. On a representative g : SL(2, ℝ) it is (denom g z ^ 2)⁻¹, independent of the representative by Matrix.SpecialLinearGroup.denom_mapGL_neg.

Equations
Instances For
    source
    @[simp]
    theorem Matrix.SpecialLinearGroup.smulDeriv_coe (g : SpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) :
    ProjectiveSpecialLinearGroup.smulDeriv (↑g) z = (UpperHalfPlane.denom ((mapGL ℝ) g) ↑z ^ 2)⁻¹

    The derivative of the transformation of a representative, in terms of its automorphy factor.

    source
    @[simp]
    theorem Matrix.ProjectiveSpecialLinearGroup.smulDeriv_ne_zero (q : ProjectiveSpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) :
    q.smulDeriv z ≠ 0

    A Möbius transformation of ℍ has nowhere vanishing derivative.

    source
    theorem Matrix.ProjectiveSpecialLinearGroup.norm_smulDeriv_of_smul_eq_self {q : ProjectiveSpecialLinearGroup (Fin 2) ℝ} {z : UpperHalfPlane} (hz : q • z = z) :
    ‖q.smulDeriv z‖ = 1

    A Möbius transformation of ℍ fixing a point is a rotation there: its derivative at a fixed point has modulus one.

    source
    @[simp]
    theorem Matrix.ProjectiveSpecialLinearGroup.smulDeriv_one (z : UpperHalfPlane) :
    smulDeriv 1 z = 1

    The identity transformation has derivative 1.

    source
    @[simp]
    theorem Matrix.ProjectiveSpecialLinearGroup.smulDeriv_mul (q₁ q₂ : ProjectiveSpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) :
    (q₁ * q₂).smulDeriv z = q₁.smulDeriv (q₂ • z) * q₂.smulDeriv z

    The chain rule for the PSL(2, ℝ)-action: the derivative is a cocycle.

    source
    @[simp]
    theorem Matrix.ProjectiveSpecialLinearGroup.smulDeriv_inv (q : ProjectiveSpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) :
    q⁻¹.smulDeriv (q • z) = (q.smulDeriv z)⁻¹

    The inverse transformation has the inverse derivative at the image point.

    source
    theorem Matrix.ProjectiveSpecialLinearGroup.hasStrictDerivAt_coe_smul (q : ProjectiveSpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) :
    HasStrictDerivAt (fun (w : ℂ) => ↑(q • ↑UpperHalfPlane.ofComplex w)) (q.smulDeriv z) ↑z

    smulDeriv is the derivative of the Möbius transformation. The transformation is read on ℂ through Mathlib's partial inverse UpperHalfPlane.ofComplex of the inclusion ℍ → ℂ, which is the identity on the upper half-plane and so does not affect the derivative there.

    source
    @[simp]
    theorem Matrix.ProjectiveSpecialLinearGroup.deriv_coe_smul (q : ProjectiveSpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) :
    deriv (fun (w : ℂ) => ↑(q • ↑UpperHalfPlane.ofComplex w)) ↑z = q.smulDeriv z

    The derivative of a Möbius transformation of ℍ, in the form deriv.

    source
    theorem Matrix.ProjectiveSpecialLinearGroup.smulDeriv_dilation (s : ℝ) (z : UpperHalfPlane) :
    smulDeriv (↑(SpecialLinearGroup.dilation s)) z = ↑(Real.exp s)

    The derivative of the dilation z ↦ exp s * z is exp s.