Hyperbolic space in the upper half-space model

For a real inner product space E, the upper half-space model UpperHalfSpace E of real hyperbolic space is the open upper half-space {(x, t) | 0 < t} of the Euclidean product E × ℝ (that is, WithLp 2 (E × ℝ)), with the Riemannian metric (‖dx‖² + dt²) / t²: the Euclidean inner product of two tangent vectors at (x, t) divided by t². For 1 ≤ n, taking E = EuclideanSpace ℝ (Fin (n - 1)) gives hyperbolic n-space ℍⁿ; in particular E = EuclideanSpace ℝ (Fin 2) gives the model space ℍ³ of hyperbolic three-manifolds.

The metric is the Euclidean metric of E × ℝ, restricted to the upper half-space and rescaled by the analytic positive function t⁻², so it is an analytic Riemannian metric.

For 0 < c, a linear isometry A of E and b ∈ E, the similarity (x, t) ↦ (c • A x + b, c • t) preserves the upper half-space and scales tangent vectors and the height t by the same factor c, so it is a Riemannian isometry. These similarities act transitively, so the upper half-space model is a homogeneous Riemannian manifold.

Analyticity of the metric and homogeneity are established here. The module UpperHalfSpace.Curvature proves constant curvature -1, and UpperHalfSpace.Metric combines this with completeness to construct a TauCeti.HyperbolicMetric.

Main definitions

• TauCeti.upperHalfSpaceOpens E: the open upper half-space in E × ℝ.
• TauCeti.UpperHalfSpace E: the upper half-space as a manifold, with its hyperbolic metric as RiemannianBundle instance.
• TauCeti.UpperHalfSpace.height: the last coordinate t of a point.
• TauCeti.UpperHalfSpace.riemannianMetric: the analytic hyperbolic metric.
• TauCeti.UpperHalfSpace.similarity: the isometry (x, t) ↦ (c • A x + b, c • t).

Main results

• TauCeti.UpperHalfSpace.inner_def: the inner product of tangent vectors at x is their Euclidean inner product divided by height x ^ 2 (TauCeti.UpperHalfSpace.riemannianMetric_inner is the same formula for the bundled metric riemannianMetric); TauCeti.UpperHalfSpace.norm_def and TauCeti.UpperHalfSpace.enorm_def are the corresponding norm forms.
• TauCeti.UpperHalfSpace.contMDiff_coe_comp_iff: a map into the upper half-space is C^n iff its composite with the inclusion into E × ℝ is.
• TauCeti.UpperHalfSpace.isPretransitive_isom: the isometry group of the upper half-space model acts transitively on it.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 3 (the upper half-space model of hyperbolic space and its isometries).
• W. P. Thurston, Three-Dimensional Geometry and Topology, Vol. 1, Princeton (1997), §2.4 and §3.8 (the upper half-space model, and hyperbolic space among the eight model geometries).

def TauCeti.upperHalfSpaceOpens (E : Type u_1) [NormedAddCommGroup E] : TopologicalSpace.Opens (WithLp 2 (E × ℝ))

The open upper half-space {(x, t) | 0 < t} in the Euclidean product E × ℝ.

@[simp]

theorem TauCeti.mem_upperHalfSpaceOpens {E : Type u_1} [NormedAddCommGroup E] {p : WithLp 2 (E × ℝ)} : p ∈ upperHalfSpaceOpens E ↔ 0 < p.snd

def TauCeti.UpperHalfSpace (E : Type u_1) [NormedAddCommGroup E] : Type u_1

The upper half-space model of real hyperbolic space: the open upper half-space {(x, t) | 0 < t} of E × ℝ, with the hyperbolic metric (‖dx‖² + dt²) / t² as its RiemannianBundle instance. For 1 ≤ n and E = EuclideanSpace ℝ (Fin (n - 1)) this is hyperbolic n-space.

@[instance_reducible]

noncomputable instance TauCeti.UpperHalfSpace.instTopologicalSpace (E : Type u_1) [NormedAddCommGroup E] : TopologicalSpace (UpperHalfSpace E)

@[instance_reducible]

noncomputable instance TauCeti.UpperHalfSpace.instChartedSpaceWithLpOfNatENNRealProdReal (E : Type u_1) [NormedAddCommGroup E] : ChartedSpace (WithLp 2 (E × ℝ)) (UpperHalfSpace E)

