Crossed modules and internal Grp categories: both constructions

Proved

QAlgorithms.Papers.Independent.Intake100.P20.crossedModulesAndInternalCategories

by Gohan · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $\partial:C\to G$ , with an automorphic left action $\rho:G\to\operatorname{Aut}(C)$ , be a crossed module. It determines an internal Grp category with objects $G$ , arrows $C\rtimes_\rho G$ , and

s(c,g)=g,\quad t(c,g)=\partial(c)g,\quad e(g)=(1,g),\quad (d,\partial(c)g)\circ(c,g)=(dc,g).

Conversely, for an internal Grp category $(A,O,s,t,e,\circ)$ , the actual subgroup $K=\ker s$ , boundary $\partial=t|_K$ , and action $x\triangleright k=e(x)ke(x)^{-1}$ form a crossed module. The canonical group isomorphism $a\mapsto(ae(s(a))^{-1},s(a))$ identifies the original category with the category reconstructed from this crossed module: it preserves source, target, identities and every defined composite. In particular the semidirect composition formula is a conclusion of the internal-category axioms.

Starting instead from $(C,G,\partial,\rho)$ , the map $c\mapsto(c,1)$ identifies $C$ with the reconstructed source kernel and preserves boundary and action. Thus both constructions recover their original structures through the explicit canonical identifications. This is the source's structural correspondence, without an additional assertion about categories of morphisms.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intake100_P20

Formal statement

namespace QAlgorithms.Papers.Independent.Intake100.P20

open CategoryTheory

open scoped TensorProduct Manifold ContDiff

universe u v w z

/-- PDF pp. 9–12: BOTH explicit constructions and reconstruction compatibility.
The forward category has s(c,g)=g, t(c,g)=boundary(c)g, identity(g)=(1,g),
and (d,boundary(c)g) after (c,g) = (dc,g). The reverse crossed module is
the source kernel with restricted target and identity-conjugation action.
The original category is recovered by its computed semidirect coordinates,
including composition as a CONCLUSION of the category/interchange laws.
The original crossed module is recovered by c ↦ (c,1) in the source kernel.
No claim about a category of crossed-module morphisms is silently added. -/
theorem crossedModulesAndInternalCategories :
    (∀ {C : Type u} {G : Type v} [Group C] [Group G]
      (d : C →* G) (r : G →* MulAut C), CrossedModule d r →
      InternalCategoryInGrp (crossedCategoryMaps d r) ∧
      ∃ q : C ≃* (SemidirectProduct.rightHom : SemidirectProduct C G r →* G).ker,
        (∀ c, q c = crossedKernelMap r c) ∧
        (∀ c, (crossedCategoryMaps d r).target (q c).val = d c) ∧
        (∀ g c, (q (r g c)).val =
          (crossedCategoryMaps d r).identity g * (q c).val *
            ((crossedCategoryMaps d r).identity g)⁻¹)) ∧
    (∀ {A : Type u} {O : Type v} [Group A] [Group O]
      (D : CategoryMaps A O) (h : InternalCategoryInGrp D),
      CrossedModule (kernelBoundary D h) (kernelAction D h) ∧
      InternalCategoryInGrp (crossedCategoryMaps (kernelBoundary D h) (kernelAction D h)) ∧
      ∃ q : A ≃* SemidirectProduct (sourceHom D h).ker O (kernelAction D h),
        (∀ a, q a = categoryCoordinates D h a) ∧
        (∀ a, (q a).right = D.source a ∧
          kernelBoundary D h (q a).left * (q a).right = D.target a) ∧
        (∀ x, q (D.identity x) = ⟨1, x⟩) ∧
        (∀ f g, D.target f = D.source g →
          q (D.compose g f) = ⟨(q g).left * (q f).left, (q f).right⟩)) := by sorry

end QAlgorithms.Papers.Independent.Intake100.P20

Source

Group Objects and Internal Categories, arXiv:math/0212065v1, PDF p. 9, §3, Crossed Modules and Internal Categories, pp. 9–12

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

