Dominance order on partitions

This file defines dominance of partitions of a fixed natural number by comparing all partial sums of their decreasingly sorted parts. It proves that dominance is a partial order and that dominance implies the corresponding lexicographic comparison, strictly for strict dominance.

The dominance order is the triangular order governing Kostka numbers and the occurrence of Specht modules in permutation modules. It is the “Orders on partitions” target in Layer 0 of the symmetric-group and Schur–Weyl roadmap.

References

• Mathlib PR #42725 (Kim Morrison) — the draft upstream adaptation of this file; the ℕ-indexed definition of Dominates and the Fin-indexed decidability characterization follow the form prepared for that PR.

@[instance_reducible]

def TauCeti.PartitionLex.partitionLinearOrder {n : ℕ} : LinearOrder n.Partition

The lexicographic linear order on partitions, obtained from their decreasingly sorted parts. Activate it with open scoped TauCeti.PartitionLex.

Equations

• TauCeti.PartitionLex.partitionLinearOrder = LinearOrder.lift' (fun (μ : n.Partition) => μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2) ⋯

@[simp]

theorem TauCeti.PartitionLex.partition_lt_iff {n : ℕ} {μ ν : n.Partition} : μ < ν ↔ (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2) < ν.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2

Partition comparison in the lexicographic order is comparison of the decreasingly sorted parts.

@[simp]

theorem TauCeti.PartitionLex.partition_le_iff {n : ℕ} {μ ν : n.Partition} : μ ≤ ν ↔ (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2) ≤ ν.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2

Partition comparison in the non-strict lexicographic order is comparison of the decreasingly sorted parts.

def TauCeti.Dominates {n : ℕ} (μ ν : n.Partition) : Prop

A partition μ dominates a partition ν when every partial sum of the decreasingly sorted parts of μ is at least the corresponding partial sum of ν.

The definition quantifies over all of ℕ, following the form prepared for Mathlib PR #42725; use dominates_iff to unfold it outside this module and dominates_iff_forall_fin to reduce to the first n + 1 partial sums.

Equations

• TauCeti.Dominates μ ν = ∀ (k : ℕ), (List.take k (ν.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2)).sum ≤ (List.take k (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2)).sum

theorem TauCeti.dominates_iff {n : ℕ} {μ ν : n.Partition} : Dominates μ ν ↔ ∀ (k : ℕ), (List.take k (ν.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2)).sum ≤ (List.take k (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2)).sum

The defining partial-sum characterization of dominance.

theorem TauCeti.dominates_iff_forall_fin {n : ℕ} {μ ν : n.Partition} : Dominates μ ν ↔ ∀ (k : Fin (n + 1)), (List.take (↑k) (ν.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2)).sum ≤ (List.take (↑k) (μ.parts.sort fun (x1 x2 : ℕ) => x1 ≥ x2)).sum

Partial sums of sorted parts of partitions of n agree from index n on, so dominance is determined by the first n + 1 partial sums. In particular it is decidable.

@[instance_reducible]

instance TauCeti.instDecidableDominates {n : ℕ} (μ ν : n.Partition) : Decidable (Dominates μ ν)

Equations

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

@[simp]

theorem TauCeti.dominates_refl {n : ℕ} (μ : n.Partition) : Dominates μ μ

Every partition dominates itself.

theorem TauCeti.Dominates.trans {n : ℕ} {μ ν ξ : n.Partition} (hμν : Dominates μ ν) (hνξ : Dominates ν ξ) : Dominates μ ξ

Dominance is transitive.

theorem TauCeti.Dominates.antisymm {n : ℕ} {μ ν : n.Partition} (hμν : Dominates μ ν) (hνμ : Dominates ν μ) : μ = ν

Dominance is antisymmetric.

@[instance_reducible]

def TauCeti.DominanceOrder.partitionPartialOrder {n : ℕ} : PartialOrder n.Partition

The dominance partial order on partitions, oriented so that ν ≤ μ means that μ dominates ν. Activate it with open scoped TauCeti.DominanceOrder.

Equations

• TauCeti.DominanceOrder.partitionPartialOrder = { le := fun (μ ν : n.Partition) => TauCeti.Dominates ν μ, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[simp]

theorem TauCeti.DominanceOrder.partition_le_iff {n : ℕ} {μ ν : n.Partition} : μ ≤ ν ↔ Dominates ν μ

Partition comparison in the dominance order is dominance in the reverse direction.

@[simp]

theorem TauCeti.DominanceOrder.partition_lt_iff {n : ℕ} {μ ν : n.Partition} : μ < ν ↔ Dominates ν μ ∧ μ ≠ ν

Strict partition comparison in the dominance order is strict dominance in the reverse direction.

def TauCeti.StrictlyDominates {n : ℕ} (μ ν : n.Partition) : Prop

Strict dominance is the strict relation of the dominance partial order.

Equations

• TauCeti.StrictlyDominates μ ν = (ν < μ)

@[simp]

theorem TauCeti.strictlyDominates_iff {n : ℕ} {μ ν : n.Partition} : StrictlyDominates μ ν ↔ Dominates μ ν ∧ μ ≠ ν

Strict dominance is dominance between unequal partitions.

instance TauCeti.instIsStrictOrderPartitionStrictlyDominates {n : ℕ} : IsStrictOrder n.Partition StrictlyDominates

Strict dominance is a strict order on partitions, inherited from the dominance partial order.

@[instance_reducible]

instance TauCeti.instDecidableStrictlyDominates {n : ℕ} (μ ν : n.Partition) : Decidable (StrictlyDominates μ ν)

Equations

• TauCeti.instDecidableStrictlyDominates μ ν = ⋯.mpr inferInstance

theorem TauCeti.lex_lt_of_strictlyDominates {n : ℕ} {μ ν : n.Partition} (h : StrictlyDominates μ ν) : ν < μ

Strict dominance refines the lexicographic linear order on partitions.

theorem TauCeti.lex_le_of_dominates {n : ℕ} {μ ν : n.Partition} (h : Dominates μ ν) : ν ≤ μ

Dominance refines the lexicographic linear order on partitions.

@[simp]

theorem TauCeti.indiscrete_dominates {n : ℕ} (μ : n.Partition) : Dominates (Nat.Partition.indiscrete n) μ

The one-part partition dominates every partition of the same natural number.

@[simp]

theorem TauCeti.dominates_indiscrete_iff {n : ℕ} {μ : n.Partition} : Dominates μ (Nat.Partition.indiscrete n) ↔ μ = Nat.Partition.indiscrete n

A partition dominates the one-part partition only when it is that partition.