Prove2Me

Proposition 3.4, p. 20 — (η, ψ, γ) is a morphism of E2(H, G) iff there is a unique r : G → H with (35)–(37)

Proved
CrossedProductGroups.Classification.proposition_3_4

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

category-theorycrossed-productgroup-extensionp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let (α,f)(\alpha, f) and (α′,f′)(\alpha', f') be normalized crossed systems, η:H→H\eta : H \to H and γ:G→G\gamma : G \to G group morphisms, and ψ:H×G→H×G\psi : H \times G \to H \times G a map. Then (η,ψ,γ)(\eta, \psi, \gamma) is a morphism (α,f)→(α′,f′)(\alpha, f) \to (\alpha', f') of E2(H,G)\mathcal{E}_2(H, G) if and only if there is a unique map r:G→Hr : G \to H such that for all h∈Hh \in H and g,g1,g2∈Gg, g_1, g_2 \in G

η(g▹h) r(g)=r(g) (γ(g)▹′η(h)),(35)r(g1) (γ(g1)▹′r(g2)) f′(γ(g1),γ(g2))=η(f(g1,g2)) r(g1g2),(36)ψ(h,g)=(η(h) r(g),  γ(g)).(37)\begin{aligned} \eta(g \triangleright h)\, r(g) &= r(g)\,\big(\gamma(g) \triangleright' \eta(h)\big), &(35)\\ r(g_1)\,\big(\gamma(g_1) \triangleright' r(g_2)\big)\, f'\big(\gamma(g_1), \gamma(g_2)\big) &= \eta\big(f(g_1, g_2)\big)\, r(g_1g_2), &(36)\\ \psi(h, g) &= \big(\eta(h)\, r(g),\; \gamma(g)\big). &(37) \end{aligned}

This parametrizes the morphisms of E2(H,G)\mathcal{E}_2(H, G) with fixed outer components η,γ\eta, \gamma by maps rr subject to two conditions.

Formalization Note. The paper's "η, γ are morphisms of groups" is carried by their types (H →* H, G →* G), since they are components of the triple. "(η,ψ,γ)(\eta, \psi, \gamma) is a morphism of E2(H,G)\mathcal{E}_2(H, G)" is stated as the existence of an E2Hom c c' with these three components.

Preamble
import Mathlib
import Definitions.Def_CrossedProductGroups_Classification_CrossedSystem
import Definitions.Def_CrossedProductGroups_Classification_E2
Formal statement
namespace CrossedProductGroups.Classification

theorem proposition_3_4 {H G : Type*} [Group H] [Group G] (c c' : E2 H G)
    (η : H →* H) (γ : G →* G) (ψ : H × G → H × G) :
    (∃ m : E2Hom c c', m.η = η ∧ m.γ = γ ∧ m.ψ = ψ) ↔
      ∃! r : G → H,
        (∀ g : G, ∀ h : H, η (c.1.1 g h) * r g = r g * c'.1.1 (γ g) (η h)) ∧
        (∀ g₁ g₂ : G, r g₁ * c'.1.1 (γ g₁) (r g₂) * c'.1.2 (γ g₁) (γ g₂) =
          η (c.1.2 g₁ g₂) * r (g₁ * g₂)) ∧
        ∀ h : H, ∀ g : G, ψ (h, g) = (η h * r g, γ g) := by sorry

end CrossedProductGroups.Classification
Source
Agore & Militaru, Crossed product of groups. Applications, arXiv:0805.4077v2, p. 20, Proposition 3.4, (35)–(37)
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