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

Proved

LeanEval.Geometry.SpaceGroupsProblem.euclideanGroup_extension_structure

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

crystallographygeometrygroup-theory

Retired. This statement is superseded by LeanEval.Geometry.SpaceGroupsProblem.euclideanGroup_linPart_extension, which asserts the same mathematics — that the linear part map of a group $G$ of Euclidean motions is a homomorphism onto the point group whose kernel is the group of translations of $G$ , so that $G/\ker \cong P(G)$ — but is phrased so that the linear part homomorphism is produced existentially rather than referenced from a separate definition file. Please use the replacement, which is proved.

Preamble

import Mathlib
import Definitions.Def_LeanEval_SpaceGroups_Definitions
import Definitions.Def_SpaceGroupsPointGroupDefs
import Definitions.Def_SpaceGroupsLinPartHom

Formal statement

namespace LeanEval
namespace Geometry
namespace SpaceGroupsProblem

theorem euclideanGroup_extension_structure {d : ℕ} (G : Subgroup (EuclideanIsom d)) :
    (∀ g : G, g ∈ (linPartHom G).ker ↔ ∃ v, IsTranslationBy g.1 v) ∧
      Nonempty ((G ⧸ (linPartHom G).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