From c95510950f52cc2a4176e50074ccf394cf7345fc Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxu.math@gmail.com>
Date: Wed, 6 May 2026 22:33:48 +0200
Subject: [PATCH 1/5] feat/chore: move definition of surfaces

---
 .../Topology/ClassificationOfSurfaces.lean    | 51 ++-----------
 LeanEval/Topology/Prelude.lean                | 72 +++++++++++++++++++
 manifests/problems.toml                       |  8 +++
 3 files changed, 86 insertions(+), 45 deletions(-)
 create mode 100644 LeanEval/Topology/Prelude.lean

diff --git a/LeanEval/Topology/ClassificationOfSurfaces.lean b/LeanEval/Topology/ClassificationOfSurfaces.lean
index 98f98e3..4c48861 100644
--- a/LeanEval/Topology/ClassificationOfSurfaces.lean
+++ b/LeanEval/Topology/ClassificationOfSurfaces.lean
@@ -1,66 +1,27 @@
 import Mathlib.Analysis.Complex.Circle
 import Mathlib.Geometry.Manifold.Instances.Real
+import LeanEval.Topology.Prelude
 import EvalTools.Markers
 
 /-!
-Benchmark statements for topological classification of compact connected surfaces with boundary.
-
-The representative surface in each homeomorphism class is obtained by
-gluing certain arcs in the boundary of the unit disc.
+Benchmark statement for topological classification of compact connected surfaces with boundary.
 
 Reference: Jean Gallier & Dianna Xu, *A Guide to the Classification Theorem for Compact Surfaces*,
 Definition 6.5, Lemma 6.1, Theorem 6.1.
 https://www.cis.upenn.edu/~jean/surfclassif-root.pdf
 -/
 
-namespace Complex
-
-/-- The closed unit disc in the complex plane. -/
-abbrev ClosedUnitDisc : Type := Metric.closedBall (0 : ℂ) 1
-
-/-- The boundary point exp(2πir) on the boundary of the closed unit disc in the complex plane. -/
-noncomputable def ClosedUnitDisc.bdyPtOfReal (r : ℝ) : ClosedUnitDisc :=
-  ⟨r.fourierChar, r.fourierChar.2.le⟩
-
-end Complex
-
-namespace LeanEval.Topology.ClassificationOfSurfaces
-
-open Complex Set
-
-/-- The representative orientable surface homeomorphic to a closed orientable genus `p`
-surface with `n` discs removed, obtained by identifying the boundary of a disc in the pattern
-`a₁b₁a₁⁻¹b₁⁻¹⋯aₚbₚaₚ⁻¹bₚ⁻¹c₁h₁c₁⁻¹⋯cₙhₙcₙ⁻¹`. -/
-inductive OrientableRel (p n : ℕ) : ClosedUnitDisc → ClosedUnitDisc → Prop
-  | a (x : Icc (0 : ℝ) 1) (i : Fin p) : OrientableRel p n
-      (.bdyPtOfReal <| (4 * i + x) / (4 * p + 3 * n))
-      (.bdyPtOfReal <| (4 * i + 3 - x) / (4 * p + 3 * n))
-  | b (x : Icc (0 : ℝ) 1) (i : Fin p) : OrientableRel p n
-      (.bdyPtOfReal <| (4 * i + 1 + x) / (4 * p + 3 * n))
-      (.bdyPtOfReal <| (4 * i + 4 - x) / (4 * p + 3 * n))
-  | c (x : Icc (0 : ℝ) 1) (i : Fin n) : OrientableRel p n
-      (.bdyPtOfReal <| - (3 * i + x) / (4 * p + 3 * n))
-      (.bdyPtOfReal <| - (3 * i + 3 - x) / (4 * p + 3 * n))
+namespace LeanEval.Topology
 
-/-- The representative non-orientable surface homeomorphic to a direct sum of `p` projective
-planes with `n` discs removed, obtained by identifying the boundary of a disc in the pattern
-`a₁a₁⋯aₚaₚc₁h₁c₁⁻¹⋯cₙhₙcₙ⁻¹`. -/
-inductive NonOrientableRel (p n : ℕ) : ClosedUnitDisc → ClosedUnitDisc → Prop
-  | a (x : Icc (0 : ℝ) 1) (i : Fin p) : NonOrientableRel p n
-      (.bdyPtOfReal <| (2 * i + x) / (2 * p + 3 * n))
-      (.bdyPtOfReal <| (2 * i + 1 + x) / (2 * p + 3 * n))
-  | c (x : Icc (0 : ℝ) 1) (i : Fin n) : NonOrientableRel p n
-      (.bdyPtOfReal <| -(3 * i + x) / (2 * p + 3 * n))
-      (.bdyPtOfReal <| -(3 * i + 3 - x) / (2 * p + 3 * n))
+open Surface
 
 @[eval_problem]
 theorem classification_of_surfaces (S : Type*) [TopologicalSpace S]
     [T2Space S] [ConnectedSpace S] [CompactSpace S]
