Crystallographic groups

AbbreviationEuclidean space \(\mathbb{R}^d\)#✓fully proved

For a natural number \(d\), \(E(d)\) is the \(d\)-dimensional Euclidean space \(\mathbb{R}^d\), with coordinates indexed by \(0, 1, \dots, d - 1\) and the standard inner product.

abbrev E (d : ℕ) := EuclideanSpace ℝ (Fin d)

Used by 6

Used byOrientation-preserving affine equivalence · Number of orientation-preserving affine classes of crystallographic groups · Number of orientation-preserving affine classes of orientation-preserving crystallographic groups · Orientation-preserving isometry · The 230 space groups · There are exactly 17 wallpaper groups

AbbreviationEuclidean space \(\mathbb{R}^d\) for the space-group problem#✓fully proved

For a natural number \(d\), this is the \(d\)-dimensional real Euclidean space \(\mathbb{R}^d\) with its standard inner product.

abbrev E (d : ℕ) := EuclideanSpace ℝ (Fin d)

DefinitionOrientation-preserving isometry#✓fully proved

An affine isometry of the Euclidean space \(\mathbb{R}^d\) is orientation-preserving if its linear part has positive determinant.

def IsOrientationPreservingIsom {d : ℕ} (g : EuclideanIsom d) : Prop :=
  0 < (g.toAffineEquiv.linear.det : ℝ)

Uses 1 · Used by 1

Statement usesEuclidean space \(\mathbb{R}^d\)

Used byNumber of orientation-preserving affine classes of orientation-preserving crystallographic groups

DefinitionOrientation-preserving affine equivalence#✓fully proved

Two subgroups \(G_1\) and \(G_2\) of the group of affine isometries of the Euclidean space \(\mathbb{R}^d\) are orientation-preserving affinely equivalent if there is an affine bijection \(\varphi\) of \(\mathbb{R}^d\) whose linear part has positive determinant such that \(\{\varphi g \varphi^{-1} : g \in G_1\} = G_2\) as sets of affine maps of \(\mathbb{R}^d\).

def AffOPEquivalent {d : ℕ} (G₁ G₂ : Subgroup (EuclideanIsom d)) : Prop :=
  ∃ φ : AffineGroup d, 0 < (φ.linear.det : ℝ) ∧
    {h : AffineGroup d | ∃ g ∈ G₁, h = φ * g.toAffineEquiv * φ⁻¹} =
    {h : AffineGroup d | ∃ g ∈ G₂, h = g.toAffineEquiv}

Uses 1 · Used by 2

Statement usesEuclidean space \(\mathbb{R}^d\)

Used byNumber of orientation-preserving affine classes of crystallographic groups · Number of orientation-preserving affine classes of orientation-preserving crystallographic groups

DefinitionNumber of orientation-preserving affine classes of crystallographic groups#✓fully proved

For a natural number \(d\), this is the number, in \(\mathbb{N} \cup \{\infty\}\), of classes of \(d\)-dimensional crystallographic groups under orientation-preserving affine equivalence. Here a crystallographic group is a subgroup \(G\) of the group of affine isometries of \(\mathbb{R}^d\) that is discrete (for every point \(x\) and every \(\varepsilon > 0\) only finitely many \(g \in G\) satisfy \(\operatorname{dist}(g x, x) \le \varepsilon\)) and contains translations by \(d\) linearly independent vectors.

noncomputable def crystallographicCountOP (d : ℕ) : ℕ∞ :=
  Set.encard {S : Set (CrystallographicGroup d) |
    ∃ G₀ : CrystallographicGroup d,
      S = {H : CrystallographicGroup d | AffOPEquivalent G₀.1 H.1}}

Uses 2 · Used by 1

Statement usesEuclidean space \(\mathbb{R}^d\) · Orientation-preserving affine equivalence

Used byThe 230 space groups

DefinitionNumber of orientation-preserving affine classes of orientation-preserving crystallographic groups#✓fully proved

