Kourovka 2.9

### What is the conjecture
> Do there exist regular associative operations on the class of groups satisfying the weakened Mal’cev condition (that is, monomorphisms of the factors of an arbitrary product can be glued together, generally speaking, into a homomorphism of the whole product), but not satisfying the analogous condition for epimorphisms of the factors?

The concepts and the specific problem are discussed in mathematical literature outside of the Kourovka Notebook, primarily in the field of **group operations** and **polyverbal operations**.

Here are the key places where this is discussed:

1. **O. N. Golovin's Papers:**
* The problem stems directly from Golovin's foundational work on "regular products" (regular operations). He introduced the theory of **regular associative operations** (which include the direct product and free product as special cases) in a series of papers in the 1960s.
* Specific papers include "Polyverbal operations" (*Trudy Moskov. Mat. Obshch.*) and "The axioms of regular operations". In these works, he defines the "Mal'cev postulates" (related to the gluing of homomorphisms) and the "associativity postulate".

2. **S. V. Ivanov's Work:**
* The area received significant attention from **S. V. Ivanov**. For instance, Ivanov solved the closely related **Problem 2.8** (also by Golovin) in his 1993 paper *"On regular associative operations on groups"* (*Trans. Moscow Math. Soc.*). In that paper, he proved the existence of regular associative operations with the "heredity property," answering Golovin's question affirmatively. This paper discusses the general framework of Golovin's operations and the Mal'cev conditions.

3. **Literature on Polyverbal Operations:**
* The problem is part of the broader study of **neutral polyverbal operations**. Papers by researchers such as **A. L. Shmel'kin**, **S. Moran**, and **O. N. Golovin** discuss the properties of these operations, specifically whether they satisfy the Mal'cev condition (gluing of homomorphisms).
* For example, it is known that for nontrivial verbal operations, the full Mal'cev postulate often does not hold, which motivates the question about the "weakened" version (monomorphisms only).

The theoretical machinery to address it exists in the works of Ivanov and Ol'shanskii.

### Prerequisites needed
To state **Problem 2.9 (Golovin)** from the Kourovka Notebook in Lean 4, you do not need new foundational mathematics (Mathlib already has advanced Category Theory and Group Theory). However, you are missing the **specific domain-specific definitions** introduced by O. N. Golovin in the 1960s regarding "Regular Operations."

Mathlib does not have a bundled definition for a "Regular Associative Operation." To state the problem, you would first need to define a structure representing such an operation.

Here are the specific definitions and structures missing from `Mathlib` that you would need to implement to state the question:

### 1. The Structure of a "Group Operation"
Mathlib has `FreeProduct` and `Pi` (Direct Product), but it does not have an abstract type representing "An arbitrary operation on the class of groups."

You would need to define a structure that maps a family of groups to a resulting group.
* **Missing Definition:** A type representing a function $\Pi^\circ$ that takes an index type $\iota$ and a family of groups $G : \iota \to \text{Group}$, returning a single `Group`.
* *Lean signature conceptualization:*
`def GroupOperation := ∀ {ι : Type u} (G : ι → GroupCat.{u}), GroupCat.{u}`

### 2. The Axioms of "Regularity"
Golovin defined a product to be "regular" if it satisfies specific conditions regarding how the factors sit inside the product. These are not standard predicates in Mathlib.

* **Missing Structure:** A predicate or structure `IsRegular` on a `GroupOperation`. This must postulate:
1. **Embeddings:** Existence of canonical monomorphisms $\sigma_i: G_i \to \Pi^\circ(G)$.
2. **Generation:** The product $\Pi^\circ(G)$ is generated by the images of these embeddings.
3. **Regular Intersection (The "Mal'cev" intersection property):** The intersection of one factor with the normal closure of the others is trivial. (Note: This specific intersection axiom differentiates regular products from arbitrary functors).

### 3. The Definition of "Associativity" for Operations
While Mathlib has `IsAssociative` for algebraic operations (like `a * b`), it does not have a pre-baked definition for the associativity of a **class operation**.

* **Missing Definition:** You need to define what it means for the operation to be associative.
* This requires stating that for a nested family of groups, there is a natural isomorphism: $\Pi^\circ_{j}(\Pi^\circ_{k} G_{jk}) \cong \Pi^\circ_{j,k} (G_{jk})$.

### 4. The Mal'cev Conditions (Functoriality)
The core of the problem compares "Weakened Mal'cev" (monomorphisms) vs "Epimorphism" conditions. In modern terms, this asks about the **functoriality** of the operation restricted to specific subcategories.

* **Missing Predicate (Weakened Mal'cev):** A definition stating that the operation defines a functor on the category of groups where morphisms are restricted to **Monomorphisms**.
* *Requirement:* If $\phi_i: G_i \hookrightarrow H_i$ are monomorphisms, there exists a homomorphism $\Phi: \Pi^\circ(G) \to \Pi^\circ(H)$ making the diagram commute.
* **Missing Predicate (Epimorphism Condition):** The analogous definition where $\phi_i$ are restricted to **Epimorphisms**.

### Summary of Lean 4 Implementation Needs

To state the question, you would need to author a file roughly containing the following conceptual code (which implies the missing structures):

```lean
import Mathlib.Algebra.Category.GroupCat.Basic
import Mathlib.Algebra.Category.GroupCat.Adjunctions

-- 1. Missing Structure: Abstract Group Operation
structure GroupOperation (u : Level) :=
(obj : ∀ {ι : Type u} (G : ι → GroupCat.{u}), GroupCat.{u})
-- 2. Missing Structure: Canonical Embeddings (Part of Regularity)
(ι : ∀ {ι : Type u} (G : ι → GroupCat.{u}) (i : ι), G i ⟶ obj G)

-- 3. Missing Definition: Regularity Predicate
def IsRegular (op : GroupOperation u) : Prop :=
-- (A) Embeddings are injective
-- (B) Images generate the group
-- (C) Trivial intersection condition (Golovin's Regularity axiom)
sorry

-- 4. Missing Definition: Associativity for Operations
def IsAssociative (op : GroupOperation u) : Prop :=
-- Existence of Natural Isomorphism between (A op B) op C and A op (B op C)
sorry

-- 5. Missing Definition: Weakened Mal'cev (Functoriality on Monos)
def SatisfiesWeakMalcev (op : GroupOperation u) : Prop :=
∀ {ι : Type u} (G H : ι → GroupCat.{u}) (f : ∀ i, G i ⟶ H i),
(∀ i, Mono (f i)) →
∃ (F : op.obj G ⟶ op.obj H), ∀ i, op.ι G i ≫ F = f i ≫ op.ι H i

-- 6. Missing Definition: Epimorphism Condition
def SatisfiesEpiMalcev (op : GroupOperation u) : Prop :=
∀ {ι : Type u} (G H : ι → GroupCat.{u}) (f : ∀ i, G i ⟶ H i),
(∀ i, Epi (f i)) →
∃ (F : op.obj G ⟶ op.obj H), ∀ i, op.ι G i ≫ F = f i ≫ op.ι H i
```

**The Missing Question:**
"Does there exist a `op : GroupOperation` such that `IsRegular op`, `IsAssociative op`, `SatisfiesWeakMalcev op` is true, but `SatisfiesEpiMalcev op` is false?"

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

* ams-20

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