-    [ChartedSpace (EuclideanHalfSpace 2) S]
-    [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] :
+    [ChartedSpace (EuclideanHalfSpace 2) S] :
     Nonempty (S ≃ₜ Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1) ∨
     ∃ p n, ((1 ≤ p ∨ 1 ≤ n) ∧ Nonempty (S ≃ₜ Quot (OrientableRel p n))) ∨
       (1 ≤ p ∧ Nonempty (S ≃ₜ Quot (NonOrientableRel p n))) := by
   sorry
 
-end LeanEval.Topology.ClassificationOfSurfaces
+end LeanEval.Topology
diff --git a/LeanEval/Topology/Prelude.lean b/LeanEval/Topology/Prelude.lean
new file mode 100644
index 0000000..97ad3f6
--- /dev/null
+++ b/LeanEval/Topology/Prelude.lean
@@ -0,0 +1,72 @@
+import Mathlib.Analysis.Complex.Circle
+import EvalTools.Markers
+
+/-!
+# Basic definitions in topology
+
+In this file we define a representative surface in each homeomorphism class of surfaces by
+gluing certain arcs in the boundary of the unit disc.
+
+We also define a representative 3-dimensional handlebody for each genus.
+See https://en.wikipedia.org/wiki/Handlebody#3-dimensional_handlebodies.
+
+We pose it as a LeanEval problem to show that the boundary of the handlebody is homeomorphic
+to the corresponding representative surface.
+-/
+
+namespace Complex
+
+/-- The closed unit disc in the complex plane. -/
+abbrev ClosedUnitDisc : Type := Metric.closedBall (0 : ℂ) 1
+
+/-- The boundary point exp(2πir) on the boundary of the closed unit disc in the complex plane. -/
+noncomputable def ClosedUnitDisc.bdyPtOfReal (r : ℝ) : ClosedUnitDisc :=
+  ⟨r.fourierChar, r.fourierChar.2.le⟩
+
+end Complex
+
+namespace LeanEval.Topology
+
+namespace Surface
+
+open Complex Set
+
+/-- The representative orientable surface homeomorphic to a closed orientable genus `p`
+surface with `n` discs removed (if `p` and `n` are not both zero), obtained by identifying
+the boundary of a disc in the pattern `a₁b₁a₁⁻¹b₁⁻¹⋯aₚbₚaₚ⁻¹bₚ⁻¹c₁h₁c₁⁻¹⋯cₙhₙcₙ⁻¹`. -/
+inductive OrientableRel (p n : ℕ) : ClosedUnitDisc → ClosedUnitDisc → Prop
+  | a (x : Icc (0 : ℝ) 1) (i : Fin p) : OrientableRel p n
+      (.bdyPtOfReal <| (4 * i + x) / (4 * p + 3 * n))
+      (.bdyPtOfReal <| (4 * i + 3 - x) / (4 * p + 3 * n))
+  | b (x : Icc (0 : ℝ) 1) (i : Fin p) : OrientableRel p n
+      (.bdyPtOfReal <| (4 * i + 1 + x) / (4 * p + 3 * n))
+      (.bdyPtOfReal <| (4 * i + 4 - x) / (4 * p + 3 * n))
+  | c (x : Icc (0 : ℝ) 1) (i : Fin n) : OrientableRel p n
+      (.bdyPtOfReal <| - (3 * i + x) / (4 * p + 3 * n))
+      (.bdyPtOfReal <| - (3 * i + 3 - x) / (4 * p + 3 * n))
+
+/-- The representative non-orientable surface homeomorphic to a direct sum of `p` projective
+planes with `n` discs removed, obtained by identifying the boundary of a disc in the pattern
+`a₁a₁⋯aₚaₚc₁h₁c₁⁻¹⋯cₙhₙcₙ⁻¹`. -/
+inductive NonOrientableRel (p n : ℕ) : ClosedUnitDisc → ClosedUnitDisc → Prop
+  | a (x : Icc (0 : ℝ) 1) (i : Fin p) : NonOrientableRel p n
+      (.bdyPtOfReal <| (2 * i + x) / (2 * p + 3 * n))
+      (.bdyPtOfReal <| (2 * i + 1 + x) / (2 * p + 3 * n))
+  | c (x : Icc (0 : ℝ) 1) (i : Fin n) : NonOrientableRel p n
+      (.bdyPtOfReal <| -(3 * i + x) / (2 * p + 3 * n))
+      (.bdyPtOfReal <| -(3 * i + 3 - x) / (2 * p + 3 * n))
+
+end Surface
+
+open Set
+
+/-- A 3-dimensional handlebody of genus `g`. -/
+def handlebody (g : ℕ) : Set (ℝ × ℝ × ℝ) :=
+  Icc 0 1 ×ˢ (Icc 0 (2 * (g : ℝ) + 1) ×ˢ Icc 0 3 \ ⋃ i : Fin g, Ioo (2 * (i : ℝ) + 1) (2 * i + 2) ×ˢ Ioo 1 2)
+
+@[eval_problem]
+theorem nonempty_frontier_handlebody_homeomorph_quot_orientableRel (g : ℕ) (hg : g ≠ 0) :
+    Nonempty (frontier (handlebody g) ≃ₜ Quot (Surface.OrientableRel g 0)) := by
+  sorry
+
+end LeanEval.Topology
diff --git a/manifests/problems.toml b/manifests/problems.toml
index 0bc4664..fbd03ab 100644
--- a/manifests/problems.toml
+++ b/manifests/problems.toml
@@ -645,3 +645,11 @@ module = "LeanEval.NumberTheory.NeukirchUchida"
 holes = ["neukirch_uchida"]
 submitter = "Junyan Xu"
 source = "Jürgen Neukirch, Alexander Schmidt, Kay Wingberg. *Cohomology of Number Fields*, Theorem 12.2.1."
