Lattices of quasivarieties

DefinitionQuasivariety generated by a finite group#✓fully proved

For a group \(K\), a group \(X\) lies in the class \(Q(K)\) when \(X\) embeds in a direct power of \(K\): there are a set \(I\) and an injective homomorphism \(X \to K^I\).

For a finite group \(K\), the only case used, \(Q(K)\) is the quasivariety generated by \(K\), since ultrapowers of a finite group are isomorphic to it.

def InQuasivariety (K : Type) [Group K] (X : Type) [Group X] : Prop :=
  ∃ (I : Type) (f : X →* (I → K)), Function.Injective f

Used by 1

Used byKourovka Problem 10.9 (Budkin): quasivarieties generated by finite \(p\)-groups form a sublattice

DefinitionJoin of the quasivarieties generated by two finite groups#✓fully proved

For groups \(G\) and \(H\), a group \(X\) lies in the class \(Q(G, H)\) when \(X\) embeds in the product of a direct power of \(G\) and a direct power of \(H\): there are sets \(I\) and \(J\) and an injective homomorphism \(X \to G^I \times H^J\).

For finite groups \(G\) and \(H\), \(Q(G, H)\) is the join of the quasivarieties generated by \(G\) and by \(H\), that is, the quasivariety generated by both.

def InQuasivarietyJoin (G H : Type) [Group G] [Group H] (X : Type) [Group X] : Prop :=
  ∃ (I J : Type) (f : X →* (I → G) × (J → H)), Function.Injective f

Used by 1

Used byKourovka Problem 10.9 (Budkin): quasivarieties generated by finite \(p\)-groups form a sublattice

DefinitionKourovka Problem 10.9 (Budkin): quasivarieties generated by finite \(p\)-groups form a sublattice#✓fully proved

Kourovka Problem 10.9 (Budkin): quasivarieties generated by finite \(p\)-groups form a sublattice. For every prime \(p\) and all finite \(p\)-groups \(G\) and \(H\), there is a finite \(p\)-group \(K\) such that a group lies in the quasivariety generated by \(K\) exactly when it lies in both the quasivariety generated by \(G\) and the quasivariety generated by \(H\), and there is a finite \(p\)-group \(K'\) such that a group lies in the quasivariety generated by \(K'\) exactly when it lies in the join of the quasivarieties generated by \(G\) and by \(H\). Equivalently, the set \(L_p\) of quasivarieties generated by a single finite \(p\)-group is a sublattice of the lattice of all quasivarieties of groups.

def finitePGroupQuasivarietiesSublattice : Prop :=
  ∀ p : ℕ, p.Prime → ∀ (G H : Type) [Group G] [Finite G] [Group H] [Finite H],
    IsPGroup p G → IsPGroup p H →
    (∃ (K : Type) (_ : Group K) (_ : Finite K), IsPGroup p K ∧
      ∀ (X : Type) [Group X], InQuasivariety K X ↔ (InQuasivariety G X ∧ InQuasivariety H X)) ∧
    (∃ (K : Type) (_ : Group K) (_ : Finite K), IsPGroup p K ∧
      ∀ (X : Type) [Group X], InQuasivariety K X ↔ InQuasivarietyJoin G H X)

def InQuasivariety (K : Type) [Group K] (X : Type) [Group X] : Prop :=
  ∃ (I : Type) (f : X →* (I → K)), Function.Injective f

WantedExt/GroupTheory/FinitePGroupQuasivarietiesSublatticeKourovka10Problem9Wanted.lean:41

def InQuasivarietyJoin (G H : Type) [Group G] [Group H] (X : Type) [Group X] : Prop :=
  ∃ (I J : Type) (f : X →* (I → G) × (J → H)), Function.Injective f

WantedExt/GroupTheory/FinitePGroupQuasivarietiesSublatticeKourovka10Problem9Wanted.lean:46

Uses 2 · Used by 1

Statement usesQuasivariety generated by a finite group · Join of the quasivarieties generated by two finite groups

Used byQuasivarieties generated by finite \(p\)-groups need not form a sublattice

TheoremQuasivarieties generated by finite \(p\)-groups need not form a sublattice#●ready to prove

For some prime \(p\) there are finite \(p\)-groups \(G\) and \(H\) such that no finite \(p\)-group generates the intersection of the quasivarieties generated by \(G\) and by \(H\), or no finite \(p\)-group generates their join. This answers Kourovka Problem 10.9 (Budkin) in the negative.

Since the join is always generated by the finite \(p\)-group \(G \times H\), it is the intersection that fails to be generated by a finite \(p\)-group.

public theorem_wanted finitePGroupQuasivarietiesSublattice_refuted :
    ¬ finitePGroupQuasivarietiesSublattice

def finitePGroupQuasivarietiesSublattice : Prop :=
  ∀ p : ℕ, p.Prime → ∀ (G H : Type) [Group G] [Finite G] [Group H] [Finite H],
    IsPGroup p G → IsPGroup p H →
    (∃ (K : Type) (_ : Group K) (_ : Finite K), IsPGroup p K ∧
      ∀ (X : Type) [Group X], InQuasivariety K X ↔ (InQuasivariety G X ∧ InQuasivariety H X)) ∧
    (∃ (K : Type) (_ : Group K) (_ : Finite K), IsPGroup p K ∧
      ∀ (X : Type) [Group X], InQuasivariety K X ↔ InQuasivarietyJoin G H X)

WantedExt/GroupTheory/FinitePGroupQuasivarietiesSublatticeKourovka10Problem9Wanted.lean:52

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 10.9 (A. I. Budkin); resolution: S. A. Shakhova, Math. Notes 53, no. 3 (1993), 345-347, Kourovka Archive, Problem 10.9 ("No, not always").

Uses 1

Statement usesKourovka Problem 10.9 (Budkin): quasivarieties generated by finite \(p\)-groups form a sublattice

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.