Documentation

TauCeti.Geometry.Manifold.Riemannian.Hyperbolic.Volume

Volumes of hyperbolic metrics #

This file connects the bundled TauCeti.HyperbolicMetric with the Riemannian volume API. A hyperbolic metric is data, so its volume is defined as the total volume of the carried Riemannian metric. Metric-independence is the volume consequence of Mostow rigidity, which is taken here as the hypothesis TauCeti.IsMostowRigid rather than proved.

The volume construction follows J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Chapter 2. Metric-independence uses Mostow rigidity in J. Ratcliffe, Foundations of Hyperbolic Manifolds, 3rd ed., Theorem 11.8.5.

Main definitions #

source
noncomputable def TauCeti.hypVolumeOfMetric {E : Type uE} {H : Type uH} {M : Type uM} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [T3Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [PreconnectedSpace M] [CompactSpace M] [MeasurableSpace M] [BorelSpace M] (g : HyperbolicMetric) :
ℝ

The total Riemannian volume carried by a bundled complete constant-curvature -1 metric.

Instances For
    source
    theorem TauCeti.hypVolumeOfMetric_def {E : Type uE} {H : Type uH} {M : Type uM} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [T3Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [PreconnectedSpace M] [CompactSpace M] [MeasurableSpace M] [BorelSpace M] (g : HyperbolicMetric) :
    hypVolumeOfMetric g = riemannianTotalVolume I M

    hypVolumeOfMetric is the total volume for the metric carried by g.

    source
    theorem TauCeti.hypVolumeOfMetric_nonneg {E : Type uE} {H : Type uH} {M : Type uM} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [T3Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [PreconnectedSpace M] [CompactSpace M] [MeasurableSpace M] [BorelSpace M] (g : HyperbolicMetric) :
    0 ≤ hypVolumeOfMetric g

    Hyperbolic volume is nonnegative, as a total Riemannian volume.

    source
    theorem TauCeti.hypVolumeOfMetric_eq_of_isometry {E : Type uE} {H : Type uH} {M : Type uM} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [T3Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [PreconnectedSpace M] [CompactSpace M] [MeasurableSpace M] [BorelSpace M] (g g' : HyperbolicMetric) (Φ : g.Isometry g') :
    hypVolumeOfMetric g = hypVolumeOfMetric g'

    The volume is preserved by any bundled hyperbolic-metric isometry.

    source
    theorem TauCeti.hypVolumeOfMetric_eq_of_mostow {E : Type uE} {H : Type uH} {M : Type uM} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [T3Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [PreconnectedSpace M] [CompactSpace M] [MeasurableSpace M] [BorelSpace M] [BoundarylessManifold I M] (hConn : ConnectedSpace M) (hdim : 3 ≤ Module.finrank ℝ E) (h : IsMostowRigid) (g g' : HyperbolicMetric) :
    hypVolumeOfMetric g = hypVolumeOfMetric g'

    Mostow rigidity identifies the total volumes of any two bundled hyperbolic metrics.

    Metric-independent hyperbolic volume #

    source
    noncomputable def TauCeti.hypVolume {E : Type uE} {H : Type uH} {M : Type uM} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [T3Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [PreconnectedSpace M] [CompactSpace M] [MeasurableSpace M] [BorelSpace M] (h : IsHyperbolic) :
    ℝ

    The hyperbolic volume of a compact manifold carrying a hyperbolic metric.

    The definition chooses one bundled hyperbolic metric. On a closed connected manifold of dimension at least three, TauCeti.hypVolume_eq_hypVolumeOfMetric shows that, under the Mostow-rigidity hypothesis TauCeti.IsMostowRigid, the result equals the volume of every hyperbolic metric. Mostow rigidity itself is not proved in this file.

    Instances For
      source
      theorem TauCeti.hypVolume_def {E : Type uE} {H : Type uH} {M : Type uM} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [T3Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [PreconnectedSpace M] [CompactSpace M] [MeasurableSpace M] [BorelSpace M] (h : IsHyperbolic) :
      hypVolume h = hypVolumeOfMetric (Classical.choice ⋯)

      Hyperbolic volume is the volume of the chosen bundled hyperbolic metric.

      source
      theorem TauCeti.hypVolume_nonneg {E : Type uE} {H : Type uH} {M : Type uM} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [T3Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [PreconnectedSpace M] [CompactSpace M] [MeasurableSpace M] [BorelSpace M] (h : IsHyperbolic) :
      0 ≤ hypVolume h

      The hyperbolic volume of a compact hyperbolic manifold is nonnegative.

      source
      theorem TauCeti.hypVolume_eq_hypVolumeOfMetric {E : Type uE} {H : Type uH} {M : Type uM} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [T3Space M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [PreconnectedSpace M] [CompactSpace M] [MeasurableSpace M] [BorelSpace M] [BoundarylessManifold I M] (hConn : ConnectedSpace M) (hdim : 3 ≤ Module.finrank ℝ E) (hMostow : IsMostowRigid) (h : IsHyperbolic) (g : HyperbolicMetric) :
      hypVolume h = hypVolumeOfMetric g

      On a closed connected manifold of dimension at least three, Mostow rigidity makes hyperbolic volume independent of the metric chosen in its definition.