+
+[[problem]]
+id = "handlebody_boundary"
+title = "Boundary of a 3-dimensional handlebody"
+test = false
+module = "LeanEval.Topology.Prelude"
+holes = ["nonempty_frontier_handlebody_homeomorph_quot_orientableRel"]
+submitter = "Junyan Xu"
\ No newline at end of file

From 8c8cdf2ff4914fc0acf4d008786e9e2ee9ae62e9 Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxu.math@gmail.com>
Date: Wed, 6 May 2026 22:50:54 +0200
Subject: [PATCH 2/5] give names to representatives

---
 LeanEval/Topology/ClassificationOfSurfaces.lean | 4 ++--
 LeanEval/Topology/Prelude.lean                  | 8 ++++++--
 manifests/problems.toml                         | 2 +-
 3 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/LeanEval/Topology/ClassificationOfSurfaces.lean b/LeanEval/Topology/ClassificationOfSurfaces.lean
index 4c48861..b562123 100644
--- a/LeanEval/Topology/ClassificationOfSurfaces.lean
+++ b/LeanEval/Topology/ClassificationOfSurfaces.lean
@@ -20,8 +20,8 @@ theorem classification_of_surfaces (S : Type*) [TopologicalSpace S]
     [T2Space S] [ConnectedSpace S] [CompactSpace S]
     [ChartedSpace (EuclideanHalfSpace 2) S] :
     Nonempty (S ≃ₜ Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1) ∨
-    ∃ p n, ((1 ≤ p ∨ 1 ≤ n) ∧ Nonempty (S ≃ₜ Quot (OrientableRel p n))) ∨
-      (1 ≤ p ∧ Nonempty (S ≃ₜ Quot (NonOrientableRel p n))) := by
+    ∃ p n, ((1 ≤ p ∨ 1 ≤ n) ∧ Nonempty (S ≃ₜ OrientableRepr p n)) ∨
+      (1 ≤ p ∧ Nonempty (S ≃ₜ NonOrientableRepr p n)) := by
   sorry
 
 end LeanEval.Topology
