Discreteness of the translation subgroup: if the translation subgroup acts freely on a nonempty open alcove $C$ by genuine additive translations, then there is a uniform lower bound $\varepsilon > 0$ on the norm of every nontrivial translation vector $w \cdot 0$.
Existence of a compact fundamental domain for the translation subgroup: with finite linear-part group and a closed-alcove cover by $W$, the union $Y = \bigcup_{\bar w} \bar w \cdot \overline C$ is compact and is hit by every $W_T$-orbit. This realises $E / W_T$ as a torus quotient.
Cleanup of exists_compact_fundamental_domain: dropping the explicit
stabiliser-surjection hypothesis by using the unconditional surjection
W.stabilizer_surjects_unconditional.
Translation elements act by addition: any $w$ in the kernel of the linear-part homomorphism is a genuine translation $y \mapsto y + w(0)$.
Every alcove is nonempty, since it is connected by definition.
For an essential indecomposable affine reflection group, at least one alcove exists: the connected component of any point in the complement of the locally finite hyperplane arrangement.
Alcoves are open in $E$: each point of $C$ has a small ball avoiding every hyperplane locally near it, and the union with $C$ is connected and still in the complement, hence is contained in $C$ by maximality.
A nontrivial translation cannot map an alcove to itself: $C$ and $w(C)$ are disjoint for $w \neq 1$ in the translation subgroup. The proof uses the boundedness of the simplicial alcove against the iterated translates.
The "normal direction" of an affine hyperplane: the 1-dimensional submodule spanned by its normal vector. Two parallel hyperplanes share the same normal direction.
Instances For
For every hyperplane $\eta$ in the arrangement, the translation subgroup contains a translation whose vector pairs with $\eta.\mathrm{normal}$ to $-\eta.\mathrm{offset}$, i.e. moves the parallel-through-zero hyperplane onto $\eta$.
Using the translation produced by translation_lattice_covers_offset, every
hyperplane $\eta$ can be mapped to the parallel-through-the-origin hyperplane by
some $g \in W$.
For each hyperplane $\eta$ in the arrangement, there is another hyperplane $\eta'$ in the arrangement parallel to $\eta$ (normals are nonzero scalar multiples) and passing through the origin.
Existence of a special point: in an essential indecomposable affine reflection group, the origin is a special point of the arrangement.
Two hyperplanes with nonzero scalar-multiple normals have the same normal direction.
Finiteness of parallelism classes: in an essential indecomposable affine reflection group, the set of normal directions of hyperplanes in the arrangement is finite. Each parallelism class contains a representative through any given special point, and local finiteness of the arrangement bounds these.
If an affine isometry $g$ maps the carrier of $\eta$ bijectively to that of $\eta'$, then the linear part sends vectors orthogonal to $\eta.\mathrm{normal}$ to vectors orthogonal to $\eta'.\mathrm{normal}$.
Inner-product characterisation of $\mathrm{span}\{a\}$: if every vector orthogonal to $a$ is also orthogonal to $b$, then $b \in \mathrm{span}\{a\}$.
The linear-part group permutes the set of normal directions of the hyperplane arrangement: $\bar w(\mathrm{normalDirection}(\eta))$ is again the normal direction of some hyperplane in the arrangement.
An isometry that fixes the line $\mathbb R n$ sends $n$ to either $n$ or $-n$, since $|a| = 1$ for the scalar $a$ with $\bar w n = a n$.
The linear part of an affine reflection $s$ across $\eta$ fixes every vector orthogonal to the normal of $\eta$.
A consequence of essentiality: a vector orthogonal to every hyperplane normal is zero, since the only $\bar W$-invariant vector is $0$.
If an isometry sends $n_1$ to $\varepsilon_1 n_1$ and $n_2$ to $\varepsilon_2 n_2$ with $\varepsilon_i \in \{\pm 1\}$ and $\varepsilon_1 \neq \varepsilon_2$, then $n_1 \perp n_2$.
The linear-isometry part of an affine isometry that pointwise fixes $\eta$ fixes every vector orthogonal to $\eta.\mathrm{normal}$.
Reconstruction formula: if $s$ fixes $p$, then $s(x) = s_{\mathrm{lin}}(x-p)+p$.
If $s$ fixes $\eta'$ and the two normals $\eta.\mathrm{normal}$ and $\eta'.\mathrm{normal}$ are orthogonal, then $s$ preserves the inner product $\langle \eta.\mathrm{normal}, \cdot\rangle$.
If the linear part of $s$ fixes $y - x$, then $s$ translates $x$ to $y$ by the same vector: $s(y) = s(x) + (y - x)$.
Two affine reflections whose hyperplane normals are orthogonal commute: this is the classical commutativity criterion $s_{\eta_1} s_{\eta_2} = s_{\eta_2} s_{\eta_1}$ when $\eta_1 \perp \eta_2$.
An affine reflection group is NegIdFree if the linear-part group does not
contain the negation $-\mathrm{id}_E$. This rules out the "$\bar W = \{\pm 1\}$"
degeneracy that would obstruct faithfulness of $\bar W$ on normal directions.
Instances
Direct restatement of the NegIdFree axiom in the presence of the standard
essential / indecomposable / rank $\ge 2$ hypotheses.
If $\bar w$ sends every hyperplane normal to its negative, then $\bar w = -\mathrm{id}_E$
on the span of the normals; combined with essentiality this gives $\bar w = -\mathrm{id}_E$
everywhere, contradicting NegIdFree.
Sign-consistency under indecomposability: if $\bar w$ sends each hyperplane normal to $\pm \mathrm{normal}$, then by the indecomposability hypothesis (using that the $+$-reflections and $-$-reflections must commute and partition the reflections) all signs must be $+$.
Faithfulness of $\bar W$ on normal directions: in the NegIdFree, essential,
indecomposable, rank $\ge 2$ setting, if $\bar w$ fixes every normal direction
setwise, then $\bar w = 1$.
Finiteness of the linear-part group $\bar W$: with NegIdFree, essentiality,
indecomposability, and rank $\ge 2$, the linear-part group $\bar W$ injects into
the finite group of permutations of normal directions, hence is finite.
Each alcove has compact closure: its closure is contained in the convex hull of finitely many vertices (the alcove being a simplex).
Every point of $E$ is in the closure of some alcove: this is a key step toward the cover-by-translates theorem, using a small ball around $x$ avoiding the locally finite hyperplane union and a segment argument to find a nearby point in the complement.
The affine reflection group acts transitively on alcoves: for any two alcoves $C, D$ there exists $w \in W$ with $w(D) = C$.
Cover-by-translates: $W$-translates of $\overline C$ cover $E$. Every $x \in E$ has some $w \in W$ such that $w^{-1}(x) \in \overline C$.
Proposition 12.4: the translation subgroup of an essential indecomposable affine reflection group is discrete, i.e. there is a positive lower bound on the norm of any nontrivial translation vector. This is the central discreteness statement supporting the semi-direct product decomposition.
For an affine Weyl group, the parallel-through-origin hyperplane of any arrangement hyperplane $\eta$ is itself in the arrangement (it corresponds to the integer offset $k = 0$ for the root $\alpha = \eta.\mathrm{normal}$).
The origin is a special point of the affine Weyl group: for each hyperplane $\eta$ there is a parallel hyperplane in the arrangement passing through $0$.
Extensionality for affine hyperplanes: two affine hyperplanes are equal iff
their normal and offset fields agree.
The affine arrangement $\{H_{\alpha,k} : \alpha \in \Phi, k \in \mathbb Z\}$ is locally finite: around any point $x$, only finitely many hyperplanes meet the unit ball, because $|k - \langle \alpha, x \rangle| < \|\alpha\| + 1$ bounds $k$ to a finite range for each fixed root $\alpha$ in the finite root set.
The (finite) Weyl group $W$ normalizes the coroot lattice $\Lambda(\Phi^\vee)$: this is the structural input to the semi-direct product decomposition $W_a = \Lambda(\Phi^\vee) \rtimes W$.
Convenience restatement of AffineWeylGroupData.weylGroup_normalizes_corootLattice
for the bundled AffineWeylGroup $Wa$.
Package an affine Weyl group $Wa$ (together with compatible full-data
$dFull$) as an AffineWeylSemidirectData, providing the data needed to express
the semi-direct product $W_a = \Lambda(\Phi^\vee) \rtimes W$.
Instances For
Section 12.4 main result: the affine Weyl subgroup is isomorphic, as a group, to the semi-direct product $\Lambda(\Phi^\vee) \rtimes W$.