From f57d0723f01928b06fea1884c71345a8f0d56b18 Mon Sep 17 00:00:00 2001
From: Vlad Tsyrklevich <vlad@tsyrklevi.ch>
Date: Wed, 29 Jul 2026 18:02:35 +0200
Subject: [PATCH] feat(Topology): First singular homology group of the Hawaiian
 earring.

---
 .../Topology/HawaiianEarringHomology.lean     | 33 +++++++++++++++++++
 ...ng_first_singularHomology_isomorphism.toml |  7 ++++
 2 files changed, 40 insertions(+)
 create mode 100644 LeanEval/Topology/HawaiianEarringHomology.lean
 create mode 100644 manifests/problems/hawaiian_earring_first_singularHomology_isomorphism.toml

diff --git a/LeanEval/Topology/HawaiianEarringHomology.lean b/LeanEval/Topology/HawaiianEarringHomology.lean
new file mode 100644
index 00000000..1ee2f43f
--- /dev/null
+++ b/LeanEval/Topology/HawaiianEarringHomology.lean
@@ -0,0 +1,33 @@
+import Mathlib.Algebra.Category.Grp.Abelian
+import Mathlib.AlgebraicTopology.SingularHomology.Basic
+
+namespace LeanEval.Topology
+
+open AlgebraicTopology
+
+/-!
+First singular homology group of the Hawaiian earring.
+
+Theorem 3.1 of K. Eda and K. Kawamura's paper "The singular homology of the Hawaiian earring"
+computes the first singular homology group of the Hawaiian earring.
+This is isomorphic to the version given below using the isomorphism given in S. Balcerzyk
+"On factor groups of some subgroups of a complete direct sum of infinite cyclic groups".
+-/
+
+/-- The Hawaiian earring as a subset of `ℝ²`. -/
+def HawaiianEarring : Set (ℝ × ℝ) :=
+  ⋃ n : ℕ, {p | (p.1 - 1 / (n + 1 : ℝ)) ^ 2 + p.2 ^ 2 = (1 / (n + 1 : ℝ)) ^ 2}
+
+/-- The direct sum `⊕ i : ℕ, ℤ` embedded in the product `∏ i : ℕ, ℤ`. -/
+noncomputable abbrev directSum : AddSubgroup (ℕ → ℤ) :=
+  (Finsupp.coeFnAddHom (ι := ℕ) (M := ℤ)).range
+
+/-- The first singular homology group of the Hawaiian earring is isomorphic to
+`(∏ i : ℕ, ℤ) × (∏ i : ℕ, ℤ / ⊕ i : ℕ, ℤ)` -/
+@[eval_problem]
+theorem hawaiian_earring_first_singularHomology_isomorphism :
+  Nonempty ((singularHomologyFunctor Ab 1 |>.obj (.of ℤ) |>.obj <| .of HawaiianEarring) ≃+
+    (ℕ → ℤ) × ((ℕ → ℤ) ⧸ directSum)) := by
+  sorry
+
+end LeanEval.Topology
diff --git a/manifests/problems/hawaiian_earring_first_singularHomology_isomorphism.toml b/manifests/problems/hawaiian_earring_first_singularHomology_isomorphism.toml
new file mode 100644
index 00000000..f78d4ab4
--- /dev/null
+++ b/manifests/problems/hawaiian_earring_first_singularHomology_isomorphism.toml
@@ -0,0 +1,7 @@
+id = "hawaiian_earring_first_singularHomology_isomorphism"
+title = "First singular homology group of the Hawaiian Earring"
+test = false
+module = "LeanEval.Topology.HawaiianEarringHomology"
+holes = ["hawaiian_earring_first_singularHomology_isomorphism"]
+submitter = "Vlad Tsyrklevich"
+source = "K. Eda, K. Kawamura, *The singular homology of the Hawaiian earring*"