Quasivarieties of groups

StructureQuasi-identities of groups#✓fully proved

A quasi-identity in \(n\) unknowns \(x_0, \dots, x_{n-1}\) is a formula \(\forall x\,(w_1 = 1 \wedge \dots \wedge w_k = 1 \to w = 1)\), given by the number \(n\), a finite list of premises \(w_1, \dots, w_k\) and a conclusion \(w\), all of them elements of the free group on \(x_0, \dots, x_{n-1}\).

structure QuasiIdentity where
  /-- The number of unknowns. -/
  n : ℕ
  /-- The premises `w₁, …, wₖ`. -/
  premises : List (FreeGroup (Fin n))
  /-- The conclusion `w`. -/
  conclusion : FreeGroup (Fin n)

Used by 8

Used byIndependent basis of quasi-identities · Consequence of a set of quasi-identities · Budkin's problem on maximal subquasivarieties (Kourovka 14.25) · Quasi-identities holding in a group · Maximal proper subquasivarieties · The quasivariety defined by a set of quasi-identities · The quasi-identities of a group · Inclusion of quasivarieties

DefinitionQuasi-identities holding in a group#✓fully proved

A quasi-identity \(\forall x\,(w_1 = 1 \wedge \dots \wedge w_k = 1 \to w = 1)\) in the unknowns \(x_0, \dots, x_{n-1}\) holds in a group \(G\) when every assignment of elements of \(G\) to the unknowns under which each premise \(w_1, \dots, w_k\) evaluates to \(1\) in \(G\) also makes the conclusion \(w\) evaluate to \(1\).

def QuasiIdentity.HoldsIn (q : QuasiIdentity) (G : Type*) [Group G] : Prop :=
  ∀ x : Fin q.n → G, (∀ w ∈ q.premises, FreeGroup.lift x w = 1) →
    FreeGroup.lift x q.conclusion = 1

Uses 1 · Used by 4

Statement usesQuasi-identities of groups

Used byIndependent basis of quasi-identities · Consequence of a set of quasi-identities · The quasivariety defined by a set of quasi-identities · The quasi-identities of a group

DefinitionThe quasivariety defined by a set of quasi-identities#✓fully proved

For a set \(Q\) of quasi-identities, a group \(H\) belongs to the quasivariety defined by \(Q\) when every quasi-identity in \(Q\) holds in \(H\). Every quasivariety of groups has this form.

Only groups in the lowest universe are considered; a quasivariety is determined by its countable members.

def Models (Q : Set QuasiIdentity) (H : Type) [Group H] : Prop :=
  ∀ q ∈ Q, q.HoldsIn H

Uses 2 · Used by 2

Statement usesQuasi-identities of groups · Quasi-identities holding in a group

Used byConsequence of a set of quasi-identities · Inclusion of quasivarieties

DefinitionThe quasi-identities of a group#✓fully proved

The quasi-theory of a group \(G\) is the set of all quasi-identities that hold in \(G\). The quasivariety defined by this set is the quasivariety \(qG\) generated by \(G\).

def quasiTheory (G : Type) [Group G] : Set QuasiIdentity :=
  {q | q.HoldsIn G}

Uses 2 · Used by 1

Statement usesQuasi-identities of groups · Quasi-identities holding in a group

Used byMaximal proper subquasivarieties

DefinitionInclusion of quasivarieties#✓fully proved

For sets \(Q_1\) and \(Q_2\) of quasi-identities, the quasivariety defined by \(Q_1\) is contained in the quasivariety defined by \(Q_2\): every group in which all quasi-identities of \(Q_1\) hold also satisfies all quasi-identities of \(Q_2\).

Only groups in the lowest universe are considered; a quasivariety is determined by its countable members.

def QVLe (Q₁ Q₂ : Set QuasiIdentity) : Prop :=
  ∀ (H : Type) [Group H], Models Q₁ H → Models Q₂ H

Uses 2 · Used by 2

Statement usesThe quasivariety defined by a set of quasi-identities · Quasi-identities of groups

Used byBudkin's problem on maximal subquasivarieties (Kourovka 14.25) · Maximal proper subquasivarieties

DefinitionMaximal proper subquasivarieties#✓fully proved

Let \(G\) be a group and let \(qG\) be the quasivariety generated by \(G\), that is, the quasivariety defined by the set of all quasi-identities that hold in \(G\). A set \(Q\) of quasi-identities defines a maximal proper subquasivariety of \(qG\) when the quasivariety defined by \(Q\) is contained in \(qG\) but does not contain \(qG\), and every quasivariety \(V\) defined by a set of quasi-identities with \(V\) containing the quasivariety defined by \(Q\) and contained in \(qG\) either is contained in the quasivariety defined by \(Q\) or contains \(qG\).

def IsMaximalProperSubquasivariety (G : Type) [Group G] (Q : Set QuasiIdentity) : Prop :=
  QVLe Q (quasiTheory G) ∧ ¬ QVLe (quasiTheory G) Q ∧
    ∀ Q' : Set QuasiIdentity, QVLe Q Q' → QVLe Q' (quasiTheory G) →
      QVLe Q' Q ∨ QVLe (quasiTheory G) Q'

Uses 3 · Used by 1

Statement usesInclusion of quasivarieties · Quasi-identities of groups · The quasi-identities of a group

Used byBudkin's problem on maximal subquasivarieties (Kourovka 14.25)

DefinitionBudkin's problem on maximal subquasivarieties (Kourovka 14.25)#✓fully proved

The statement that there is a finitely generated group \(G\) such that the quasivariety \(qG\) generated by \(G\) has infinitely many maximal proper subquasivarieties: for every natural number \(k\) there are sets of quasi-identities \(Q_0, \dots, Q_{k-1}\), each defining a maximal proper subquasivariety of \(qG\), such that for \(i \ne j\) the quasivarieties defined by \(Q_i\) and \(Q_j\) are different.

def finitelyGeneratedGroupInfinitelyManyMaximalSubquasivarieties : Prop :=
  ∃ (G : Type) (_ : Group G), Group.FG G ∧
    ∀ k : ℕ, ∃ Q : Fin k → Set QuasiIdentity, (∀ i, IsMaximalProperSubquasivariety G (Q i)) ∧
      ∀ i j, i ≠ j → ¬ (QVLe (Q i) (Q j) ∧ QVLe (Q j) (Q i))

Uses 3 · Used by 1

Statement usesMaximal proper subquasivarieties · Inclusion of quasivarieties · Quasi-identities of groups

Used bySome finitely generated group has infinitely many maximal subquasivarieties

TheoremSome finitely generated group has infinitely many maximal subquasivarieties#●ready to prove

There is a finitely generated group \(G\) such that the quasivariety \(qG\) generated by \(G\) has infinitely many maximal proper subquasivarieties: for every natural number \(k\) there are sets of quasi-identities \(Q_0, \dots, Q_{k-1}\), each defining a maximal proper subquasivariety of \(qG\), such that for \(i \ne j\) the quasivarieties defined by \(Q_i\) and \(Q_j\) are different.

This answers Kourovka Problem 14.25 positively; the answer is due to Bludov.

public theorem_wanted finitelyGeneratedGroupInfinitelyManyMaximalSubquasivarieties_holds :
    finitelyGeneratedGroupInfinitelyManyMaximalSubquasivarieties

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 14.25 (A. I. Budkin); resolution: V. V. Bludov, Algebra and Logic 41 (2002), no. 1, 1-8, Kourovka Archive, Problem 14.25 (answer: Yes, it is).

Uses 1

Statement usesBudkin's problem on maximal subquasivarieties (Kourovka 14.25)

7 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.