def IsAffineCoxeter {B : Type u_1} [Fintype B] (M : CoxeterMatrix B) : Prop

A Coxeter matrix is of affine type if its bilinear form is indecomposable, positive semidefinite, and degenerate. Equivalently, it has Coxeter graph of affine Dynkin type.

def affineHyperplane {B : Type u_1} [Fintype B] (_M : CoxeterMatrix B) (v₀ : B → ℝ) : Set (B → ℝ)

The affine hyperplane $E = \{\mu : \langle v_0, \mu\rangle = 1\}$ on which the affine Weyl group acts. Here $v_0$ is the positive radical vector of the Coxeter form.

class TitsConeConvexity {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : Prop

Typeclass packaging the convexity of the Tits cone $\mathcal U$. Used locally to allow the affine criterion to be stated abstractly.

• convex (x y : B → ℝ) : x ∈ TitsCone.titsConeSet M → y ∈ TitsCone.titsConeSet M → ∀ (t : ℝ), 0 ≤ t → t ≤ 1 → (fun (s : B) => (1 - t) * x s + t * y s) ∈ TitsCone.titsConeSet M

instance titsConeConvexity_instance {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : TitsConeConvexity M

Default instance: convexity of $\mathcal U$ follows from titsConeSet_convex.

class ChamberChasingProperty {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : Prop

Typeclass packaging the chamber-chasing / orbit-density property: every point of the affine hyperplane $E$ lies on a segment between two points of the Tits cone.

• orbit_density (v₀ : B → ℝ) : (∀ (s : B), v₀ s > 0) → (∀ (t : B), ∑ u : B, v₀ u * CoxeterGroup.formVal M u t = 0) → IsAffineCoxeter M → ∀ x ∈ affineHyperplane M v₀, ∃ (p₁ : B → ℝ) (p₂ : B → ℝ) (t : ℝ), p₁ ∈ TitsCone.titsConeSet M ∧ p₂ ∈ TitsCone.titsConeSet M ∧ 0 ≤ t ∧ t ≤ 1 ∧ ∀ (s : B), x s = (1 - t) * p₁ s + t * p₂ s

theorem chamberChasingProperty_instance {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [TitsCone.RootSystemData M] : ChamberChasingProperty M

Default constructor: chamber-chasing follows from the local finiteness of nonposRoots and the characterization of the Tits cone in terms of $\nu$-finite points.

instance instChamberChasingPropertyOfRootSystemData {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [TitsCone.RootSystemData M] : ChamberChasingProperty M

Instance form of chamberChasingProperty_instance.

theorem pos_root_nonneg_coeff {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [TitsCone.RootSystemData M] (α : B → ℝ) (hα : α ∈ TitsCone.RootSystemData.Φpos M) (t : B) : α t ≥ 0

Every positive root has nonnegative coordinates in the simple-root basis: $\alpha_t \ge 0$ for $\alpha \in \Phi^+$. Proved by contradiction using a face $F_I$ test point.

theorem affineHyperplane_mem_titsCone_of_ne_zero {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [TitsCone.RootSystemData M] (v₀ : B → ℝ) (hv₀_pos : ∀ (s : B), v₀ s > 0) (hv₀_rad : ∀ (t : B), ∑ u : B, v₀ u * CoxeterGroup.formVal M u t = 0) (hAff : IsAffineCoxeter M) (x : B → ℝ) (hx : x ∈ affineHyperplane M v₀) (_hx_ne : x ≠ 0) : x ∈ TitsCone.titsConeSet M

Nonzero points on the affine hyperplane $E$ lie in the Tits cone $\mathcal U$: this is the "upward step" toward proving $E \subseteq \mathcal U$ for affine Coxeter systems.

theorem affine_nonposRoots_finite_of_level_bound {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [TitsCone.RootSystemData M] (v₀ : B → ℝ) (hv₀_pos : ∀ (s : B), v₀ s > 0) (hv₀_rad : ∀ (t : B), ∑ u : B, v₀ u * CoxeterGroup.formVal M u t = 0) (hAff : IsAffineCoxeter M) (x : B → ℝ) (hx : x ∈ affineHyperplane M v₀) (hx_ne : x ≠ 0) : (TitsCone.nonposRoots (TitsCone.RootSystemData.Φpos M) x).Finite

For affine Coxeter systems, the set of positive roots with $\langle \alpha, x\rangle \le 0$ is finite at any nonzero point $x$ of the affine hyperplane $E$.

theorem affine_nuFiniteAt {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [TitsCone.RootSystemData M] (v₀ : B → ℝ) (hv₀_pos : ∀ (s : B), v₀ s > 0) (hv₀_rad : ∀ (t : B), ∑ u : B, v₀ u * CoxeterGroup.formVal M u t = 0) (hAff : IsAffineCoxeter M) (x : B → ℝ) (hx : x ∈ affineHyperplane M v₀) (hx_ne : x ≠ 0) : TitsCone.nuFiniteAt (TitsCone.RootSystemData.Φpos M) x

Restatement: every nonzero point of $E$ is $\nu$-finite in $\Phi^+$.

theorem galleryChasingReflectsIntoFundClosure {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [TitsCone.RootSystemData M] (v₀ : B → ℝ) (hv₀_pos : ∀ (s : B), v₀ s > 0) (hv₀_rad : ∀ (t : B), ∑ u : B, v₀ u * CoxeterGroup.formVal M u t = 0) (hAff : IsAffineCoxeter M) (x : B → ℝ) (hx : x ∈ affineHyperplane M v₀) : ∃ (ws : List B), ∀ (s : B), TitsCone.wordAction M ws x s ≥ 0

Gallery chasing: any point of the affine hyperplane $E$ can be reflected into the closed fundamental chamber by a finite sequence of simple reflections.

theorem galleryChasingOrbitDensity {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [TitsCone.RootSystemData M] (v₀ : B → ℝ) (hv₀_pos : ∀ (s : B), v₀ s > 0) (hv₀_rad : ∀ (t : B), ∑ u : B, v₀ u * CoxeterGroup.formVal M u t = 0) (hAff : IsAffineCoxeter M) (x : B → ℝ) (hx : x ∈ affineHyperplane M v₀) : ∃ (p₁ : B → ℝ) (p₂ : B → ℝ) (t : ℝ), p₁ ∈ TitsCone.titsConeSet M ∧ p₂ ∈ TitsCone.titsConeSet M ∧ 0 ≤ t ∧ t ≤ 1 ∧ ∀ (s : B), x s = (1 - t) * p₁ s + t * p₂ s

Orbit density: every point of $E$ lies on a segment between two points of the Tits cone.

theorem galleryChasingReachesTitsCone {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [TitsCone.RootSystemData M] (v₀ : B → ℝ) (hv₀_pos : ∀ (s : B), v₀ s > 0) (hv₀_rad : ∀ (t : B), ∑ u : B, v₀ u * CoxeterGroup.formVal M u t = 0) (hAff : IsAffineCoxeter M) (x : B → ℝ) (hx : x ∈ affineHyperplane M v₀) : x ∈ TitsCone.titsConeSet M

Gallery chasing reaches the Tits cone: any point of $E$ is in $\mathcal U$. Combines orbit density with convexity of $\mathcal U$.

theorem affineHyperplane_subset_titsCone {B : Type u_1} [DecidableEq B] [Fintype B] [Nonempty B] (M : CoxeterMatrix B) [TitsCone.RootSystemData M] (hAff : IsAffineCoxeter M) (v₀ : B → ℝ) (hv₀_pos : ∀ (s : B), v₀ s > 0) (hv₀_rad : ∀ (t : B), ∑ u : B, v₀ u * CoxeterGroup.formVal M u t = 0) : affineHyperplane M v₀ ⊆ TitsCone.titsConeSet M

The affine criterion: in an affine Coxeter system, the affine hyperplane $E$ is entirely contained in the Tits cone $\mathcal U$. Equivalently, $W$ acts on $E$ as an affine reflection group.

theorem affineHyperplane_inter_titsCone_eq {B : Type u_1} [DecidableEq B] [Fintype B] [Nonempty B] (M : CoxeterMatrix B) [TitsCone.RootSystemData M] (hAff : IsAffineCoxeter M) (v₀ : B → ℝ) (hv₀_pos : ∀ (s : B), v₀ s > 0) (hv₀_rad : ∀ (t : B), ∑ u : B, v₀ u * CoxeterGroup.formVal M u t = 0) : affineHyperplane M v₀ ∩ TitsCone.titsConeSet M = affineHyperplane M v₀

Restatement of the affine criterion: $E \cap \mathcal U = E$.