Tableaux

This file relates Hecke factorizations of 321-avoiding ASP permutations to set-valued Young tableaux defined on the inversion set.

This material is not present in An extended Demazure product.

This file is largely experimental and is still under development. Use at your own risk.

Links and two-factor data

A Link packages the data needed to split a triangle-free ASP set into two pieces that behave like the two inversion-set components in a Demazure factorization. This section proves that such links are equivalent to two-factor factorizations.

def Tableaux.linked (A B : Set (ℤ × ℤ)) : Prop

Equations

• Tableaux.linked A B = ∀ p ∈ A, ∀ q ∈ B, p ≼ q → p = q

structure Tableaux.Link : Type

A decomposition of a triangle-free ASP set into two linked pieces, together with the shifts attached to the two factors.

• A : Set (ℤ × ℤ)
• B : Set (ℤ × ℤ)
• S : ASP321a.tfas
• χa : ℤ
• χb : ℤ
• union_eq : self.A ∪ self.B = self.S.I
• sep : linked self.A self.B

def Tableaux.link_of_sets {A B : Set (ℤ × ℤ)} (sep : linked A B) (tf : ASP321a.set_321a_prop (A ∪ B)) (χa χb : ℤ) : Link

Equations

• Tableaux.link_of_sets sep tf χa χb = { A := A, B := B, S := { I := A ∪ B, prop := ⋯, prop_321a := tf }, χa := χa, χb := χb, union_eq := ⋯, sep := sep }

def Tableaux.Link.chi (L : Link) : ℤ

Equations

• L.chi = L.χa + L.χb

theorem Tableaux.Link.B_subset (L : Link) : L.B ⊆ L.S.I

theorem Tableaux.Link.A_subset (L : Link) : L.A ⊆ L.S.I

theorem Tableaux.Link.mem_A_of_mem_inv_not_mem_B (L : Link) {p : ℤ × ℤ} (hpτ : p ∈ L.S.I) (hpB : p ∉ L.B) : p ∈ L.A

theorem Tableaux.Link.ext {L₁ L₂ : Link} (hA : L₁.A = L₂.A) (hB : L₁.B = L₂.B) (hχa : L₁.χa = L₂.χa) (hχb : L₁.χb = L₂.χb) : L₁ = L₂

theorem Tableaux.Link.B_AspSet_prop (L : Link) : AspSet_prop L.B

theorem Tableaux.Link.B_set_321a_prop (L : Link) : ASP321a.set_321a_prop L.B

def Tableaux.Link.B_AspSet (L : Link) : AspSet

Equations

• L.B_AspSet = { I := L.B, prop := ⋯ }

noncomputable def Tableaux.Link.τ (L : Link) : AspPerm

Equations

• L.τ = L.S.toAspPerm L.chi

@[simp]

theorem Tableaux.Link.inv_set_τ (L : Link) : inv_set L.τ.func = L.S.I

theorem Tableaux.Link.is_321a_τ (L : Link) : is_321a L.τ.func

@[simp]

theorem Tableaux.Link.chi_tau (L : Link) : L.τ.χ = L.chi

noncomputable def Tableaux.Link.β (L : Link) : AspPerm

Equations

• L.β = L.B_AspSet.toAspPerm L.χb

@[simp]

theorem Tableaux.Link.inv_set_β (L : Link) : inv_set L.β.func = L.B

@[simp]

theorem Tableaux.Link.chi_beta (L : Link) : L.β.χ = L.χb

theorem Tableaux.Link.A_AspSet_prop (L : Link) : AspSet_prop (L.τ.rev_map '' L.A)

def Tableaux.Link.A_AspSet (L : Link) : AspSet

Equations

• L.A_AspSet = { I := L.τ.rev_map '' L.A, prop := ⋯ }

noncomputable def Tableaux.Link.α (L : Link) : AspPerm

Equations

• L.α = (L.A_AspSet.toAspPerm (-L.χa))⁻¹

@[simp]

