Kourovka 1.74 - Abelian Examples

### What is the conjecture
Is every abelian minimal topological group isomorphic to a dense subgroup of $\mathbb{R}$ or $\mathbb{T}$? (This essentially asks if the rank 1 abelian groups are the only abelian examples).

This is one of the questions to answer to resolve **Problem 1.74** from the **Kourovka Notebook** (Unsolved Problems in Group Theory), proposed by **V. P. Platonov** in the 1st edition (1965):
**"Describe all minimal topological groups, that is, non-discrete groups all of whose closed subgroups are discrete."**

* **Terminology Note:** The term "minimal topological group" in this problem is defined specifically as *a non-discrete group having no proper non-discrete closed subgroups*. This should not be confused with the more common modern definition of "minimal topological groups" (attributed to R.M. Stephenson), which refers to groups whose topology is minimal among all Hausdorff group topologies. To avoid confusion, these are sometimes referred to as **Platonov minimal groups** or **groups with discrete closed subgroups**.

### Prerequisites needed (by Gemini)
Based on the current state of **Mathlib (Lean 4)**, **no definitions or structures are missing** to state this specific question.

You can formalize the question using existing structures for real numbers ($\mathbb{R}$), the circle group ($\mathbb{T}$), subgroups, and topological equivalence.

### Choice of Notation (Additive vs. Multiplicative)
There is a minor technical choice to make regarding notation:
* **$\mathbb{R}$** is defined in Lean as a `Ring`, but its group structure is an **additive group** (you add real numbers, you don't multiply them to form a group).
* **$\mathbb{T}$** (the circle group) can be defined multiplicatively (as unit complex numbers) or additively (as $\mathbb{R}/\mathbb{Z}$).

To state the question cleanly in a single boolean expression without mixing notations, it is best to treat the abstract group $G$ as an **Additive Abelian Group** (`AddCommGroup`). This matches the native structure of $\mathbb{R}$.

### The Formal Statement in Lean 4

Here is how you can state the question: *"Is every abelian Platonov minimal group isomorphic to a dense subgroup of $\mathbb{R}$ or $\mathbb{T}$?"*

```lean
import Mathlib.Topology.Algebra.Group.Basic
import Mathlib.Topology.Instances.AddCircle
import Mathlib.Topology.Instances.Real
import Mathlib.GroupTheory.Subgroup.Basic

-- 1. Redefine Platonov Minimal Group for the Additive case
-- (Previous definition was generic/multiplicative; we need AddCommGroup for compatibility with ℝ)
def IsPlatonovMinimalAddGroup
(G : Type*) [AddCommGroup G] [TopologicalSpace G] : Prop :=
TopologicalAddGroup G ∧
T2Space G ∧
¬ DiscreteTopology G ∧
∀ (H : AddSubgroup G), IsClosed (H : Set G) → H ≠ ⊤ → DiscreteTopology H

-- 2. Define "Isomorphic as a Topological Group"
-- We say G is iso to H if there exists an Additive Equivalence that is also a Homeomorphism.
def IsTopologicalAddGroupIso {G H : Type*}
[AddCommGroup G] [TopologicalSpace G]
[AddCommGroup H] [TopologicalSpace H] (f : G ≃+ H) : Prop :=
Continuous f ∧ Continuous f.symm

-- 3. The Statement of the Problem
def AbelianMinimalProblemStatement : Prop :=
∀ (G : Type*) [AddCommGroup G] [TopologicalSpace G],
IsPlatonovMinimalAddGroup G →
(
-- Case 1: Isomorphic to a dense subgroup of ℝ
(∃ (S : AddSubgroup ℝ), Dense (S : Set ℝ) ∧
∃ (f : G ≃+ S), IsTopologicalAddGroupIso f)
∨
-- Case 2: Isomorphic to a dense subgroup of 𝕋 (represented as ℝ/ℤ)
(∃ (S : AddSubgroup (AddCircle (1 : ℝ))), Dense (S : Set (AddCircle (1 : ℝ))) ∧
∃ (f : G ≃+ S), IsTopologicalAddGroupIso f)
)
```

### Explanation of Used Structures
* **`AddCommGroup`**: Specifies that $G$ is an abelian group using additive notation ($+$), allowing direct comparison with $\mathbb{R}$.
* **`AddSubgroup \R`**: Represents a subgroup of the real numbers.
* **`AddCircle (1 : \R)`**: This is the Lean definition for the torus/circle group $\mathbb{R}/\mathbb{Z}$ (where the period is 1). It is a topological group by definition.
* **`Dense`**: A standard predicate in Mathlib (`Topology.Basic`) stating that the closure of a set is the whole space.
* **`≃+` (AddEquiv)**: Represents an algebraic isomorphism between two additive groups. We combine this with `Continuous` to ensure it is a topological isomorphism.

### Are "Rank 1" definitions missing?
The prompt mentions that the problem "essentially asks if the rank 1 abelian groups are the only examples."
* You **do not** need a formal definition of "Rank 1" to state the problem as asking about embeddings into $\mathbb{R}$ or $\mathbb{T}$.
* However, if you specifically wanted to state the theorem in terms of the abstract concept of Rank (e.g., "Every minimal group has Rank 1"), Mathlib does have `Module.rank`, but the phrasing using embeddings into $\mathbb{R}$ and $\mathbb{T}$ (as done above) is more concrete and standard for topological group classification.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-22

### Choose either option
- [ ] I plan on adding this conjecture to the repository
- [X] This issue is up for grabs: I would like to see this conjecture added by somebody else