LeanEval crystallographic groups, affine equivalences, and counting functions

E. For every natural number $d$, $E(d)$ denotes the real Euclidean space with coordinates indexed by $\{0,\ldots,d-1\}$, equipped with its Euclidean inner product. This includes $d=0$, when the space consists of a single zero vector.

EuclideanIsom. For every natural number $d$, $\operatorname{EuclideanIsom}(d)$ denotes the type of bijective real affine isometries from the coordinate Euclidean space $\mathbb R^d$ to itself. Dimension zero is included.

AffineGroup. For every natural number $d$, $\operatorname{AffineGroup}(d)$ denotes the type of bijective real affine maps from the coordinate Euclidean space $\mathbb R^d$ to itself, with group operation given by composition. These maps need not preserve distances. Dimension zero is included.

IsTranslationBy. For any natural number $d$, any bijective real affine isometry $g$ of $\mathbb R^d$, and any vector $v\in\mathbb R^d$, this predicate means that $g(x)=x+v$ for every $x\in\mathbb R^d$. The vector $v$ may be zero; dimension zero is also allowed.

IsDiscrete. For any natural number $d$ and any subgroup $G$ of the group of bijective real affine isometries of $\mathbb R^d$, this predicate means that, for every $x\in\mathbb R^d$ and every real $\varepsilon>0$, the set $\{g\in G:\operatorname{dist}(g(x),x)\leq\varepsilon\}$ is finite. The inequality includes its boundary, and the finiteness concerns the isometries themselves, not just their images of $x$. Dimension zero is included.

IsCrystallographicGroup. For any natural number $d$ and any subgroup $G$ of the group of bijective real affine isometries of $\mathbb R^d$, this proposition requires both of the following: for every $x\in\mathbb R^d$ and every real $\varepsilon>0$, the set $\{g\in G:\operatorname{dist}(g(x),x)\leq\varepsilon\}$ is finite; and there exists a real-linearly independent family $(v_i)_{i\in\{0,\ldots,d-1\}}$ of vectors in $\mathbb R^d$ such that, for every index $i$, some $g\in G$ satisfies $g(x)=x+v_i$ for every $x\in\mathbb R^d$. The second requirement is the field named cocompact. When $d=0$, the family is empty, its linear independence holds, and the requirement for each index is vacuous.

CrystallographicGroup. For every natural number $d$, this defines the type of subgroups $G$ of the bijective real affine isometries of $\mathbb R^d$, together with evidence that they satisfy these two conditions: for every point $x$ and every real $\varepsilon>0$, only finitely many $g\in G$ satisfy $\operatorname{dist}(g(x),x)\leq\varepsilon$; and there exist $d$ real-linearly independent vectors $v_i$ such that each map $x\mapsto x+v_i$ belongs to $G$. Dimension zero is included, with an empty family of vectors and no translation requirements from that family.

IsOrientationPreservingIsom. For any natural number $d$ and any bijective real affine isometry $g$ of $\mathbb R^d$, this predicate means that the real determinant of the linear part of $g$ is strictly positive. There is no condition on its translation part. When $d=0$, the determinant is $1$, so the predicate holds.

AffinelyEquivalent. For any natural number $d$ and any two subgroups $G_1,G_2$ of the bijective real affine isometries of $\mathbb R^d$, this predicate means that there exists a bijective real affine map $\varphi:\mathbb R^d\to\mathbb R^d$ such that $\{\varphi\circ g\circ\varphi^{-1}:g\in G_1\}=\{g:g\in G_2\}$ as sets of bijective affine maps. The map $\varphi$ need not be an isometry and has no determinant-sign restriction. Neither subgroup is assumed to satisfy any discreteness or translation condition. Dimension zero is included.

AffOPEquivalent. For any natural number $d$ and any two subgroups $G_1,G_2$ of the bijective real affine isometries of $\mathbb R^d$, this predicate means that there exists a bijective real affine map $\varphi:\mathbb R^d\to\mathbb R^d$ whose linear part has strictly positive real determinant and for which $\{\varphi\circ g\circ\varphi^{-1}:g\in G_1\}=\{g:g\in G_2\}$ as sets of bijective affine maps. The map $\varphi$ need not preserve distances, and the elements of $G_1$ and $G_2$ are not required to have positive determinant. Neither subgroup is assumed discrete or required to contain specified translations. Dimension zero is included, where the determinant restriction holds automatically.

crystallographicCount. For every natural number $d$, let $\mathcal C_d$ be the type of subgroups $G$ of the bijective real affine isometries of $\mathbb R^d$ satisfying both: for every $x\in\mathbb R^d$ and real $\varepsilon>0$, the set $\{g\in G:\operatorname{dist}(g(x),x)\leq\varepsilon\}$ is finite; and $G$ contains the translations by each vector in some real-linearly independent family of $d$ vectors. This definition assigns the extended natural cardinality of the set of subsets $S\subseteq\mathcal C_d$ for which there exists $G_0\in\mathcal C_d$ such that $S$ consists exactly of those $H\in\mathcal C_d$ for which some bijective real affine map $\varphi$ satisfies $\{\varphi\circ g\circ\varphi^{-1}:g\in G_0\}=\{h:h\in H\}$. There is no determinant restriction on $\varphi$. Distinct subsets are counted, rather than choices of representatives or conjugating maps; the value is $\infty$ if there are infinitely many such subsets, and $0$ if there are none. Dimension zero is included, where the family of translation vectors is empty.

crystallographicCountOP. For every natural number $d$, let $\mathcal C_d$ be the type of subgroups $G$ of the bijective real affine isometries of $\mathbb R^d$ such that, for every point $x$ and real $\varepsilon>0$, only finitely many $g\in G$ satisfy $\operatorname{dist}(g(x),x)\leq\varepsilon$, and such that $G$ contains translations by all vectors in some real-linearly independent family of $d$ vectors. This definition assigns the extended natural cardinality of the set of subsets $S\subseteq\mathcal C_d$ for which there exists $G_0\in\mathcal C_d$ such that $S$ consists exactly of those $H\in\mathcal C_d$ satisfying $\{\varphi\circ g\circ\varphi^{-1}:g\in G_0\}=\{h:h\in H\}$ for some bijective real affine map $\varphi$ with strictly positive determinant of its linear part. Group elements themselves have no determinant-sign restriction. Distinct subsets are counted, not representatives or maps; infinitely many subsets give $\infty$, and no subsets give $0$. Dimension zero is included, with an empty translation family and determinant $1$ for the conjugating map.

crystallographicCountOPOnly. For every natural number $d$, let $\mathcal C_d^+$ be the type of subgroups $G$ of the bijective real affine isometries of $\mathbb R^d$ satisfying all three conditions: for every $x$ and every real $\varepsilon>0$, the set $\{g\in G:\operatorname{dist}(g(x),x)\leq\varepsilon\}$ is finite; $G$ contains translations by every vector in some real-linearly independent family of $d$ vectors; and every $g\in G$ has strictly positive determinant of its linear part. This definition assigns the extended natural cardinality of the set of subsets $S\subseteq\mathcal C_d^+$ for which there exists $G_0\in\mathcal C_d^+$ such that $S$ consists exactly of those $H\in\mathcal C_d^+$ for which some bijective real affine map $\varphi$ with strictly positive determinant of its linear part satisfies $\{\varphi\circ g\circ\varphi^{-1}:g\in G_0\}=\{h:h\in H\}$. Distinct subsets are counted, not representatives or conjugating maps; the value is $\infty$ for infinitely many subsets and $0$ for none. Dimension zero is included, where the translation family is empty and all the determinant conditions hold with determinant $1$.