noncomputable def linearPartHom {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : (E ≃ᵃⁱ[ℝ] E) →* E ≃ₗᵢ[ℝ] E

The monoid homomorphism sending an affine isometry equivalence to its linear part.

structure AffineReflectionGroup (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] : Type u_2

An affine reflection group on $E$ consists of a subgroup of affine isometries together with a locally finite hyperplane arrangement that is stable under the group, with each hyperplane realized as the fixed set of a non-trivial reflection in the group; the group is generated by these reflections, and parallel reflecting hyperplanes give the same linear part.

• group : Subgroup (E ≃ᵃⁱ[ℝ] E)
• arrangement : HyperplaneArrangement E
• locallyFinite : self.arrangement.IsLocallyFinite
• stable (g : E ≃ᵃⁱ[ℝ] E) : g ∈ self.group → ∀ η ∈ self.arrangement.hyperplanes, ∃ η' ∈ self.arrangement.hyperplanes, ∀ (x : E), g x ∈ η'.carrier ↔ x ∈ η.carrier
• has_reflection (η : AffineHyperplane E) : η ∈ self.arrangement.hyperplanes → ∃ s ∈ self.group, (∀ y ∈ η.carrier, s y = y) ∧ s * s = 1 ∧ s ≠ 1
• generated_by_reflections : self.group = Subgroup.closure {s : E ≃ᵃⁱ[ℝ] E | s ∈ self.group ∧ ∃ η ∈ self.arrangement.hyperplanes, (∀ y ∈ η.carrier, s y = y) ∧ s * s = 1}
• parallel_reflections_same_linear_part (s₁ : E ≃ᵃⁱ[ℝ] E) : s₁ ∈ self.group → ∀ s₂ ∈ self.group, ∀ η₁ ∈ self.arrangement.hyperplanes, ∀ η₂ ∈ self.arrangement.hyperplanes, (∀ y ∈ η₁.carrier, s₁ y = y) → s₁ * s₁ = 1 → (∀ y ∈ η₂.carrier, s₂ y = y) → s₂ * s₂ = 1 → (∃ (t : ℝ), η₂.normal = t • η₁.normal) → linearPartHom s₁ = linearPartHom s₂

def AffineReflectionGroup.Alcove {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) : Type u_1

An alcove is a chamber of the underlying hyperplane arrangement.

def AffineReflectionGroup.GoodPoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (x : E) : Prop

A point $x$ is good if it lies in the complement of every reflecting hyperplane.

def AffineReflectionGroup.SpecialPoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (x : E) : Prop

A point $x$ is special if for every hyperplane $η$ of the arrangement there is a parallel hyperplane $η'$ in the arrangement passing through $x$.

noncomputable def AffineReflectionGroup.LinearPartGroup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) : Subgroup (E ≃ₗᵢ[ℝ] E)

The linear part subgroup is the image of $W$ under the linear-part homomorphism.

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

The translation subgroup of $W$: those elements with trivial linear part.

def AffineReflectionGroup.IsEssential {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) : Prop

The group $W$ is essential if its linear part has no nonzero fixed vector.

def AffineReflectionGroup.IsIndecomposable {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) : Prop

The group $W$ is indecomposable if its set of reflections cannot be partitioned into two pairwise-commuting nonempty subsets.

def AffineReflectionGroup.openHalfSpaceIntersection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (n : ℕ) (normals : Fin (n + 1) → E) (offsets : Fin (n + 1) → ℝ) : Set E

Intersection of $n+1$ open half-spaces $\{x : ⟨n_i, x⟩ > c_i\}$.