theorem Tableaux.Link.inv_set_α (L : Link) : L.A = L.τ.sr L.α '' inv_set L.α.func

@[simp]

theorem Tableaux.Link.chi_alpha (L : Link) : L.α.χ = L.χa

theorem Tableaux.Link.dprod (L : Link) : L.α ⋆ L.β = L.τ

noncomputable def Tableaux.Link_of_dprod {τ : AspPerm} (h_321a : is_321a τ.func) {α β : AspPerm} (dprod : α ⋆ β = τ) : Link

Equations

• Tableaux.Link_of_dprod h_321a dprod = { A := τ.sr α '' inv_set α.func, B := inv_set β.func, S := ASP321a.tfas_of_perm h_321a, χa := α.χ, χb := β.χ, union_eq := ⋯, sep := ⋯ }

theorem Tableaux.rev_A_eq_inv_inv_of_Link_of_dprod {τ : AspPerm} (h_321a : is_321a τ.func) {α β : AspPerm} (dprod : α ⋆ β = τ) : τ.rev_map '' (Link_of_dprod h_321a dprod).A = inv_set α⁻¹.func

noncomputable def Tableaux.link_equiv_dprod {τ : AspPerm} (h_321a : is_321a τ.func) : ↑{L : Link | L.τ = τ} ≃ ↑{(α, β) : AspPerm × AspPerm | α ⋆ β = τ}

Links with ambient permutation τ are equivalent to Demazure factorizations τ = α ⋆ β.

Equations

• One or more equations did not get rendered due to their size.

Chains and Hecke factorizations

This section iterates the two-factor link construction to compare Hecke factorizations of a 321-avoiding ASP permutation with chains of inversion-box data whose union and total shift recover τ.

def Tableaux.HeckeFactorization (τ : AspPerm) : Type

A Hecke factorization of τ, represented as a list of ASP permutations whose Demazure product is τ.

Equations

