Direct-sum cancellation for torsion-free abelian groups

DefinitionTorsion-free abelian group#✓fully proved

An abelian group \(A\), written additively, is torsion-free when for every natural number \(n \ne 0\) and every \(a \in A\), \(n a = 0\) implies \(a = 0\).

def IsTorsionFreeAddGroup (A : Type*) [AddCommGroup A] : Prop :=
  ∀ (n : ℕ) (a : A), n ≠ 0 → n • a = 0 → a = 0

Used by 2

Used byBergman's absorption question (Kourovka 17.21(a)) · Bergman's absorption question for isomorphic summands (Kourovka 17.21(b))

DefinitionBergman's absorption question (Kourovka 17.21(a))#✓fully proved

The statement that for all torsion-free abelian groups \(A\), \(B\), \(C\), if \(A \cong A \oplus B \oplus C\) then \(A \cong A \oplus B\).

def torsionFreeAbsorbsDirectSummand : Prop :=
  ∀ (A B C : Type) [AddCommGroup A] [AddCommGroup B] [AddCommGroup C],
    IsTorsionFreeAddGroup A → IsTorsionFreeAddGroup B → IsTorsionFreeAddGroup C →
      Nonempty (A ≃+ A × B × C) → Nonempty (A ≃+ A × B)

Uses 1 · Used by 1

Statement usesTorsion-free abelian group

Used byFailure of direct-summand absorption for torsion-free abelian groups

DefinitionBergman's absorption question for isomorphic summands (Kourovka 17.21(b))#✓fully proved

The statement that for all torsion-free abelian groups \(A\), \(B\), \(C\) with \(B \cong C\), if \(A \cong A \oplus B \oplus C\) then \(A \cong A \oplus B\).

def torsionFreeAbsorbsDirectSummandOfIso : Prop :=
  ∀ (A B C : Type) [AddCommGroup A] [AddCommGroup B] [AddCommGroup C],
    IsTorsionFreeAddGroup A → IsTorsionFreeAddGroup B → IsTorsionFreeAddGroup C →
      Nonempty (B ≃+ C) → Nonempty (A ≃+ A × B × C) → Nonempty (A ≃+ A × B)

Uses 1 · Used by 1

Statement usesTorsion-free abelian group

Used byFailure of direct-summand absorption with isomorphic summands

TheoremFailure of direct-summand absorption for torsion-free abelian groups#●ready to prove

There exist torsion-free abelian groups \(A\), \(B\), \(C\) with \(A \cong A \oplus B \oplus C\) but \(A \not\cong A \oplus B\); thus the answer to Kourovka Problem 17.21(a) is negative.

The Kourovka Archive answers 17.21 "No, not necessarily, even in case b)", citing Corner (1964) and Bergman (letter of 2011, an example with \(B\) and \(C\) of rank 1).

public theorem_wanted torsionFreeAbsorbsDirectSummand_refuted : ¬ torsionFreeAbsorbsDirectSummand

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 17.21 (G. M. Bergman); resolution: A. L. S. Corner, in Proc. Colloq. Abelian Groups (Tihany, 1963), Budapest, 1964, 43-48; G. M. Bergman, letter of 20 February 2011, as recorded in the Kourovka Archive, Kourovka Archive, Problem 17.21 (No, not necessarily, even in case b); see Corner (1964); Bergman also has an example with B and C of rank 1).

Uses 1

Statement usesBergman's absorption question (Kourovka 17.21(a))

TheoremFailure of direct-summand absorption with isomorphic summands#●ready to prove

There exist torsion-free abelian groups \(A\), \(B\), \(C\) with \(B \cong C\) and \(A \cong A \oplus B \oplus C\) but \(A \not\cong A \oplus B\); thus the answer to Kourovka Problem 17.21(b) is negative.

The Kourovka Archive answers 17.21(b) negatively as well ("even in case b)", Corner 1964; Bergman, letter of 2011).

public theorem_wanted torsionFreeAbsorbsDirectSummandOfIso_refuted :
    ¬ torsionFreeAbsorbsDirectSummandOfIso

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 17.21 (G. M. Bergman); resolution: A. L. S. Corner, in Proc. Colloq. Abelian Groups (Tihany, 1963), Budapest, 1964, 43-48; G. M. Bergman, letter of 20 February 2011, as recorded in the Kourovka Archive, Kourovka Archive, Problem 17.21 (No, not necessarily, even in case b); see Corner (1964); Bergman also has an example with B and C of rank 1).

Uses 1

Statement usesBergman's absorption question for isomorphic summands (Kourovka 17.21(b))

3 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.