Theorem 1.3, p. 4 — (8) is associative iff (H, G, α, f) is a crossed system; then H #^f_α G is a group with unit (f(1, 1)⁻¹, 1)

Proved

CrossedProductGroups.Classification.theorem_1_3

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

associativitycrossed-productgroup-extensionp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $H$ and $G$ be groups and let $\alpha : G \to \mathrm{Aut}(H)$ and $f : G \times G \to H$ be arbitrary maps. Equip $H \times G$ with the multiplication

(h_1, g_1) \cdot (h_2, g_2) = \big(h_1\,(g_1 \triangleright h_2)\, f(g_1, g_2),\; g_1g_2\big).

Then:

this multiplication is associative if and only if $(H, G, \alpha, f)$ is a crossed system;
in that case $(H \times G, \cdot)$ is a group with identity element $\big(f(1,1)^{-1}, 1\big)$ : this element is a two-sided unit, and every element has a two-sided inverse.

The group so obtained is the crossed product $H \#_\alpha^f G$ . The theorem says that the cocycle conditions of Definition 1.1 are exactly what is needed for (8) to define a group.

Formalization Note. The crossed system is not assumed normalized. "Is a group with unit $u$ " is stated as associativity together with the two-sided unit and two-sided inverse properties of $u = (f(1,1)^{-1}, 1)$ for the operation crossedMul α f.

Preamble

import Mathlib
import Definitions.Def_CrossedProductGroups_Classification_CrossedSystem

Formal statement

namespace CrossedProductGroups.Classification

theorem theorem_1_3 {H G : Type*} [Group H] [Group G] (α : G → MulAut H) (f : G → G → H) :
    ((∀ x y z : H × G,
        crossedMul α f (crossedMul α f x y) z = crossedMul α f x (crossedMul α f y z)) ↔
      IsCrossedSystem α f) ∧
    (IsCrossedSystem α f →
      (∀ x : H × G, crossedMul α f ((f 1 1)⁻¹, 1) x = x ∧ crossedMul α f x ((f 1 1)⁻¹, 1) = x) ∧
      ∀ x : H × G, ∃ y : H × G,
        crossedMul α f y x = ((f 1 1)⁻¹, 1) ∧ crossedMul α f x y = ((f 1 1)⁻¹, 1)) := by sorry

end CrossedProductGroups.Classification

Source

Agore & Militaru, Crossed product of groups. Applications, arXiv:0805.4077v2, p. 4, Theorem 1.3

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph