The hemispheres of S² as graphs over the unit disc

The closed upper and lower hemispheres of the unit sphere S² ⊆ ℝ³ are the graphs of u ↦ ±√(1 - ‖u‖²) over the closed unit disc of ℂ, identified with the plane x₂ = 0 by u ↦ (Re u, Im u). For a sign c (that is, c ^ 2 = 1), TauCeti.hemisphereGraph sends a point u of the disc to (Re u, Im u, c √(1 - ‖u‖²)). The two hemispheres cover the sphere, agree on the equator ‖u‖ = 1, and meet only there.

These are the hemispheres TauCeti.prodHemisphereGraph of the unit sphere of WithLp 2 (ℂ × ℝ), moved into ℝ³ by the linear isometry TauCeti.complexProdRealLinearIsometryEquiv, (u, t) ↦ (Re u, Im u, t), and their properties are derived from the general ones there. They are also the coordinate form, over the unit disc of ℂ, of the inverse of TauCeti.hemisphereHomeomorph, which parametrizes the closed hemisphere around any unit vector p of a real inner product space by the closed unit ball of (ℝ ∙ p)ᗮ. The disc of ℂ is the one used by D² × S¹ solid tori, so these graphs are the solid tori S¹ × D²₊ and S¹ × D²₋ of S¹ × S².

Main definitions

• TauCeti.complexProdRealLinearIsometryEquiv: the linear isometry WithLp 2 (ℂ × ℝ) ≃ ℝ³, (u, t) ↦ (Re u, Im u, t).
• TauCeti.hemisphereGraphPoint c u: the point (Re u, Im u, c √(1 - ‖u‖²)) of ℝ³.
• TauCeti.hemisphereGraph hc: the hemisphere of sign c of S², as a map from the closed unit disc of ℂ.

Main results

• TauCeti.eq_of_hemisphereGraph_eq: a point of a hemisphere determines the point of the disc.
• TauCeti.hemisphereGraph_eq_of_norm_eq_one: the hemispheres agree on the equator.
• TauCeti.norm_eq_one_of_hemisphereGraph_eq: hemispheres of opposite signs meet only over the boundary of the disc.
• TauCeti.exists_hemisphereGraph_eq: every point of S² lies on the hemisphere of the sign of its last coordinate.

def TauCeti.complexProdRealLinearIsometryEquiv : WithLp 2 (ℂ × ℝ) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 3)

The linear isometry WithLp 2 (ℂ × ℝ) ≃ₗᵢ[ℝ] ℝ³ sending (u, t) to (Re u, Im u, t).

@[simp]

theorem TauCeti.complexProdRealLinearIsometryEquiv_apply (x : WithLp 2 (ℂ × ℝ)) : complexProdRealLinearIsometryEquiv x = !₂[x.fst.re, x.fst.im, x.snd]

TauCeti.complexProdRealLinearIsometryEquiv sends (u, t) to (Re u, Im u, t).

@[simp]

theorem TauCeti.complexProdRealLinearIsometryEquiv_symm_apply (y : EuclideanSpace ℝ (Fin 3)) : complexProdRealLinearIsometryEquiv.symm y = WithLp.toLp 2 ({ re := y.ofLp 0, im := y.ofLp 1 }, y.ofLp 2)

The inverse of TauCeti.complexProdRealLinearIsometryEquiv sends (x₀, x₁, x₂) to (x₀ + i x₁, x₂).

noncomputable def TauCeti.hemisphereGraphPoint (c : ℝ) (u : ℂ) : EuclideanSpace ℝ (Fin 3)

The point (Re u, Im u, c √(1 - ‖u‖²)) of ℝ³, the image of TauCeti.prodHemisphereGraphPoint c u under TauCeti.complexProdRealLinearIsometryEquiv; for c = 1 and c = -1 and u in the closed unit disc this is the upper and the lower hemisphere of S².

@[simp]

theorem TauCeti.hemisphereGraphPoint_apply_zero (c : ℝ) (u : ℂ) : (hemisphereGraphPoint c u).ofLp 0 = u.re

