Brieskorn spheres, lens spaces, $P\#(-P)$ , and realizations of simplicial complexes

Definition

hsbb_spaces

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

3-manifoldstopology

Concrete 3-manifolds for the homology-ball mission.

Brieskorn manifolds. For $p,q,r \in \mathbb N$ ,

\Sigma(p,q,r) = \{ z \in \mathbb C^3 : z_0^p + z_1^q + z_2^r = 0,\ \|z\| = 1 \},

with the subspace topology. The Poincaré homology sphere is $P = \Sigma(2,3,5)$ .

Lens spaces. $L(p,q)$ is the quotient of the unit sphere $S^3 \subset \mathbb C^2$ by the relation $a \sim b$ iff $b = (\zeta^k a_0, \zeta^{qk} a_1)$ for some $k \in \mathbb N$ , where $\zeta = e^{2\pi i/p}$ , with the quotient topology.

The double of a punctured manifold. For a space $M$ with an atlas modelled on $\mathbb R^3$ , a point $x$ and a radius $r$ , let $\varphi$ be the chart at $x$ , $B = \varphi^{-1}(\mathrm{ball}(\varphi x, r))$ and $S = \varphi^{-1}(\mathrm{sphere}(\varphi x, r))$ . The double $D(M\setminus B)$ is the quotient of two copies of $M \setminus B$ in which each point of $S$ in the first copy is identified with the same point in the second copy. When the closed ball lies in the chart target, $D(M\setminus B)$ is homeomorphic to the connected sum $M \# (-M)$ .

Realizations of simplicial complexes. A finite simplicial complex is a list $K$ of simplices, each a list of vertex labels in $\mathbb N$ . Its realization is

|K| = \bigcup_{\sigma \in K} \Bigl\{ x \in \mathbb R^{\mathbb N} : x \ge 0,\ x_i = 0 \text{ for } i \notin \sigma,\ \textstyle\sum_{i\in\sigma} x_i = 1 \Bigr\},

with the subspace topology of the product topology. This is the input format for algorithms on 3-manifolds.

Formalization Note. For $p = 0$ the formula gives $\zeta = 1$ ; lens spaces are only used with $p \ge 4$ in this mission.

Definition code

import Mathlib

/-!
# Concrete 3-manifolds for the homology-ball mission

Brieskorn spheres, lens spaces, the double of a manifold minus an open chart ball
(a model of `M # (-M)`), and geometric realizations of finite simplicial complexes
(used to feed 3-manifolds to an algorithm).
-/

open scoped Manifold

namespace HomologySpheresBoundBalls

/-- The Brieskorn manifold `Σ(p,q,r) = {z ∈ ℂ³ : z₀^p + z₁^q + z₂^r = 0, |z| = 1}`,
with the subspace topology from `ℂ³`. -/
def BrieskornSphere (p q r : ℕ) : Set (EuclideanSpace ℂ (Fin 3)) :=
  {z | z 0 ^ p + z 1 ^ q + z 2 ^ r = 0 ∧ ‖z‖ = 1}

/-- The Poincaré homology sphere (Poincaré dodecahedral space) `Σ(2,3,5)`. -/
abbrev PoincareSphere : Set (EuclideanSpace ℂ (Fin 3)) := BrieskornSphere 2 3 5

/-- The unit 3-sphere in `ℂ²`. -/
abbrev ComplexSphere3 : Type := Metric.sphere (0 : EuclideanSpace ℂ (Fin 2)) 1

/-- The relation on `S³ ⊆ ℂ²` whose classes are the orbits of the `ℤ/p`-action generated by
`(z₀, z₁) ↦ (ζ z₀, ζ^q z₁)`, `ζ = e^{2πi/p}`. -/
def lensRel (p q : ℕ) (a b : ComplexSphere3) : Prop :=
  ∃ k : ℕ, (b : EuclideanSpace ℂ (Fin 2)) 0 =
      Complex.exp (2 * Real.pi * Complex.I / p) ^ k * (a : EuclideanSpace ℂ (Fin 2)) 0 ∧
    (b : EuclideanSpace ℂ (Fin 2)) 1 =
      Complex.exp (2 * Real.pi * Complex.I / p) ^ (q * k) * (a : EuclideanSpace ℂ (Fin 2)) 1

/-- The lens space `L(p,q) = S³ / (ℤ/p)`, with the quotient topology. -/
def LensSpace (p q : ℕ) : Type := Quot (lensRel p q)

instance (p q : ℕ) : TopologicalSpace (LensSpace p q) :=
  inferInstanceAs (TopologicalSpace (Quot (lensRel p q)))

section Double

variable {M : Type} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 3)) M]

/-- The open chart ball `B(x,r) = φ⁻¹(ball(φ x, r))` for the chart `φ` at `x`. -/
def chartBall (x : M) (r : ℝ) : Set M :=
  (chartAt (EuclideanSpace ℝ (Fin 3)) x).symm ''
    Metric.ball (chartAt (EuclideanSpace ℝ (Fin 3)) x x) r

/-- The chart sphere `φ⁻¹(sphere(φ x, r))`. -/
def chartSphere (x : M) (r : ℝ) : Set M :=
  (chartAt (EuclideanSpace ℝ (Fin 3)) x).symm ''
    Metric.sphere (chartAt (EuclideanSpace ℝ (Fin 3)) x x) r

/-- `M` with the open chart ball `B(x,r)` removed. -/
abbrev Punctured (x : M) (r : ℝ) : Type := ↥((chartBall x r)ᶜ)

/-- Gluing relation for the double: a point of the boundary sphere in the first copy is
identified with the same point in the second copy. -/
def doubleRel (x : M) (r : ℝ) : Punctured x r ⊕ Punctured x r → Punctured x r ⊕ Punctured x r → Prop
  | .inl a, .inr b => a = b ∧ (a : M) ∈ chartSphere x r
  | _, _ => False

/-- The double `D(M ∖ B) = (M ∖ B) ∪_{∂B} (M ∖ B)` of `M` minus an open chart ball,
with the quotient topology. Topologically this is the connected sum `M # (-M)`. -/
def PuncturedDouble (x : M) (r : ℝ) : Type := Quot (doubleRel x r)

instance (x : M) (r : ℝ) : TopologicalSpace (PuncturedDouble x r) :=
  inferInstanceAs (TopologicalSpace (Quot (doubleRel x r)))

end Double

/-- The geometric realization `|K| ⊆ ℝ^ℕ` of a finite simplicial complex `K` given by a list
of simplices, each simplex a list of vertex labels in `ℕ`: the union over `σ ∈ K` of the
standard simplices `{x ≥ 0, supp x ⊆ σ, ∑_{i ∈ σ} x_i = 1}`. Topology: subspace of the product. -/
def realization (K : List (List ℕ)) : Set (ℕ → ℝ) :=
  {x | ∃ σ ∈ K, (∀ i, 0 ≤ x i) ∧ (∀ i, i ∉ σ → x i = 0) ∧ ∑ i ∈ σ.toFinset, x i = 1}

end HomologySpheresBoundBalls

Source

Open Problem Garden, 'Which homology 3-spheres bound homology 4-balls?' (rybu, 2009), http://www.openproblemgarden.org/op/which_homology_3_spheres_bound_homology_4_balls

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Brieskorn spheres, lens spaces, P#(−P)P\#(-P)P#(−P), and realizations of simplicial complexes

Brieskorn spheres, lens spaces, $P\#(-P)$ , and realizations of simplicial complexes