theorem AffineReflectionGroup.chamber_eq_halfspace_inter_of_locally_finite {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (arr : HyperplaneArrangement E) (hlf : arr.IsLocallyFinite) (C : arr.Chamber) : ∃ (m : ℕ) (normals : Fin (m + 1) → E) (offsets : Fin (m + 1) → ℝ), C.set = ⋂ (i : Fin (m + 1)), {x : E | inner ℝ (normals i) x > offsets i}

Any chamber of a locally finite hyperplane arrangement is an intersection of finitely many open half-spaces.

theorem AffineReflectionGroup.alcove_eq_open_halfspace_inter {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (A : W.Alcove) : ∃ (m : ℕ) (normals : Fin (m + 1) → E) (offsets : Fin (m + 1) → ℝ), A.set = openHalfSpaceIntersection m normals offsets

Every alcove is a finite intersection of open half-spaces.

def AffineReflectionGroup.separatingHyperplanes {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (C D : W.arrangement.Chamber) : Set (AffineHyperplane E)

The set of hyperplanes of the arrangement that separate two chambers $C$ and $D$.

theorem AffineReflectionGroup.reflection_of_wall_chamber {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (C D : W.arrangement.Chamber) (s : E ≃ᵃⁱ[ℝ] E) (hs_mem : s ∈ W.group) (η : AffineHyperplane E) (hη : η ∈ W.arrangement.hyperplanes) (hwall : η.IsWall C.set) (hfix : ∀ y ∈ η.carrier, s y = y) (hinv : s * s = 1) (hne_id : s ≠ 1) (hsep : HyperplaneArrangement.SeparatesChambers η hη C D) : ∃ (D' : W.arrangement.Chamber), (∀ x ∈ C.set, s x ∈ D'.set) ∧ (W.separatingHyperplanes D' D).ncard < (W.separatingHyperplanes C D).ncard

If $s$ is the reflection in a wall $η$ of chamber $C$, and $η$ separates $C$ from $D$, then $s$ sends $C$ into some chamber $D'$ that is strictly closer to $D$ in the sense of having fewer separating hyperplanes.

theorem AffineReflectionGroup.wall_separation_step {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (C D : W.arrangement.Chamber) (hne : C.set ≠ D.set) : ∃ (s : E ≃ᵃⁱ[ℝ] E) (_ : s ∈ W.group) (η : AffineHyperplane E) (_ : η ∈ W.arrangement.hyperplanes) (_ : η.IsWall C.set) (_ : ∀ y ∈ η.carrier, s y = y) (_ : s * s = 1) (D' : W.arrangement.Chamber), (∀ x ∈ C.set, s x ∈ D'.set) ∧ (W.separatingHyperplanes D' D).ncard < (W.separatingHyperplanes C D).ncard

Wall-separation reduction step: given two distinct chambers $C ≠ D$, there exists a wall-reflection of $C$ that sends $C$ to some chamber $D'$ with strictly fewer separating hyperplanes from $D$.

theorem AffineReflectionGroup.hyperplane_carrier_interior_empty {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (η : AffineHyperplane E) : interior η.carrier = ∅

The interior of an affine hyperplane is empty.

theorem AffineReflectionGroup.hyperplane_carrier_isClosed {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (η : AffineHyperplane E) : IsClosed η.carrier

Every affine hyperplane is a closed subset of $E$.

theorem AffineReflectionGroup.finite_iUnion_empty_interior {X : Type u_2} [TopologicalSpace X] (S : Finset (Set X)) (hclosed : ∀ s ∈ S, IsClosed s) (hint : ∀ s ∈ S, interior s = ∅) : interior (⋃ s ∈ S, s) = ∅

A finite union of closed sets with empty interior has empty interior (Baire-type fact).

theorem AffineReflectionGroup.exists_generic_point_on_hyperplane {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (η : AffineHyperplane E) (hη : η ∈ W.arrangement.hyperplanes) : ∃ z₀ ∈ η.carrier, ∀ η' ∈ W.arrangement.hyperplanes, η'.carrier ≠ η.carrier → z₀ ∉ η'.carrier

There exists a generic point on $η$ that lies on no other hyperplane of the arrangement.

theorem AffineReflectionGroup.half_ball_in_one_chamber {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (arr : HyperplaneArrangement E) (η : AffineHyperplane E) (hη : η ∈ arr.hyperplanes) (z₀ : E) (hz₀ : z₀ ∈ η.carrier) (hz₀_generic : ∀ η' ∈ arr.hyperplanes, η'.carrier ≠ η.carrier → z₀ ∉ η'.carrier) (δ : ℝ) (hδ : 0 < δ) (hδ_small : ∀ η' ∈ arr.hyperplanes, η'.carrier ≠ η.carrier → Metric.ball z₀ δ ∩ η'.carrier = ∅) : ∃ (C : arr.Chamber), Metric.ball z₀ δ ∩ η.positiveHalfSpace ⊆ C.set

A small half-ball $B(z_0, δ) ∩ η^+$ around a generic point of $η$ lies in a single chamber.

theorem AffineReflectionGroup.hyperplane_is_wall_of_some_chamber {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (η : AffineHyperplane E) (hη : η ∈ W.arrangement.hyperplanes) : ∃ (D : W.arrangement.Chamber), η.IsWall D.set

Every hyperplane $η$ of the arrangement is a wall of at least one chamber.

theorem AffineReflectionGroup.conjugate_wall_reflection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (C D : W.arrangement.Chamber) (w : E ≃ᵃⁱ[ℝ] E) (hw : w ∈ W.group) (hw_maps : ∀ x ∈ C.set, w x ∈ D.set) (s : E ≃ᵃⁱ[ℝ] E) (hs : s ∈ W.group) (η : AffineHyperplane E) (hη : η ∈ W.arrangement.hyperplanes) (hη_wall : η.IsWall D.set) (hs_fix : ∀ y ∈ η.carrier, s y = y) (hs_inv : s * s = 1) : w⁻¹ * s * w ∈ Subgroup.closure {t : E ≃ᵃⁱ[ℝ] E | t ∈ W.group ∧ ∃ ζ ∈ W.arrangement.hyperplanes, ζ.IsWall C.set ∧ (∀ y ∈ ζ.carrier, t y = y) ∧ t * t = 1}

Conjugating a wall reflection of $D$ by an element $w$ taking $C → D$ lies in the subgroup generated by wall reflections of $C$.

theorem AffineReflectionGroup.conjugate_in_wall_closure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (C : W.arrangement.Chamber) (s : E ≃ᵃⁱ[ℝ] E) (hs_group : s ∈ W.group) (hs_wall : ∃ η ∈ W.arrangement.hyperplanes, η.IsWall C.set ∧ (∀ y ∈ η.carrier, s y = y) ∧ s * s = 1) (D' : W.arrangement.Chamber) (hs_maps : ∀ x ∈ C.set, s x ∈ D'.set) (w' : E ≃ᵃⁱ[ℝ] E) (hw' : w' ∈ Subgroup.closure {t : E ≃ᵃⁱ[ℝ] E | t ∈ W.group ∧ ∃ η ∈ W.arrangement.hyperplanes, η.IsWall D'.set ∧ (∀ y ∈ η.carrier, t y = y) ∧ t * t = 1}) : s * w' * s ∈ Subgroup.closure {t : E ≃ᵃⁱ[ℝ] E | t ∈ W.group ∧ ∃ η ∈ W.arrangement.hyperplanes, η.IsWall C.set ∧ (∀ y ∈ η.carrier, t y = y) ∧ t * t = 1}

The wall-reflection closure is stable under conjugation by a wall reflection $s$ of $C$ when $s$ maps $C$ to $D'$.

theorem AffineReflectionGroup.wall_closure_compose_step {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (C D D' : W.arrangement.Chamber) (s : E ≃ᵃⁱ[ℝ] E) (hs_group : s ∈ W.group) (hs_wall : ∃ η ∈ W.arrangement.hyperplanes, η.IsWall C.set ∧ (∀ y ∈ η.carrier, s y = y) ∧ s * s = 1) (hs_maps : ∀ x ∈ C.set, s x ∈ D'.set) (w' : E ≃ᵃⁱ[ℝ] E) (hw'_mem : w' ∈ Subgroup.closure {t : E ≃ᵃⁱ[ℝ] E | t ∈ W.group ∧ ∃ η ∈ W.arrangement.hyperplanes, η.IsWall D'.set ∧ (∀ y ∈ η.carrier, t y = y) ∧ t * t = 1}) (hw'_maps : ∀ x ∈ D'.set, w' x ∈ D.set) : ∃ w ∈ Subgroup.closure {t : E ≃ᵃⁱ[ℝ] E | t ∈ W.group ∧ ∃ η ∈ W.arrangement.hyperplanes, η.IsWall C.set ∧ (∀ y ∈ η.carrier, t y = y) ∧ t * t = 1}, ∀ x ∈ C.set, w x ∈ D.set

Composition step: combining a wall reflection $s : C → D'$ with an element $w' : D' → D$ in the wall closure of $D'$ produces an element in the wall closure of $C$ mapping $C → D$.

theorem AffineReflectionGroup.wall_closure_transitive_aux {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (n : ℕ) (A B : W.arrangement.Chamber) : (W.separatingHyperplanes A B).ncard = n → ∃ w ∈ Subgroup.closure {s : E ≃ᵃⁱ[ℝ] E | s ∈ W.group ∧ ∃ η ∈ W.arrangement.hyperplanes, η.IsWall A.set ∧ (∀ y ∈ η.carrier, s y = y) ∧ s * s = 1}, ∀ x ∈ A.set, w x ∈ B.set

Induction on the number of separating hyperplanes: for any two chambers $A,B$ there is an element of the wall-reflection closure of $A$ sending $A$ to $B$.

theorem AffineReflectionGroup.wall_closure_transitive_on_chambers {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (C D : W.arrangement.Chamber) : ∃ w ∈ Subgroup.closure {s : E ≃ᵃⁱ[ℝ] E | s ∈ W.group ∧ ∃ η ∈ W.arrangement.hyperplanes, η.IsWall C.set ∧ (∀ y ∈ η.carrier, s y = y) ∧ s * s = 1}, ∀ x ∈ C.set, w x ∈ D.set

The wall-reflection closure of a chamber $C$ acts transitively on chambers.

theorem AffineReflectionGroup.all_reflections_in_wall_closure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (C : W.arrangement.Chamber) : {s : E ≃ᵃⁱ[ℝ] E | s ∈ W.group ∧ ∃ η ∈ W.arrangement.hyperplanes, (∀ y ∈ η.carrier, s y = y) ∧ s * s = 1} ⊆ ↑(Subgroup.closure {s : E ≃ᵃⁱ[ℝ] E | s ∈ W.group ∧ ∃ η ∈ W.arrangement.hyperplanes, η.IsWall C.set ∧ (∀ y ∈ η.carrier, s y = y) ∧ s * s = 1})

Every reflection in $W$ belongs to the subgroup generated by the wall reflections of a fixed chamber $C$.

theorem AffineReflectionGroup.wall_reflections_generate_group {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (C : W.arrangement.Chamber) : W.group = Subgroup.closure {s : E ≃ᵃⁱ[ℝ] E | s ∈ W.group ∧ ∃ η ∈ W.arrangement.hyperplanes, η.IsWall C.set ∧ (∀ y ∈ η.carrier, s y = y) ∧ s * s = 1}

For any chamber $C$, the wall reflections of $C$ generate the whole group $W$.

theorem AffineReflectionGroup.linear_part_fixes_hyperplane_direction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (s : E ≃ᵃⁱ[ℝ] E) (η : AffineHyperplane E) (hs_fix : ∀ y ∈ η.carrier, s y = y) (hsp : s η.basePoint = η.basePoint) (v : E) : inner ℝ η.normal v = 0 → s.linearIsometryEquiv v = v

The linear part of an isometry fixing an affine hyperplane fixes every vector orthogonal to the hyperplane normal.

theorem AffineReflectionGroup.wall_normal_parallel_to_halfspace_normal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (A : W.Alcove) {m : ℕ} (normals : Fin (m + 1) → E) (offsets : Fin (m + 1) → ℝ) (hdesc : A.set = openHalfSpaceIntersection m normals offsets) (η : AffineHyperplane E) (hη_hyp : η ∈ W.arrangement.hyperplanes) (hη_wall : η.IsWall A.set) : ∃ (i : Fin (m + 1)) (c : ℝ), η.normal = c • normals i

If $A$ is described as the intersection of open half-spaces with given normals, then the normal of any wall of $A$ is parallel to one of these defining normals.

theorem AffineReflectionGroup.wall_normals_ortho_fixed {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (hess : W.IsEssential) (hind : W.IsIndecomposable) (A : W.Alcove) {m : ℕ} (normals : Fin (m + 1) → E) (offsets : Fin (m + 1) → ℝ) (hdesc : A.set = openHalfSpaceIntersection m normals offsets) (v : E) (hv : ∀ (i : Fin (m + 1)), inner ℝ v (normals i) = 0) (wbar : E ≃ₗᵢ[ℝ] E) : wbar ∈ W.LinearPartGroup → wbar v = v

A vector orthogonal to all defining normals of an alcove $A$ is fixed by every element of the linear part group $W̄$.

theorem AffineReflectionGroup.wall_normals_span_top {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (hess : W.IsEssential) (hind : W.IsIndecomposable) (A : W.Alcove) {m : ℕ} (normals : Fin (m + 1) → E) (offsets : Fin (m + 1) → ℝ) (hdesc : A.set = openHalfSpaceIntersection m normals offsets) : Submodule.span ℝ (Set.range normals) = ⊤

For an essential, indecomposable affine reflection group, the wall normals of any alcove span $E$.

noncomputable def AffineReflectionGroup.normalLinearCombinationMap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {m : ℕ} (normals : Fin (m + 1) → E) : (Fin (m + 1) → ℝ) →ₗ[ℝ] E

The linear-combination map sending coefficients $(c_i)$ to $\sum_i c_i n_i$.

theorem AffineReflectionGroup.indecomposable_normal_ker_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (hess : W.IsEssential) (hind : W.IsIndecomposable) (A : W.Alcove) {m : ℕ} (normals : Fin (m + 1) → E) (offsets : Fin (m + 1) → ℝ) (hdesc : A.set = openHalfSpaceIntersection m normals offsets) (hspan : Submodule.span ℝ (Set.range normals) = ⊤) : Module.finrank ℝ ↥(normalLinearCombinationMap normals).ker = 1

For an essential, indecomposable group, the kernel of the linear-combination map of the alcove normals is one-dimensional.

theorem AffineReflectionGroup.alcove_normals_finrank {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (hess : W.IsEssential) (hind : W.IsIndecomposable) (A : W.Alcove) {m : ℕ} (normals : Fin (m + 1) → E) (offsets : Fin (m + 1) → ℝ) (hdesc : A.set = openHalfSpaceIntersection m normals offsets) : Module.finrank ℝ E = m

If an alcove is bounded by $m+1$ half-spaces in an essential, indecomposable group, then $\dim E = m$.

theorem AffineReflectionGroup.alcove_normals_general_position {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (hess : W.IsEssential) (hind : W.IsIndecomposable) (A : W.Alcove) {m : ℕ} (normals : Fin (m + 1) → E) (offsets : Fin (m + 1) → ℝ) (hdesc : A.set = openHalfSpaceIntersection m normals offsets) (i : Fin (m + 1)) : LinearIndependent ℝ (normals ∘ i.succAbove)

Any $m$ of the $m+1$ alcove normals are linearly independent (general position).

theorem AffineReflectionGroup.alcove_halfspace_description {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (hess : W.IsEssential) (hind : W.IsIndecomposable) (A : W.Alcove) : ∃ (n : ℕ) (normals : Fin (n + 1) → E) (offsets : Fin (n + 1) → ℝ), Module.finrank ℝ E = n ∧ Submodule.span ℝ (Set.range normals) = ⊤ ∧ (∀ (i : Fin (n + 1)), LinearIndependent ℝ (normals ∘ i.succAbove)) ∧ A.set = openHalfSpaceIntersection n normals offsets

Full half-space description of an alcove: every alcove is bounded by $n+1$ hyperplanes whose normals span $E$ and are in general position, with $n = \dim E$.

theorem AffineReflectionGroup.spanning_halfspace_intersection_is_simplex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} {normals : Fin (n + 1) → E} {offsets : Fin (n + 1) → ℝ} (hdim : Module.finrank ℝ E = n) (hspan : Submodule.span ℝ (Set.range normals) = ⊤) (hgp : ∀ (i : Fin (n + 1)), LinearIndependent ℝ (normals ∘ i.succAbove)) (hne : (openHalfSpaceIntersection n normals offsets).Nonempty) : ∃ (vertices : Fin (n + 1) → E), openHalfSpaceIntersection n normals offsets = interior ((convexHull ℝ) (Set.range vertices)) ∧ AffineIndependent ℝ vertices

A nonempty intersection of $n+1$ open half-spaces in $n$-dimensional general position is the interior of an affine $n$-simplex.

theorem AffineReflectionGroup.alcove_is_simplex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (hess : W.IsEssential) (hind : W.IsIndecomposable) (A : W.Alcove) : ∃ (n : ℕ) (vertices : Fin (n + 1) → E), A.set = interior ((convexHull ℝ) (Set.range vertices)) ∧ AffineIndependent ℝ vertices

Every alcove of an essential, indecomposable affine reflection group is the interior of a simplex spanned by $n+1$ affinely independent vertices, where $n = \dim E$.

theorem AffineReflectionGroup.walls_finite {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (hess : W.IsEssential) (hind : W.IsIndecomposable) (C : W.arrangement.Chamber) : {η : AffineHyperplane E | η ∈ W.arrangement.hyperplanes ∧ η.IsWall C.set}.Finite

The set of walls of a single chamber is finite.

theorem AffineReflectionGroup.involutive_isometry_normal_eigenvalue {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E ≃ₗᵢ[ℝ] E) (n : E) (hn : n ≠ 0) (h_fix_hyp : ∀ (v : E), inner ℝ n v = 0 → f v = v) : f n = -n ∨ f n = n

A linear isometry fixing the orthogonal complement of $n$ acts on $n$ by $±1$.

theorem AffineReflectionGroup.reflection_fixes_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (s : E ≃ᵃⁱ[ℝ] E) (η : AffineHyperplane E) (hs_inv : s * s = 1) (hs_fix : ∀ y ∈ η.carrier, s y = y) (hs_ne : s ≠ 1) (x : E) : x ∈ η.carrier ↔ s x = x

A non-trivial involutive reflection fixing $η$ has fixed-point set exactly $η$.

theorem AffineReflectionGroup.chamber_exists {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (arr : HyperplaneArrangement E) (hlf : arr.IsLocallyFinite) : Nonempty arr.Chamber

Any locally finite hyperplane arrangement admits at least one chamber.

theorem AffineReflectionGroup.reflection_unique {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (s₁ s₂ : E ≃ᵃⁱ[ℝ] E) (η : AffineHyperplane E) (h₁_inv : s₁ * s₁ = 1) (h₁_fix : ∀ y ∈ η.carrier, s₁ y = y) (h₂_inv : s₂ * s₂ = 1) (h₂_fix : ∀ y ∈ η.carrier, s₂ y = y) (h₁_ne : s₁ ≠ 1) (h₂_ne : s₂ ≠ 1) : s₁ = s₂

The reflection across an affine hyperplane is unique: any two non-trivial involutions fixing the same hyperplane coincide.

theorem AffineReflectionGroup.is_coxeter_system {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (hess : W.IsEssential) (hind : W.IsIndecomposable) : ∃ (S : Finset (E ≃ᵃⁱ[ℝ] E)), (∀ s ∈ S, s ∈ W.group ∧ s * s = 1) ∧ Subgroup.closure ↑S = W.group ∧ ∀ s ∈ S, ∃ η ∈ W.arrangement.hyperplanes, ∀ (x : E), x ∈ η.carrier ↔ s x = x

Main result: an essential, indecomposable affine reflection group has a finite set $S$ of wall reflections of any chosen alcove that satisfies the defining property of a Coxeter system — each element is an involution in $W$, the set generates $W$, and each element is the unique reflection across some hyperplane of the arrangement.

def RootLattice {E : Type u_1} [NormedAddCommGroup E] (Φ : Set E) : Submodule ℤ E

The integer-linear span $\mathbb Z Φ$ of a set of roots $Φ$ is the root lattice.

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

Data underlying an affine Weyl group: a reduced root system $Φ$ in $E$, the linear Weyl subgroup, and a coroot lattice stable under the Weyl group.

• 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

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

The affine hyperplane arrangement $\{H_{α,k} : α ∈ Φ,\ k ∈ ℤ\}$ associated to the root system data.

theorem AffineReflectionGroup.goodPoint_iff_not_on_hyperplanes {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) (x : E) : W.GoodPoint x ↔ ∀ η ∈ W.arrangement.hyperplanes, x ∉ η.carrier

A point is good iff it lies on no hyperplane of the arrangement.

theorem AffineReflectionGroup.translationSubgroup_le_group {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (W : AffineReflectionGroup E) : W.TranslationSubgroup ≤ W.group

The translation subgroup is contained in $W$.

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

The pointwise stabilizer of $p ∈ E$ inside $W$.

structure AffineWeylGroup (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] : Type u_2

An affine Weyl group on $E$: a packaging of root-system data with a compatible affine reflection group whose arrangement is the affine arrangement $\{H_{α,k}\}$ and whose linear part equals the linear Weyl group.

• data : AffineWeylGroupData E
• reflGroup : AffineReflectionGroup E
• arrangement_eq : self.reflGroup.arrangement = self.data.affineArrangement
• linearPart_eq : self.reflGroup.LinearPartGroup = self.data.weylGroup

theorem AffineWeylGroup.IsAffineCoxeter {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Wa : AffineWeylGroup E) (hess : Wa.reflGroup.IsEssential) (hind : Wa.reflGroup.IsIndecomposable) : ∃ (S : Finset (E ≃ᵃⁱ[ℝ] E)), (∀ s ∈ S, s ∈ Wa.reflGroup.group ∧ s * s = 1) ∧ Subgroup.closure ↑S = Wa.reflGroup.group ∧ ∀ s ∈ S, ∃ η ∈ Wa.reflGroup.arrangement.hyperplanes, ∀ (x : E), x ∈ η.carrier ↔ s x = x

An essential, indecomposable affine Weyl group is an (affine) Coxeter system, generated by the finitely many wall reflections of an alcove.

theorem inner_root_specialPoint_int {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Wa : AffineWeylGroup E) (z : E) (hz : Wa.reflGroup.SpecialPoint z) (α : E) (hα : α ∈ Wa.data.roots) : ∃ (k : ℤ), inner ℝ α z = ↑k

For any special point $z$ and any root $α$, the pairing $⟨α, z⟩$ is an integer.