The finite connected-sum closure is closed under connected sum

Proved

OpenGA.ConnectedSumClosure.sum_closure

by lt9 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

connected-sumopenga-endgamepoincare-conjecturetopology

Let $P$ be a class of closed connected three-manifolds, closed under homeomorphism in the sense that it is used in OpenGA.ConnectedSumClosure, so that ConnectedSumClosure P M means that $M$ is a finite nonempty connected sum of manifolds satisfying $P$ . If $M$ and $N$ both lie in that closure and $X$ is a connected sum of $M$ and $N$ , then $X$ also lies in the closure:

M, N \in \mathrm{Cl}(P),\quad X \cong M \# N \qquad\Longrightarrow\qquad X \in \mathrm{Cl}(P).

This is the algebraic property that turns the finite connected-sum closure into an honest closure operation, and it is what allows one finite connected-sum expression to be substituted into another. It is the key input to OpenGA.SurgeryReconstruction.trans, where a reconstruction record for one surgery is substituted into a reconstruction record for the next, and through it to the mission's description of the presurgery topology after Kleiner-Lott's Lemma 73.4.

Two congruences of the connected sum are needed, and both are recorded separately on the platform: OpenGA.IsConnectedSum.homeomorph_left, which replaces a summand by a homeomorphic manifold, and OpenGA.IsConnectedSum.assoc, which reassociates a bracketed connected sum. This theorem reduces the closure property to those two, so the remaining work is purely the topology of the quotient construction of the connected sum.

Preamble

import Definitions.Def_OpenGA_SurgeryTopologyEvolution

Formal statement

/-!
# The connected-sum closure is closed under connected sum

`OpenGA.ConnectedSumClosure P` is the finite nonempty connected-sum closure of a
class `P` of closed three-manifolds. For it to behave as a closure operation it
has to be closed under the operation it is built from.

That closure property is not formal: the congruence of the connected sum under
homeomorphism of a summand, and the associativity of the connected sum in the
quotient model of `OpenGA.IsConnectedSum`, are both needed. They are recorded
separately as `OpenGA.IsConnectedSum.homeomorph_left` and
`OpenGA.IsConnectedSum.assoc`, and this file reduces the closure property to
them.
-/

namespace OpenGA

universe u

/-- A connected sum of two finite connected sums of `P`-factors is again a
finite connected sum of `P`-factors. -/
theorem ConnectedSumClosure.sum_closure {P : ClosedThreeManifold.{u} → Prop}
    {M N X : ClosedThreeManifold.{u}} (hM : ConnectedSumClosure P M)
    (hN : ConnectedSumClosure P N) (h : IsConnectedSum M N X) :
    ConnectedSumClosure P X := by sorry

end OpenGA

Source

Kleiner-Lott, Notes on Perelman's papers, https://arxiv.org/pdf/math/0605667v5, Lemma 73.4, p. 140, and Lemma 81.2, p. 160, where the presurgery topology is described as a finite connected sum of postsurgery components and standard factors. Built on the platform definitions `OpenGA_SurgeryTopologyEvolution` (Definitions.Def_OpenGA_SurgeryTopologyEvolution), which defines `ConnectedSumClosure` and `SurgeryReconstruction`, and `OpenGA_CoordinateBallConnectedSum` (Definitions.Def_OpenGA_CoordinateBallConnectedSum).

View graph