diff --git a/LeanEval/Topology/Prelude.lean b/LeanEval/Topology/Prelude.lean
index 97ad3f6..1372847 100644
--- a/LeanEval/Topology/Prelude.lean
+++ b/LeanEval/Topology/Prelude.lean
@@ -56,6 +56,10 @@ inductive NonOrientableRel (p n : ℕ) : ClosedUnitDisc → ClosedUnitDisc → P
       (.bdyPtOfReal <| -(3 * i + x) / (2 * p + 3 * n))
       (.bdyPtOfReal <| -(3 * i + 3 - x) / (2 * p + 3 * n))
 
+abbrev OrientableRepr (p n : ℕ) := Quot (Surface.OrientableRel p n)
+
+abbrev NonOrientableRepr (p n : ℕ) := Quot (Surface.NonOrientableRel p n)
+
 end Surface
 
 open Set
@@ -65,8 +69,8 @@ def handlebody (g : ℕ) : Set (ℝ × ℝ × ℝ) :=
   Icc 0 1 ×ˢ (Icc 0 (2 * (g : ℝ) + 1) ×ˢ Icc 0 3 \ ⋃ i : Fin g, Ioo (2 * (i : ℝ) + 1) (2 * i + 2) ×ˢ Ioo 1 2)
 
 @[eval_problem]
-theorem nonempty_frontier_handlebody_homeomorph_quot_orientableRel (g : ℕ) (hg : g ≠ 0) :
-    Nonempty (frontier (handlebody g) ≃ₜ Quot (Surface.OrientableRel g 0)) := by
+theorem nonempty_frontier_handlebody_homeomorph_orientableRepr (g : ℕ) (hg : g ≠ 0) :
+    Nonempty (frontier (handlebody g) ≃ₜ Surface.OrientableRepr g 0) := by
   sorry
 
 end LeanEval.Topology
diff --git a/manifests/problems.toml b/manifests/problems.toml
index fbd03ab..1a0a74f 100644
--- a/manifests/problems.toml
+++ b/manifests/problems.toml
@@ -651,5 +651,5 @@ id = "handlebody_boundary"
 title = "Boundary of a 3-dimensional handlebody"
 test = false
 module = "LeanEval.Topology.Prelude"
-holes = ["nonempty_frontier_handlebody_homeomorph_quot_orientableRel"]
+holes = ["nonempty_frontier_handlebody_homeomorph_orientableRepr"]
 submitter = "Junyan Xu"
\ No newline at end of file

From 43fdfe866927ca6b56e092208a34dfe2a39ca95b Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxu.math@gmail.com>
Date: Wed, 6 May 2026 23:00:23 +0200
Subject: [PATCH 3/5] two more problems

---
 LeanEval/Topology/Prelude.lean | 15 +++++++++++++--
 manifests/problems.toml        | 20 ++++++++++++++++++--
 2 files changed, 31 insertions(+), 4 deletions(-)

diff --git a/LeanEval/Topology/Prelude.lean b/LeanEval/Topology/Prelude.lean
index 1372847..4b225c6 100644
--- a/LeanEval/Topology/Prelude.lean
+++ b/LeanEval/Topology/Prelude.lean
@@ -1,4 +1,5 @@
 import Mathlib.Analysis.Complex.Circle
+import Mathlib.Analysis.InnerProductSpace.PiL2
 import EvalTools.Markers
 
 /-!
@@ -69,8 +70,18 @@ def handlebody (g : ℕ) : Set (ℝ × ℝ × ℝ) :=
   Icc 0 1 ×ˢ (Icc 0 (2 * (g : ℝ) + 1) ×ˢ Icc 0 3 \ ⋃ i : Fin g, Ioo (2 * (i : ℝ) + 1) (2 * i + 2) ×ˢ Ioo 1 2)
 
 @[eval_problem]
-theorem nonempty_frontier_handlebody_homeomorph_orientableRepr (g : ℕ) (hg : g ≠ 0) :
-    Nonempty (frontier (handlebody g) ≃ₜ Surface.OrientableRepr g 0) := by
+def frontierHandlebodyHomeomorphOrientableRepr (g : ℕ) (hg : g ≠ 0) :
+    frontier (handlebody g) ≃ₜ Surface.OrientableRepr g 0 := by
+  sorry
+
+@[eval_problem]
+def frontierHandlebodyHomeomorphSphere :
+    frontier (handlebody 0) ≃ₜ Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1 := by
+  sorry
+
+@[eval_problem]
+def frontierHandlebodyHomeomorphAddCircleProd :
+    frontier (handlebody 1) ≃ₜ AddCircle (1 : ℝ) × AddCircle (1 : ℝ) := by
   sorry
 
 end LeanEval.Topology
