Affine simple-reflection reduction

This file supplies the affine Coxeter reduction input isolated in AffineReductionData. A positive k-inversion count gives an adjacent descent of the inverse permutation. Simultaneously swapping that adjacent pair in every residue-period removes exactly one normalized inversion class.

def Bananas.affineReflectionSupport (k : ℕ) (i : ℤ) : Set ℤ

The support of the affine simple reflection indexed by i modulo k.

Equations

• Bananas.affineReflectionSupport k i = {n : ℤ | ↑k ∣ n - i}

@[simp]

theorem Bananas.mem_affineReflectionSupport_iff (k : ℕ) (i n : ℤ) : n ∈ affineReflectionSupport k i ↔ ↑k ∣ n - i

theorem Bananas.affineReflectionSupport_noConsecutive (k : ℕ) (hk : 2 ≤ k) (i : ℤ) : Transpositions.NoConsecutive (affineReflectionSupport k i)

theorem Bananas.affineReflectionSupport_congr (k : ℕ) (i : ℤ) {l₁ l₂ : ℤ} (h₁ : l₁ ∈ affineReflectionSupport k i) (h₂ : l₂ ∈ affineReflectionSupport k i) : ↑k ∣ l₂ - l₁

noncomputable def Bananas.affineReflection (k : ℕ) (i : ℤ) (hk : 2 ≤ k) : AspPerm

The ASP permutation implementing one affine simple reflection.

Equations

• Bananas.affineReflection k i hk = Transpositions.sigma (Bananas.affineReflectionSupport k i) ⋯

theorem Bananas.affineReflection_apply_of_mem (k : ℕ) (i : ℤ) (hk : 2 ≤ k) {n : ℤ} (hn : n ∈ affineReflectionSupport k i) : (affineReflection k i hk).func n = n + 1

theorem Bananas.affineReflection_apply_of_pred_mem (k : ℕ) (i : ℤ) (hk : 2 ≤ k) {n : ℤ} (hn : n - 1 ∈ affineReflectionSupport k i) : (affineReflection k i hk).func n = n - 1

theorem Bananas.affineReflection_apply_of_neither (k : ℕ) (i : ℤ) (hk : 2 ≤ k) {n : ℤ} (hn : n ∉ affineReflectionSupport k i) (hpred : n - 1 ∉ affineReflectionSupport k i) : (affineReflection k i hk).func n = n

theorem Bananas.affineReflection_inversion_iff (k : ℕ) (i : ℤ) (hk : 2 ≤ k) {a b : ℤ} (hab : a < b) : (affineReflection k i hk).func b < (affineReflection k i hk).func a ↔ a ∈ affineReflectionSupport k i ∧ b = a + 1

theorem Bananas.affineReflection_isKAffine (k : ℕ) (i : ℤ) (hk : 2 ≤ k) : IsKAffine k (affineReflection k i hk).func

theorem Bananas.IsKAffine.aspPerm_inv {k : ℕ} {β : AspPerm} (hβ : IsKAffine k β.func) : IsKAffine k β⁻¹.func

theorem Bananas.kInversionCount_affineReflection_le_one (k : ℕ) (i : ℤ) (hk : 2 ≤ k) : kInversionCount k (affineReflection k i hk).func ≤ 1

A single periodic affine simple reflection has at most one normalized inversion class.

def Bananas.affineExceptionalInversions (k : ℕ) (i : ℤ) (β : AspPerm) : Set (ℤ × ℤ)

The normalized inversion class removed by a chosen affine left descent.

Equations

• Bananas.affineExceptionalInversions k i β = {p : ℤ × ℤ | p ∈ Bananas.kInversions k β.func ∧ β.func p.2 ∈ Bananas.affineReflectionSupport k i ∧ β.func p.1 = β.func p.2 + 1}

theorem Bananas.kInversionCount_left_mul_affineReflection_add_one {k : ℕ} {β : AspPerm} (hβ : IsKAffine k β.func) (i : ℤ) (hk : 2 ≤ k) (hi : β⁻¹.func (i + 1) < β⁻¹.func i) : kInversionCount k (affineReflection k i hk * β).func + 1 = kInversionCount k β.func

theorem Bananas.exists_affineReflection_reduction {k : ℕ} {β : AspPerm} (hβ : IsKAffine k β.func) (hpos : 0 < kInversionCount k β.func) : ∃ (i : ℤ) (hk : 2 ≤ k) (β' : AspPerm), β = affineReflection k i hk ⋆ β' ∧ IsKAffine k β'.func ∧ kInversionCount k β'.func + 1 = kInversionCount k β.func

A positive affine inversion count admits a direct reduction by one periodic affine simple reflection. This is the concrete version of the AffineReductionData.reduce field; exposing the residue index is useful when the other factor in a Demazure product must be compared with the same reflection.

theorem Bananas.affineReductionData (k : ℕ) : AffineReductionData k

The affine simple-reflection reduction required by Proposition 6.13.

theorem Bananas.sci_star_le (k : ℕ) (α β : AspPerm) (hβ : IsKAffine k β.func) (hbudget : ↑(sci α.func) + ↑(kInversionCount k β.func) < ↑k) : ↑(sci (α ⋆ β).func) ≤ ↑(sci α.func) + ↑(kInversionCount k β.func)

Paper Proposition 6.13 (prop:sciInvStar), with the affine Coxeter reduction discharged unconditionally.