theorem affineWeylGroup_locallyFinite {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylGroupFullData E) : d.affineArr.IsLocallyFinite

Proposition 12.5 (i): the affine hyperplane arrangement $\{H_{α,k}\}$ associated to a crystallographic root system is locally finite.

theorem affineWeylGroup_semidirectProduct {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylGroupFullData E) : (∀ α ∈ d.roots, ∀ (k : ℤ) (v : E), ∃ t ∈ d.corootLattice, d.affineReflFun α k v = d.linearReflFun α v + t) ∧ (∀ w ∈ d.weylGroup, ∀ v ∈ d.corootLattice, w v ∈ d.corootLattice) ∧ ∀ (w : E ≃ₗᵢ[ℝ] E) (t : E), (∀ (v : E), w v = v + t) → t = 0 ∧ w = 1

Proposition 12.5 (ii): the affine Weyl group has the semidirect-product structure $W_a = W ⋉ Λ(\check Φ)$ — every affine reflection is a linear reflection plus a coroot translation, $W$ stabilizes the coroot lattice, and the linear-part kernel is trivial.

theorem affineWeylGroup_stable {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylGroupFullData E) : (∀ v ∈ d.corootLattice, ∀ η ∈ d.affineArr.hyperplanes, ∃ η' ∈ d.affineArr.hyperplanes, η'.normal = η.normal ∧ ∀ (x : E), x ∈ η'.carrier ↔ x - v ∈ η.carrier) ∧ ∀ w ∈ d.weylGroup, ∀ η ∈ d.affineArr.hyperplanes, ∃ η' ∈ d.affineArr.hyperplanes, η'.normal = w η.normal ∧ η'.offset = η.offset

Proposition 12.5 (iii): the affine arrangement is stable under coroot translations and under the linear Weyl group.

theorem coroot_translation_eq_composition {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylGroupFullData E) (α : E) (hα : α ∈ d.roots) (v : E) : v + d.coroot α = d.affineReflFun α 1 (d.affineReflFun α 0 v)

Translation by $\check α$ equals the composition $s_{α,1} \circ s_{α,0}$ of two affine reflections.