diff --git a/manifests/problems.toml b/manifests/problems.toml
index 1a0a74f..900450e 100644
--- a/manifests/problems.toml
+++ b/manifests/problems.toml
@@ -648,8 +648,24 @@ source = "Jürgen Neukirch, Alexander Schmidt, Kay Wingberg. *Cohomology of Numb
 
 [[problem]]
 id = "handlebody_boundary"
-title = "Boundary of a 3-dimensional handlebody"
+title = "Boundary of a 3-dimensional handlebody with nonzero genus"
 test = false
 module = "LeanEval.Topology.Prelude"
-holes = ["nonempty_frontier_handlebody_homeomorph_orientableRepr"]
+holes = ["frontierHandlebodyHomeomorphOrientableRepr"]
+submitter = "Junyan Xu"
+
+[[problem]]
+id = "handlebody_boundary_sphere"
+title = "Boundary of a 3-dimensional handlebody with zero genus"
+test = false
+module = "LeanEval.Topology.Prelude"
+holes = ["frontierHandlebodyHomeomorphSphere"]
+submitter = "Junyan Xu"
+
+[[problem]]
+id = "handlebody_boundary_S1xS1"
+title = "Boundary of a 3-dimensional handlebody with genus 1"
+test = false
+module = "LeanEval.Topology.Prelude"
+holes = ["frontierHandlebodyHomeomorphAddCircleProd"]
 submitter = "Junyan Xu"
\ No newline at end of file

From 8c96ca5c98aae4a59870d96c20668f36367432c5 Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxu.math@gmail.com>
Date: Thu, 7 May 2026 00:23:15 +0200
Subject: [PATCH 4/5] add some more definitions

---
 LeanEval/Topology/Prelude.lean | 74 ++++++++++++++++++++++++++++++----
 1 file changed, 67 insertions(+), 7 deletions(-)

diff --git a/LeanEval/Topology/Prelude.lean b/LeanEval/Topology/Prelude.lean
index 4b225c6..5ca7e39 100644
--- a/LeanEval/Topology/Prelude.lean
+++ b/LeanEval/Topology/Prelude.lean
@@ -1,3 +1,6 @@
+import Mathlib.Algebra.Category.Grp.Basic
+import Mathlib.Algebra.Category.Grp.Abelian
+import Mathlib.AlgebraicTopology.SingularHomology.Basic
 import Mathlib.Analysis.Complex.Circle
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import EvalTools.Markers
@@ -5,16 +8,73 @@ import EvalTools.Markers
 /-!
 # Basic definitions in topology
 
-In this file we define a representative surface in each homeomorphism class of surfaces by
-gluing certain arcs in the boundary of the unit disc.
+## Main definitions
 
-We also define a representative 3-dimensional handlebody for each genus.
++ `singularHomology`, `bettiNumber`: the singular homology and Betti numbers of a topological
+space with coefficients in an abelian group.
+
++ `ContinuousMap.toEndSingularHomology`: the homomorphism from the monoid of continuous maps
+from a space to itself to the endomorphism monoid of one of its singular homology groups.
+
++ `Surface.OrientableRepr`, `Surface.NonOrientableRepr`: a representative surface in each
+homeomorphism class of surfaces, obtained by gluing certain arcs in the boundary of the unit disc.
+
++ `handlebody₃`: a representative 3-dimensional handlebody for each genus.
 See https://en.wikipedia.org/wiki/Handlebody#3-dimensional_handlebodies.
 
 We pose it as a LeanEval problem to show that the boundary of the handlebody is homeomorphic
 to the corresponding representative surface.
 -/
 
