theorem AffineReflectionGroup.translationSubgroup_normal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) : (W.TranslationSubgroup.subgroupOf W.group).Normal

The translation subgroup $T \subseteq W$ is normal in the affine Weyl group $W$.

def AffineReflectionGroup.Stabilizer {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (x : E) : Subgroup (E ≃ᵃⁱ[ℝ] E)

The stabilizer subgroup $W_x = \{g \in W : g \cdot x = x\}$ of a point $x \in E$.

theorem AffineReflectionGroup.stabilizer_le_group {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (x : E) : W.Stabilizer x ≤ W.group

The stabilizer $W_x$ is a subgroup of $W$.

theorem AffineReflectionGroup.stabilizer_surjects_unconditional {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (x : E) (hx : W.SpecialPoint x) (wbar : E ≃ₗᵢ[ℝ] E) : wbar ∈ W.LinearPartGroup → ∃ g ∈ W.Stabilizer x, linearPartHom g = wbar

The linear part map sends the stabilizer $W_x$ surjectively onto the finite linear part group $\overline W$: for any $\overline w \in \overline W$ there is $g \in W_x$ with linear part $\overline w$. This is the key surjectivity used in the semidirect-product decomposition.

theorem AffineReflectionGroup.semidirect_product_decomposition {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (x : E) (hx : W.SpecialPoint x) (hgen : ∀ wbar ∈ W.LinearPartGroup, ∃ g ∈ W.Stabilizer x, linearPartHom g = wbar) (w : E ≃ᵃⁱ[ℝ] E) : w ∈ W.group → ∃ t ∈ W.TranslationSubgroup, ∃ s ∈ W.Stabilizer x, w = t * s

Semidirect product decomposition $W = T \rtimes W_x$: every $w \in W$ factors uniquely as $w = t \cdot s$ with $t \in T$ a translation and $s \in W_x$ a stabilizer element of a special point $x$.

theorem AffineReflectionGroup.semidirect_product_decomposition_unconditional {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (x : E) (hx : W.SpecialPoint x) (w : E ≃ᵃⁱ[ℝ] E) : w ∈ W.group → ∃ t ∈ W.TranslationSubgroup, ∃ s ∈ W.Stabilizer x, w = t * s

Unconditional form of the semidirect product decomposition $W = T \rtimes W_x$: combines semidirect_product_decomposition with the surjectivity stabilizer_surjects_unconditional.