instance TauCeti.UpperHalfSpace.instT3Space (E : Type u_1) [NormedAddCommGroup E] : T3Space (UpperHalfSpace E)

noncomputable def TauCeti.UpperHalfSpace.coe {E : Type u_1} [NormedAddCommGroup E] (x : UpperHalfSpace E) : WithLp 2 (E × ℝ)

The point of E × ℝ represented by a point of the upper half-space.

@[instance_reducible]

noncomputable instance TauCeti.UpperHalfSpace.instCoeOutWithLpOfNatENNRealProdReal {E : Type u_1} [NormedAddCommGroup E] : CoeOut (UpperHalfSpace E) (WithLp 2 (E × ℝ))

noncomputable def TauCeti.UpperHalfSpace.mk {E : Type u_1} [NormedAddCommGroup E] (p : WithLp 2 (E × ℝ)) (hp : 0 < p.snd) : UpperHalfSpace E

The point of the upper half-space represented by a point of E × ℝ with positive last coordinate.

@[simp]

theorem TauCeti.UpperHalfSpace.coe_mk {E : Type u_1} [NormedAddCommGroup E] (p : WithLp 2 (E × ℝ)) (hp : 0 < p.snd) : ↑(mk p hp) = p

theorem TauCeti.UpperHalfSpace.coe_injective {E : Type u_1} [NormedAddCommGroup E] : Function.Injective coe

A point of the upper half-space is determined by the point of E × ℝ it represents.

theorem TauCeti.UpperHalfSpace.ext {E : Type u_1} [NormedAddCommGroup E] {x y : UpperHalfSpace E} (h : ↑x = ↑y) : x = y

theorem TauCeti.UpperHalfSpace.ext_iff {E : Type u_1} [NormedAddCommGroup E] {x y : UpperHalfSpace E} : x = y ↔ ↑x = ↑y

noncomputable def TauCeti.UpperHalfSpace.height {E : Type u_1} [NormedAddCommGroup E] (x : UpperHalfSpace E) : ℝ

The height of a point (x, t) of the upper half-space: its last coordinate t.

@[simp]

theorem TauCeti.UpperHalfSpace.snd_coe {E : Type u_1} [NormedAddCommGroup E] (x : UpperHalfSpace E) : (↑x).snd = x.height

theorem TauCeti.UpperHalfSpace.height_pos {E : Type u_1} [NormedAddCommGroup E] (x : UpperHalfSpace E) : 0 < x.height

Points of the upper half-space have positive height.

theorem TauCeti.UpperHalfSpace.coe_ne_toLp {E : Type u_1} [NormedAddCommGroup E] (x : UpperHalfSpace E) (a : E) : ↑x ≠ WithLp.toLp 2 (a, 0)

A point of the upper half-space is not a point (a, 0) of its boundary hyperplane.

@[simp]

theorem TauCeti.UpperHalfSpace.mk_coe {E : Type u_1} [NormedAddCommGroup E] (x : UpperHalfSpace E) : mk ↑x ⋯ = x

@[simp]

theorem TauCeti.UpperHalfSpace.height_mk {E : Type u_1} [NormedAddCommGroup E] (p : WithLp 2 (E × ℝ)) (hp : 0 < p.snd) : (mk p hp).height = p.snd

theorem TauCeti.UpperHalfSpace.ext_fst_height {E : Type u_1} [NormedAddCommGroup E] {x y : UpperHalfSpace E} (hfst : (↑x).fst = (↑y).fst) (hheight : x.height = y.height) : x = y

Two points of the upper half-space with the same horizontal coordinate and the same height are equal.

instance TauCeti.UpperHalfSpace.instContractibleSpace (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] : ContractibleSpace (UpperHalfSpace E)

The upper half-space is contractible, by straight-line contraction inside the convex positive-height half-space. No finite-dimensional or inner-product hypothesis is needed.

instance TauCeti.UpperHalfSpace.instIsManifoldRealWithLpOfNatENNRealProdModelWithCornersSelfTopWithTopENat (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] : IsManifold (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) ⊤ (UpperHalfSpace E)

