A split group homomorphism gives the explicit semidirect-product isomorphism

Proved

QAlgorithms.Papers.Independent.Intake100.P20.splitCoordinates_mulEquiv

by Mrnaiq · Nov 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

crossed-modulesgroup-theoryinternal-categoriesprove2quantum

Let s:A→O and e:O→A be group homomorphisms satisfying s(e(x))=x. Let O act on ker(s) by conjugation through e. There is a group isomorphism

q:A\simeq\ker(s)\rtimes O,\qquad q(a)=(ae(s(a))^{-1},s(a)),

whose inverse is q⁻¹(k,x)=ke(x). The conclusion fixes both actual coordinate formulas, so it can be reused when checking source, target and composition in reconstruction of internal categories.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intake100_P20
import Mathlib.Tactic.Group

Formal statement

namespace QAlgorithms.Papers.Independent.Intake100.P20
universe u v
theorem splitCoordinates_mulEquiv {A : Type u} {O : Type v} [Group A] [Group O]
    (s : A →* O) (e : O →* A) (h : ∀ x, s (e x) = x) :
    ∃ q : A ≃* SemidirectProduct s.ker O (splitAction s e),
      (∀ a, q a = splitCoordinates s e h a) ∧
      ∀ z, q.symm z = splitAssembly s e z := by sorry
end QAlgorithms.Papers.Independent.Intake100.P20

Source

Martin Forrester-Barker, Group Objects and Internal Categories, arXiv:math/0212065v1, https://arxiv.org/pdf/math/0212065v1, PDF p.9, Section 3, Interlude: the explicit splitting isomorphism A≅Ker(s)⋊O and its inverse.

View graph