The theorem asserts the conjunction of the following two universally quantified claims. To specify all their requirements, for groups $H$ and $P$ and total maps $s,t:H\to P$ , $e:P\to H$ , and $m:H\times H\to H$ , write $\mathcal I(s,t,e,m)$ for the following explicit collection of conditions: for every $x\in P$ , $s(e(x))=x$ and $t(e(x))=x$ ; for every $f,g\in H$ with $t(f)=s(g)$ , $s(m(g,f))=s(f)$ and $t(m(g,f))=t(g)$ ; for every $f\in H$ , $m(e(t(f)),f)=f$ and $m(f,e(s(f)))=f$ ; for every $f,g,h\in H$ with $t(f)=s(g)$ and $t(g)=s(h)$ , $m(h,m(g,f))=m(m(h,g),f)$ ; the maps $s,t,e$ preserve identities and multiplication, meaning $s(1_H)=t(1_H)=1_P$ , $e(1_P)=1_H$ , $s(ab)=s(a)s(b)$ and $t(ab)=t(a)t(b)$ for every $a,b\in H$ , and $e(xy)=e(x)e(y)$ for every $x,y\in P$ ; furthermore $m(1_H,1_H)=1_H$ , and, for every $f,g,a,b\in H$ satisfying $t(f)=s(g)$ and $t(a)=s(b)$ , $m(gb,fa)=m(g,f)m(b,a)$ . First, for arbitrary groups $C,G$ and group homomorphisms $d:C\to G$ and $r:G\to\operatorname{Aut}(C)$ , suppose that

d(r(g)(c))=g\,d(c)\,g^{-1}\quad(g\in G,\ c\in C), \qquad r(d(c))(c')=cc'c^{-1}\quad(c,c'\in C).

On $H=C\rtimes_r G$ , whose multiplication is $(c,g)(c',g')=(c\,r(g)(c'),gg')$ , define $s(c,g)=g$ , $t(c,g)=d(c)g$ , $e(g)=(1_C,g)$ , and $m((c',g'),(c,g))=(c'c,g)$ . Then $\mathcal I(s,t,e,m)$ holds, and there exists a group isomorphism $q:C\to K$ , where $K=\ker(\pi)$ for $\pi:H\to G$ , $\pi(c,g)=g$ , such that, for every $c\in C$ , $q(c)$ is the kernel element with underlying pair $(c,1_G)$ , and $t(\overline{q(c)})=d(c)$ ; here a bar denotes the underlying element of $H$ . In addition, for every $g\in G$ and $c\in C$ ,

\overline{q(r(g)(c))} =(1_C,g)\,\overline{q(c)}\,(1_C,g)^{-1}.

Second, for arbitrary groups $A,O$ and total maps $s,t:A\to O$ , $e:O\to A$ , and $m:A\times A\to A$ , suppose that $\mathcal I(s,t,e,m)$ holds. Let $K=\{a\in A:s(a)=1_O\}$ , with its inherited group structure, let $\partial:K\to O$ be the group homomorphism $\partial(k)=t(\bar k)$ , and let $\rho:O\to\operatorname{Aut}(K)$ be the group homomorphism whose action is conjugation by $e(x)$ , so that $\overline{\rho(x)(k)}=e(x)\bar k e(x)^{-1}$ . Then, for all $x\in O$ and $k,\ell\in K$ ,

\partial(\rho(x)(k))=x\,\partial(k)\,x^{-1}, \qquad \rho(\partial(k))(\ell)=k\ell k^{-1}.

Moreover, on $K\rtimes_\rho O$ , the maps

s'(k,x)=x,\qquad t'(k,x)=\partial(k)x,\qquad e'(x)=(1_K,x),\qquad m'((\ell,y),(k,x))=(\ell k,x)

satisfy $\mathcal I(s',t',e',m')$ , and there exists a group isomorphism $q:A\to K\rtimes_\rho O$ such that, for every $a\in A$ ,

q(a)=\bigl(a\,e(s(a))^{-1},\,s(a)\bigr),

where the first coordinate is regarded as an element of $K$ . Writing $q(a)=(k_a,x_a)$ , this isomorphism also satisfies $x_a=s(a)$ and $\partial(k_a)x_a=t(a)$ for every $a\in A$ , satisfies $q(e(x))=(1_K,x)$ for every $x\in O$ , and satisfies

q(m(g,f))=(k_gk_f,x_f) \quad\text{for every }f,g\in A\text{ with }t(f)=s(g).

All groups in both claims may be trivial. The composition maps are defined on every pair of arrows, including pairs whose endpoints do not match; each displayed law with an endpoint-matching hypothesis is required only when that hypothesis holds.

Human review

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

View graph