+section Topology
+
+variable (X : Type*) [TopologicalSpace X]
+
+instance : Monoid C(X, X) where
+  mul := .comp
+  mul_assoc _ _ _ := rfl
+  one := .id X
+  one_mul _ := rfl
+  mul_one _ := rfl
+
+instance : Group (X ≃ₜ X) where
+  mul f g := g.trans f
+  mul_assoc _ _ _ := rfl
+  one := .refl _
+  one_mul _ := rfl
+  mul_one _ := rfl
+  inv := .symm
+  inv_mul_cancel f := by ext; apply f.left_inv
+
+def Homeomorph.toContinuousMap : (X ≃ₜ X) →* C(X, X) where
+  toFun := (↑)
+  map_one' := rfl
+  map_mul' _ _ := rfl
+
+end Topology
+
+section AlgebraicTopology
+
+open AlgebraicTopology CategoryTheory
+
+universe u in
+instance : Limits.HasCoproducts.{u} AddCommGrpCat.{u} := inferInstance
+
+variable (n : ℕ) (X : Type*) [TopologicalSpace X] (G : Type) [AddCommGroup G]
+
+noncomputable abbrev singularHomology :=
+  ((singularHomologyFunctor AddCommGrpCat n).obj (.of (ULift G))).obj (.of X)
+
+noncomputable def bettiNumber : ℕ := Module.finrank ℤ <| singularHomology n X ℤ
+
+noncomputable def ContinuousMap.toEndSingularHomology :
+    C(X, X) →* AddMonoid.End (singularHomology n X G) where
+  toFun f := (((singularHomologyFunctor AddCommGrpCat n).obj _).map <| TopCat.ofHom f).hom
+  map_one' := AddCommGrpCat.ofHom_injective <| by simp; exact CategoryTheory.Functor.map_id ..
+  map_mul' _ _ := AddCommGrpCat.ofHom_injective <| by simp; exact Functor.map_comp ..
+
+end AlgebraicTopology
+
 namespace Complex
 
 /-- The closed unit disc in the complex plane. -/
@@ -66,22 +126,22 @@ end Surface
 open Set
 
 /-- A 3-dimensional handlebody of genus `g`. -/
-def handlebody (g : ℕ) : Set (ℝ × ℝ × ℝ) :=
+def handlebody₃ (g : ℕ) : Set (ℝ × ℝ × ℝ) :=
   Icc 0 1 ×ˢ (Icc 0 (2 * (g : ℝ) + 1) ×ˢ Icc 0 3 \ ⋃ i : Fin g, Ioo (2 * (i : ℝ) + 1) (2 * i + 2) ×ˢ Ioo 1 2)
 
 @[eval_problem]
 def frontierHandlebodyHomeomorphOrientableRepr (g : ℕ) (hg : g ≠ 0) :
-    frontier (handlebody g) ≃ₜ Surface.OrientableRepr g 0 := by
+    frontier (handlebody₃ g) ≃ₜ Surface.OrientableRepr g 0 := by
   sorry
 
 @[eval_problem]
 def frontierHandlebodyHomeomorphSphere :
-    frontier (handlebody 0) ≃ₜ Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1 := by
+    frontier (handlebody₃ 0) ≃ₜ Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1 := by
   sorry
 
 @[eval_problem]
 def frontierHandlebodyHomeomorphAddCircleProd :
-    frontier (handlebody 1) ≃ₜ AddCircle (1 : ℝ) × AddCircle (1 : ℝ) := by
+    frontier (handlebody₃ 1) ≃ₜ AddCircle (1 : ℝ) × AddCircle (1 : ℝ) := by
   sorry
 
 end LeanEval.Topology

From 8149bde1a7fe14ebad4a54360984809a093795d9 Mon Sep 17 00:00:00 2001
From: Junyan Xu <junyanxu.math@gmail.com>
Date: Thu, 7 May 2026 01:12:56 +0200
Subject: [PATCH 5/5] fix docstring + one more problem

---
 .../Topology/ClassificationOfSurfaces.lean    |  1 -
 LeanEval/Topology/Prelude.lean                | 22 ++++++++++++++-----
 manifests/problems.toml                       | 14 +++++++++---
 3 files changed, 27 insertions(+), 10 deletions(-)

diff --git a/LeanEval/Topology/ClassificationOfSurfaces.lean b/LeanEval/Topology/ClassificationOfSurfaces.lean
index b562123..bfecfe9 100644
--- a/LeanEval/Topology/ClassificationOfSurfaces.lean
+++ b/LeanEval/Topology/ClassificationOfSurfaces.lean
@@ -1,4 +1,3 @@
-import Mathlib.Analysis.Complex.Circle
 import Mathlib.Geometry.Manifold.Instances.Real
 import LeanEval.Topology.Prelude
 import EvalTools.Markers
diff --git a/LeanEval/Topology/Prelude.lean b/LeanEval/Topology/Prelude.lean
index 5ca7e39..8972ec1 100644
--- a/LeanEval/Topology/Prelude.lean
+++ b/LeanEval/Topology/Prelude.lean
@@ -10,8 +10,10 @@ import EvalTools.Markers
 
 ## Main definitions
 
