def AffineCoxeterFaces.affineReflectionHyperplane {B : Type u_1} [Fintype B] (M : CoxeterMatrix B) (v₀ : B → ℝ) (s : B) : Set (B → ℝ)

The affine reflection hyperplane $H_{s} \cap E$ obtained by intersecting the Coxeter wall $H_s = \{x : x_s = 0\}$ with the affine hyperplane $E = \{x : \langle v_0, x\rangle = 1\}$.

def AffineCoxeterFaces.affineHyperplaneSystem {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [inst : TitsCone.RootSystemData M] (v₀ : B → ℝ) : Set (Set (B → ℝ))

The arrangement of affine reflection hyperplanes in $E$: one hyperplane $\{y : \langle\alpha, y\rangle = 0\} \cap E$ for each positive root $\alpha \in \Phi^+$.

theorem AffineCoxeterFaces.zero_not_mem_affineHyperplane {B : Type u_1} [DecidableEq B] [Fintype B] [Nonempty B] (M : CoxeterMatrix B) (v₀ : B → ℝ) (hv₀_pos : ∀ (s : B), v₀ s > 0) : 0 ∉ affineHyperplane M v₀

The origin $0$ does not lie on the affine hyperplane $E = \{x : \sum_s v_0(s) x_s = 1\}$ when $v_0 > 0$, since the equation evaluates to $0 \ne 1$ at $x = 0$.

theorem AffineCoxeterFaces.ne_zero_of_mem_affineHyperplane {B : Type u_1} [DecidableEq B] [Fintype B] [Nonempty B] (M : CoxeterMatrix B) (v₀ : B → ℝ) (hv₀_pos : ∀ (s : B), v₀ s > 0) (x : B → ℝ) (hx : x ∈ affineHyperplane M v₀) : x ≠ 0

Corollary: any point on the affine hyperplane $E$ is nonzero.

theorem AffineCoxeterFaces.mem_titsCone_sdiff_zero_of_mem_E {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) (x : B → ℝ) (hx : x ∈ affineHyperplane M v₀) : x ∈ TitsCone.titsConeSet M \ {0}

The affine hyperplane $E$ lies inside $\mathcal U \setminus \{0\}$ when $v_0$ is in the radical of the Coxeter form; i.e. $E \subseteq \mathcal U \setminus \{0\}$.

def AffineCoxeterFaces.affineFace {B : Type u_1} [Fintype B] (M : CoxeterMatrix B) (v₀ : B → ℝ) (I : Finset B) : Set (B → ℝ)

The affine face of type $I \subseteq B$: intersection of the Tits face $F_I$ with the affine hyperplane $E$.

def AffineCoxeterFaces.affineFundamentalChamber {B : Type u_1} [Fintype B] (M : CoxeterMatrix B) (v₀ : B → ℝ) : Set (B → ℝ)

The affine fundamental chamber $C \cap E$: the strict fundamental chamber for $W$ acting on $E$.

theorem AffineCoxeterFaces.affine_reflection_group_chamber {B : Type u_1} [DecidableEq B] [Fintype B] [Nonempty B] (M : CoxeterMatrix B) [inst : 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) (x : B → ℝ) : x ∈ affineFundamentalChamber M v₀ → ∀ α ∈ TitsCone.RootSystemData.Φpos M, TitsCone.pairing α x ≠ 0

Points in the open affine fundamental chamber $C \cap E$ lie strictly off every reflecting hyperplane: $\langle \alpha, x \rangle \ne 0$ for all $\alpha \in \Phi^+$.

theorem AffineCoxeterFaces.chambers_compact_closure {B : Type u_1} [DecidableEq B] [Fintype B] [Nonempty B] (M : CoxeterMatrix B) [inst : 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) : IsCompact (closure (affineFundamentalChamber M v₀))

In the affine case the closed fundamental chamber $\overline{C \cap E}$ is compact (this is what justifies calling the action "cocompact").

def AffineCoxeterFaces.vertexMapToE {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (v₀ : B → ℝ) (s₀ : B) : Set (B → ℝ)

The vertex of $\overline{C \cap E}$ opposite to the wall $H_{s_0}$: the codimension-$(|B|-1)$ face $F_{\{s_0\}^c} \cap E$.

theorem AffineCoxeterFaces.geometric_realization_homeomorphism {B : Type u_1} [DecidableEq B] [Fintype B] [Nonempty B] (M : CoxeterMatrix B) [inst : 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) (x : B → ℝ) : x ∈ affineHyperplane M v₀ → ∃! I : Finset B, x ∈ affineFace M v₀ I

Every point of $E$ lies on a unique affine face $F_I \cap E$: the affine faces partition $E$, realizing the geometric Coxeter complex as a stratification of the affine hyperplane.

def AffineCoxeterFaces.affineFaceLE {B : Type u_1} [Fintype B] (M : CoxeterMatrix B) (v₀ : B → ℝ) (I J : Finset B) : Prop

Face order: $I \le J$ means the affine face $F_J \cap E$ is contained in the closure of $F_I \cap E$, i.e. $F_J \cap E$ is a face of $F_I \cap E$.