§3, p. 21 — normalized crossed systems are 2-equivalent iff isomorphic in E2(H, G); ≈2 is an equivalence relation

Proved

CrossedProductGroups.Classification.iso_iff_equiv2

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

category-theorycrossed-productequivalence-relationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $H$ and $G$ be groups. For normalized crossed systems $(\alpha, f), (\alpha', f') \in \mathrm{Crossed}(H, G)$ ,

(H, G, \alpha, f) \approx_2 (H, G, \alpha', f') \iff (\alpha, f) \cong (\alpha', f') \text{ in } \mathcal{E}_2(H, G),

and $\approx_2$ is an equivalence relation on $\mathrm{Crossed}(H, G)$ .

This is the bridge between the explicit relation of Definition 3.7 and the categorical notion of isomorphism; it is the content of the paragraph following Definition 3.7.

Formalization Note. The source states this as an unnumbered consequence of Corollary 3.5 (p. 21). Isomorphism in $\mathcal{E}_2(H, G)$ is Nonempty (c ≅ c') for the category instance on E2 H G.

Preamble

import Mathlib
import Definitions.Def_CrossedProductGroups_Classification_CrossedSystem
import Definitions.Def_CrossedProductGroups_Classification_E2

Formal statement

namespace CrossedProductGroups.Classification

theorem iso_iff_equiv2 (H G : Type*) [Group H] [Group G] :
    (∀ c c' : E2 H G, Nonempty (c ≅ c') ↔ Equiv2 c c') ∧
      Equivalence (Equiv2 (H := H) (G := G)) := by sorry

end CrossedProductGroups.Classification

Source

Agore & Militaru, Crossed product of groups. Applications, arXiv:0805.4077v2, p. 21, §3, paragraph after Definition 3.7

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