Documentation

TauCeti.Geometry.Manifold.Riemannian.Hyperbolic.Mostow

Mostow rigidity for hyperbolic metrics #

This file records the metric-level statement of Mostow rigidity for closed hyperbolic manifolds. The resulting relation supports comparing the total volumes carried by different hyperbolic metrics.

The formulation follows Ratcliffe, Foundations of Hyperbolic Manifolds, 3rd ed., Theorem 11.8.5.

source
def TauCeti.IsMostowRigid {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] :
Prop

The metric-level conclusion of Mostow rigidity for one fixed manifold and dimension.

The predicate asserts that every pair of bundled hyperbolic metrics on a closed, connected, boundaryless manifold of real dimension at least three is related by a bundled isometry.

Instances For
    source
    theorem TauCeti.isMostowRigid_iff {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] :
    IsMostowRigid ↔ ∀ [BoundarylessManifold I M] [CompactSpace M] [inst : ConnectedSpace M], 3 ≤ Module.finrank ℝ E → ∀ (g g' : HyperbolicMetric), Nonempty (g.Isometry g')

    A fixed-manifold Mostow-rigidity predicate is equivalent to its characteristic statement.

    source
    theorem TauCeti.isMostowRigid_of {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] (h : ∀ [BoundarylessManifold I M] [CompactSpace M] [inst : ConnectedSpace M], 3 ≤ Module.finrank ℝ E → ∀ (g g' : HyperbolicMetric), Nonempty (g.Isometry g')) :
    IsMostowRigid

    Introduce fixed-manifold Mostow rigidity from its characteristic statement.

    source
    theorem TauCeti.IsMostowRigid.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] [BoundarylessManifold I M] [CompactSpace M] [ConnectedSpace M] (h : IsMostowRigid) {hdim : 3 ≤ Module.finrank ℝ E} (g g' : HyperbolicMetric) :
    Nonempty (g.Isometry g')

    Extract the isometry conclusion from a fixed-manifold Mostow-rigidity hypothesis.

    source
    def TauCeti.MostowRigidity :
    Prop

    The Mostow rigidity statement, universally over closed connected manifolds.

    Instances For
      source
      theorem TauCeti.MostowRigidity.isMostowRigid {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] (h : MostowRigidity) :
      IsMostowRigid

      Specialize the universal Mostow-rigidity statement to one manifold.