Kourovka 1.86

### What is the conjecture

> **"Is it true that the identical relations of a polycyclic group have a finite basis?"**

### Status of the Problem
Based on the most recent editions of the Kourovka Notebook (including the 19th edition in 2018 and the description of the 21st edition slated for 2026), this problem appears to remain **unsolved (open)**.

* It is one of the few remaining unsolved problems from the very first issue of the Kourovka Notebook (1965).
* While the **Finite Basis Property** (having a finite basis of identities) has been proven for several related classes of groups, the specific case for **polycyclic groups** is not settled in the general case.

### Related Results Discussed in Research
The problem is discussed in research papers concerning the **identities of solvable groups** and the **finite basis property**. Key related results include:
1. **Finite Groups:** Oates and Powell (1964) proved that the identities of any finite group have a finite basis.
2. **Nilpotent Groups:** Lyndon (1952) proved that the identities of a nilpotent group have a finite basis.
3. **Metabelian Groups:** D. E. Cohen (1967) proved that the identities of a metabelian group have a finite basis (solving Shmel'kin's Problem 1.85).
4. **Solvable Groups:** In contrast, it is known that solvable groups in general do **not** necessarily have a finite basis of identities (counterexamples were found by Yu. A. Bakhturin, A. Yu. Ol'shanskii, and M. R. Vaughan-Lee).
5. **Matrix Groups:** Shmel'kin also posed the related Problem 1.87: "The same question for matrix groups (at least over a field of characteristic 0)." Since polycyclic groups are linear over $\mathbb{Z}$ (and thus over fields of characteristic 0), a positive answer to 1.87 would imply a positive answer to 1.86.

Because polycyclic groups are solvable and satisfy the maximal condition on subgroups (Max), they are "close" to the classes known to have a finite basis, but the property has not been successfully proven for the entire class, nor has a counterexample been found.

### Prerequisites needed
To state the problem **"Is it true that the identical relations of a polycyclic group have a finite basis?"** in Lean 4, the following definitions and structures are currently missing or require construction from primitive components in Mathlib:

### 1. Polycyclic Groups
While Mathlib has `IsSolvable` and `IsNilpotent`, it does not yet appear to have a specific typeclass or predicate for **polycyclic groups**.
* **Missing Definition**: `IsPolycyclic` (or `PolycyclicGroup`).
* **Structure Needed**: A definition stating that a group $G$ has a subnormal series $1 = G_0 \lhd G_1 \lhd \dots \lhd G_n = G$ such that each factor $G_{i+1}/G_i$ is a cyclic group. (Existing `SubnormalSeries` API could be used to define this).

### 2. Group Laws (Identities)
Mathlib has `FreeGroup`, but the specific machinery for **identities** (laws) and **varieties of groups** is likely missing.
* **Missing Definition**: The concept of a word $w$ in a free group of countable rank (e.g., `FreeGroup ℕ`) being an **identity** (or law) in a group $G$.
* *Formalization*: $w$ is an identity of $G$ if for every homomorphism $\phi: \text{FreeGroup } \mathbb{N} \to G$, $\phi(w) = 1$.
* **Missing Structure**: The set of all identities of a group, typically denoted $Id(G)$.

### 3. Verbal Subgroups and Consequences
To define a "basis," you need the notion of logical consequence for identities.
* **Missing Definition**: **Verbal Subgroup**. The subgroup of a free group generated by all endomorphic images of a set of words.
* **Missing Definition**: **Fully Invariant Subgroup**. A subgroup mapped into itself by every endomorphism of the group. (The set of identities $Id(G)$ is a fully invariant subgroup of the free group).
* **Missing Definition**: The **closure** of a set of identities. A word $u$ is a consequence of a set of words $W$ if $u$ belongs to the fully invariant subgroup generated by $W$.

### 4. Finite Basis Property
Finally, the question asks about a *finite basis*.
* **Missing Definition**: **Finite Basis of Identities**. A group $G$ has a finite basis of identities if there exists a **finite** set of words $B \subset \text{FreeGroup } \mathbb{N}$ such that the set of all identities of $G$ is exactly the fully invariant closure of $B$.

### Summary of Missing Identifiers
To state the question, you would effectively need to define:
```lean
def IsPolycyclic (G : Type*) [Group G] : Prop := ...

def IsIdentity (w : FreeGroup ℕ) (G : Type*) [Group G] : Prop :=
∀ φ : FreeGroup ℕ →* G, φ w = 1

def IsBasisForIdentities (B : Set (FreeGroup ℕ)) (G : Type*) [Group G] : Prop :=
-- The set of identities of G is the fully invariant closure of B
...

def HasFiniteBasisOfIdentities (G : Type*) [Group G] : Prop :=
∃ B : Finset (FreeGroup ℕ), IsBasisForIdentities B G
```
None of these specific definitions (`IsPolycyclic`, `IsIdentity`, `HasFiniteBasisOfIdentities`) are currently standard parts of Mathlib.

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

* ams-16

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