Documentation

Atlas.Buildings.code.AffineCoxeter.TitsConeCorollary

theorem TitsCone.continuous_pairing {B : Type u_1} [DecidableEq B] [Fintype B] (α : B) :
Continuous fun (x : B) => pairing α x

The pairing $x \mapsto \sum_s \alpha_s\, x_s$ is continuous in $x$, as a finite sum of continuous functions.

theorem TitsCone.isOpen_pairing_pos {B : Type u_1} [DecidableEq B] [Fintype B] (α : B) :
IsOpen {x : B | pairing α x > 0}

The open half-space $\{x : \langle \alpha, x\rangle > 0\}$ is open in $B \to \mathbb R$.

theorem TitsCone.sigma_fixes_radical {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (v₀ : B) (hv₀_rad : ∀ (t : B), u : B, v₀ u * CoxeterGroup.formVal M u t = 0) (s : B) :
CoxeterGroup.sigma M s v₀ = v₀

A radical vector $v_0$ (one satisfying $\sum_u v_0(u)\,B(e_u, e_t) = 0$ for all $t$) is fixed by every simple reflection $\sigma_s$ acting on the root space.

theorem TitsCone.sigmaWord_fixes_radical {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (v₀ : B) (hv₀_rad : ∀ (t : B), u : B, v₀ u * CoxeterGroup.formVal M u t = 0) (ws : List B) :
sigmaWord M ws v₀ = v₀

A radical vector is fixed by the iterated reflection action $\sigma_{ws}$ for any word $ws$, by induction on the length of $ws$.

theorem TitsCone.dualSigmaWord_preserves_radical_pairing {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [Nonempty B] [RootSystemData M] (v₀ : B) (hv₀_rad : ∀ (t : B), u : B, v₀ u * CoxeterGroup.formVal M u t = 0) (ws : List B) (x : B) :
pairing v₀ (dualSigmaWord M ws x) = pairing v₀ x

Pairing-invariance: the pairing with a radical vector $v_0$ is invariant under the dual word action, since $\sigma$ and its dual are mutually transpose.

theorem TitsCone.titsCone_sdiff_zero_radical_pairing_pos {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [Nonempty B] [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) (x : B) (hx : x titsConeSet M) (hx_ne : x 0) :
pairing v₀ x > 0

Forward direction: a nonzero point of the Tits cone has strictly positive pairing with any strictly-positive radical vector $v_0$.

theorem TitsCone.nonposRoots_pos_scale {B : Type u_1} [DecidableEq B] [Fintype B] (Φ : Set (B)) (x : B) (c : ) (hc : c > 0) :
(nonposRoots Φ fun (s : B) => c * x s) = nonposRoots Φ x

The set of nonpositive roots at $x$ is invariant under positive scaling of $x$, since the sign of $\langle \alpha, x\rangle$ is preserved.

theorem TitsCone.nuFiniteAt_of_radical_pairing_pos {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [Nonempty B] [inst : 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) (x : B) (hpair : pairing v₀ x > 0) :

Reverse direction: if $\langle v_0, x\rangle > 0$ then the nonpositive-roots set at $x$ is finite; we rescale to the hyperplane $\langle v_0, x'\rangle = 1$ and apply finiteness on that hyperplane.

theorem TitsCone.titsCone_sdiff_zero_eq_radical_pos {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [Nonempty B] [inst : 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) :
titsConeSet M \ {0} = {x : B | pairing v₀ x > 0}

Main characterisation: the Tits cone minus the origin equals the open half-space $\{x : \langle v_0, x\rangle > 0\}$ cut out by any strictly positive radical vector $v_0$ — this is the Perron–Frobenius corollary in the affine Coxeter setting.

theorem TitsCone.nuFiniteAt_of_mem_titsCone_sdiff_zero {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [Nonempty B] [inst : 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) (x : B) (hx : x titsConeSet M \ {0}) :

A nonzero point of the Tits cone has finitely many positive roots on which it is nonpositive — the nu-finiteness consequence of the previous theorem.

theorem TitsCone.zeroRoots_finite {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [Nonempty B] [inst : 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) (x : B) (hx : x titsConeSet M \ {0}) :

At a nonzero point $x$ of the Tits cone, only finitely many positive roots $\alpha$ satisfy $\langle \alpha, x\rangle = 0$ (a subset of the nu-finite set).

theorem TitsCone.locallyFinite_hyperplanes_pointwise {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [Nonempty B] [inst : 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) (x : B) (hx : x titsConeSet M \ {0}) :
{η : Set (B) | (∃ αRootSystemData.Φpos M, η = {y : B | pairing α y = 0}) x η}.Finite

Pointwise local finiteness of the root-hyperplane arrangement: at any nonzero point of the Tits cone, only finitely many root hyperplanes $\{\langle \alpha, y\rangle = 0\}$ pass through it.