• Tableaux.HeckeFactorization τ = { P : List AspPerm // AspPerm.DProd P = τ }

def Tableaux.boxUnion : List (Set (ℤ × ℤ) × ℤ) → Set (ℤ × ℤ)

Equations

• Tableaux.boxUnion [] = ∅
• Tableaux.boxUnion (head :: tail) = head.1 ∪ Tableaux.boxUnion tail

def Tableaux.chiSum : List (Set (ℤ × ℤ) × ℤ) → ℤ

Equations

• Tableaux.chiSum [] = 0
• Tableaux.chiSum (head :: tail) = head.2 + Tableaux.chiSum tail

def Tableaux.isChain : List (Set (ℤ × ℤ) × ℤ) → Prop

Equations

• Tableaux.isChain [] = True
• Tableaux.isChain ((A, snd) :: Q) = (Tableaux.linked A (Tableaux.boxUnion Q) ∧ Tableaux.isChain Q)

def Tableaux.PChain (τ : AspPerm) : Type

A chain of box sets with shifts whose union is inv_set τ, whose total shift is τ.χ, and whose pieces are linked in order.

Equations

• Tableaux.PChain τ = { C : List (Set (ℤ × ℤ) × ℤ) // Tableaux.isChain C ∧ Tableaux.boxUnion C = inv_set τ.func ∧ Tableaux.chiSum C = τ.χ }

noncomputable def Tableaux.LSet_of_LPerm : List AspPerm → List (Set (ℤ × ℤ) × ℤ)

Equations

• Tableaux.LSet_of_LPerm [] = []
• Tableaux.LSet_of_LPerm (α :: L) = ((AspPerm.DProd (α :: L)).sr α '' inv_set α.func, α.χ) :: Tableaux.LSet_of_LPerm L

theorem Tableaux.LSet_cons (α : AspPerm) (L : List AspPerm) : LSet_of_LPerm (α :: L) = ((AspPerm.DProd (α :: L)).sr α '' inv_set α.func, α.χ) :: LSet_of_LPerm L

theorem Tableaux.LSet_chiSum {τ : AspPerm} (h_321a : is_321a τ.func) (A : HeckeFactorization τ) : chiSum (LSet_of_LPerm ↑A) = τ.χ

theorem Tableaux.LSet_boxUnion {τ : AspPerm} (h_321a : is_321a τ.func) (A : HeckeFactorization τ) : boxUnion (LSet_of_LPerm ↑A) = inv_set τ.func

theorem Tableaux.LSet_isChain {τ : AspPerm} (h_321a : is_321a τ.func) (A : HeckeFactorization τ) : isChain (LSet_of_LPerm ↑A)

noncomputable def Tableaux.PChain_of_HF {τ : AspPerm} (h_321a : is_321a τ.func) (A : HeckeFactorization τ) : PChain τ

Equations

• Tableaux.PChain_of_HF h_321a A = ⟨Tableaux.LSet_of_LPerm ↑A, ⋯⟩

noncomputable def Tableaux.LPerm_of_Chain (C : List (Set (ℤ × ℤ) × ℤ)) : isChain C → ASP321a.set_321a_prop (boxUnion C) → List AspPerm

Equations

• Tableaux.LPerm_of_Chain [] x_3 x_4 = []
• Tableaux.LPerm_of_Chain ((A, χ) :: Q) hC htfas = (Tableaux.link_of_sets ⋯ htfas χ (Tableaux.chiSum Q)).α :: Tableaux.LPerm_of_Chain Q ⋯ ⋯

theorem Tableaux.DProd_LPerm_of_Chain (C : List (Set (ℤ × ℤ) × ℤ)) (hC : isChain C) (htfas : ASP321a.set_321a_prop (boxUnion C)) : AspPerm.DProd (LPerm_of_Chain C hC htfas) = { I := boxUnion C, prop := ⋯ }.toAspPerm (chiSum C)

noncomputable def Tableaux.HF_of_PChain {τ : AspPerm} (h_321a : is_321a τ.func) (C : PChain τ) : HeckeFactorization τ

Equations

• Tableaux.HF_of_PChain h_321a C = ⟨Tableaux.LPerm_of_Chain ↑C ⋯ ⋯, ⋯⟩

theorem Tableaux.LSet_of_LPerm_of_Chain (C : List (Set (ℤ × ℤ) × ℤ)) (hC : isChain C) (htfas : ASP321a.set_321a_prop (boxUnion C)) : LSet_of_LPerm (LPerm_of_Chain C hC htfas) = C

theorem Tableaux.PChain_of_HF_of_PChain {τ : AspPerm} (h_321a : is_321a τ.func) (C : PChain τ) : PChain_of_HF h_321a (HF_of_PChain h_321a C) = C

theorem Tableaux.HF_of_PChain_of_HF {τ : AspPerm} (h_321a : is_321a τ.func) (A : HeckeFactorization τ) : HF_of_PChain h_321a (PChain_of_HF h_321a A) = A

noncomputable def Tableaux.HF_equiv_PChain {τ : AspPerm} (h_321a : is_321a τ.func) : HeckeFactorization τ ≃ PChain τ

Hecke factorizations of a 321-avoiding ASP permutation are equivalent to chains of box sets with shifts.

Equations

• Tableaux.HF_equiv_PChain h_321a = { toFun := Tableaux.PChain_of_HF h_321a, invFun := Tableaux.HF_of_PChain h_321a, left_inv := ⋯, right_inv := ⋯ }

Set-valued tableaux and label chains

This section recodes chains of box sets by distributing labels 1, ..., n among the boxes of inv_set τ. The order condition on labels is exactly the chain-separation condition in tableau form.

structure Tableaux.SetValuedTableau_prop {τ : AspPerm} {n : ℕ} (T : ↑(inv_set τ.func) → Finset (Fin n)) : Prop

The semistandard-style conditions on a set-valued tableau on inv_set τ: every box is nonempty, and labels weakly decrease along the order ≼.

• nonempty (p : ↑(inv_set τ.func)) : (T p).Nonempty
• weak {p q : ↑(inv_set τ.func)} {i j : Fin n} : i ∈ T p → j ∈ T q → ↑p ≼ ↑q → p ≠ q → j ≤ i

def Tableaux.SetValuedTableau (τ : AspPerm) (n : ℕ) : Type

A set-valued tableau on inv_set τ with symbols 1, ..., n.

Equations

• Tableaux.SetValuedTableau τ n = { T : ↑(inv_set τ.func) → Finset (Fin n) // Tableaux.SetValuedTableau_prop T }

structure Tableaux.LabelChain_prop {τ : AspPerm} {n : ℕ} (C : Fin n → Set (ℤ × ℤ)) : Prop

The compatibility conditions on a label chain: the labeled box sets cover inv_set τ, and earlier labels are separated from later ones.

• cover (p : ℤ × ℤ) : p ∈ inv_set τ.func ↔ ∃ (i : Fin n), p ∈ C i
• sep {i j : Fin n} : i < j → ∀ p ∈ C i, ∀ q ∈ C j, p ≼ q → p = q

def Tableaux.LabelChain (τ : AspPerm) (n : ℕ) : Type

A fixed-length chain of subsets of inv_set τ, indexed by the symbols 1, ..., n.

Equations

• Tableaux.LabelChain τ n = { C : Fin n → Set (ℤ × ℤ) // Tableaux.LabelChain_prop C }

def Tableaux.labelChainOfTableau {τ : AspPerm} {n : ℕ} (T : SetValuedTableau τ n) : LabelChain τ n

Convert a tableau to the corresponding family of label sets.

Equations

• Tableaux.labelChainOfTableau T = ⟨fun (i : Fin n) (p : ℤ × ℤ) => ∃ (hp : p ∈ inv_set τ.func), i ∈ ↑T ⟨p, hp⟩, ⋯⟩

noncomputable def Tableaux.tableauOfLabelChain {τ : AspPerm} {n : ℕ} (C : LabelChain τ n) : SetValuedTableau τ n

Convert a fixed-length chain of label sets to the corresponding tableau.

Equations

• Tableaux.tableauOfLabelChain C = ⟨fun (p : ↑(inv_set τ.func)) => {i : Fin n | ↑p ∈ ↑C i}, ⋯⟩

theorem Tableaux.mem_labelChainOfTableau_iff {τ : AspPerm} {n : ℕ} (T : SetValuedTableau τ n) (p : ↑(inv_set τ.func)) (i : Fin n) : ↑p ∈ ↑(labelChainOfTableau T) i ↔ i ∈ ↑T p

theorem Tableaux.mem_labelChainOfTableau_tableauOfLabelChain_iff {τ : AspPerm} {n : ℕ} (C : LabelChain τ n) (p : ℤ × ℤ) (i : Fin n) : p ∈ ↑(labelChainOfTableau (tableauOfLabelChain C)) i ↔ p ∈ ↑C i

theorem Tableaux.tableauOfLabelChain_labelChainOfTableau {τ : AspPerm} {n : ℕ} (T : SetValuedTableau τ n) : tableauOfLabelChain (labelChainOfTableau T) = T

The tableau reconstructed from the label-chain of T is T itself.

theorem Tableaux.labelChainOfTableau_tableauOfLabelChain {τ : AspPerm} {n : ℕ} (C : LabelChain τ n) : labelChainOfTableau (tableauOfLabelChain C) = C

The label-chain reconstructed from the tableau of C is C itself.

noncomputable def Tableaux.setValuedTableauEquivLabelChain (τ : AspPerm) (n : ℕ) : SetValuedTableau τ n ≃ LabelChain τ n

Set-valued tableaux on inv_set τ with labels 1, ..., n are equivalent to fixed-length label chains.

Equations

• Tableaux.setValuedTableauEquivLabelChain τ n = { toFun := Tableaux.labelChainOfTableau, invFun := Tableaux.tableauOfLabelChain, left_inv := ⋯, right_inv := ⋯ }

Prescribed chi data

Fix a list of shifts. This section refines the chain/Hecke-factorization correspondence by keeping track of the individual χ-values of the factors, yielding a tableau model for factorizations with prescribed χ-list.

noncomputable def Tableaux.chiList {τ : AspPerm} (A : HeckeFactorization τ) : List ℤ

The list of shifts of the factors in a Hecke factorization, in order.

Equations

• Tableaux.chiList A = List.map AspPerm.χ ↑A

def Tableaux.chainChiList {τ : AspPerm} (C : PChain τ) : List ℤ

Equations

• Tableaux.chainChiList C = List.map Prod.snd ↑C

def Tableaux.FixedChiPChain (τ : AspPerm) (n : ℕ) (χs : Fin n → ℤ) : Type

Equations

• Tableaux.FixedChiPChain τ n χs = { C : Tableaux.PChain τ // (↑C).length = n ∧ Tableaux.chainChiList C = List.ofFn χs }

def Tableaux.FixedChiHeckeFactorization (τ : AspPerm) (n : ℕ) (χs : Fin n → ℤ) : Type

The subtype of Hecke factorizations of τ of length n whose ordered list of shifts is List.ofFn χs.

Equations

• Tableaux.FixedChiHeckeFactorization τ n χs = { A : Tableaux.HeckeFactorization τ // (↑A).length = n ∧ Tableaux.chiList A = List.ofFn χs }

theorem Tableaux.chiSum_eq_sum_map_snd (L : List (Set (ℤ × ℤ) × ℤ)) : chiSum L = (List.map Prod.snd L).sum

theorem Tableaux.mem_boxUnion_iff_exists_mem {L : List (Set (ℤ × ℤ) × ℤ)} {p : ℤ × ℤ} : p ∈ boxUnion L ↔ ∃ x ∈ L, p ∈ x.1

theorem Tableaux.mem_boxUnion_iff_exists_index {L : List (Set (ℤ × ℤ) × ℤ)} {p : ℤ × ℤ} : p ∈ boxUnion L ↔ ∃ (i : ℕ) (h : i < L.length), p ∈ L[i].1

theorem Tableaux.isChain_of_sep_ofFn {n : ℕ} (A : Fin n → Set (ℤ × ℤ)) (χs : Fin n → ℤ) (hsep : ∀ {i j : Fin n}, i < j → ∀ p ∈ A i, ∀ q ∈ A j, p ≼ q → p = q) : isChain (List.ofFn fun (i : Fin n) => (A i, χs i))

theorem Tableaux.eq_of_isChain_getElem {L : List (Set (ℤ × ℤ) × ℤ)} (hChain : isChain L) {i j : ℕ} (hi : i < L.length) (hj : j < L.length) : i < j → ∀ p ∈ L[i].1, ∀ q ∈ L[j].1, p ≼ q → p = q

noncomputable def Tableaux.pChainOfLabelChain {τ : AspPerm} {n : ℕ} (χs : Fin n → ℤ) (hχs : (List.ofFn χs).sum = τ.χ) (C : LabelChain τ n) : PChain τ

Equations

• Tableaux.pChainOfLabelChain χs hχs C = ⟨List.ofFn fun (i : Fin n) => (↑C i, χs i), ⋯⟩

noncomputable def Tableaux.fixedChiPChainOfLabelChain {τ : AspPerm} {n : ℕ} (χs : Fin n → ℤ) (hχs : (List.ofFn χs).sum = τ.χ) (C : LabelChain τ n) : FixedChiPChain τ n χs

Equations

• Tableaux.fixedChiPChainOfLabelChain χs hχs C = ⟨Tableaux.pChainOfLabelChain χs hχs C, ⋯⟩

noncomputable def Tableaux.labelChainOfFixedChiPChain {τ : AspPerm} {n : ℕ} {χs : Fin n → ℤ} (C : FixedChiPChain τ n χs) : LabelChain τ n

Equations

• Tableaux.labelChainOfFixedChiPChain C = ⟨fun (i : Fin n) => (↑↑C)[↑i].1, ⋯⟩

noncomputable def Tableaux.labelChainEquivFixedChiPChain {τ : AspPerm} {n : ℕ} (χs : Fin n → ℤ) (hχs : (List.ofFn χs).sum = τ.χ) : LabelChain τ n ≃ FixedChiPChain τ n χs

Equations

• Tableaux.labelChainEquivFixedChiPChain χs hχs = { toFun := Tableaux.fixedChiPChainOfLabelChain χs hχs, invFun := Tableaux.labelChainOfFixedChiPChain, left_inv := ⋯, right_inv := ⋯ }

theorem Tableaux.length_LSet_of_LPerm (L : List AspPerm) : (LSet_of_LPerm L).length = L.length

theorem Tableaux.chainChiList_LSet_of_LPerm (L : List AspPerm) : List.map Prod.snd (LSet_of_LPerm L) = List.map AspPerm.χ L

theorem Tableaux.length_PChain_of_HF {τ : AspPerm} (h_321a : is_321a τ.func) (A : HeckeFactorization τ) : (↑(PChain_of_HF h_321a A)).length = (↑A).length

theorem Tableaux.chainChiList_PChain_of_HF {τ : AspPerm} (h_321a : is_321a τ.func) (A : HeckeFactorization τ) : chainChiList (PChain_of_HF h_321a A) = chiList A

noncomputable def Tableaux.fixedChiHeckeFactorizationEquivFixedChiPChain {τ : AspPerm} {n : ℕ} (h_321a : is_321a τ.func) (χs : Fin n → ℤ) : FixedChiHeckeFactorization τ n χs ≃ FixedChiPChain τ n χs

Equations

• Tableaux.fixedChiHeckeFactorizationEquivFixedChiPChain h_321a χs = (Tableaux.HF_equiv_PChain h_321a).subtypeEquiv ⋯

noncomputable def Tableaux.labelChainEquivFixedChiHeckeFactorization {τ : AspPerm} {n : ℕ} (h_321a : is_321a τ.func) (χs : Fin n → ℤ) (hχs : (List.ofFn χs).sum = τ.χ) : LabelChain τ n ≃ FixedChiHeckeFactorization τ n χs

A label chain is equivalent to a Hecke factorization with prescribed ordered shift data.

Equations

• Tableaux.labelChainEquivFixedChiHeckeFactorization h_321a χs hχs = (Tableaux.labelChainEquivFixedChiPChain χs hχs).trans (Tableaux.fixedChiHeckeFactorizationEquivFixedChiPChain h_321a χs).symm

noncomputable def Tableaux.setValuedTableauEquivFixedChiHeckeFactorization {τ : AspPerm} {n : ℕ} (h_321a : is_321a τ.func) (χs : Fin n → ℤ) (hχs : (List.ofFn χs).sum = τ.χ) : SetValuedTableau τ n ≃ FixedChiHeckeFactorization τ n χs

Equations

• Tableaux.setValuedTableauEquivFixedChiHeckeFactorization h_321a χs hχs = (Tableaux.setValuedTableauEquivLabelChain τ n).trans (Tableaux.labelChainEquivFixedChiHeckeFactorization h_321a χs hχs)

noncomputable def Tableaux.setValuedTableauEquivHeckeFactorization {τ : AspPerm} {n : ℕ} (h_321a : is_321a τ.func) (χs : List ℤ) (h_len : χs.length = n) (h_sum : χs.sum = τ.χ) : SetValuedTableau τ n ≃ { A : HeckeFactorization τ // (↑A).length = n ∧ chiList A = χs }

For a prescribed length-n list of shifts summing to τ.χ, set-valued tableaux on inv_set τ are equivalent to Hecke factorizations of τ with exactly that ordered χ-list.

Equations

• Tableaux.setValuedTableauEquivHeckeFactorization h_321a χs h_len h_sum = ⋯.mp (Tableaux.setValuedTableauEquivFixedChiHeckeFactorization h_321a (fun (i : Fin n) => χs[↑i]) ⋯)