Two-disk quotients and their hemisphere comparison map

Definition

SP4Gluing

by ryanshin · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

manifoldssp4-foundationstopologytwo-disk-gluing

Let $m\ge0$ , let $D^{m+1}$ be the closed unit disk in $\mathbb R^{m+1}$ , and let $S^m=\partial D^{m+1}$ carry its usual subspace topology. For a boundary homeomorphism $\varphi:S^m\to S^m$ , this bundle defines the space

Q_\varphi=(D^{m+1}_L\sqcup D^{m+1}_R)/{\sim},\qquad (u,L)\sim(\varphi(u),R)\quad(u\in S^m),

where the equivalence relation is generated by the displayed boundary identifications and the space has the quotient topology. Its compactness is included.

The bundle also fixes the upper and lower hemispheres of $S^{m+1}$ , their explicit coordinate-dropping homeomorphisms with the disk, first-coordinate reflection, and the radial extension $A_\varphi(x)=\|x\|\varphi(x/\|x\|)$ for $x\ne0$ , with $A_\varphi(0)=0$ . The extension takes values in the disk and agrees with $\varphi$ on its boundary. These definitions produce a well-defined comparison map $F_\varphi:Q_\varphi\to S^{m+1}$ by mapping the left disk to the upper hemisphere and the right disk, after applying $A_{\varphi^{-1}}$ , to the lower hemisphere.

This supplies the data and constructor properties for the topological two-disk gluing theorem. Continuity and bijectivity of the comparison map, and hence the final quotient-to-sphere homeomorphism, are proved separately. No smooth structure on the quotient or differentiability of the radial extension is asserted.

Definition code

import Mathlib.Geometry.Manifold.Instances.Sphere
import Mathlib.Analysis.InnerProductSpace.EuclideanDist

import Mathlib
import Definitions.Def_SPC4DiskCharts

set_option autoImplicit false
namespace SP4Gluing
open SPC4Disk
open Set Metric

open scoped ContDiff Manifold

section Hemisphere

variable {m : ℕ}

lemma euclidean_norm_sq_cons (a : ℝ) (w : EuclideanSpace ℝ (Fin (m + 1))) :
    ‖(WithLp.toLp 2 (Fin.cons a (fun i => w i)) :
      EuclideanSpace ℝ (Fin (m + 2)))‖ ^ 2 = a ^ 2 + ‖w‖ ^ 2 := by
  have hw : ‖w‖ ^ 2 = ∑ i : Fin (m + 1), ‖w i‖ ^ 2 := by
    rw [EuclideanSpace.norm_eq, Real.sq_sqrt (by positivity)]
  rw [EuclideanSpace.norm_eq, Real.sq_sqrt (by positivity), hw, Fin.sum_univ_succ]
  simp [Real.norm_eq_abs, sq_abs]

lemma euclidean_norm_sq_tail (x : EuclideanSpace ℝ (Fin (m + 2))) :
    ‖(WithLp.toLp 2 (Fin.tail (fun i => x i)) :
      EuclideanSpace ℝ (Fin (m + 1)))‖ ^ 2 = ‖x‖ ^ 2 - x 0 ^ 2 := by
  have h := euclidean_norm_sq_cons (x 0)
    (WithLp.toLp 2 (Fin.tail (fun i => x i)) : EuclideanSpace ℝ (Fin (m + 1)))
  have hcons : (WithLp.toLp 2 (Fin.cons (x 0) (fun i =>
      (WithLp.toLp 2 (Fin.tail (fun i => x i)) :
        EuclideanSpace ℝ (Fin (m + 1))) i)) :
      EuclideanSpace ℝ (Fin (m + 2))) = x := by
    apply WithLp.ofLp_injective
    funext j
    induction j using Fin.cases with
    | zero => simp
    | succ i => simp [Fin.tail]
  rw [hcons] at h
  linarith

def upperHemisphere (m : ℕ) : Set (sphere (0 : EuclideanSpace ℝ (Fin (m + 2))) 1) :=
  { x | 0 ≤ x.val 0 }

def lowerHemisphere (m : ℕ) : Set (sphere (0 : EuclideanSpace ℝ (Fin (m + 2))) 1) :=
  { x | x.val 0 ≤ 0 }

