Block lattices of groups

InductiveLattice terms#✓fully proved

Lattice terms in the variables \(x_0, x_1, x_2, \dots\) are built inductively: each variable \(x_n\) is a term, and for terms \(s\) and \(t\) their join \(s \vee t\) and their meet \(s \wedge t\) are terms.

inductive LatticeTerm
  /-- The variable `xₙ`. -/
  | var : ℕ → LatticeTerm
  /-- The join of two terms. -/
  | sup : LatticeTerm → LatticeTerm → LatticeTerm
  /-- The meet of two terms. -/
  | inf : LatticeTerm → LatticeTerm → LatticeTerm

Used by 3

Used byKourovka Problem 11.93: do block lattices generate all lattices? · Evaluation of lattice terms · Evaluation of lattice terms in the block lattice

DefinitionEvaluation of lattice terms#✓fully proved

Let \(L\) be a lattice and \(v\) an assignment of an element \(v(n)\) of \(L\) to each variable \(x_n\). The value of a lattice term under \(v\) is defined by recursion on the term: the variable \(x_n\) has value \(v(n)\), and a join \(s \vee t\) or meet \(s \wedge t\) has as value the join or meet in \(L\) of the values of \(s\) and \(t\).

def LatticeTerm.eval {L : Type*} [Lattice L] (v : ℕ → L) : LatticeTerm → L
  | var n => v n
  | sup a b => a.eval v ⊔ b.eval v
  | inf a b => a.eval v ⊓ b.eval v

Uses 1 · Used by 1

Statement usesLattice terms

Used byKourovka Problem 11.93: do block lattices generate all lattices?

DefinitionBlocks of a group#✓fully proved

A subset \(X\) of a group \(G\) is a block if it is empty or a coset \(gN\) of a normal subgroup \(N\) of \(G\) (Kourovka Notebook, Archive 9.62). Ordered by inclusion, the blocks of \(G\) form the block lattice \(C(G)\).

def IsBlock {G : Type*} [Group G] (X : Set G) : Prop :=
  X = ∅ ∨ ∃ (N : Subgroup G) (g : G), N.Normal ∧ X = {x | g⁻¹ * x ∈ N}

Used by 2

Used byKourovka Problem 11.93: do block lattices generate all lattices? · Join in the block lattice

DefinitionJoin in the block lattice#✓fully proved

For subsets \(X\) and \(Y\) of a group \(G\), their block join is the intersection of all blocks of \(G\) that contain \(X \cup Y\). Since blocks are closed under intersections and \(G\) itself is a block, this is the smallest block containing \(X \cup Y\); for blocks \(X\) and \(Y\) it is their join in the block lattice of \(G\).

def blockSup {G : Type*} [Group G] (X Y : Set G) : Set G :=
  ⋂₀ {Z | IsBlock Z ∧ X ∪ Y ⊆ Z}

Uses 1 · Used by 1

Statement usesBlocks of a group

Used byEvaluation of lattice terms in the block lattice

DefinitionEvaluation of lattice terms in the block lattice#✓fully proved

Let \(G\) be a group and \(v\) an assignment of a subset \(v(n)\) of \(G\) to each variable \(x_n\). The value of a lattice term under \(v\) is defined by recursion on the term: the variable \(x_n\) has value \(v(n)\), a meet \(s \wedge t\) has as value the intersection of the values of \(s\) and \(t\), and a join \(s \vee t\) has as value the block join of the values of \(s\) and \(t\), the intersection of all blocks of \(G\) containing their union. When every \(v(n)\) is a block, this is the value of the term in the block lattice of \(G\).

def LatticeTerm.evalBlock {G : Type*} [Group G] (v : ℕ → Set G) : LatticeTerm → Set G
  | var n => v n
  | sup a b => blockSup (a.evalBlock v) (b.evalBlock v)
  | inf a b => a.evalBlock v ∩ b.evalBlock v

Uses 2 · Used by 1

Statement usesLattice terms · Join in the block lattice

Used byKourovka Problem 11.93: do block lattices generate all lattices?

DefinitionKourovka Problem 11.93: do block lattices generate all lattices?#✓fully proved

Kourovka Problem 11.93: do block lattices generate all lattices? The proposition, asked by D. M. Smirnov, that the block lattices of finite groups generate the variety of all lattices. Here the blocks of a group \(G\) are the cosets of normal subgroups of \(G\) and the empty set; ordered by inclusion they form the block lattice of \(G\), whose meet is intersection and whose join of two blocks is the intersection of all blocks containing their union. Formally, the proposition states: for all lattice terms \(p\) and \(q\), if \(p\) and \(q\) take the same value in the block lattice of every finite group \(G\) under every assignment of blocks of \(G\) to the variables, then \(p\) and \(q\) take the same value in every lattice \(L\) under every assignment of elements of \(L\) to the variables.

By Birkhoff's theorem this is equivalent to the variety generated by these block lattices being the variety of all lattices.

def blockLatticesGenerateAllLattices : Prop :=
  ∀ p q : LatticeTerm,
    (∀ (G : Type) [Group G] [Finite G] (v : ℕ → Set G), (∀ n, IsBlock (v n)) →
      p.evalBlock v = q.evalBlock v) →
    ∀ (L : Type) [Lattice L] (v : ℕ → L), p.eval v = q.eval v

Uses 4 · Used by 1

Statement usesBlocks of a group · Lattice terms · Evaluation of lattice terms · Evaluation of lattice terms in the block lattice

Used bySmirnov's negative answer to Kourovka Problem 11.93

TheoremSmirnov's negative answer to Kourovka Problem 11.93#●ready to prove

The block lattices of finite groups do not generate the variety of all lattices: there are lattice terms \(p\) and \(q\) such that \(p\) and \(q\) take the same value in the block lattice of every finite group \(G\) under every assignment of blocks of \(G\) to the variables, but take different values in some lattice \(L\) under some assignment of elements of \(L\) to the variables. Here the blocks of \(G\) are the cosets of normal subgroups of \(G\) and the empty set, and the block lattice of \(G\) is the set of blocks ordered by inclusion.

Smirnov shows that the variety generated by the block lattices of groups does not contain all finite lattices: for each element \(g\) of a group \(G\), the filter of blocks containing \(g\) is a modular, even arguesian, lattice.

public theorem_wanted blockLatticesGenerateAllLattices_refuted : ¬ blockLatticesGenerateAllLattices

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 11.93 (D. M. Smirnov); resolution: D. M. Smirnov, Siberian Math. J. 33, no. 4 (1992), 663-668, Kourovka Archive, Problem 11.93: "No, it is not"; Archive 9.62: the variety generated by the block lattices of groups does not contain all finite lattices, https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesKourovka Problem 11.93: do block lattices generate all lattices?

6 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.