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; it gives an additional formal correspondence between fixed-shift set-valued tableaux and Hecke factorizations for the 321-avoiding case.

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 LeanPool.DemazureProduct.Tableaux.linked (A B : Set (ℤ × ℤ)) : Prop

Two box sets are linked if comparable boxes are forced to be equal.

Equations

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

structure LeanPool.DemazureProduct.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 (ℤ × ℤ)

  The first part of the box decomposition.

• B : Set (ℤ × ℤ)

  The second part of the box decomposition.

• S : ASP321a.tfas

  The ambient triangle-free ASP set.

• χa : ℤ

  The shift assigned to A.

• χb : ℤ

  The shift assigned to B.

• union_eq : self.A ∪ self.B = self.S.I

  The two pieces cover the ambient set.

• sep : linked self.A self.B

  The pieces are linked in order.

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

Build a link from linked pieces and a triangle-free union.

Equations

• LeanPool.DemazureProduct.Tableaux.linkOfSets 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 LeanPool.DemazureProduct.Tableaux.Link.chi (L : Link) : ℤ

The total shift of a link.

Equations

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

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

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

theorem LeanPool.DemazureProduct.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 LeanPool.DemazureProduct.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 LeanPool.DemazureProduct.Tableaux.Link.B_AspSet_prop (L : Link) : AspSet_prop L.B

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

def LeanPool.DemazureProduct.Tableaux.Link.bAspSet (L : Link) : AspSet

The abstract ASP set represented by the second piece of a link.

Equations

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

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

The ambient ASP permutation of a link.

Equations

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

@[simp]

theorem LeanPool.DemazureProduct.Tableaux.Link.inv_set_τ (L : Link) : invSet L.τ.func = L.S.I

theorem LeanPool.DemazureProduct.Tableaux.Link.is_321a_τ (L : Link) : is321a L.τ.func

@[simp]

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

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

The second ASP factor associated to a link.

Equations

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

@[simp]

theorem LeanPool.DemazureProduct.Tableaux.Link.inv_set_β (L : Link) : invSet L.β.func = L.B

@[simp]

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

theorem LeanPool.DemazureProduct.Tableaux.Link.A_AspSet_prop (L : Link) : AspSet_prop (L.τ.revMap '' L.A)

def LeanPool.DemazureProduct.Tableaux.Link.aAspSet (L : Link) : AspSet

The abstract ASP set represented by the first piece of a link.

Equations

• L.aAspSet = { I := L.τ.revMap '' L.A, prop := ⋯ }

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

The first ASP factor associated to a link.

Equations

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

@[simp]

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

@[simp]

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

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

noncomputable def LeanPool.DemazureProduct.Tableaux.linkOfDprod {τ : AspPerm} (h_321a : is321a τ.func) {α β : AspPerm} (dprod : α ⋆ β = τ) : Link

The link associated to a Demazure factorization of a 321-avoiding permutation.

Equations

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

theorem LeanPool.DemazureProduct.Tableaux.rev_A_eq_inv_inv_of_Link_of_dprod {τ : AspPerm} (h_321a : is321a τ.func) {α β : AspPerm} (dprod : α ⋆ β = τ) : τ.revMap '' (linkOfDprod h_321a dprod).A = invSet α⁻¹.func

