Documentation

Atlas.Buildings.code.AffineCoxeter.TitsConeConvexity

noncomputable def TitsCone.wordAction {B : Type u_1} (M : CoxeterMatrix B) (ws : List B) (y : B) :
B

The iterated dual-sigma word action: applying $\sigma_{s_1}^* \sigma_{s_2}^* \cdots$ in left-to-right order. This is the "co-action" version of the reflection action.

Instances For
    @[simp]
    theorem TitsCone.wordAction_nil {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (y : B) :

    The empty word acts as the identity.

    theorem TitsCone.wordAction_cons {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (ws : List B) (y : B) :
    wordAction M (s :: ws) y = wordAction M ws (dualSigma M s y)

    Cons step: prepending $s$ to the word means first applying the dual sigma at $s$.

    theorem TitsCone.wordAction_append {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (ws₁ ws₂ : List B) (y : B) :
    wordAction M (ws₁ ++ ws₂) y = wordAction M ws₂ (wordAction M ws₁ y)

    Concatenation: the word action is the composition $\sigma^*_{ws_2} \circ \sigma^*_{ws_1}$.

    theorem TitsCone.wordAction_singleton {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (y : B) :

    Singleton word action: $\sigma^*_s$ applied to $y$.

    theorem TitsCone.wordAction_reverse_cancel {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (ws : List B) (y : B) :
    wordAction M ws.reverse (wordAction M ws y) = y

    Applying the reverse word cancels: $\sigma^*_{\overline{ws}} \circ \sigma^*_{ws} = \mathrm{id}$.

    theorem TitsCone.wordAction_cancel_reverse {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (ws : List B) (y : B) :
    wordAction M ws (wordAction M ws.reverse y) = y

    Symmetric cancellation: $\sigma^*_{ws} \circ \sigma^*_{\overline{ws}} = \mathrm{id}$.

    theorem TitsCone.dualSigma_linear {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (a b : ) (x y : B) :
    (dualSigma M s fun (t : B) => a * x t + b * y t) = fun (t : B) => a * dualSigma M s x t + b * dualSigma M s y t

    $\sigma^*_s$ is $\mathbb{R}$-linear in the input.

    theorem TitsCone.wordAction_linear {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (ws : List B) (a b : ) (x y : B) :
    (wordAction M ws fun (t : B) => a * x t + b * y t) = fun (t : B) => a * wordAction M ws x t + b * wordAction M ws y t

    The iterated word action is $\mathbb{R}$-linear: composition of linear maps.

    theorem TitsCone.titsConeSet_wordAction_closed {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (ws : List B) (x : B) (hx : x titsConeSet M) :

    The Tits cone is closed under the dual word action: $\sigma^*_w$ sends $\mathcal U$ to itself.

    theorem TitsCone.dualSigma_fixed_on_wall {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (ν : B) ( : ν s = 0) :
    dualSigma M s ν = ν

    The simple reflection $\sigma_s^*$ fixes any vector lying on the wall $\nu_s = 0$.

    theorem TitsCone.dualSigma_sigma_transpose {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (y v : B) :
    t : B, dualSigma M s y t * v t = t : B, y t * CoxeterGroup.sigma M s v t

    Transpose identity: $\langle \sigma_s^* y, v\rangle = \langle y, \sigma_s v\rangle$, expressing that $\sigma$ and $\sigma^*$ are mutually adjoint.

    theorem TitsCone.wordAction_transpose {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (ws : List B) (y : B) (s : B) :
    wordAction M ws y s = t : B, y t * CoxeterGroup.wordSigma M ws (CoxeterGroup.e s) t

    Coordinate formula via transpose: $(\sigma^*_w y)(s) = \sum_t y_t \cdot (\sigma_w e_s)_t$.

    theorem TitsCone.wordAction_eq_of_wordProd_eq {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (ws₁ ws₂ : List B) (h : M.toCoxeterSystem.wordProd ws₁ = M.toCoxeterSystem.wordProd ws₂) (y : B) :
    wordAction M ws₁ y = wordAction M ws₂ y

    The word action depends only on the group element $\mathrm{wordProd}(ws)$, not on the word: two words representing the same Coxeter group element induce the same dual word action.

    theorem TitsCone.isRightDescent_of_wordAction_neg {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (ws : List B) (y : B) (hy : ∀ (t : B), y t 0) (s : B) (hneg : wordAction M ws y s < 0) :

    Descent detection: if the dual word action sends a nonnegative vector to a vector with a negative $s$-coordinate, then $s$ is a right descent of the group element $\mathrm{wordProd}(ws)$.

    theorem TitsCone.exchange_condition {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (ws : List B) (y : B) :
    (∀ (s : B), y s 0)∀ (s : B), wordAction M ws y s < 0∃ (ws' : List B) (y' : B), ws'.length < ws.length (∀ (s : B), y' s 0) dualSigma M s (wordAction M ws y) = wordAction M ws' y'

    Geometric exchange condition: when $(\sigma^*_w y)(s) < 0$ for $y \ge 0$, the vector $\sigma_s^*(\sigma^*_w y)$ can be re-expressed via a shorter word $ws'$, shrinking word length via the strong exchange property.

    noncomputable def TitsCone.wallParam {B : Type u_1} (x μ : B) (neg_set : Finset B) (hne : neg_set.Nonempty) (hx : ∀ (s : B), x s 0) ( : sneg_set, μ s < 0) :

    The wall parameter $t_0 = \min_{s \in \mathrm{neg\_set}} \frac{x_s}{x_s - \mu_s}$: the smallest $t \in [0,1]$ for which the convex combination $(1-t)x + t\mu$ reaches the wall $\{z : z_s = 0\}$ for some $s$.

    Instances For
      theorem TitsCone.wallParam_le_ratio {B : Type u_1} [DecidableEq B] [Fintype B] (x μ : B) (neg_set : Finset B) (hne : neg_set.Nonempty) (hx : ∀ (s : B), x s 0) ( : sneg_set, μ s < 0) (s : B) (hs : s neg_set) :
      wallParam x μ neg_set hne hx x s / (x s - μ s)

      The wall parameter is the minimum over the negative set, so it bounds each individual ratio.

      theorem TitsCone.wallParam_eq_some_ratio {B : Type u_1} [DecidableEq B] [Fintype B] (x μ : B) (neg_set : Finset B) (hne : neg_set.Nonempty) (hx : ∀ (s : B), x s 0) ( : sneg_set, μ s < 0) :
      s₀neg_set, wallParam x μ neg_set hne hx = x s₀ / (x s₀ - μ s₀)

      The wall parameter is attained: some $s_0 \in \mathrm{neg\_set}$ realises the minimum ratio $x_{s_0} / (x_{s_0} - \mu_{s_0})$.

      theorem TitsCone.wallParam_nonneg {B : Type u_1} [DecidableEq B] [Fintype B] (x μ : B) (neg_set : Finset B) (hne : neg_set.Nonempty) (hx : ∀ (s : B), x s 0) ( : sneg_set, μ s < 0) :
      0 wallParam x μ neg_set hne hx

      The wall parameter is nonnegative, since each individual ratio is.

      theorem TitsCone.wallParam_le_one {B : Type u_1} [DecidableEq B] [Fintype B] (x μ : B) (neg_set : Finset B) (hne : neg_set.Nonempty) (hx : ∀ (s : B), x s 0) ( : sneg_set, μ s < 0) :
      wallParam x μ neg_set hne hx 1

      The wall parameter lies in $[0, 1]$: for each $s$ in the negative set $x_s / (x_s - \mu_s) \le 1$ since $\mu_s < 0$.

      theorem TitsCone.wallPoint_nonneg {B : Type u_1} [DecidableEq B] [Fintype B] (x μ : B) (neg_set : Finset B) (hne : neg_set.Nonempty) (hx : ∀ (s : B), x s 0) (hμ_neg : sneg_set, μ s < 0) (hμ_pos : sneg_set, μ s 0) (s' : B) :
      have t₀ := wallParam x μ neg_set hne hx hμ_neg; (1 - t₀) * x s' + t₀ * μ s' 0

      The wall point $(1-t_0)\,x + t_0\,\mu$ at the wall parameter has nonnegative coordinates at every $s'$: at indices in the negative set the choice of $t_0$ keeps the coordinate $\ge 0$; at others both summands are nonnegative.

      theorem TitsCone.wallPoint_zero {B : Type u_1} [DecidableEq B] [Fintype B] (x μ : B) (neg_set : Finset B) (hne : neg_set.Nonempty) (hx : ∀ (s : B), x s 0) (hμ_neg : sneg_set, μ s < 0) :
      s₀neg_set, have t₀ := wallParam x μ neg_set hne hx hμ_neg; (1 - t₀) * x s₀ + t₀ * μ s₀ = 0

      The wall point hits zero at the minimising index: some $s_0$ has wall-point coordinate equal to $0$.

      theorem TitsCone.convex_closure_titsCone {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (n : ) (ws : List B) :
      ws.length n∀ (y : B), (∀ (s : B), y s 0)∀ (x : B), (∀ (s : B), x s 0)∀ (a b : ), 0 a0 ba + b = 1(fun (t : B) => a * x t + b * wordAction M ws y t) titsConeSet M

      Strong induction on word length: any convex combination of $x \in \mathcal D_0$ and $\sigma^*_w y$ (with $y$ nonneg) lies in the Tits cone. This is the key step of convexity; the wall-parameter / exchange-condition machinery shrinks $|w|$.

      theorem TitsCone.convex_closure_titsCone_bounded {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (n : ) (ws : List B) :
      ws.length n∀ (y : B), (∀ (s : B), y s 0)∀ (x : B), (∀ (s : B), x s 0)∀ (a b : ), 0 a0 ba + b = 1∃ (ws' : List B) (y' : B), (∀ (s : B), y' s 0) ws'.length n (fun (t : B) => a * x t + b * wordAction M ws y t) = wordAction M ws' y'

      Bounded version of convex_closure_titsCone: not only does the convex combination lie in $\mathcal U$, but it is realised as $\sigma^*_{ws'} y'$ with word length bounded by the input bound $n$.

      The Tits cone $\mathcal U \subset (B \to \mathbb R)$ is convex.

      theorem TitsCone.dualSigma_smul {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (c : ) (x : B) :
      (dualSigma M s fun (t : B) => c * x t) = fun (t : B) => c * dualSigma M s x t

      Scalar compatibility of $\sigma^*_s$: $\sigma^*_s(c \cdot x) = c \cdot \sigma^*_s(x)$.

      theorem TitsCone.wordAction_smul {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (ws : List B) (c : ) (x : B) :
      (wordAction M ws fun (t : B) => c * x t) = fun (t : B) => c * wordAction M ws x t

      Scalar compatibility of the iterated word action: $\sigma^*_w(c \cdot x) = c \cdot \sigma^*_w(x)$.

      theorem TitsCone.titsConeSet_cone {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (x : B) (hx : x titsConeSet M) (c : ) (hc : 0 c) :

      The Tits cone $\mathcal U$ is closed under nonnegative scaling: if $x \in \mathcal U$ and $c \ge 0$ then $c \cdot x \in \mathcal U$.

      theorem TitsCone.fundamental_domain_existence {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (x : B) (hx : x titsConeSet M) :
      ∃ (ws : List B), ytitsFundamentalClosure M, x = wordAction M ws y

      Existence in the fundamental domain: every $x \in \mathcal U$ is $\sigma^*_w$-image of some $y$ in the closed fundamental chamber $\overline{C}$.

      def TitsCone.wordFace {B : Type u_1} (M : CoxeterMatrix B) (ws : List B) (I : Finset B) :
      Set (B)

      The face $w \cdot F_I = \sigma^*_w(F_I)$: image of the standard face indexed by $I \subseteq S$ under the word action of $w$.

      Instances For
        theorem TitsCone.segment_word_length_bounded {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (x μ : B) (hx : x titsConeSet M) ( : μ titsConeSet M) :
        ∃ (N : ), ∀ (t : ), 0 tt 1∃ (ws : List B) (y : B), (∀ (s : B), y s 0) ws.length N (fun (s : B) => (1 - t) * x s + t * μ s) = wordAction M ws y

        Uniform bound: along the segment $[x, \mu] \subset \mathcal U$, every point can be written as $\sigma^*_w(y)$ for $y \ge 0$ with $|w|$ bounded by a fixed $N$ depending only on $x, \mu$.

        theorem TitsCone.segment_finite_face_covering {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (x μ : B) (hx : x titsConeSet M) ( : μ titsConeSet M) :
        ∃ (N : ), ∀ (z : B), (∃ (t : ), 0 t t 1 z = fun (s : B) => (1 - t) * x s + t * μ s)∃ (ws : List B) (I : Finset B), ws.length N z wordFace M ws I

        The segment $[x, \mu]$ is covered by finitely many faces $w \cdot F_I$ with $|w|$ bounded by a constant $N$ depending only on the endpoints.

        theorem TitsCone.face_intersection_property {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (ws : List B) (I J : Finset B) :
        (wordFace M ws I titsFaceDual M J).NonemptyI = J ytitsFaceDual M I, wordAction M ws y = y

        Face intersection rigidity: if $w \cdot F_I \cap F_J \ne \emptyset$ then $I = J$ and $w$ fixes $F_I$ pointwise. This is the key combinatorial property of the face decomposition of $\mathcal U$.

        theorem TitsCone.closure_mem_face {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (y : B) (hy : y titsFundamentalClosure M) :
        y titsFaceDual M {s : B | y s = 0}

        Every point of the closed fundamental chamber lies on the face $F_I$ where $I$ is its zero-coordinate set $\{s : y_s = 0\}$.

        theorem TitsCone.fundamental_domain_uniqueness {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (y₁ y₂ : B) :
        y₁ titsFundamentalClosure My₂ titsFundamentalClosure M∀ (ws : List B), wordAction M ws y₂ = y₁y₁ = y₂

        Uniqueness in the fundamental domain: if $y_1, y_2 \in \overline{C}$ and $\sigma^*_w(y_2) = y_1$ for some $w$, then $y_1 = y_2$. Combined with existence, this shows $\overline{C}$ is a strict fundamental domain for the $W$-action on $\mathcal U$.

        theorem TitsCone.titsCone_segment_finite_faces {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (x μ : B) (hx : x titsConeSet M) ( : μ titsConeSet M) :
        {F : Set (B) | (∃ (ws : List B) (I : Finset B), F = wordFace M ws I) tSet.Icc 0 1, (fun (s : B) => (1 - t) * x s + t * μ s) F}.Finite

        Local finiteness of the face stratification along a segment: a segment $[x,\mu] \subset \mathcal U$ meets only finitely many faces $w \cdot F_I$.

        theorem TitsCone.titsCone_main_theorem {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) :
        Convex (titsConeSet M) (∀ xtitsConeSet M, ∀ (c : ), 0 cc x titsConeSet M) (∀ xtitsConeSet M, ∃ (ws : List B), ytitsFundamentalClosure M, x = wordAction M ws y) (∀ (y₁ y₂ : B), y₁ titsFundamentalClosure My₂ titsFundamentalClosure M∀ (ws : List B), wordAction M ws y₂ = y₁y₁ = y₂) (∀ (ws : List B) (I J : Finset B), (wordFace M ws I titsFaceDual M J).NonemptyI = J ytitsFaceDual M I, wordAction M ws y = y) ∀ (x μ : B), x titsConeSet Mμ titsConeSet M∃ (N : ), ∀ (z : B), (∃ (t : ), 0 t t 1 z = fun (s : B) => (1 - t) * x s + t * μ s)∃ (ws : List B) (I : Finset B), ws.length N z wordFace M ws I

        Main theorem on the Tits cone $\mathcal U$. Bundles convexity, cone closure under nonnegative scaling, existence and uniqueness of the closed fundamental chamber $\overline{C}$, the face intersection rigidity property, and uniform finiteness of the face covering on any segment.