Closed hemispheres of a unit sphere

For a unit vector p of a real inner product space E, the closed hemisphere {x ∈ S | 0 ≤ ⟪x, p⟫} of the unit sphere S of E is homeomorphic to the closed unit ball of the hyperplane (ℝ ∙ p)ᗮ. The homeomorphism removes the component of x along p; its inverse lifts a point y of the ball to y + √(1 - ‖y‖²) • p.

The closed hemispheres around p and -p cover the sphere and meet in the equator, the unit sphere of (ℝ ∙ p)ᗮ, included in S by TauCeti.equatorInclusion p. Closed hemispheres are the discs out of which the sphere is built in the inductive computations of the homology of the complement of an embedded sphere.

Main definitions

• TauCeti.hemisphereHomeomorph p: the closed hemisphere around p is homeomorphic to the closed unit ball of (ℝ ∙ p)ᗮ.
• TauCeti.equatorInclusion p: the inclusion of the equator, the unit sphere of (ℝ ∙ p)ᗮ, into the unit sphere of E.

Main results

• TauCeti.coe_hemisphereHomeomorph_apply and TauCeti.coe_hemisphereHomeomorph_symm_apply: the formulas for the homeomorphism and its inverse.
• TauCeti.range_equatorInclusion: the equator is the intersection of the closed hemispheres around p and -p.

noncomputable def TauCeti.hemisphereHomeomorph {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : ↑(Metric.sphere 0 1)) : { x : ↑(Metric.sphere 0 1) // 0 ≤ inner ℝ ↑x ↑p } ≃ₜ ↑(Metric.closedBall 0 1)

The closed hemisphere around p is a disc. For a point p of the unit sphere of a real inner product space E, the closed hemisphere {x | 0 ≤ ⟪x, p⟫} of the unit sphere is homeomorphic to the closed unit ball of the orthogonal complement (ℝ ∙ p)ᗮ. The homeomorphism sends x to x - ⟪x, p⟫ • p (TauCeti.coe_hemisphereHomeomorph_apply), and its inverse sends y to y + √(1 - ‖y‖²) • p (TauCeti.coe_hemisphereHomeomorph_symm_apply).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.coe_hemisphereHomeomorph_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : ↑(Metric.sphere 0 1)) (x : { x : ↑(Metric.sphere 0 1) // 0 ≤ inner ℝ ↑x ↑p }) : ↑↑((hemisphereHomeomorph p) x) = ↑↑x - inner ℝ ↑↑x ↑p • ↑p

TauCeti.hemisphereHomeomorph p removes the component along p.

@[simp]

theorem TauCeti.coe_hemisphereHomeomorph_symm_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : ↑(Metric.sphere 0 1)) (y : ↑(Metric.closedBall 0 1)) : ↑↑((hemisphereHomeomorph p).symm y) = ↑↑y + √(1 - ‖↑y‖ ^ 2) • ↑p

The inverse of TauCeti.hemisphereHomeomorph p lifts a point y of the closed unit ball of (ℝ ∙ p)ᗮ to y + √(1 - ‖y‖²) • p.

def TauCeti.equatorInclusion {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : ↑(Metric.sphere 0 1)) : ↑(Metric.sphere 0 1) → ↑(Metric.sphere 0 1)

The inclusion of the equator, the unit sphere of (ℝ ∙ p)ᗮ, into the unit sphere of E.

Equations

• TauCeti.equatorInclusion p y = ⟨↑↑y, ⋯⟩

@[simp]

theorem TauCeti.coe_equatorInclusion_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : ↑(Metric.sphere 0 1)) (y : ↑(Metric.sphere 0 1)) : ↑(equatorInclusion p y) = ↑↑y

TauCeti.equatorInclusion p is the inclusion of (ℝ ∙ p)ᗮ into E.

theorem TauCeti.continuous_equatorInclusion {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : ↑(Metric.sphere 0 1)) : Continuous (equatorInclusion p)

The inclusion of the equator is continuous.

theorem TauCeti.injective_equatorInclusion {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : ↑(Metric.sphere 0 1)) : Function.Injective (equatorInclusion p)

The inclusion of the equator is injective.

theorem TauCeti.range_equatorInclusion {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : ↑(Metric.sphere 0 1)) : Set.range (equatorInclusion p) = {x : ↑(Metric.sphere 0 1) | 0 ≤ inner ℝ ↑x ↑p} ∩ {x : ↑(Metric.sphere 0 1) | 0 ≤ inner ℝ ↑x ↑(-p)}

The equator is the set of points of the sphere orthogonal to p, the intersection of the two closed hemispheres around p and -p.