The unit sphere of an L² product as a union of two solid pieces

Let F and G be real normed spaces. A point x of the unit sphere of the L² product WithLp 2 (F × G) satisfies ‖x.fst‖ ^ 2 + ‖x.snd‖ ^ 2 = 1, so the sphere is the union of the two closed pieces ‖x.fst‖ ≤ ‖x.snd‖ and ‖x.snd‖ ≤ ‖x.fst‖, which meet in the common frontier ‖x.fst‖ = ‖x.snd‖. The first piece is homeomorphic to the product of the closed unit ball of F with the unit sphere of G, through x ↦ (x.fst / ‖x.snd‖, x.snd / ‖x.snd‖), whose inverse sends (u, v) to (u, v) / √(1 + ‖u‖ ^ 2); symmetrically, the second piece is homeomorphic to the product of the unit sphere of F with the closed unit ball of G.

This is the decomposition of the join S(F) * S(G) = S(F ⊕ G) into the two mapping cylinders. For F = G = ℂ it writes the 3-sphere as the union of two solid tori D² × S¹ and S¹ × D² glued along the torus ‖x.fst‖ = ‖x.snd‖, the genus-one Heegaard splitting of the 3-sphere.

Main definitions

• TauCeti.sphereProdFstLeHomeomorph F G: the piece ‖x.fst‖ ≤ ‖x.snd‖ of the unit sphere of WithLp 2 (F × G) is homeomorphic to closedBall (0 : F) 1 × sphere (0 : G) 1.
• TauCeti.sphereProdSndLeHomeomorph F G: the piece ‖x.snd‖ ≤ ‖x.fst‖ is homeomorphic to sphere (0 : F) 1 × closedBall (0 : G) 1.

Main results

• TauCeti.frontier_setOf_norm_fst_le_norm_snd and TauCeti.frontier_setOf_norm_snd_le_norm_fst: the frontier of each piece in the unit sphere is the set where ‖x.fst‖ = ‖x.snd‖.
• TauCeti.norm_sphereProdFstLeHomeomorph_fst_eq_one_iff and TauCeti.norm_sphereProdSndLeHomeomorph_snd_eq_one_iff: each homeomorphism carries this common frontier onto the product of the two unit spheres.

References

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Chapter 0 (joins; the decomposition of S³ into two solid tori).

noncomputable def TauCeti.sphereProdFstLeHomeomorph (F : Type u_1) (G : Type u_2) [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NormedSpace ℝ F] [NormedSpace ℝ G] : ↑{x : ↑(Metric.sphere 0 1) | ‖(↑x).fst‖ ≤ ‖(↑x).snd‖} ≃ₜ ↑(Metric.closedBall 0 1) × ↑(Metric.sphere 0 1)

The piece ‖x.fst‖ ≤ ‖x.snd‖ of the unit sphere of WithLp 2 (F × G) is homeomorphic to the product of the closed unit ball of F with the unit sphere of G, through x ↦ (x.fst / ‖x.snd‖, x.snd / ‖x.snd‖), with inverse (u, v) ↦ (u, v) / √(1 + ‖u‖ ^ 2).

@[simp]

theorem TauCeti.coe_sphereProdFstLeHomeomorph_apply_fst {F : Type u_1} {G : Type u_2} [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NormedSpace ℝ F] [NormedSpace ℝ G] (x : ↑{x : ↑(Metric.sphere 0 1) | ‖(↑x).fst‖ ≤ ‖(↑x).snd‖}) : ↑((sphereProdFstLeHomeomorph F G) x).1 = ‖(↑↑x).snd‖⁻¹ • (↑↑x).fst

@[simp]

theorem TauCeti.coe_sphereProdFstLeHomeomorph_apply_snd {F : Type u_1} {G : Type u_2} [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NormedSpace ℝ F] [NormedSpace ℝ G] (x : ↑{x : ↑(Metric.sphere 0 1) | ‖(↑x).fst‖ ≤ ‖(↑x).snd‖}) : ↑((sphereProdFstLeHomeomorph F G) x).2 = ‖(↑↑x).snd‖⁻¹ • (↑↑x).snd

@[simp]

theorem TauCeti.coe_sphereProdFstLeHomeomorph_symm_apply {F : Type u_1} {G : Type u_2} [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NormedSpace ℝ F] [NormedSpace ℝ G] (p : ↑(Metric.closedBall 0 1) × ↑(Metric.sphere 0 1)) : ↑↑((sphereProdFstLeHomeomorph F G).symm p) = WithLp.toLp 2 ((√(1 + ‖↑p.1‖ ^ 2))⁻¹ • ↑p.1, (√(1 + ‖↑p.1‖ ^ 2))⁻¹ • ↑p.2)

theorem TauCeti.norm_sphereProdFstLeHomeomorph_fst_eq_one_iff {F : Type u_1} {G : Type u_2} [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NormedSpace ℝ F] [NormedSpace ℝ G] (x : ↑{x : ↑(Metric.sphere 0 1) | ‖(↑x).fst‖ ≤ ‖(↑x).snd‖}) : ‖↑((sphereProdFstLeHomeomorph F G) x).1‖ = 1 ↔ ‖(↑↑x).fst‖ = ‖(↑↑x).snd‖

