structure AffineWeylGroupFullData (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] extends AffineWeylGroupData E : Type u_2

Full data for the affine Weyl group $W_a = W ⋉ Λ(\check Φ)$ in an inner product space $E$: a finite reduced root system, the coroot map $\check α = (2/⟨α,α⟩) α$, the coroot lattice, crystallographic integrality, stability of roots under $W$, and integrality of coroot-lattice pairings with roots.

• roots : Set E
• roots_ne_zero (α : E) : α ∈ self.roots → α ≠ 0
• roots_reduced (α : E) : α ∈ self.roots → ∀ (t : ℝ), t • α ∈ self.roots → t = 1 ∨ t = -1
• weylGroup : Subgroup (E ≃ₗᵢ[ℝ] E)
• corootLattice : AddSubgroup E
• weylGroup_stable_corootLattice (w : E ≃ₗᵢ[ℝ] E) : w ∈ self.weylGroup → ∀ v ∈ self.corootLattice, w v ∈ self.corootLattice
• roots_finite : self.roots.Finite
• coroot : E → E
• coroot_def (α : E) : α ∈ self.roots → self.coroot α = (2 / inner ℝ α α) • α
• coroot_mem_lattice (α : E) : α ∈ self.roots → self.coroot α ∈ self.corootLattice
• crystallographic (α : E) : α ∈ self.roots → ∀ β ∈ self.roots, ∃ (n : ℤ), inner ℝ (self.coroot α) β = ↑n
• weylGroup_stable_roots (w : E ≃ₗᵢ[ℝ] E) : w ∈ self.weylGroup → ∀ α ∈ self.roots, w α ∈ self.roots
• corootLattice_int (α : E) : α ∈ self.roots → ∀ v ∈ self.corootLattice, ∃ (m : ℤ), inner ℝ v α = ↑m

def AffineWeylGroupFullData.affineArr {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylGroupFullData E) : HyperplaneArrangement E

Shorthand for the underlying affine hyperplane arrangement of the affine Weyl data.

theorem AffineWeylGroupFullData.affineHyperplane_ext {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (h1 h2 : AffineHyperplane E) (hn : h1.normal = h2.normal) (ho : h1.offset = h2.offset) : h1 = h2

Two affine hyperplanes are equal if their normals and offsets match.

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

Section 12.5 of the textbook: the affine hyperplane arrangement $\{H_{α,k} : α ∈ Φ, k ∈ ℤ\}$ is locally finite — around every point only finitely many walls accumulate.

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

Translation by an element of the coroot lattice carries any affine wall to another wall with the same normal direction.

theorem AffineWeylGroupFullData.stable_weylGroup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylGroupFullData E) (w : E ≃ₗᵢ[ℝ] E) : w ∈ d.weylGroup → ∀ η ∈ d.affineArr.hyperplanes, ∃ η' ∈ d.affineArr.hyperplanes, η'.normal = w η.normal ∧ η'.offset = η.offset

The finite Weyl group $W$ permutes affine walls, sending $H_{α,k}$ to $H_{wα,k}$.

def AffineWeylGroupFullData.affineReflFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylGroupFullData E) (α : E) (k : ℤ) (v : E) : E

Formula for the affine reflection across $H_{α,k}$: $s_{α,k}(v) = v - (⟨α,v⟩ - k) \check α$.

def AffineWeylGroupFullData.linearReflFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylGroupFullData E) (α v : E) : E

Formula for the linear reflection through the hyperplane perpendicular to $α$: $s_α(v) = v - ⟨α,v⟩ \check α$.

theorem AffineWeylGroupFullData.affineRefl_eq_translation_comp_linearRefl {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylGroupFullData E) (α : E) (hα : α ∈ d.roots) (k : ℤ) (v : E) : d.affineReflFun α k v = d.linearReflFun α v + ↑k • d.coroot α

$s_{α,k}(v) = s_α(v) + k · \check α$: the affine reflection factors as the linear reflection followed by translation by $k \check α$.

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

Translation by $\check α$ realized as a composition of two affine reflections: $v + \check α = s_{α,1}(s_α(v))$.

theorem AffineWeylGroupFullData.semidirect_product_affineWeylGroup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylGroupFullData E) (α : E) : α ∈ d.roots → ∀ (k : ℤ) (v : E), ∃ t ∈ d.corootLattice, d.affineReflFun α k v = d.linearReflFun α v + t

