Documentation

TauCeti.Analysis.Complex.UpperHalfPlane.PoincareMetric

The Poincaré Riemannian metric #

The canonical tensor on the upper half-plane is the Euclidean inner product divided by the square of the imaginary coordinate. We construct it as a smooth real Riemannian metric, the Euclidean metric rescaled by im⁻² through Bundle.ContMDiffRiemannianMetric.rescale, and install it as the Riemannian structure of the tangent bundle of ℍ.

Its Riemannian volume is Mathlib's invariant measure volume : Measure ℍ, whose density is y⁻² dx dy. In the inclusion chart the Gram matrix of the Poincaré tensor is y⁻² times the Euclidean Gram matrix, so the Riemannian volume density is y⁻² against Lebesgue measure on ℂ. Thus the hyperbolic areas computed with volume, such as covolumes of Fuchsian groups and the Gauss–Bonnet formula, are areas for the Poincaré metric.

The convention is the upper half-plane model in J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 3.

Main results #

source
instance TauCeti.UpperHalfPlane.instIsManifoldReal :
IsManifold (modelWithCornersSelf ℝ ℂ) ⊤ UpperHalfPlane

The singleton complex chart also gives the upper half-plane its smooth real manifold structure.

source
noncomputable def TauCeti.UpperHalfPlane.poincareRiemannianMetric :
Bundle.ContMDiffRiemannianMetric (modelWithCornersSelf ℝ ℂ) ↑⊤ ℂ fun (z : UpperHalfPlane) => TangentSpace (modelWithCornersSelf ℝ ℂ) z

The smooth Poincaré metric: the Euclidean tensor rescaled by im⁻².

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem UpperHalfPlane.poincareRiemannianMetric_inner (z : UpperHalfPlane) (v w : TangentSpace (modelWithCornersSelf ℝ ℂ) z) :
    ((TauCeti.UpperHalfPlane.poincareRiemannianMetric.inner z) v) w = inner ℝ ((tangentSpaceCastModel (modelWithCornersSelf ℝ ℂ) z) v) ((tangentSpaceCastModel (modelWithCornersSelf ℝ ℂ) z) w) / z.im ^ 2

    The Poincaré tensor in the tangent coordinates of the inclusion chart.

    source
    @[instance_reducible]
    noncomputable instance TauCeti.UpperHalfPlane.instRiemannianBundle :
    Bundle.RiemannianBundle fun (z : UpperHalfPlane) => TangentSpace (modelWithCornersSelf ℝ ℂ) z

    The tangent bundle of the upper half-plane carries the Poincaré tensor.

    Equations
    source
    instance TauCeti.UpperHalfPlane.instIsContMDiffRiemannianBundle :
    IsContMDiffRiemannianBundle (modelWithCornersSelf ℝ ℂ) ↑⊤ ℂ fun (z : UpperHalfPlane) => TangentSpace (modelWithCornersSelf ℝ ℂ) z

    The Poincaré tensor is smooth as a real Riemannian bundle.

    source
    instance TauCeti.UpperHalfPlane.instIsContinuousRiemannianBundle :
    IsContinuousRiemannianBundle ℂ fun (z : UpperHalfPlane) => TangentSpace (modelWithCornersSelf ℝ ℂ) z

    Continuity of the Poincaré tensor makes the Riemannian volume construction applicable.

    source
    theorem UpperHalfPlane.riemannianVolume_eq_volume :
    TauCeti.riemannianVolume (modelWithCornersSelf ℝ ℂ) UpperHalfPlane = MeasureTheory.volume

    The Riemannian volume of the Poincaré metric is Mathlib's invariant measure on the upper half-plane, with density y⁻² dx dy against Lebesgue measure.