Projective modules over group rings

DefinitionPolycyclic group#✓fully proved

A group \(G\) is polycyclic if for some \(n \ge 0\) there are subgroups \(1 = H_0 \le H_1 \le \cdots \le H_n = G\) such that for each \(i < n\), \(H_i\) is normal in \(H_{i+1}\) and the quotient \(H_{i+1} / H_i\) is cyclic.

def IsPolycyclic (G : Type*) [Group G] : Prop :=
  ∃ (n : ℕ) (H : Fin (n + 1) → Subgroup G), H 0 = ⊥ ∧ H (Fin.last n) = ⊤ ∧
    ∀ i : Fin n, H i.castSucc ≤ H i.succ ∧
      ∃ _ : ((H i.castSucc).subgroupOf (H i.succ)).Normal,
        IsCyclic (H i.succ ⧸ (H i.castSucc).subgroupOf (H i.succ))

Used by 1

Used byAlmost polycyclic group

DefinitionAlmost polycyclic group#✓fully proved

A group \(G\) is almost polycyclic (polycyclic-by-finite) if it has a subgroup of finite index that is polycyclic.

def IsAlmostPolycyclic (G : Type*) [Group G] : Prop :=
  ∃ H : Subgroup G, H.FiniteIndex ∧ IsPolycyclic H

Uses 1 · Used by 1

Statement usesPolycyclic group

Used byArtamonov's freeness question (Kourovka 11.5)

DefinitionArtamonov's freeness question (Kourovka 11.5)#✓fully proved

This is the proposition that, for every commutative ring \(k\), every torsion-free almost polycyclic group \(G\) (no element \(g \ne 1\) of \(G\) has finite order) and every finitely generated projective module \(P\) over the group ring \(kG\), if \(P\) contains two elements that are linearly independent over \(kG\), then \(P\) is a free \(kG\)-module.

def projectiveWithTwoIndependentFree : Prop :=
  ∀ (k : Type) [CommRing k] (G : Type) [Group G], (∀ g : G, g ≠ 1 → ¬ IsOfFinOrder g) →
    IsAlmostPolycyclic G → ∀ (P : Type) [AddCommGroup P] [Module (MonoidAlgebra k G) P],
    Module.Finite (MonoidAlgebra k G) P → Module.Projective (MonoidAlgebra k G) P →
    (∃ x y : P, LinearIndependent (MonoidAlgebra k G) ![x, y]) →
    Module.Free (MonoidAlgebra k G) P

Uses 1 · Used by 1

Statement usesAlmost polycyclic group

Used byArtamonov's freeness question has a negative answer

TheoremArtamonov's freeness question has a negative answer#●ready to prove

It is not the case that for every commutative ring \(k\), every torsion-free almost polycyclic group \(G\) (no element \(g \ne 1\) of \(G\) has finite order) and every finitely generated projective module \(P\) over the group ring \(kG\) containing two elements that are linearly independent over \(kG\), the module \(P\) is free over \(kG\).

Jayadevan's counterexample takes \(k = \mathbb{F}_2 \times \mathbb{F}_2\) and the trivial group \(G\), so that \(kG = k\); then \(P = k^2 \oplus (\mathbb{F}_2 \times 0)\) is a finitely generated projective \(k\)-module containing an independent pair, but \(|P| = 32\) is not a power of \(4 = |k|\), so \(P\) is not free. The Kourovka Notebook (21st issue) marks 11.5 solved, "No, not always" (AI solution confirmed by D. Segal); the example gives nothing for field coefficients.

public theorem_wanted projectiveWithTwoIndependentFree_refuted : ¬ projectiveWithTwoIndependentFree

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 11.5 (V. A. Artamonov); resolution: A. Jayadevan, A coefficient-ring obstruction to freeness of projective group-ring modules, preprint, Zenodo record 22846603 (2026), main example: k = 𝔽₂ × 𝔽₂, G = 1, P = k² ⊕ (𝔽₂ × 0) is projective with an independent pair but has 32 elements, while finite free k-modules have 4ⁿ; the Kourovka Notebook (21st issue) marks 11.5 solved (AI solution confirmed by D. Segal), https://zenodo.org/records/22846603.

Uses 1

Statement usesArtamonov's freeness question (Kourovka 11.5)

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.