TauCeti.sphereProdFstLeHomeomorph carries the common frontier ‖x.fst‖ = ‖x.snd‖ onto sphere (0 : F) 1 × sphere (0 : G) 1, the boundary of closedBall (0 : F) 1 × sphere (0 : G) 1.

theorem TauCeti.frontier_setOf_norm_fst_le_norm_snd {F : Type u_1} {G : Type u_2} [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NormedSpace ℝ F] [NormedSpace ℝ G] : frontier {x : ↑(Metric.sphere 0 1) | ‖(↑x).fst‖ ≤ ‖(↑x).snd‖} = {x : ↑(Metric.sphere 0 1) | ‖(↑x).fst‖ = ‖(↑x).snd‖}

The frontier of the piece ‖x.fst‖ ≤ ‖x.snd‖ of the unit sphere of WithLp 2 (F × G) is the set where ‖x.fst‖ = ‖x.snd‖.

The second piece

noncomputable def TauCeti.sphereProdSndLeHomeomorph (F : Type u_1) (G : Type u_2) [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NormedSpace ℝ F] [NormedSpace ℝ G] : ↑{x : ↑(Metric.sphere 0 1) | ‖(↑x).snd‖ ≤ ‖(↑x).fst‖} ≃ₜ ↑(Metric.sphere 0 1) × ↑(Metric.closedBall 0 1)

The piece ‖x.snd‖ ≤ ‖x.fst‖ of the unit sphere of WithLp 2 (F × G) is homeomorphic to the product of the unit sphere of F with the closed unit ball of G, through x ↦ (x.fst / ‖x.fst‖, x.snd / ‖x.fst‖).

@[simp]

theorem TauCeti.coe_sphereProdSndLeHomeomorph_apply_fst {F : Type u_1} {G : Type u_2} [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NormedSpace ℝ F] [NormedSpace ℝ G] (x : ↑{x : ↑(Metric.sphere 0 1) | ‖(↑x).snd‖ ≤ ‖(↑x).fst‖}) : ↑((sphereProdSndLeHomeomorph F G) x).1 = ‖(↑↑x).fst‖⁻¹ • (↑↑x).fst

@[simp]

theorem TauCeti.coe_sphereProdSndLeHomeomorph_apply_snd {F : Type u_1} {G : Type u_2} [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NormedSpace ℝ F] [NormedSpace ℝ G] (x : ↑{x : ↑(Metric.sphere 0 1) | ‖(↑x).snd‖ ≤ ‖(↑x).fst‖}) : ↑((sphereProdSndLeHomeomorph F G) x).2 = ‖(↑↑x).fst‖⁻¹ • (↑↑x).snd

@[simp]

theorem TauCeti.coe_sphereProdSndLeHomeomorph_symm_apply {F : Type u_1} {G : Type u_2} [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NormedSpace ℝ F] [NormedSpace ℝ G] (p : ↑(Metric.sphere 0 1) × ↑(Metric.closedBall 0 1)) : ↑↑((sphereProdSndLeHomeomorph F G).symm p) = WithLp.toLp 2 ((√(1 + ‖↑p.2‖ ^ 2))⁻¹ • ↑p.1, (√(1 + ‖↑p.2‖ ^ 2))⁻¹ • ↑p.2)

theorem TauCeti.norm_sphereProdSndLeHomeomorph_snd_eq_one_iff {F : Type u_1} {G : Type u_2} [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NormedSpace ℝ F] [NormedSpace ℝ G] (x : ↑{x : ↑(Metric.sphere 0 1) | ‖(↑x).snd‖ ≤ ‖(↑x).fst‖}) : ‖↑((sphereProdSndLeHomeomorph F G) x).2‖ = 1 ↔ ‖(↑↑x).fst‖ = ‖(↑↑x).snd‖

TauCeti.sphereProdSndLeHomeomorph carries the common frontier ‖x.fst‖ = ‖x.snd‖ onto sphere (0 : F) 1 × sphere (0 : G) 1, the boundary of sphere (0 : F) 1 × closedBall (0 : G) 1.

theorem TauCeti.frontier_setOf_norm_snd_le_norm_fst {F : Type u_1} {G : Type u_2} [SeminormedAddCommGroup F] [SeminormedAddCommGroup G] [NormedSpace ℝ F] [NormedSpace ℝ G] : frontier {x : ↑(Metric.sphere 0 1) | ‖(↑x).snd‖ ≤ ‖(↑x).fst‖} = {x : ↑(Metric.sphere 0 1) | ‖(↑x).fst‖ = ‖(↑x).snd‖}

The frontier of the piece ‖x.snd‖ ≤ ‖x.fst‖ of the unit sphere of WithLp 2 (F × G) is the set where ‖x.fst‖ = ‖x.snd‖.