def hemisphereToDisk (x : upperHemisphere m) :
    closedBall (0 : EuclideanSpace ℝ (Fin (m + 1))) 1 :=
  ⟨WithLp.toLp 2 (Fin.tail (fun i => x.val.val i)), by
    have hx : ‖x.val.val‖ = 1 := mem_sphere_zero_iff_norm.mp x.val.2
    have h := euclidean_norm_sq_tail (x.val.val)
    rw [hx] at h
    have hle : ‖(WithLp.toLp 2 (Fin.tail (fun i => x.val.val i)) :
        EuclideanSpace ℝ (Fin (m + 1)))‖ ^ 2 ≤ 1 := by
      rw [h]; nlinarith [sq_nonneg (x.val.val 0)]
    rw [mem_closedBall_zero_iff]
    nlinarith [norm_nonneg (WithLp.toLp 2 (Fin.tail (fun i => x.val.val i)) :
      EuclideanSpace ℝ (Fin (m + 1)))]⟩

noncomputable def diskToHemisphere (w : closedBall (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) :
    upperHemisphere m :=
  ⟨⟨WithLp.toLp 2 (Fin.cons (Real.sqrt (1 - ‖w.val‖ ^ 2)) (fun i => w.val i)), by
    have hw : ‖w.val‖ ≤ 1 := mem_closedBall_zero_iff.mp w.2
    have hnn : (0 : ℝ) ≤ 1 - ‖w.val‖ ^ 2 := by nlinarith [norm_nonneg w.val]
    have h := euclidean_norm_sq_cons (Real.sqrt (1 - ‖w.val‖ ^ 2)) w.val
    rw [Real.sq_sqrt hnn] at h
    have h1 : ‖(WithLp.toLp 2 (Fin.cons (Real.sqrt (1 - ‖w.val‖ ^ 2))
        (fun i => w.val i)) : EuclideanSpace ℝ (Fin (m + 2)))‖ ^ 2 = 1 := by
      rw [h]; ring
    rw [mem_sphere_zero_iff_norm]
    have hfac : (‖(WithLp.toLp 2 (Fin.cons (Real.sqrt (1 - ‖w.val‖ ^ 2))
        (fun i => w.val i)) : EuclideanSpace ℝ (Fin (m + 2)))‖ - 1) *
        (‖(WithLp.toLp 2 (Fin.cons (Real.sqrt (1 - ‖w.val‖ ^ 2))
          (fun i => w.val i)) : EuclideanSpace ℝ (Fin (m + 2)))‖ + 1) = 0 := by
      nlinarith [h1]
    rcases mul_eq_zero.mp hfac with hc | hc
    · linarith
    · linarith [norm_nonneg (WithLp.toLp 2 (Fin.cons (Real.sqrt (1 - ‖w.val‖ ^ 2))
        (fun i => w.val i)) : EuclideanSpace ℝ (Fin (m + 2)))]⟩, by
    show (0 : ℝ) ≤ _
    simp [Real.sqrt_nonneg]⟩

lemma hemisphereToDisk_diskToHemisphere
    (w : closedBall (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) :
    hemisphereToDisk (diskToHemisphere w) = w := by
  apply Subtype.ext
  show (WithLp.toLp 2 (Fin.tail (fun i =>
    (WithLp.toLp 2 (Fin.cons (Real.sqrt (1 - ‖w.val‖ ^ 2))
      (fun i => w.val i)) : EuclideanSpace ℝ (Fin (m + 2))) i)) :
      EuclideanSpace ℝ (Fin (m + 1))) = w.val
  apply WithLp.ofLp_injective
  funext j
  simp [Fin.tail]

lemma diskToHemisphere_hemisphereToDisk (x : upperHemisphere m) :
    diskToHemisphere (hemisphereToDisk x) = x := by
  apply Subtype.ext
  apply Subtype.ext
  have hx : ‖x.val.val‖ = 1 := mem_sphere_zero_iff_norm.mp x.val.2
  have hpos : 0 ≤ x.val.val 0 := x.2
  have htail := euclidean_norm_sq_tail (x.val.val)
  rw [hx] at htail
  have hsq : Real.sqrt (1 - ‖(WithLp.toLp 2 (Fin.tail (fun i => x.val.val i)) :
      EuclideanSpace ℝ (Fin (m + 1)))‖ ^ 2) = x.val.val 0 := by
    rw [htail]
    have : (1 : ℝ) - (1 ^ 2 - x.val.val 0 ^ 2) = x.val.val 0 ^ 2 := by ring
    rw [this, Real.sqrt_sq hpos]
  show (WithLp.toLp 2 (Fin.cons (Real.sqrt (1 - ‖(WithLp.toLp 2
    (Fin.tail (fun i => x.val.val i)) : EuclideanSpace ℝ (Fin (m + 1)))‖ ^ 2))
      (fun i => (WithLp.toLp 2 (Fin.tail (fun i => x.val.val i)) :
        EuclideanSpace ℝ (Fin (m + 1))) i)) :
      EuclideanSpace ℝ (Fin (m + 2))) = x.val.val
  rw [hsq]
  apply WithLp.ofLp_injective
  funext j
  induction j using Fin.cases with
  | zero => simp
  | succ i => simp [Fin.tail]

lemma continuous_hemisphereToDisk :
    Continuous (hemisphereToDisk (m := m)) := by
  apply Continuous.subtype_mk
  refine (PiLp.continuous_toLp 2 _).comp (continuous_pi fun j => ?_)
  exact (PiLp.continuous_apply 2 _ j.succ).comp
    (continuous_subtype_val.comp continuous_subtype_val)

lemma continuous_diskToHemisphere :
    Continuous (diskToHemisphere (m := m)) := by
  apply Continuous.subtype_mk
  apply Continuous.subtype_mk
  refine (PiLp.continuous_toLp 2 _).comp (continuous_pi fun j => ?_)
  induction j using Fin.cases with
  | zero =>
    simp only [Fin.cons_zero]
    exact (Real.continuous_sqrt.comp ((continuous_const.sub
      ((continuous_norm.comp continuous_subtype_val).pow 2))))
  | succ i =>
    simp only [Fin.cons_succ]
    exact (PiLp.continuous_apply 2 _ i).comp continuous_subtype_val

noncomputable def upperHemisphereHomeoDisk :
    upperHemisphere m ≃ₜ closedBall (0 : EuclideanSpace ℝ (Fin (m + 1))) 1 where
  toFun := hemisphereToDisk
  invFun := diskToHemisphere
  left_inv := diskToHemisphere_hemisphereToDisk
  right_inv := hemisphereToDisk_diskToHemisphere
  continuous_toFun := continuous_hemisphereToDisk
  continuous_invFun := continuous_diskToHemisphere

private lemma nonneg_eq_of_sq_eq {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b)
    (h : a ^ 2 = b ^ 2) : a = b := by
  have hfac : (a - b) * (a + b) = 0 := by nlinarith
  rcases mul_eq_zero.mp hfac with h' | h'
  · linarith
  · have ha0 : a = 0 := by linarith
    have hb0 : b = 0 := by linarith
    rw [ha0, hb0]

lemma euclidean_norm_sq_cons' (a : ℝ) (f : Fin (m + 1) → ℝ) :
    ‖(WithLp.toLp 2 (Fin.cons a f) : EuclideanSpace ℝ (Fin (m + 2)))‖ ^ 2
      = a ^ 2 + ‖(WithLp.toLp 2 f : EuclideanSpace ℝ (Fin (m + 1)))‖ ^ 2 := by
  have h := euclidean_norm_sq_cons a (WithLp.toLp 2 f : EuclideanSpace ℝ (Fin (m + 1)))
  simpa using h

def reflectFirst (x : EuclideanSpace ℝ (Fin (m + 2))) :
    EuclideanSpace ℝ (Fin (m + 2)) :=
  WithLp.toLp 2 (Fin.cons (-(x 0)) (Fin.tail (fun i => x i)))

@[simp] lemma reflectFirst_zero (x : EuclideanSpace ℝ (Fin (m + 2))) :
    reflectFirst x 0 = -(x 0) := by
  simp [reflectFirst]

lemma reflectFirst_norm (x : EuclideanSpace ℝ (Fin (m + 2))) :
    ‖reflectFirst x‖ = ‖x‖ := by
  refine nonneg_eq_of_sq_eq (norm_nonneg _) (norm_nonneg _) ?_
  rw [reflectFirst, euclidean_norm_sq_cons', euclidean_norm_sq_tail]
  ring

lemma reflectFirst_involutive :
    Function.Involutive (reflectFirst (m := m)) := by
  intro x
  apply WithLp.ofLp_injective
  funext j
  induction j using Fin.cases with
  | zero => simp [reflectFirst]
  | succ i => simp [reflectFirst]

lemma continuous_reflectFirst : Continuous (reflectFirst (m := m)) := by
  refine (PiLp.continuous_toLp 2 _).comp (continuous_pi fun j => ?_)
  induction j using Fin.cases with
  | zero =>
    simp only [Fin.cons_zero]
    exact (PiLp.continuous_apply 2 _ 0).neg
  | succ i =>
    simp only [Fin.cons_succ, Fin.tail]
    exact PiLp.continuous_apply 2 _ i.succ

def sphereReflect : sphere (0 : EuclideanSpace ℝ (Fin (m + 2))) 1 ≃ₜ
    sphere (0 : EuclideanSpace ℝ (Fin (m + 2))) 1 where
  toFun x := ⟨reflectFirst x.val, by
    rw [mem_sphere_zero_iff_norm, reflectFirst_norm]
    exact mem_sphere_zero_iff_norm.mp x.2⟩
  invFun x := ⟨reflectFirst x.val, by
    rw [mem_sphere_zero_iff_norm, reflectFirst_norm]
    exact mem_sphere_zero_iff_norm.mp x.2⟩
  left_inv x := Subtype.ext (reflectFirst_involutive x.val)
  right_inv x := Subtype.ext (reflectFirst_involutive x.val)
  continuous_toFun := by
    apply Continuous.subtype_mk
    exact continuous_reflectFirst.comp continuous_subtype_val
  continuous_invFun := by
    apply Continuous.subtype_mk
    exact continuous_reflectFirst.comp continuous_subtype_val

def lowerHomeoUpperRefl : lowerHemisphere m ≃ₜ upperHemisphere m :=
  sphereReflect.subtype (fun x => by
    show x.val 0 ≤ 0 ↔ 0 ≤ reflectFirst x.val 0
    simp)

noncomputable def lowerHemisphereHomeoDiskRefl :
    lowerHemisphere m ≃ₜ closedBall (0 : EuclideanSpace ℝ (Fin (m + 1))) 1 :=
  lowerHomeoUpperRefl.trans upperHemisphereHomeoDisk

def sphereToDisk (u : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) :
    closedBall (0 : EuclideanSpace ℝ (Fin (m + 1))) 1 :=
  ⟨u.val, by
    rw [mem_closedBall_zero_iff]
    exact le_of_eq (mem_sphere_zero_iff_norm.mp u.2)⟩

inductive GlueRel (φ : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1 ≃ₜ
      sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) :
    (closedBall (0 : EuclideanSpace ℝ (Fin (m + 1))) 1 ⊕
      closedBall (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) →
    (closedBall (0 : EuclideanSpace ℝ (Fin (m + 1))) 1 ⊕
      closedBall (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) → Prop
  | glue (u : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) :
      GlueRel φ (Sum.inl (sphereToDisk u)) (Sum.inr (sphereToDisk (φ u)))

def TwistedSphere (φ : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1 ≃ₜ
    sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) : Type _ :=
  Quot (GlueRel φ)

instance (φ : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1 ≃ₜ
    sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) :
    TopologicalSpace (TwistedSphere φ) :=
  inferInstanceAs (TopologicalSpace (Quot (GlueRel φ)))

lemma reflectFirst_eq_self_of_coord_zero (x : EuclideanSpace ℝ (Fin (m + 2)))
    (h : x 0 = 0) : reflectFirst x = x := by
  apply WithLp.ofLp_injective
  funext j
  induction j using Fin.cases with
  | zero => simp [reflectFirst, h]
  | succ i => simp [reflectFirst, Fin.tail]

lemma diskToHemisphere_sphereToDisk_coord_zero
    (u : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) :
    ((diskToHemisphere (sphereToDisk u)).val.val) 0 = 0 := by
  have hu : ‖u.val‖ = 1 := mem_sphere_zero_iff_norm.mp u.2
  show Real.sqrt (1 - ‖(sphereToDisk u).val‖ ^ 2) = 0
  show Real.sqrt (1 - ‖u.val‖ ^ 2) = 0
  rw [hu]
  norm_num

instance diskCompactSpace : CompactSpace (closedBall (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) :=
  isCompact_iff_compactSpace.mp (isCompact_closedBall 0 1)

instance twistedSphereCompactSpace
    (φ : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1 ≃ₜ
      sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) :
    CompactSpace (TwistedSphere φ) := by
  constructor
  have h : IsCompact (Set.range (Quot.mk (GlueRel φ))) :=
    isCompact_range continuous_quot_mk
  rwa [Set.range_eq_univ.mpr Quot.mk_surjective] at h

noncomputable def alexanderExt
    (φ : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1 ≃ₜ
      sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1)
    (w : closedBall (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) :
    closedBall (0 : EuclideanSpace ℝ (Fin (m + 1))) 1 :=
  ⟨‖w.val‖ • (φ (unitOr diskNorth w.val)).val, by
    rw [mem_closedBall_zero_iff, norm_smul, Real.norm_eq_abs,
      abs_of_nonneg (norm_nonneg _),
      mem_sphere_zero_iff_norm.mp (φ (unitOr diskNorth w.val)).2, mul_one]
    exact mem_closedBall_zero_iff.mp w.2⟩

lemma alexanderExt_sphereToDisk
    (φ : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1 ≃ₜ
      sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1)
    (u : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) :
    alexanderExt φ (sphereToDisk u) = sphereToDisk (φ u) := by
  apply Subtype.ext
  show ‖u.val‖ • (φ (unitOr diskNorth u.val)).val = (φ u).val
  have hu : ‖u.val‖ = 1 := mem_sphere_zero_iff_norm.mp u.2
  have h1 : unitOr diskNorth u.val = u := by
    have := unitOr_smul (n := m + 1) diskNorth (r := 1) one_pos u
    rwa [one_smul] at this
  rw [h1, hu, one_smul]

noncomputable def twistedGlueToSphere
    (φ : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1 ≃ₜ
      sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) :
    TwistedSphere φ → sphere (0 : EuclideanSpace ℝ (Fin (m + 2))) 1 :=
  Quot.lift
    (Sum.elim (fun w => (upperHemisphereHomeoDisk.symm w).val)
      (fun w => (lowerHemisphereHomeoDiskRefl.symm (alexanderExt φ.symm w)).val))
    (by
      rintro _ _ ⟨u⟩
      show (upperHemisphereHomeoDisk.symm (sphereToDisk u)).val =
        (lowerHemisphereHomeoDiskRefl.symm
          (alexanderExt φ.symm (sphereToDisk (φ u)))).val
      rw [alexanderExt_sphereToDisk, Homeomorph.symm_apply_apply]
      apply Subtype.ext
      show (diskToHemisphere (sphereToDisk u)).val.val =
        reflectFirst (diskToHemisphere (sphereToDisk u)).val.val
      exact (reflectFirst_eq_self_of_coord_zero _
        (diskToHemisphere_sphereToDisk_coord_zero u)).symm)

end Hemisphere

end SP4Gluing

Source

Unpublished local Lean source Hemisphere.lean, SHA-256 c48843d2c4ec6987acfd7f7ab3a92bfed990376206142e74712795b4e9399828, recovered from the saved SP4 project. Gluing relation and quotient: lines 444–470; Alexander extension and inverse: lines 521–623; descended comparison map and its properties: lines 642–755; constructive capstone twistedSphereHomeoSphere: lines 765–772. The theorem records existence of the source's constructed homeomorphism. The source file was untracked; no repository-commit attribution or mathematical novelty claim is made. Legacy commentary equating smooth twisted-sphere standardness with SP4 is not part of this statement and was omitted.

View graph