theorem TauCeti.UpperHalfSpace.contMDiff_coe {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : ContMDiff (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) ⊤ coe

The inclusion of the upper half-space into E × ℝ is analytic.

theorem TauCeti.UpperHalfSpace.contMDiff_inv_height_sq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : ContMDiff (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) (modelWithCornersSelf ℝ ℝ) ⊤ fun (x : UpperHalfSpace E) => (x.height ^ 2)⁻¹

The conformal factor t⁻² of the hyperbolic metric is analytic on the upper half-space.

@[simp]

theorem TauCeti.UpperHalfSpace.contMDiff_coe_comp_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {EM : Type u_2} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_3} [TopologicalSpace HM] {I : ModelWithCorners ℝ EM HM} {M : Type u_4} [TopologicalSpace M] [ChartedSpace HM M] {n : WithTop ℕ∞} {f : M → UpperHalfSpace E} : ContMDiff I (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) n (coe ∘ f) ↔ ContMDiff I (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) n f

A map into the upper half-space is C^n iff its composite with the inclusion into E × ℝ is.

theorem TauCeti.UpperHalfSpace.tangentSpaceCastModel_mfderiv_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : UpperHalfSpace E → UpperHalfSpace E} {A : WithLp 2 (E × ℝ) → WithLp 2 (E × ℝ)} {L : WithLp 2 (E × ℝ) →L[ℝ] WithLp 2 (E × ℝ)} {x : UpperHalfSpace E} (hA : HasFDerivAt A L ↑x) (hcomp : coe ∘ f = A ∘ coe) (v : TangentSpace (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x) : (tangentSpaceCastModel (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) (f x)) ((mfderiv% f x) v) = L ((tangentSpaceCastModel (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x) v)

If a self-map f of the upper half-space is the restriction of a map A of E × ℝ with derivative L at x, then the differential of f at x is L.

noncomputable def TauCeti.UpperHalfSpace.riemannianMetric {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : Bundle.ContMDiffRiemannianMetric (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) ⊤ (WithLp 2 (E × ℝ)) fun (x : UpperHalfSpace E) => TangentSpace (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x

The analytic hyperbolic metric (‖dx‖² + dt²) / t² on the upper half-space: the Euclidean metric of E × ℝ multiplied by the positive function t⁻².

@[instance_reducible]

noncomputable instance TauCeti.UpperHalfSpace.instRiemannianBundleTangentSpaceRealWithLpOfNatENNRealProdModelWithCornersSelf {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : Bundle.RiemannianBundle fun (x : UpperHalfSpace E) => TangentSpace (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x

The upper half-space carries the hyperbolic metric (‖dx‖² + dt²) / t².

instance TauCeti.UpperHalfSpace.instIsContMDiffRiemannianBundleWithLpOfNatENNRealProdRealModelWithCornersSelfTopWithTopENatTangentSpace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : IsContMDiffRiemannianBundle (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) ⊤ (WithLp 2 (E × ℝ)) fun (x : UpperHalfSpace E) => TangentSpace (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x

The hyperbolic metric is analytic.

instance TauCeti.UpperHalfSpace.instIsContinuousRiemannianBundleWithLpOfNatENNRealProdRealTangentSpaceModelWithCornersSelf {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : IsContinuousRiemannianBundle (WithLp 2 (E × ℝ)) fun (x : UpperHalfSpace E) => TangentSpace (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x

The hyperbolic metric is continuous, as the Riemannian volume construction requires.

@[simp]

theorem TauCeti.UpperHalfSpace.riemannianMetric_inner {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : UpperHalfSpace E) (v w : TangentSpace (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x) : ((riemannianMetric.inner x) v) w = inner ℝ ((tangentSpaceCastModel (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x) v) ((tangentSpaceCastModel (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x) w) / x.height ^ 2

The hyperbolic metric evaluated on two tangent vectors at a point of the upper half-space is their Euclidean inner product divided by the square of the height. This is the characteristic lemma of the bundled metric riemannianMetric; inner_def is its form for the installed RiemannianBundle instance.

theorem TauCeti.UpperHalfSpace.riemannianBundle_g {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : Bundle.RiemannianBundle.g = riemannianMetric.toRiemannianMetric

The metric installed as the RiemannianBundle instance of the upper half-space is the hyperbolic metric riemannianMetric.

@[simp]

theorem TauCeti.UpperHalfSpace.inner_def {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : UpperHalfSpace E) (v w : TangentSpace (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x) : inner ℝ v w = inner ℝ ((tangentSpaceCastModel (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x) v) ((tangentSpaceCastModel (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x) w) / x.height ^ 2

The inner product of two tangent vectors at a point of the upper half-space is their Euclidean inner product divided by the square of the height.

@[simp]

theorem TauCeti.UpperHalfSpace.norm_def {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : UpperHalfSpace E) (v : TangentSpace (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x) : ‖v‖ = ‖(tangentSpaceCastModel (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x) v‖ / x.height

The norm of a tangent vector at a point of the upper half-space is its Euclidean norm divided by the height.

@[simp]

theorem TauCeti.UpperHalfSpace.enorm_def {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : UpperHalfSpace E) (v : TangentSpace (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x) : ‖v‖ₑ = ‖(tangentSpaceCastModel (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x) v‖ₑ / ENNReal.ofReal x.height

The extended norm of a tangent vector at a point of the upper half-space is its Euclidean extended norm divided by the height.

noncomputable def TauCeti.UpperHalfSpace.similarity {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (c : ℝ) (hc : 0 < c) (A : E ≃ₗᵢ[ℝ] E) (b : E) : Isom (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) (UpperHalfSpace E)

The similarity (x, t) ↦ (c • A x + b, c • t), for 0 < c and a linear isometry A of E, as an isometry of the upper half-space model: it scales tangent vectors and the height by the same factor c.

@[simp]

theorem TauCeti.UpperHalfSpace.coe_similarity_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (c : ℝ) (hc : 0 < c) (A : E ≃ₗᵢ[ℝ] E) (b : E) (x : UpperHalfSpace E) : ↑((similarity c hc A b) x) = WithLp.toLp 2 (c • A (↑x).fst + b, c * x.height)

The similarity similarity c hc A b sends (x, t) to (c • A x + b, c • t).

@[simp]

theorem TauCeti.UpperHalfSpace.height_similarity_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (c : ℝ) (hc : 0 < c) (A : E ≃ₗᵢ[ℝ] E) (b : E) (x : UpperHalfSpace E) : ((similarity c hc A b) x).height = c * x.height

The similarity similarity c hc A b multiplies heights by c.

theorem TauCeti.UpperHalfSpace.tangentSpaceCastModel_mfderiv_similarity {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (c : ℝ) (hc : 0 < c) (A : E ≃ₗᵢ[ℝ] E) (b : E) (x : UpperHalfSpace E) (v : TangentSpace (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x) : (tangentSpaceCastModel (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) ((similarity c hc A b) x)) ((mfderiv% ⇑(similarity c hc A b) x) v) = c • (LinearIsometryEquiv.withLpProdCongr 2 A (LinearIsometryEquiv.refl ℝ ℝ)) ((tangentSpaceCastModel (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) x) v)

The differential of the similarity similarity c hc A b is c times the linear isometry (x, t) ↦ (A x, t).

@[simp]

theorem TauCeti.UpperHalfSpace.similarity_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : similarity 1 ⋯ (LinearIsometryEquiv.refl ℝ E) 0 = 1

The similarity with factor 1, linear part the identity and translation 0 is the identity isometry.

@[simp]

theorem TauCeti.UpperHalfSpace.similarity_mul_similarity {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (c c' : ℝ) (hc : 0 < c) (hc' : 0 < c') (A A' : E ≃ₗᵢ[ℝ] E) (b b' : E) : similarity c hc A b * similarity c' hc' A' b' = similarity (c * c') ⋯ (A'.trans A) (c • A b' + b)

Composing similarities multiplies their scale factors and composes their linear parts.

@[simp]

theorem TauCeti.UpperHalfSpace.similarity_inv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (c : ℝ) (hc : 0 < c) (A : E ≃ₗᵢ[ℝ] E) (b : E) : (similarity c hc A b)⁻¹ = similarity c⁻¹ ⋯ A.symm (-(c⁻¹ • A.symm b))

The inverse of a similarity is the similarity with the inverse scale factor and the inverse linear part.

instance TauCeti.UpperHalfSpace.isPretransitive_isom {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : MulAction.IsPretransitive (Isom (modelWithCornersSelf ℝ (WithLp 2 (E × ℝ))) (UpperHalfSpace E)) (UpperHalfSpace E)

The isometry group of the upper half-space model acts transitively: it is a homogeneous Riemannian manifold.