-+ `singularHomology`, `bettiNumber`: the singular homology and Betti numbers of a topological
-space with coefficients in an abelian group.
++ `singularHomology`: the singular homology of a topological space
+with coefficients in an abelian group.
+
++ `bettiNumber`: the Betti numbers with integer coefficients of a topological space.
 
 + `ContinuousMap.toEndSingularHomology`: the homomorphism from the monoid of continuous maps
 from a space to itself to the endomorphism monoid of one of its singular homology groups.
@@ -127,21 +129,29 @@ open Set
 
 /-- A 3-dimensional handlebody of genus `g`. -/
 def handlebody₃ (g : ℕ) : Set (ℝ × ℝ × ℝ) :=
-  Icc 0 1 ×ˢ (Icc 0 (2 * (g : ℝ) + 1) ×ˢ Icc 0 3 \ ⋃ i : Fin g, Ioo (2 * (i : ℝ) + 1) (2 * i + 2) ×ˢ Ioo 1 2)
+  Icc 0 1 ×ˢ (Icc 0 (2 * (g : ℝ) + 1) ×ˢ Icc 0 3 \
+    ⋃ i : Fin g, Ioo (2 * (i : ℝ) + 1) (2 * i + 2) ×ˢ Ioo 1 2)
 
 @[eval_problem]
-def frontierHandlebodyHomeomorphOrientableRepr (g : ℕ) (hg : g ≠ 0) :
+def frontierHandlebody₃HomeomorphOrientableRepr (g : ℕ) (hg : g ≠ 0) :
     frontier (handlebody₃ g) ≃ₜ Surface.OrientableRepr g 0 := by
   sorry
 
 @[eval_problem]
-def frontierHandlebodyHomeomorphSphere :
+def frontierHandlebody₃HomeomorphSphere :
     frontier (handlebody₃ 0) ≃ₜ Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1 := by
   sorry
 
 @[eval_problem]
-def frontierHandlebodyHomeomorphAddCircleProd :
+def frontierHandlebody₃HomeomorphAddCircleProd :
     frontier (handlebody₃ 1) ≃ₜ AddCircle (1 : ℝ) × AddCircle (1 : ℝ) := by
   sorry
 
+/-- The complement of our handlebody in ℝ³ is homeomorphic to the interior of a handlebody
+with a point removed. -/
+@[eval_problem]
+def complHandelbody₃Homeomorph (g : ℕ) :
+    ↥(handlebody₃ g)ᶜ ≃ₜ ↥(interior (handlebody₃ g) \ {(0.5, 0.5, 1.5)}) := by
+  sorry
+
 end LeanEval.Topology
diff --git a/manifests/problems.toml b/manifests/problems.toml
index 900450e..83072a2 100644
--- a/manifests/problems.toml
+++ b/manifests/problems.toml
@@ -651,7 +651,7 @@ id = "handlebody_boundary"
 title = "Boundary of a 3-dimensional handlebody with nonzero genus"
 test = false
 module = "LeanEval.Topology.Prelude"
-holes = ["frontierHandlebodyHomeomorphOrientableRepr"]
+holes = ["frontierHandlebody₃HomeomorphOrientableRepr"]
 submitter = "Junyan Xu"
 
 [[problem]]
@@ -659,7 +659,7 @@ id = "handlebody_boundary_sphere"
 title = "Boundary of a 3-dimensional handlebody with zero genus"
 test = false
 module = "LeanEval.Topology.Prelude"
-holes = ["frontierHandlebodyHomeomorphSphere"]
+holes = ["frontierHandlebody₃HomeomorphSphere"]
 submitter = "Junyan Xu"
 
 [[problem]]
@@ -667,5 +667,13 @@ id = "handlebody_boundary_S1xS1"
 title = "Boundary of a 3-dimensional handlebody with genus 1"
 test = false
 module = "LeanEval.Topology.Prelude"
-holes = ["frontierHandlebodyHomeomorphAddCircleProd"]
+holes = ["frontierHandlebody₃HomeomorphAddCircleProd"]
+submitter = "Junyan Xu"
+
+[[problem]]
+id = "complHandelbodyHomeomorph"
+title = "The complement of a 3-dimensional handlebody"
+test = false
+module = "LeanEval.Topology.Prelude"
+holes = ["complHandelbody₃Homeomorph"]
 submitter = "Junyan Xu"
\ No newline at end of file