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 τ.

@[reducible, inline]

noncomputable abbrev Tableaux.DProd (L : List AspPerm) : AspPerm

Equations

• Tableaux.DProd L = List.foldr AspPerm.star AspPerm.id L

theorem Tableaux.DProd_cons (α : AspPerm) (Q : List AspPerm) : DProd (α :: Q) = α ⋆ DProd Q

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 // Tableaux.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) = ((Tableaux.DProd (α :: L)).sr α '' inv_set α.func, α.χ) :: Tableaux.LSet_of_LPerm L

theorem Tableaux.LSet_cons (α : AspPerm) (L : List AspPerm) : LSet_of_LPerm (α :: L) = ((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)) : 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]) ⋯)