Lattices of centralizers

DefinitionCentralizer subgroups#✓fully proved

A subgroup \(H\) of a group \(G\) is a centralizer if \(H = C_G(X)\) for some subset \(X \subseteq G\), where \(C_G(X)\) is the subgroup of elements of \(G\) that commute with every element of \(X\).

def IsCentralizer {G : Type*} [Group G] (H : Subgroup G) : Prop :=
  ∃ X : Set G, H = Subgroup.centralizer X

Used by 1

Used byModularity of centralizer sublattices (Kourovka 11.4)

DefinitionModularity of centralizer sublattices (Kourovka 11.4)#✓fully proved

Call a subgroup of a group \(G\) a centralizer if it equals \(C_G(X)\) for some subset \(X \subseteq G\). This is the proposition that for every group \(G\) in which the join (in the subgroup lattice) of any two centralizers is again a centralizer, any three centralizers \(A\), \(B\), \(C\) of \(G\) with \(A \le C\) satisfy the modular law \((A \sqcup B) \sqcap C = A \sqcup (B \sqcap C)\), where \(\sqcup\) and \(\sqcap\) are the join and meet in the subgroup lattice of \(G\).

Centralizers are always closed under intersection, so the hypothesis says that they form a sublattice of the subgroup lattice. The question is due to V. A. Antonov.

def centralizerSublatticeModular : Prop :=
  ∀ (G : Type) [Group G],
    (∀ A B : Subgroup G, IsCentralizer A → IsCentralizer B → IsCentralizer (A ⊔ B)) →
    ∀ A B C : Subgroup G, IsCentralizer A → IsCentralizer B → IsCentralizer C → A ≤ C →
      (A ⊔ B) ⊓ C = A ⊔ (B ⊓ C)

Uses 1 · Used by 1

Statement usesCentralizer subgroups

Used byLattices of centralizers need not be modular (Kourovka 11.4)

TheoremLattices of centralizers need not be modular (Kourovka 11.4)#●ready to prove

Call a subgroup of a group \(G\) a centralizer if it equals \(C_G(X)\) for some subset \(X \subseteq G\). Modularity of centralizer sublattices fails: there is a group \(G\) in which the join (in the subgroup lattice) of any two centralizers is again a centralizer, but which has centralizers \(A\), \(B\), \(C\) with \(A \le C\) and \((A \sqcup B) \sqcap C \ne A \sqcup (B \sqcap C)\), where \(\sqcup\) and \(\sqcap\) are the join and meet in the subgroup lattice of \(G\).

The Kourovka Archive answers 11.4 "No, not always" (Obraztsov); for finite groups the answer is yes.

public theorem_wanted centralizerSublatticeModular_refuted : ¬ centralizerSublatticeModular

def centralizerSublatticeModular : Prop :=
  ∀ (G : Type) [Group G],
    (∀ A B : Subgroup G, IsCentralizer A → IsCentralizer B → IsCentralizer (A ⊔ B)) →
    ∀ A B C : Subgroup G, IsCentralizer A → IsCentralizer B → IsCentralizer C → A ≤ C →
      (A ⊔ B) ⊓ C = A ⊔ (B ⊓ C)

WantedExt/GroupTheory/CentralizerLatticeModularKourovka11Problem4Wanted.lean:45

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.4 (V. A. Antonov); resolution: V. N. Obraztsov, J. Algebra 199, no. 1 (1998), 337-343, Kourovka Archive, Problem 11.4: "No, not always", https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesModularity of centralizer sublattices (Kourovka 11.4)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.