A group of Euclidean isometries is an extension of its point group by its translations

Proved

LeanEval.Geometry.SpaceGroupsProblem.euclideanGroup_linPart_extension

by Gabewhigham · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

crystallographygeometrygroup-theory

Let $G$ be a subgroup of the Euclidean motion group $E_d$ of $\mathbb{R}^d$ . Every isometry $g$ decomposes as $g(x)=\mathrm{lin}(g)(x)+g(0)$ with linear part $\mathrm{lin}(g)\in O(d)$ .

The theorem asserts that $\mathrm{lin}$ is a group homomorphism $G\to O(d)$ with the following properties:

its image is the point group $P(G)$ ;
its kernel consists exactly of those elements of $G$ that are translations $x\mapsto x+v$ ;
the induced map on the quotient is a group isomorphism

G/\ker(\mathrm{lin})\;\cong\;P(G).

Equivalently, $G$ is an extension

1\longrightarrow T(G)\longrightarrow G\longrightarrow P(G)\longrightarrow 1

of its point group by its group of translations. For a crystallographic group the kernel is a lattice of rank $d$ and the quotient is finite; this exact sequence is the frame in which space groups are classified by cohomological extension data.

Preamble

import Mathlib
import Definitions.Def_LeanEval_SpaceGroups_Definitions
import Definitions.Def_SpaceGroupsPointGroupDefs

Formal statement

namespace LeanEval
namespace Geometry
namespace SpaceGroupsProblem

theorem euclideanGroup_linPart_extension {d : ℕ} (G : Subgroup (EuclideanIsom d)) :
    ∃ f : G →* (E d ≃ₗᵢ[ℝ] E d),
      (∀ g : G, f g = linPart g.1) ∧
      f.range = pointGroup G ∧
      (∀ g : G, g ∈ f.ker ↔ ∃ v, IsTranslationBy g.1 v) ∧
      Nonempty ((G ⧸ f.ker) ≃* pointGroup G) := by sorry

end SpaceGroupsProblem
end Geometry
end LeanEval

Source

L. S. Charlap, Bieberbach Groups and Flat Manifolds, Springer 1986, Chapter I, Section 1 (the exact sequence 1 -> translations -> G -> point group -> 1).

View graph