The first coordinate of TauCeti.hemisphereGraphPoint c u is the real part of u.

@[simp]

theorem TauCeti.hemisphereGraphPoint_apply_one (c : ℝ) (u : ℂ) : (hemisphereGraphPoint c u).ofLp 1 = u.im

The second coordinate of TauCeti.hemisphereGraphPoint c u is the imaginary part of u.

@[simp]

theorem TauCeti.hemisphereGraphPoint_apply_two (c : ℝ) (u : ℂ) : (hemisphereGraphPoint c u).ofLp 2 = c * √(1 - ‖u‖ ^ 2)

The last coordinate of TauCeti.hemisphereGraphPoint c u is c √(1 - ‖u‖²).

theorem TauCeti.hemisphereGraphPoint_mem_sphere {c : ℝ} (hc : c ^ 2 = 1) (u : ↑(Metric.closedBall 0 1)) : hemisphereGraphPoint c ↑u ∈ Metric.sphere 0 1

For a sign c, the points TauCeti.hemisphereGraphPoint c u over the closed unit disc lie on the unit sphere.

noncomputable def TauCeti.hemisphereGraph {c : ℝ} (hc : c ^ 2 = 1) (u : ↑(Metric.closedBall 0 1)) : ↑(Metric.sphere 0 1)

The hemisphere of S² of sign c, the graph of u ↦ c √(1 - ‖u‖²) over the closed unit disc of ℂ: the hemisphere TauCeti.prodHemisphereGraph hc of the unit sphere of WithLp 2 (ℂ × ℝ), moved into ℝ³ by TauCeti.complexProdRealLinearIsometryEquiv.

@[simp]

theorem TauCeti.coe_hemisphereGraph_apply {c : ℝ} (hc : c ^ 2 = 1) (u : ↑(Metric.closedBall 0 1)) : ↑(hemisphereGraph hc u) = hemisphereGraphPoint c ↑u

TauCeti.hemisphereGraph hc u is the point TauCeti.hemisphereGraphPoint c u.

theorem TauCeti.continuous_hemisphereGraph {c : ℝ} (hc : c ^ 2 = 1) : Continuous (hemisphereGraph hc)

The hemisphere graphs are continuous.

theorem TauCeti.eq_of_hemisphereGraph_eq {c c' : ℝ} {hc : c ^ 2 = 1} {hc' : c' ^ 2 = 1} {u v : ↑(Metric.closedBall 0 1)} (h : hemisphereGraph hc u = hemisphereGraph hc' v) : u = v

The first two coordinates of a point of a hemisphere recover the point of the disc, whatever the signs of the two hemispheres.

theorem TauCeti.hemisphereGraph_eq_of_norm_eq_one {c c' : ℝ} (hc : c ^ 2 = 1) (hc' : c' ^ 2 = 1) {u : ↑(Metric.closedBall 0 1)} (hu : ‖↑u‖ = 1) : hemisphereGraph hc u = hemisphereGraph hc' u

The hemispheres of any two signs agree on the equator.

theorem TauCeti.norm_eq_one_of_hemisphereGraph_eq {c c' : ℝ} {hc : c ^ 2 = 1} {hc' : c' ^ 2 = 1} (hcc' : c ≠ c') {u v : ↑(Metric.closedBall 0 1)} (h : hemisphereGraph hc u = hemisphereGraph hc' v) : ‖↑v‖ = 1

Hemispheres of opposite signs meet only over the boundary of the disc.

theorem TauCeti.exists_hemisphereGraph_eq {c : ℝ} (hc : c ^ 2 = 1) (x : ↑(Metric.sphere 0 1)) (hx : 0 ≤ c * (↑x).ofLp 2) : ∃ (u : ↑(Metric.closedBall 0 1)), hemisphereGraph hc u = x

Every point of S² whose last coordinate x₂ has 0 ≤ c x₂ lies on the hemisphere of sign c, over the point x₀ + i x₁ of the disc.