Kourovka 1.74 - Existence of Non-Abelian Examples

### What is the conjecture
Does there exist a non-abelian topological group $G$ which is non-discrete and Hausdorff, such that every proper closed subgroup of $G$ is discrete?

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**.
* **Locally Compact Case:** As the problem statement notes, the classification in the locally compact case is straightforward. The only locally compact examples are the **circle group $\mathbb{T}$** (isomorphic to $\mathbb{R}/\mathbb{Z}$) and the **real line $\mathbb{R}$**. (Proof sketch: Totally disconnected locally compact groups have compact open subgroups, which would be non-discrete proper closed subgroups unless the group is discrete. Connected locally compact groups are limits of Lie groups; if the dimension is $>1$, they contain proper 1-parameter subgroups. Thus, only 1-dimensional connected groups remain).

### Discussion in Research
The problem is discussed in the context of topological group theory, specifically regarding **groups with no small subgroups (NSS)** and the structure of subgroups of topological groups.
* **General Case Complexity:** The "general case" (non-locally compact) is complicated because it includes all **dense subgroups of $\mathbb{R}$ and $\mathbb{T}$** (e.g., the rational numbers $\mathbb{Q}$ with the subspace topology). In such groups, any proper closed subgroup is the intersection of the group with a closed subgroup of $\mathbb{R}$ (which is either $\mathbb{R}$, $\{0\}$, or discrete $a\mathbb{Z}$), resulting in a discrete subgroup.
* **Potential Non-Abelian Examples:** A major open sub-problem is whether there exist **non-abelian** minimal topological groups. This is related to the existence of **topologizable Tarski monsters** (infinite groups where every proper subgroup is finite). If a Tarski monster admits a non-discrete Hausdorff group topology, it would be a minimal topological group because all its proper subgroups (being finite) would be discrete. The existence of such topologies is a subject of research in "topologizability of infinite groups" (involving work by Olshanskii, Klyachko, etc.).

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

All the necessary mathematical components—topological groups, subgroups, separation axioms (Hausdorff), and the discrete topology—are foundational parts of Mathlib.

Here is how you can formally state the question in Lean 4 right now.

### The Formal Statement in Lean 4

```lean
import Mathlib.Topology.Algebra.Group.Basic
import Mathlib.Topology.Separation
import Mathlib.GroupTheory.Subgroup.Basic

/--
Platonov's definition of a minimal topological group:
A non-discrete group where every closed proper subgroup is discrete.
-/
def IsPlatonovMinimalGroup
(G : Type*) [Group G] [TopologicalSpace G] : Prop :=
-- 1. It is a Topological Group (compatibility)
TopologicalGroup G ∧
-- 2. It is Hausdorff
T2Space G ∧
-- 3. It is not discrete itself
¬ DiscreteTopology G ∧
-- 4. Condition on subgroups
∀ (H : Subgroup G), IsClosed (H : Set G) → H ≠ ⊤ → DiscreteTopology H

/--
The Formal Question: Does there exist a non-abelian Platonov minimal group?
-/
def PlatonovProblemStatement : Prop :=
∃ (G : Type*)
(grp : Group G)
(top : TopologicalSpace G),
IsPlatonovMinimalGroup G ∧ ¬ (∀ x y : G, x * y = y * x)
```

### Breakdown of Existing Definitions Used
You can define this immediately because the following structures are already in Mathlib:

1. **`TopologicalGroup G`**: Available in `Mathlib.Topology.Algebra.Group.Basic`. This handles the continuity of multiplication and inversion.
2. **`Subgroup G`**: Available in `Mathlib.GroupTheory.Subgroup.Basic`. Mathlib treats subgroups as bundled terms.
3. **`IsClosed`**: Standard topology definition. Note that `H` (a subgroup) coerces to a `Set G` automatically, allowing you to apply topological predicates to algebraic structures.
4. **`DiscreteTopology`**: This is a typeclass on a topological space.
* *Crucial Detail:* When we write `DiscreteTopology H` where `H` is a subgroup, Lean automatically treats `H` as a subtype (`↥H`), infers the **subspace topology** from `G`, and then asks if that induced topology is discrete. This logic is fully implemented.
5. **`⊤` (Top)**: The lattice of subgroups is complete. `H ≠ ⊤` is the standard way to state "H is a proper subgroup" (i.e., $H \neq G$).

### Summary
The concept of "Minimal Topological Group" (in Platonov's sense) is not pre-bundled as a single definition in Mathlib, but the logic required to construct it is fully available.

### [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