Hecke factorizations and shape chains

This file classifies the Hecke factorizations $\sigma_S = \alpha_1 \star \dots \star \alpha_n$ into shift-$0$ factors. They correspond, via $(A_1, \dots, A_n) \mapsto (\sigma_{A_1}, \dots, \sigma_{A_n})$, to shape chains: lists of skew shapes covering $S$ such that each prefix union is closed to the northwest within $S$, each suffix union is closed to the southeast, and each prefix union meets the matching suffix union in a nonattacking set.

The first draft of this file was written by Claude Opus 5.5, following a design by Nathan Pflueger.

def SkewShapes.boxUnion : List SkewShape → Set (ℤ × ℤ)

The boxes lying in some shape of a list.

Equations

• SkewShapes.boxUnion [] = ∅
• SkewShapes.boxUnion (A :: L) = A.boxes ∪ SkewShapes.boxUnion L

@[simp]

theorem SkewShapes.boxUnion_nil : boxUnion [] = ∅

@[simp]

theorem SkewShapes.boxUnion_cons (A : SkewShape) (L : List SkewShape) : boxUnion (A :: L) = A.boxes ∪ boxUnion L

theorem SkewShapes.boxUnion_append (L₁ L₂ : List SkewShape) : boxUnion (L₁ ++ L₂) = boxUnion L₁ ∪ boxUnion L₂

theorem SkewShapes.boxUnion_take_union_drop (L : List SkewShape) (k : ℕ) : boxUnion (List.take k L) ∪ boxUnion (List.drop k L) = boxUnion L

theorem SkewShapes.boxUnion_take_subset (L : List SkewShape) (k : ℕ) : boxUnion (List.take k L) ⊆ boxUnion L

theorem SkewShapes.boxUnion_drop_subset (L : List SkewShape) (k : ℕ) : boxUnion (List.drop k L) ⊆ boxUnion L

structure SkewShapes.IsShapeChain (S : SkewShape) (L : List SkewShape) : Prop

A list of skew shapes $A_1, \dots, A_n$ is a shape chain for $S$ if the $A_i$ cover $S$ and, for each $k$, the prefix union $P_k = A_1 \cup \dots \cup A_k$ is closed to the northwest within $S$, the suffix union $Q_k = A_{k+1} \cup \dots \cup A_n$ is closed to the southeast within $S$, and $P_k \cap Q_k$ is nonattacking.

• union_eq : boxUnion L = S.boxes
• take_ler (k : ℕ) : lerSet (boxUnion (List.take k L)) S
• drop_lel (k : ℕ) : lelSet (boxUnion (List.drop k L)) S
• inter_nonattacking (k : ℕ) : nonattacking (boxUnion (List.take k L) ∩ boxUnion (List.drop k L))

theorem SkewShapes.IsShapeChain.nil {S : SkewShape} (h : S.boxes = ∅) : IsShapeChain S []

theorem SkewShapes.IsShapeChain.head_ler {S A : SkewShape} {L : List SkewShape} (h : IsShapeChain S (A :: L)) : A ≤R S

theorem SkewShapes.IsShapeChain.tail_lelSet {S A : SkewShape} {L : List SkewShape} (h : IsShapeChain S (A :: L)) : lelSet (boxUnion L) S

theorem SkewShapes.IsShapeChain.head_union {S A : SkewShape} {L : List SkewShape} (h : IsShapeChain S (A :: L)) : A.boxes ∪ boxUnion L = S.boxes

theorem SkewShapes.IsShapeChain.head_nonattacking {S A : SkewShape} {L : List SkewShape} (h : IsShapeChain S (A :: L)) : nonattacking (A.boxes ∩ boxUnion L)

theorem SkewShapes.IsShapeChain.tail {S A : SkewShape} {L : List SkewShape} (h : IsShapeChain S (A :: L)) : IsShapeChain (ofLelSet S (boxUnion L) ⋯) L

The tail of a shape chain is a shape chain for the union of its shapes.

theorem SkewShapes.IsShapeChain.cons {S A : SkewShape} {L : List SkewShape} {Q : SkewShape} (hA : A ≤R S) (hQ : Q ≤L S) (hu : A.boxes ∪ Q.boxes = S.boxes) (hna : nonattacking (A.boxes ∩ Q.boxes)) (hL : IsShapeChain Q L) : IsShapeChain S (A :: L)

Prepending a shape to a shape chain of a piece of a two-factor decomposition of $S$ gives a shape chain of $S$.

theorem SkewShapes.IsShapeChain.dprod {S : SkewShape} {L : List SkewShape} (h : IsShapeChain S L) : AspPerm.DProd (List.map SkewShape.σ L) = S.σ

The permutations of a shape chain multiply to $\sigma_S$.

theorem SkewShapes.IsShapeChain.eq_of_map_σ_eq {S : SkewShape} {L L' : List SkewShape} (h : IsShapeChain S L) (h' : IsShapeChain S L') (hσ : List.map SkewShape.σ L = List.map SkewShape.σ L') : L = L'

A shape chain of $S$ is determined by the permutations of its shapes.

theorem SkewShapes.exists_isShapeChain {S : SkewShape} (M : List AspPerm) (hχ : ∀ α ∈ M, α.χ = 0) (hM : AspPerm.DProd M = S.σ) : ∃ (L : List SkewShape), IsShapeChain S L ∧ List.map SkewShape.σ L = M

Every Hecke factorization of $\sigma_S$ into shift-$0$ factors comes from a shape chain.

@[reducible, inline]

abbrev SkewShapes.HeckeFactorization (S : SkewShape) : Type

Hecke factorizations $\sigma_S = \alpha_1 \star \dots \star \alpha_n$ into shift-$0$ factors.

Equations

• SkewShapes.HeckeFactorization S = { M : List AspPerm // (∀ α ∈ M, α.χ = 0) ∧ AspPerm.DProd M = S.σ }

@[reducible, inline]

abbrev SkewShapes.ShapeChain (S : SkewShape) : Type

Shape chains of $S$.

Equations

• SkewShapes.ShapeChain S = { L : List SkewShapes.SkewShape // SkewShapes.IsShapeChain S L }

noncomputable def SkewShapes.shapeChainEquiv (S : SkewShape) : ShapeChain S ≃ HeckeFactorization S

Shape chains of $S$ correspond bijectively, via $(A_1, \dots, A_n) \mapsto (\sigma_{A_1}, \dots, \sigma_{A_n})$, to Hecke factorizations of $\sigma_S$ into shift-$0$ factors.

Equations

• SkewShapes.shapeChainEquiv S = Equiv.ofBijective (fun (L : SkewShapes.ShapeChain S) => ⟨List.map SkewShapes.SkewShape.σ ↑L, ⋯⟩) ⋯

@[simp]

theorem SkewShapes.shapeChainEquiv_apply {S : SkewShape} (L : ShapeChain S) : ↑((shapeChainEquiv S) L) = List.map SkewShape.σ ↑L

noncomputable def SkewShapes.shapeChainEquivOfLength (S : SkewShape) (n : ℕ) : { L : ShapeChain S // (↑L).length = n } ≃ { M : HeckeFactorization S // (↑M).length = n }

Shape chains of $S$ of length $n$ correspond bijectively to Hecke factorizations of $\sigma_S$ into $n$ shift-$0$ factors.

Equations

• SkewShapes.shapeChainEquivOfLength S n = (SkewShapes.shapeChainEquiv S).subtypeEquiv ⋯