Semidirect-product structure: every affine reflection decomposes as a linear reflection composed with translation by an element of $Λ(\check Φ)$.

theorem AffineWeylGroupFullData.linear_inter_translation_trivial {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (w : E ≃ₗᵢ[ℝ] E) (t : E) (h : ∀ (v : E), w v = v + t) : t = 0 ∧ w = 1

The intersection of the linear part group with the translation subgroup is trivial: if $w v = v + t$ for all $v$, then $t = 0$ and $w = 1$.

theorem AffineWeylGroupFullData.weylGroup_normalizes_lattice {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylGroupFullData E) (w : E ≃ₗᵢ[ℝ] E) : w ∈ d.weylGroup → ∀ v ∈ d.corootLattice, w v ∈ d.corootLattice

Restatement of the axiom that the Weyl group stabilizes the coroot lattice.

theorem AffineWeylGroupFullData.reflection_involutive {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] (η : AffineHyperplane E) : η.reflectionMap * η.reflectionMap = 1

Reflection across any affine hyperplane is an involution.

theorem AffineWeylGroupFullData.linearRefl_eq_affineRefl_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylGroupFullData E) (α v : E) : d.linearReflFun α v = d.affineReflFun α 0 v

The linear reflection coincides with the affine reflection across $H_{α,0}$.

theorem AffineWeylGroupFullData.affineReflFun_involutive {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylGroupFullData E) (α : E) (hα : α ∈ d.roots) (k : ℤ) (v : E) : d.affineReflFun α k (d.affineReflFun α k v) = v

Affine reflection $s_{α,k}$ is involutive: $s_{α,k}^2 = \mathrm{id}$.

theorem AffineWeylGroupFullData.affineReflFun_fixed_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylGroupFullData E) (α : E) (hα : α ∈ d.roots) (k : ℤ) (v : E) : d.affineReflFun α k v = v ↔ inner ℝ α v = ↑k

The fixed-point set of $s_{α,k}$ is exactly the hyperplane $⟨α, v⟩ = k$.

theorem AffineWeylGroupFullData.affineWeylGroup_uniqueDecomposition {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (w₁ w₂ : E ≃ₗᵢ[ℝ] E) (t₁ t₂ : E) (h : ∀ (v : E), w₁ v + t₁ = w₂ v + t₂) : w₁ = w₂ ∧ t₁ = t₂

Uniqueness of the semidirect decomposition: if $w_1 v + t_1 = w_2 v + t_2$ for all $v ∈ E$, then $w_1 = w_2$ and $t_1 = t_2$.

theorem AffineWeylGroupFullData.corootTranslation_eq_comp_affineRefls {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 α$ is the composition of two affine reflections $s_{α,1} \circ s_{α,0}$.

theorem AffineWeylGroupFullData.neg_corootTranslation_eq_comp_affineRefls {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 α$ is the composition $s_{α,-1} \circ s_{α,0}$.

theorem AffineWeylGroupFullData.reflections_generate_affineWeylGroup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (d : AffineWeylGroupFullData E) : (∀ α ∈ d.roots, ∀ (v : E), d.linearReflFun α v = d.affineReflFun α 0 v) ∧ (∀ α ∈ d.roots, ∀ (v : E), v + d.coroot α = d.affineReflFun α 1 (d.affineReflFun α 0 v)) ∧ (∀ α ∈ d.roots, ∀ (v : E), v - d.coroot α = d.affineReflFun α (-1) (d.affineReflFun α 0 v)) ∧ ∀ α ∈ d.roots, ∀ (k : ℤ) (v : E), d.affineReflFun α k v = d.linearReflFun α v + ↑k • d.coroot α

The affine Weyl group $W_a$ is generated by affine reflections: linear reflections $s_α$ equal $s_{α,0}$, translations by $±\check α$ are products of two affine reflections, and every affine reflection factors as a linear reflection composed with translation.

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

Proposition 12.5 (first part): the affine hyperplane arrangement is locally finite.

theorem AffineWeylGroupFullData.proposition_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 (second part): the semidirect-product structure $W_a = W ⋉ Λ(\check Φ)$ — every affine reflection decomposes as linear part plus a coroot translation, $W$ normalizes the coroot lattice, and the kernel of the linear-part map is trivial.

theorem AffineWeylGroupFullData.proposition_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 (third part): the affine arrangement is stable under translation by the coroot lattice and under the action of the linear Weyl group.