noncomputable def LeanPool.DemazureProduct.Tableaux.linkEquivDprod {τ : AspPerm} (h_321a : is321a τ.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 LeanPool.DemazureProduct.Tableaux.HeckeFactorization (τ : AspPerm) : Type

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

Equations

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

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

The union of all box sets in a shifted chain.

Equations

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

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

The sum of all shifts in a shifted chain.

Equations

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

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

The predicate that adjacent pieces form a linked shifted chain.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.DemazureProduct.Tableaux.isChain [] = True

def LeanPool.DemazureProduct.Tableaux.PChain (τ : AspPerm) : Type

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

Equations

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

noncomputable def LeanPool.DemazureProduct.Tableaux.lSetOfLPerm : List AspPerm → List (Set (ℤ × ℤ) × ℤ)

Convert a list of ASP permutations to its chain of inversion-box pieces and shifts.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.DemazureProduct.Tableaux.lSetOfLPerm [] = []

theorem LeanPool.DemazureProduct.Tableaux.LSet_cons (α : AspPerm) (L : List AspPerm) : lSetOfLPerm (α :: L) = ((AspPerm.DProd (α :: L)).sr α '' invSet α.func, α.χ) :: lSetOfLPerm L

theorem LeanPool.DemazureProduct.Tableaux.LSet_chiSum {τ : AspPerm} (h_321a : is321a τ.func) (A : HeckeFactorization τ) : chiSum (lSetOfLPerm ↑A) = τ.χ

theorem LeanPool.DemazureProduct.Tableaux.LSet_boxUnion {τ : AspPerm} (h_321a : is321a τ.func) (A : HeckeFactorization τ) : boxUnion (lSetOfLPerm ↑A) = invSet τ.func

theorem LeanPool.DemazureProduct.Tableaux.LSet_isChain {τ : AspPerm} (h_321a : is321a τ.func) (A : HeckeFactorization τ) : isChain (lSetOfLPerm ↑A)

noncomputable def LeanPool.DemazureProduct.Tableaux.pChainOfHf {τ : AspPerm} (h_321a : is321a τ.func) (A : HeckeFactorization τ) : PChain τ

Convert a Hecke factorization to the corresponding shifted chain.

Equations

• LeanPool.DemazureProduct.Tableaux.pChainOfHf h_321a A = ⟨LeanPool.DemazureProduct.Tableaux.lSetOfLPerm ↑A, ⋯⟩

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

Reconstruct a list of ASP permutations from a shifted chain.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.DemazureProduct.Tableaux.lPermOfChain [] x_3 x_4 = []

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

noncomputable def LeanPool.DemazureProduct.Tableaux.hfOfPChain {τ : AspPerm} (h_321a : is321a τ.func) (C : PChain τ) : HeckeFactorization τ

Convert a shifted chain back to a Hecke factorization.

Equations

• LeanPool.DemazureProduct.Tableaux.hfOfPChain h_321a C = ⟨LeanPool.DemazureProduct.Tableaux.lPermOfChain ↑C ⋯ ⋯, ⋯⟩

theorem LeanPool.DemazureProduct.Tableaux.LSet_of_LPerm_of_Chain (C : List (Set (ℤ × ℤ) × ℤ)) (hC : isChain C) (htfas : ASP321a.set_321a_prop (boxUnion C)) : lSetOfLPerm (lPermOfChain C hC htfas) = C

theorem LeanPool.DemazureProduct.Tableaux.PChain_of_HF_of_PChain {τ : AspPerm} (h_321a : is321a τ.func) (C : PChain τ) : pChainOfHf h_321a (hfOfPChain h_321a C) = C

theorem LeanPool.DemazureProduct.Tableaux.HF_of_PChain_of_HF {τ : AspPerm} (h_321a : is321a τ.func) (A : HeckeFactorization τ) : hfOfPChain h_321a (pChainOfHf h_321a A) = A

noncomputable def LeanPool.DemazureProduct.Tableaux.hfEquivPChain {τ : AspPerm} (h_321a : is321a τ.func) : HeckeFactorization τ ≃ PChain τ

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

Equations

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

Set-valued tableaux and label chains

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

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

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

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

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

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

Equations

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

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

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

• cover (p : ℤ × ℤ) : p ∈ invSet τ.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 LeanPool.DemazureProduct.Tableaux.LabelChain (τ : AspPerm) (n : ℕ) : Type

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

Equations

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

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

Convert a tableau to the corresponding family of label sets.

Equations

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

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

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

Equations

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

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

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

theorem LeanPool.DemazureProduct.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 LeanPool.DemazureProduct.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 LeanPool.DemazureProduct.Tableaux.setValuedTableauEquivLabelChain (τ : AspPerm) (n : ℕ) : SetValuedTableau τ n ≃ LabelChain τ n

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

Equations

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

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 LeanPool.DemazureProduct.Tableaux.chiList {τ : AspPerm} (A : HeckeFactorization τ) : List ℤ

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

Equations

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

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

The ordered list of shifts in a shifted chain.

Equations

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

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

Shifted chains of fixed length with prescribed shift list.

Equations

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

def LeanPool.DemazureProduct.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

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

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

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

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

theorem LeanPool.DemazureProduct.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 LeanPool.DemazureProduct.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 LeanPool.DemazureProduct.Tableaux.pChainOfLabelChain {τ : AspPerm} {n : ℕ} (χs : Fin n → ℤ) (hχs : (List.ofFn χs).sum = τ.χ) (C : LabelChain τ n) : PChain τ

Convert a label chain with prescribed shifts to a shifted chain.

Equations

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

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

Convert a label chain to a fixed-shift shifted chain.

Equations

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

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

Convert a fixed-shift shifted chain to a label chain.

Equations

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

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

Equivalence between label chains and fixed-shift shifted chains.

Equations

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

theorem LeanPool.DemazureProduct.Tableaux.length_LSet_of_LPerm (L : List AspPerm) : (lSetOfLPerm L).length = L.length

theorem LeanPool.DemazureProduct.Tableaux.chainChiList_LSet_of_LPerm (L : List AspPerm) : List.map Prod.snd (lSetOfLPerm L) = List.map AspPerm.χ L

theorem LeanPool.DemazureProduct.Tableaux.length_PChain_of_HF {τ : AspPerm} (h_321a : is321a τ.func) (A : HeckeFactorization τ) : (↑(pChainOfHf h_321a A)).length = (↑A).length

theorem LeanPool.DemazureProduct.Tableaux.chainChiList_PChain_of_HF {τ : AspPerm} (h_321a : is321a τ.func) (A : HeckeFactorization τ) : chainChiList (pChainOfHf h_321a A) = chiList A

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

Equivalence between fixed-shift Hecke factorizations and fixed-shift chains.

Equations

• LeanPool.DemazureProduct.Tableaux.fixedChiHeckeFactorizationEquivFixedChiPChain h_321a χs = (LeanPool.DemazureProduct.Tableaux.hfEquivPChain h_321a).subtypeEquiv ⋯

noncomputable def LeanPool.DemazureProduct.Tableaux.labelChainEquivFixedChiHeckeFactorization {τ : AspPerm} {n : ℕ} (h_321a : is321a τ.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

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

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

Equivalence between set-valued tableaux and fixed-shift Hecke factorizations.

Equations

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

noncomputable def LeanPool.DemazureProduct.Tableaux.setValuedTableauEquivHeckeFactorization {τ : AspPerm} {n : ℕ} (h_321a : is321a τ.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 invSet τ are equivalent to Hecke factorizations of τ with exactly that ordered χ-list.

Equations

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