Number of orientation-preserving affine classes of orientation-preserving crystallographic groups. For a natural number \(d\), this is the number, in \(\mathbb{N} \cup \{\infty\}\), of classes under orientation-preserving affine equivalence of those \(d\)-dimensional crystallographic groups all of whose elements are orientation-preserving isometries. Here a crystallographic group is a subgroup \(G\) of the group of affine isometries of \(\mathbb{R}^d\) that is discrete (for every point \(x\) and every \(\varepsilon > 0\) only finitely many \(g \in G\) satisfy \(\operatorname{dist}(g x, x) \le \varepsilon\)) and contains translations by \(d\) linearly independent vectors.

noncomputable def crystallographicCountOPOnly (d : ℕ) : ℕ∞ :=
  Set.encard {S : Set { G : CrystallographicGroup d //
                          ∀ g, g ∈ G.1 → IsOrientationPreservingIsom g } |
    ∃ G₀ : { G : CrystallographicGroup d //
              ∀ g, g ∈ G.1 → IsOrientationPreservingIsom g },
      S = {H | AffOPEquivalent G₀.1.1 H.1.1}}

Uses 3 · Used by 1

Statement usesEuclidean space \(\mathbb{R}^d\) · Orientation-preserving affine equivalence · Orientation-preserving isometry

Used byThe 230 space groups

TheoremThe 230 space groups#●ready to prove

In dimension \(3\) there are exactly \(230\) classes of crystallographic groups under orientation-preserving affine equivalence, exactly \(219\) classes of crystallographic groups under affine equivalence (conjugation by an arbitrary affine bijection of \(\mathbb{R}^3\)), and exactly \(65\) classes under orientation-preserving affine equivalence of crystallographic groups all of whose elements are orientation-preserving isometries.

public theorem_wanted space_groups :
    crystallographicCountOP 3 = 230 ∧
      crystallographicCount 3 = 219 ∧
        crystallographicCountOPOnly 3 = 65

Sources

• E. Fedorov, 'Симметрія правильныхъ системъ фигуръ' (Symmetry of regular systems of figures), Trans. Min. Soc. St. Petersburg 28 (1891) 1–146; A. Schoenflies, Krystallsysteme und Krystallstructur, Teubner 1891, independently. Listed as §94 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem space_groups_230 of the lean-eval benchmark.

Uses 3

Statement usesEuclidean space \(\mathbb{R}^d\) · Number of orientation-preserving affine classes of crystallographic groups · Number of orientation-preserving affine classes of orientation-preserving crystallographic groups

AbbreviationEuclidean space for wallpaper groups#✓fully proved

For a natural number \(d\), the \(d\)-dimensional real Euclidean space \(\mathbb{R}^d\) with its standard inner product.

abbrev E (d : ℕ) := EuclideanSpace ℝ (Fin d)

TheoremThere are exactly 17 wallpaper groups#●ready to prove

Call a group \(G\) of isometries of the Euclidean plane \(\mathbb{R}^2\) crystallographic if it is discrete, meaning that for every point \(x\) and every \(\varepsilon > 0\) only finitely many \(g \in G\) satisfy \(\operatorname{dist}(g x, x) \le \varepsilon\), and it contains translations by two linearly independent vectors. Call two such groups \(G_1\) and \(G_2\) affinely equivalent if some invertible affine map \(\varphi\) of \(\mathbb{R}^2\) satisfies \(\{\varphi g \varphi^{-1} : g \in G_1\} = G_2\). Up to affine equivalence there are exactly \(17\) crystallographic groups of the plane.

public theorem_wanted there_are_17_wallpaper_groups :
    crystallographicCount 2 = 17

Sources

• G. Pólya, 'Über die Analogie der Kristallsymmetrie in der Ebene', Z. Kristallogr. 60 (1924) 278–282; P. Niggli, 'Die Flächensymmetrien homogener Diskontinuen', Z. Kristallogr. 60 (1924) 283–298. Listed as §94 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem wallpaper_groups_17 of the lean-eval benchmark.

Uses 1

Statement usesEuclidean space \(\mathbb{R}^d\)

7 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.