HEXAGONbeta

Bruck loops with abelian inner mapping groups: a short proof

Primarily AI-generated textHuman understanding: all partsmath.GR — Group Theory

Contributed by Bartosz Naskrecki ↗

Version 1 / Oct 11, 2026 / CC BY 4.0

Abstract

Phillips and Stanovský proved that a Bruck loop with abelian inner mapping group has central nilpotency class at most two and asked for a human-friendly proof. We give a short self-contained proof: a displacement cocycle produces a commutant-valued endomorphism, right alternativity for commutant elements forces its image to be fixed, and cocycle rigidity makes that image central. This yields the abelian center quotient.

Provenance statement

GPT-Astra generated the exposition and Lean development under the author's direction. Inspection of the original Phillips–Stanovský proof suggested the displacement approach. The cocycle calculation was reconstructed from automated proof-search output and checked in Lean. The author confirms that all parts have been checked and understood by a human. Complete Lean formalization at the verified revision: https://github.com/nasqret/bruck-palomar/tree/2b9313afa2364c4af3b5b0390bdc5b3d2ed2aa72 Palomar submission svl2zwiscn4f has completed mechanical verification (https://github.com/PalomarRegistry/PalomarSubmission/actions/runs/38102682798); registry review is pending. No permanent Palomar registration is claimed.

Tools used

OpenAI
GPT-Astra

References

  1. J. D. Phillips and D. Stanovský, https://doi.org/10.1080/00927872.2011.579587 Bruck loops with abelian inner mapping groups , Comm. Algebra 40 (2012), no. 7, 2449--2454.DOI
  2. A. Kreuzer, https://doi.org/10.1017/S0305004197001771 Inner mappings of Bruck loops , Math. Proc. Cambridge Philos. Soc. 123 (1998), 53--57.DOI
  3. M. K. Kinyon, J. D. Phillips, and P. Vojtěchovský, https://doi.org/10.1090/S0002-9947-07-04391-7 When is the commutant of a Bol loop a subloop? , Trans. Amer. Math. Soc. 360 (2008), no. 5, 2393--2408.DOI

Version history

  1. v1Submitted by Bartosz NaskreckiInitial depositCurrentOct 11, 2026