N-Partitions

This file provides the canonical definition of NPartition N, which represents a weakly decreasing N-tuple of nonnegative integers (Definition def.sf.Npar in the source).

Main definitions

• IsNPartition - predicate for N-tuples that are weakly decreasing
• NPartition N - a weakly decreasing N-tuple of nonnegative integers
• NPartition.parts - the entries of the partition as a function Fin N → ℕ
• NPartition.antitone - proof that the entries are weakly decreasing
• NPartition.size - the sum of all entries
• NPartition.zero - the zero partition (0, 0, ..., 0)
• NPartition.add - component-wise addition of N-partitions
• NPartition.youngDiagram - the Young diagram Y(λ) as a Finset (Fin N × ℕ)
• NPartition.skewYoungDiagram - the skew Young diagram Y(λ/μ) as a Finset (Fin N × ℕ)
• NPartition.instFintypeBounded - Fintype instance for partitions with bounded entries
• NPartition.instFintypeSizeBounded - Fintype instance for partitions with bounded size

Design notes

This file provides the canonical NPartition structure. We use antitone as the field name since it matches Mathlib conventions.

The weakly decreasing condition means: if i ≤ j then parts j ≤ parts i. This is equivalent to Antitone parts in Mathlib terminology.

Duplicate definitions

For historical reasons, there is a local NPartition definition in:

1. PieriJacobiTrudi.lean (SymmetricFunctions.NPartition): Uses weaklyDecreasing field name.

Both definitions are semantically equivalent (representing weakly decreasing N-tuples of natural numbers). The local definition is retained to avoid large refactoring of the extensive APIs built on top of it. Future work may consolidate these definitions.

Note: MonomialSymmetric.lean and SchurBasics.lean have been migrated to use the canonical definition via abbrev or direct import.

Compatibility

For backwards compatibility with code using other field names:

• NPartition.monotone is an alias for NPartition.antitone
• NPartition.weaklyDecreasing is an alias for NPartition.antitone

Migration Guide

The NPartition structure is defined in this file (canonical) and has one remaining local definition:

File	Namespace	Field name	Status
NPartition.lean (this)	(top-level)	antitone	Canonical
PieriJacobiTrudi.lean	SymmetricFunctions	weaklyDecreasing	Local (with bridge)
MonomialSymmetric.lean	AlgebraicCombinatorics.SymmetricFunctions	(abbrev)	✓ Migrated
SchurBasics.lean	(top-level)	(import)	✓ Migrated

To migrate a file to use this shared definition:

1. Add import AlgebraicCombinatorics.SymmetricFunctions.NPartition to imports
2. Remove the local structure NPartition definition
3. If in a namespace, use open NPartition or create a local alias
4. Replace field accesses:
   • .monotone → .antitone or use the monotone alias theorem
   • .weaklyDecreasing → .antitone or use the weaklyDecreasing alias theorem
5. For constructors, use NPartition.mk with antitone field, or use NPartition.mk' which accepts the explicit predicate form

References

• Source: AlgebraicCombinatorics/tex/SymmetricFunctions/MonomialSymmetric.tex (Definition def.sf.Npar)

IsNPartition predicate

This predicate characterizes N-tuples that are weakly decreasing. It is equivalent to Antitone for functions Fin N → ℕ.

def IsNPartition {N : ℕ} (lam : Fin N → ℕ) : Prop

An N-partition predicate: an N-tuple is an N-partition if it is weakly decreasing. This is equivalent to Antitone for functions Fin N → ℕ. (Used throughout the source)

Equations

• IsNPartition lam = ∀ (i j : Fin N), i ≤ j → lam j ≤ lam i

instance IsNPartition.instDecidable {N : ℕ} (lam : Fin N → ℕ) : Decidable (IsNPartition lam)

IsNPartition is decidable since it's a finite conjunction of decidable inequalities.

Equations

• IsNPartition.instDecidable lam = inferInstanceAs (Decidable (∀ (i j : Fin N), i ≤ j → lam j ≤ lam i))

theorem isNPartition_iff_antitone {N : ℕ} {lam : Fin N → ℕ} : IsNPartition lam ↔ Antitone lam

IsNPartition is equivalent to Antitone.

theorem isNPartition_zero {N : ℕ} : IsNPartition 0

The zero tuple is an N-partition (trivially weakly decreasing).

theorem IsNPartition.add {N : ℕ} {α β : Fin N → ℕ} (hα : IsNPartition α) (hβ : IsNPartition β) : IsNPartition (α + β)

The sum of two N-partitions is an N-partition.

structure NPartition (N : ℕ) : Type

An N-partition is a weakly decreasing N-tuple of nonnegative integers. (Definition def.sf.Npar)

This is represented as a function Fin N → ℕ that is antitone (i.e., i ≤ j → parts j ≤ parts i).

The field is named antitone to match Mathlib conventions.

• parts : Fin N → ℕ

  The entries of the N-partition as a function from Fin N to ℕ

• antitone : Antitone self.parts

  The entries are weakly decreasing (antitone)

Compatibility aliases for field names

theorem NPartition.monotone {N : ℕ} (μ : NPartition N) (i j : Fin N) : i ≤ j → μ.parts j ≤ μ.parts i

Alias for antitone to match SchurBasics.lean naming convention. The weakly decreasing condition: if i ≤ j then parts j ≤ parts i.

theorem NPartition.weaklyDecreasing {N : ℕ} (μ : NPartition N) (i j : Fin N) : i ≤ j → μ.parts j ≤ μ.parts i

Alias for antitone to match PieriJacobiTrudi.lean naming convention. The weakly decreasing condition: if i ≤ j then parts j ≤ parts i.

theorem NPartition.parts_antitone {N : ℕ} (μ : NPartition N) : Antitone μ.parts

The antitone property as a function (for use in proofs).

theorem NPartition.isNPartition {N : ℕ} (μ : NPartition N) : IsNPartition μ.parts

An NPartition's parts satisfy the IsNPartition predicate. This connects the structure-based definition with the predicate-based definition.

Basic properties

theorem NPartition.ext {N : ℕ} {μ ν : NPartition N} (h : μ.parts = ν.parts) : μ = ν

Two N-partitions are equal if and only if their parts are equal.

theorem NPartition.ext_iff {N : ℕ} {μ ν : NPartition N} : μ = ν ↔ μ.parts = ν.parts

theorem NPartition.ext' {N : ℕ} {μ ν : NPartition N} : μ = ν ↔ ∀ (i : Fin N), μ.parts i = ν.parts i

Extensionality in terms of pointwise equality.

theorem NPartition.ext_parts {N : ℕ} {μ ν : NPartition N} (h : ∀ (i : Fin N), μ.parts i = ν.parts i) : μ = ν

Extensionality for pointwise equality (variant taking a proof for each index).

theorem NPartition.parts_ext_iff {N : ℕ} {μ ν : NPartition N} : μ = ν ↔ μ.parts = ν.parts

Extensionality in terms of parts equality.

instance NPartition.instDecidableEq {N : ℕ} : DecidableEq (NPartition N)

Decidable equality for N-partitions.

Equations

• μ.instDecidableEq ν = decidable_of_iff (μ.parts = ν.parts) ⋯

The zero partition

def NPartition.zero {N : ℕ} : NPartition N

The zero N-partition (0, 0, ..., 0)

Equations

• NPartition.zero = { parts := fun (x : Fin N) => 0, antitone := ⋯ }

instance NPartition.instZero {N : ℕ} : Zero (NPartition N)

Equations

• NPartition.instZero = { zero := NPartition.zero }

instance NPartition.instInhabited {N : ℕ} : Inhabited (NPartition N)

Equations

• NPartition.instInhabited = { default := 0 }

@[simp]

theorem NPartition.zero_parts {N : ℕ} : parts 0 = fun (x : Fin N) => 0

@[simp]

theorem NPartition.zero_parts_apply {N : ℕ} (i : Fin N) : parts 0 i = 0

Size (weight) of a partition

def NPartition.size {N : ℕ} (μ : NPartition N) : ℕ

The size (or weight) of an N-partition is the sum of its entries. If μ = (μ₁, μ₂, ..., μ_N), then |μ| = μ₁ + μ₂ + ... + μ_N.

Equations

• μ.size = ∑ i : Fin N, μ.parts i

@[simp]

theorem NPartition.size_eq_sum {N : ℕ} (μ : NPartition N) : μ.size = ∑ i : Fin N, μ.parts i

@[simp]

theorem NPartition.zero_size {N : ℕ} : size 0 = 0

theorem NPartition.parts_le_size {N : ℕ} (μ : NPartition N) (i : Fin N) : μ.parts i ≤ μ.size

Each entry of an N-partition is bounded by the size.

theorem NPartition.parts_zero_max {N : ℕ} (μ : NPartition N) (i : Fin N) (hN : 0 < N) : μ.parts i ≤ μ.parts ⟨0, hN⟩

The first entry is the largest in an N-partition (when N > 0).

theorem NPartition.parts_zero_eq_size_iff {N : ℕ} (μ : NPartition N) (hN : 0 < N) : μ.parts ⟨0, hN⟩ = μ.size ↔ ∀ (i : Fin N), ↑i ≠ 0 → μ.parts i = 0

The first entry of an N-partition equals the size iff all other entries are zero.

theorem NPartition.eq_zero_of_size_eq_zero {N : ℕ} (μ : NPartition N) (h : μ.size = 0) : μ = 0

An N-partition with size 0 is the zero partition.

@[simp]

theorem NPartition.size_eq_zero_iff {N : ℕ} (μ : NPartition N) : μ.size = 0 ↔ μ = 0

An N-partition has size 0 if and only if it is the zero partition.

theorem NPartition.size_pos_of_ne_zero {N : ℕ} {μ : NPartition N} (h : μ ≠ 0) : 0 < μ.size

A non-zero N-partition has positive size.

Addition of N-partitions

Component-wise addition of N-partitions. Since both partitions are antitone (weakly decreasing), their component-wise sum is also antitone, so the result is a valid N-partition without needing to sort.

This is the canonical Add instance for NPartition, used by all files including MonomialSymmetric.lean.

def NPartition.add {N : ℕ} (μ ν : NPartition N) : NPartition N

Component-wise addition of N-partitions. Since both partitions are antitone (weakly decreasing), their sum is also antitone.

Equations

• μ.add ν = { parts := fun (i : Fin N) => μ.parts i + ν.parts i, antitone := ⋯ }

instance NPartition.instAdd {N : ℕ} : Add (NPartition N)

Equations

• NPartition.instAdd = { add := NPartition.add }

@[simp]

theorem NPartition.add_parts {N : ℕ} (μ ν : NPartition N) (i : Fin N) : (μ + ν).parts i = μ.parts i + ν.parts i

The parts of a sum of N-partitions equals the component-wise sum.

@[simp]

theorem NPartition.add_size {N : ℕ} (μ ν : NPartition N) : (μ + ν).size = μ.size + ν.size

The size of a sum of N-partitions equals the sum of their sizes.

theorem NPartition.add_comm {N : ℕ} (μ ν : NPartition N) : μ + ν = ν + μ

Addition of N-partitions is commutative.

@[simp]

theorem NPartition.add_zero {N : ℕ} (μ : NPartition N) : μ + 0 = μ

Adding zero to an N-partition gives the same N-partition.

@[simp]

theorem NPartition.zero_add {N : ℕ} (μ : NPartition N) : 0 + μ = μ

Adding an N-partition to zero gives the same N-partition.

theorem NPartition.add_assoc {N : ℕ} (μ ν ρ : NPartition N) : μ + ν + ρ = μ + (ν + ρ)

Addition of N-partitions is associative.

instance NPartition.instAddCommMonoid {N : ℕ} : AddCommMonoid (NPartition N)

NPartition N forms an AddCommMonoid under component-wise addition. This enables using generic Mathlib lemmas about AddCommMonoid with NPartition.

Equations

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

Coercion to function

instance NPartition.instCoeFunForallFinNat {N : ℕ} : CoeFun (NPartition N) fun (x : NPartition N) => Fin N → ℕ

Coercion to a function.

Equations

• NPartition.instCoeFunForallFinNat = { coe := NPartition.parts }

@[simp]

theorem NPartition.coe_parts {N : ℕ} (μ : NPartition N) : μ.parts = μ.parts

Partial order (containment)

instance NPartition.instLE {N : ℕ} : LE (NPartition N)

Containment of partitions: μ ≤ ν means μᵢ ≤ νᵢ for all i

Equations

• NPartition.instLE = { le := fun (μ ν : NPartition N) => ∀ (i : Fin N), μ.parts i ≤ ν.parts i }

theorem NPartition.le_def {N : ℕ} (μ ν : NPartition N) : μ ≤ ν ↔ ∀ (i : Fin N), μ.parts i ≤ ν.parts i

theorem NPartition.le_iff {N : ℕ} {μ ν : NPartition N} : μ ≤ ν ↔ ∀ (i : Fin N), μ.parts i ≤ ν.parts i

Alias for le_def matching SchurBasics.lean naming.

instance NPartition.instPreorder {N : ℕ} : Preorder (NPartition N)

Equations

• NPartition.instPreorder = { le := fun (x1 x2 : NPartition N) => x1 ≤ x2, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

instance NPartition.instPartialOrder {N : ℕ} : PartialOrder (NPartition N)

Equations

• NPartition.instPartialOrder = { toPreorder := NPartition.instPreorder, le_antisymm := ⋯ }

Fintype instances for bounded partitions

noncomputable instance NPartition.instFintypeBounded {N : ℕ} (M : ℕ) : Fintype { μ : NPartition N // ∀ (i : Fin N), μ.parts i ≤ M }

The set of N-partitions with entries bounded by M is finite. This is useful for cardinality arguments in symmetric function theory.

Equations

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

noncomputable instance NPartition.instFintypeSizeBounded {N : ℕ} (n : ℕ) : Fintype { μ : NPartition N // μ.size ≤ n }

The set of N-partitions with size bounded by n is finite. This follows from the fact that if size ≤ n, then all entries are ≤ n. This is needed for counting SSYT of bounded content.

Equations

• NPartition.instFintypeSizeBounded n = Fintype.ofInjective (fun (x : { μ : NPartition N // μ.size ≤ n }) => match x with | ⟨μ, hμ⟩ => ⟨μ, ⋯⟩) ⋯

noncomputable instance NPartition.instFintypeSizeEq {N : ℕ} (n : ℕ) : Fintype { μ : NPartition N // μ.size = n }

The set of N-partitions with exact size n is finite. This is a subtype of the bounded-size type.

Equations

• NPartition.instFintypeSizeEq n = Fintype.ofInjective (fun (x : { μ : NPartition N // μ.size = n }) => match x with | ⟨μ, hμ⟩ => ⟨μ, ⋯⟩) ⋯

noncomputable def NPartition.partitionsOfSize {N : ℕ} (n : ℕ) : Finset (NPartition N)

The finite set of N-partitions with exact size n.

Equations

• NPartition.partitionsOfSize n = Finset.map { toFun := Subtype.val, inj' := ⋯ } Finset.univ

theorem NPartition.mem_partitionsOfSize {N : ℕ} (μ : NPartition N) (n : ℕ) : μ ∈ partitionsOfSize n ↔ μ.size = n

Membership in partitionsOfSize is characterized by size.

theorem NPartition.finite_of_size {N : ℕ} (n : ℕ) : {μ : NPartition N | μ.size = n}.Finite

The set of N-partitions with size n is finite (Set.Finite version).

instance NPartition.instDecidableLE {N : ℕ} : DecidableRel fun (μ ν : NPartition N) => μ ≤ ν

Decidable instance for partition containment.

Equations

• x✝¹.instDecidableLE x✝ = Fintype.decidableForallFintype

theorem NPartition.zero_le {N : ℕ} (μ : NPartition N) : 0 ≤ μ

The zero N-partition is the minimum element

theorem NPartition.size_le_of_le {N : ℕ} {μ ν : NPartition N} (h : μ ≤ ν) : μ.size ≤ ν.size

μ ≤ ν implies |μ| ≤ |ν|

Length of a partition

def NPartition.length {N : ℕ} (μ : NPartition N) : ℕ

The length of an N-partition is the number of nonzero entries.

Equations

• μ.length = {i : Fin N | μ.parts i ≠ 0}.card

@[simp]

theorem NPartition.zero_length {N : ℕ} : length 0 = 0

@[simp]

theorem NPartition.length_eq_zero_iff {N : ℕ} {μ : NPartition N} : μ.length = 0 ↔ μ = 0

An N-partition has length 0 if and only if it is the zero partition.

theorem NPartition.length_pos_of_ne_zero {N : ℕ} {μ : NPartition N} (h : μ ≠ 0) : 0 < μ.length

A nonzero N-partition has positive length.

theorem NPartition.length_le {N : ℕ} (μ : NPartition N) : μ.length ≤ N

The length is at most N.

theorem NPartition.finite_support {N : ℕ} (μ : NPartition N) : {i : Fin N | μ.parts i ≠ 0}.Finite

An N-partition is finite (has finitely many nonzero entries).

Constructor with explicit predicate

def NPartition.mk' {N : ℕ} (parts : Fin N → ℕ) (h : ∀ (i j : Fin N), i ≤ j → parts j ≤ parts i) : NPartition N

Construct an NPartition from a function and a proof that it satisfies the weakly decreasing predicate (in the explicit form used in SchurBasics.lean and PieriJacobiTrudi.lean).

Equations

• NPartition.mk' parts h = { parts := parts, antitone := h }

@[simp]

theorem NPartition.mk'_parts {N : ℕ} (parts : Fin N → ℕ) (h : ∀ (i j : Fin N), i ≤ j → parts j ≤ parts i) : (mk' parts h).parts = parts

@[simp]

theorem NPartition.mk'_antitone {N : ℕ} (parts : Fin N → ℕ) (h : ∀ (i j : Fin N), i ≤ j → parts j ≤ parts i) : ⋯ = h

Part accessor

def NPartition.part {N : ℕ} (μ : NPartition N) (i : Fin N) : ℕ

The i-th part of an N-partition (alias for parts i). This matches the naming in SchurBasics.lean.

Equations

• μ.part i = μ.parts i

@[simp]

theorem NPartition.part_eq_parts {N : ℕ} (μ : NPartition N) (i : Fin N) : μ.part i = μ.parts i

Bijection with Nat.Partition (Proposition prop.sf.Npar-as-par)

There is a bijection between partitions of length ≤ N and N-partitions. This is formalized in MonomialSymmetric.lean as NPartition.equivPartition. Here we provide the basic conversion functions.

def NPartition.ofPartition {N n : ℕ} (p : n.Partition) (_hp : p.parts.card ≤ N) : NPartition N

Convert a partition (as a Nat.Partition) to an N-partition by padding with zeros. Requires that the partition has at most N parts.

This corresponds to the map in Proposition prop.sf.Npar-as-par: (μ₁, μ₂, ..., μ_ℓ) ↦ (μ₁, μ₂, ..., μ_ℓ, 0, 0, ..., 0)

Equations

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

def NPartition.toPartition {N : ℕ} (μ : NPartition N) : μ.size.Partition

Convert an N-partition to a partition by removing trailing zeros.

Equations

• μ.toPartition = { parts := Multiset.filter (fun (x : ℕ) => x ≠ 0) (Multiset.map μ.parts Finset.univ.val), parts_pos := ⋯, parts_sum := ⋯ }

theorem NPartition.ofPartition_size {N n : ℕ} (p : n.Partition) (hp : p.parts.card ≤ N) : (ofPartition p hp).size = n

The size of ofPartition p equals n (the sum of the original partition). (Proposition prop.sf.Npar-as-par, well-definedness)

Label: prop.sf.Npar-as-par.size

theorem NPartition.toPartition_card_le {N : ℕ} (μ : NPartition N) : μ.toPartition.parts.card ≤ N

The number of non-zero parts of an N-partition is at most N. (Proposition prop.sf.Npar-as-par, boundedness)

Young Diagram (Definition def.sf.ydiag)

The Young diagram Y(λ) of an N-partition λ is the set of cells (i, j) where i ∈ [N] and j ∈ [λ_i].

Note: Mathlib has YoungDiagram which is more general (infinite diagrams). Here we define a version specific to N-partitions.

def NPartition.youngDiagram {N : ℕ} (μ : NPartition N) : Finset (Fin N × ℕ)

The Young diagram Y(λ) of an N-partition λ is the set of cells (i, j) where i ∈ Fin N and j < λ_i. Definition def.sf.ydiag in the source.

Note: Mathlib has YoungDiagram which is more general (infinite diagrams). Here we define a version specific to N-partitions.

Equations

• μ.youngDiagram = Finset.univ.biUnion fun (i : Fin N) => Finset.map { toFun := fun (j : ℕ) => (i, j), inj' := ⋯ } (Finset.range (μ.parts i))

theorem NPartition.mem_youngDiagram {N : ℕ} {μ : NPartition N} {c : Fin N × ℕ} : c ∈ μ.youngDiagram ↔ c.2 < μ.parts c.1

Membership in a Young diagram: (i, j) ∈ Y(λ) iff j < λ_i. This is the 0-indexed version of the textbook condition j ∈ [λ_i]. Definition def.sf.ydiag in the source.

theorem NPartition.mem_youngDiagram' {N : ℕ} {μ : NPartition N} {i : Fin N} {j : ℕ} : (i, j) ∈ μ.youngDiagram ↔ j < μ.parts i

Alternative characterization: membership in terms of the row index

theorem NPartition.youngDiagram_eq_empty_iff {N : ℕ} {μ : NPartition N} : μ.youngDiagram = ∅ ↔ μ = 0

The Young diagram is empty iff the partition is zero. This follows from the definition: Y(λ) = {(i,j) | j < λ_i}, which is empty iff all λ_i = 0.

theorem NPartition.youngDiagram_nonempty_iff {N : ℕ} {μ : NPartition N} : μ.youngDiagram.Nonempty ↔ μ ≠ 0

The Young diagram is nonempty iff the partition is nonzero

theorem NPartition.youngDiagram_row_card {N : ℕ} (μ : NPartition N) (i : Fin N) : {c ∈ μ.youngDiagram | c.1 = i}.card = μ.parts i

The row i of the Young diagram has exactly μ.parts i elements. This captures the definition that row i has λ_i boxes.

theorem NPartition.youngDiagram_snd_lt_parts {N : ℕ} {μ : NPartition N} {c : Fin N × ℕ} (h : c ∈ μ.youngDiagram) : c.2 < μ.parts c.1

Cells in a Young diagram have bounded column indices

theorem NPartition.youngDiagram_subset_prod {N : ℕ} (μ : NPartition N) (hN : 0 < N) : μ.youngDiagram ⊆ Finset.univ ×ˢ Finset.range (μ.parts ⟨0, hN⟩)

The Young diagram is bounded by the first row length (when N > 0). Since λ is weakly decreasing, all columns are at most λ_0.

theorem NPartition.youngDiagram_subset_prod' {N : ℕ} [NeZero N] (μ : NPartition N) : μ.youngDiagram ⊆ Finset.univ ×ˢ Finset.range (μ.parts 0)

Version of youngDiagram_subset_prod using [NeZero N] typeclass. Useful for code that already has [NeZero N] in scope.

theorem NPartition.mem_youngDiagram_zero_col {N : ℕ} {μ : NPartition N} {i : Fin N} : (i, 0) ∈ μ.youngDiagram ↔ 0 < μ.parts i

The cell (i, 0) is in the Young diagram iff μ_i > 0. This characterizes which rows are nonempty.

instance NPartition.youngDiagram_decidableMem {N : ℕ} (μ : NPartition N) : DecidablePred fun (x : Fin N × ℕ) => x ∈ μ.youngDiagram

Decidability of membership in Young diagram

Equations

• μ.youngDiagram_decidableMem c = decidable_of_iff (c.2 < μ.parts c.1) ⋯

theorem NPartition.youngDiagram_card {N : ℕ} (μ : NPartition N) : μ.youngDiagram.card = μ.size

The total number of cells in the Young diagram equals the size of the partition.

@[simp]

theorem NPartition.youngDiagram_zero {N : ℕ} : youngDiagram 0 = ∅

The zero N-partition has empty Young diagram

theorem NPartition.le_iff_youngDiagram_subset {N : ℕ} {μ ν : NPartition N} : μ ≤ ν ↔ μ.youngDiagram ⊆ ν.youngDiagram

μ ≤ ν is equivalent to Y(μ) ⊆ Y(ν). This is the key equivalence for partition containment.

Skew Young Diagram (Definition def.sf.skew-diag)

This is the canonical Finset version of skew Young diagrams.

The skew Young diagram Y(λ/μ) of two N-partitions λ and μ (where μ ⊆ λ componentwise) is the set of cells in Y(λ) but not in Y(μ). In other words: Y(λ/μ) = {(i, j) | μ_i ≤ j < λ_i}

This uses 0-indexed columns (j starts from 0), following Mathlib/programming conventions.

Alternative definitions:

• AlgebraicCombinatorics.skewYoungDiagram in LittlewoodRichardson.lean returns a Set and uses 1-indexed columns: {(i, j) | μ_i < j ≤ λ_i}. This matches textbook conventions.
• skewYoungDiagram in SchurBasics.lean is a duplicate that requires [NeZero N]. Prefer this canonical version when possible.

The two indexing conventions are equivalent via the bijection (i, j) ↔ (i, j+1). See SchurBasics.skewYoungDiagram_equiv_LR for the equivalence proof.

def NPartition.skewYoungDiagram {N : ℕ} (lam mu : NPartition N) : Finset (Fin N × ℕ)

The skew Young diagram Y(λ/μ) is the set difference Y(λ) \ Y(μ). This consists of cells (i, j) where μ_i ≤ j < λ_i. Definition def.sf.skew-diag in the source.

This is the canonical Finset version of skew Young diagrams.

Other versions exist for different use cases:

• AlgebraicCombinatorics.skewYoungDiagram in LittlewoodRichardson.lean returns a Set and uses 1-indexed columns (textbook convention)
• skewYoungDiagram in SchurBasics.lean is a duplicate that requires [NeZero N] (prefer this canonical version)

Indexing Convention: Uses 0-indexed columns (Mathlib convention).

• Here: (i, j) ∈ Y(λ/μ) iff μ_i ≤ j < λ_i
• LittlewoodRichardson: (i, j) ∈ Y(λ/μ) iff μ_i < j ≤ λ_i (1-indexed)

The bijection (i, j) ↔ (i, j+1) converts between conventions. See SchurBasics.skewYoungDiagram_equiv_LR for the equivalence proof.

Equations

• lam.skewYoungDiagram mu = lam.youngDiagram \ mu.youngDiagram

theorem NPartition.mem_skewYoungDiagram {N : ℕ} {lam mu : NPartition N} {c : Fin N × ℕ} : c ∈ lam.skewYoungDiagram mu ↔ mu.parts c.1 ≤ c.2 ∧ c.2 < lam.parts c.1

Membership in a skew Young diagram: (i, j) ∈ Y(λ/μ) iff μ_i ≤ j < λ_i. This is the 0-indexed version of the textbook condition μ_i < j ≤ λ_i.

theorem NPartition.mem_skewYoungDiagram' {N : ℕ} {lam mu : NPartition N} {i : Fin N} {j : ℕ} : (i, j) ∈ lam.skewYoungDiagram mu ↔ j ∈ Finset.Ico (mu.parts i) (lam.parts i)

Alternative characterization: membership in terms of row index

@[simp]

theorem NPartition.skewYoungDiagram_self {N : ℕ} (lam : NPartition N) : lam.skewYoungDiagram lam = ∅

The skew diagram Y(λ/λ) is empty.

@[simp]

theorem NPartition.skewYoungDiagram_zero' {N : ℕ} (lam : NPartition N) : lam.skewYoungDiagram 0 = lam.youngDiagram

The skew diagram Y(λ/0) equals Y(λ).

theorem NPartition.skewYoungDiagram_subset_youngDiagram {N : ℕ} (lam mu : NPartition N) : lam.skewYoungDiagram mu ⊆ lam.youngDiagram

The skew diagram is contained in the larger Young diagram.

instance NPartition.skewYoungDiagram_decidableMem {N : ℕ} (lam mu : NPartition N) : DecidablePred fun (x : Fin N × ℕ) => x ∈ lam.skewYoungDiagram mu

Decidability of membership in skew Young diagram

Equations

• lam.skewYoungDiagram_decidableMem mu c = decidable_of_iff (mu.parts c.1 ≤ c.2 ∧ c.2 < lam.parts c.1) ⋯

theorem NPartition.skewYoungDiagram_card {N : ℕ} (lam mu : NPartition N) : (lam.skewYoungDiagram mu).card = ∑ i : Fin N, (lam.parts i - mu.parts i)

The cardinality of a skew Young diagram.

theorem NPartition.skewYoungDiagram_eq_empty_iff {N : ℕ} {lam mu : NPartition N} : lam.skewYoungDiagram mu = ∅ ↔ ∀ (i : Fin N), lam.parts i ≤ mu.parts i

The skew diagram is empty iff λ ≤ μ componentwise.

Row and Column Partitions

Special partitions consisting of a single row or column, used in the Pieri rules and connections to symmetric functions. These are moved from PieriJacobiTrudi.lean as part of the consolidation effort.

def NPartition.rowPartition (N n : ℕ) (_hN : 0 < N) : NPartition N

The row partition (n, 0, 0, ..., 0) with n boxes in the first row. This is the partition corresponding to h_n (complete homogeneous symmetric polynomial). Requires N > 0 to have at least one row.

Equations

• NPartition.rowPartition N n _hN = { parts := fun (i : Fin N) => if ↑i = 0 then n else 0, antitone := ⋯ }

@[simp]

theorem NPartition.rowPartition_size (N n : ℕ) (hN : 0 < N) : (rowPartition N n hN).size = n

The row partition has size n.

@[simp]

theorem NPartition.rowPartition_parts_zero (N n : ℕ) (hN : 0 < N) : (rowPartition N n hN).parts ⟨0, hN⟩ = n

The first part of the row partition is n.

@[simp]

theorem NPartition.rowPartition_parts_pos (N n : ℕ) (hN : 0 < N) (i : Fin N) (hi : 0 < ↑i) : (rowPartition N n hN).parts i = 0

All other parts of the row partition are 0.

theorem NPartition.card_filter_fin_val_lt (N n : ℕ) (hn : n ≤ N) : {i : Fin N | ↑i < n}.card = n

The cardinality of elements of Fin N with value less than n is n (when n ≤ N). This is a specialized form of Fin.card_filter_val_lt for the case when n ≤ N.

Used for proving properties of colPartition.

theorem NPartition.sum_ite_fin_val_lt_eq (N n : ℕ) (hn : n ≤ N) : (∑ i : Fin N, if ↑i < n then 1 else 0) = n

The sum of indicators if i.val < n then 1 else 0 over Fin N equals n (when n ≤ N).

Used for proving properties of colPartition.

def NPartition.colPartition (N n : ℕ) (_hn : n ≤ N) : NPartition N

The column partition (1, 1, ..., 1, 0, ..., 0) with n ones (n boxes in first column). This is the partition corresponding to e_n (elementary symmetric polynomial). Requires n ≤ N (can't have more rows than N).

Equations

• NPartition.colPartition N n _hn = { parts := fun (i : Fin N) => if ↑i < n then 1 else 0, antitone := ⋯ }

@[simp]

theorem NPartition.colPartition_size (N n : ℕ) (hn : n ≤ N) : (colPartition N n hn).size = n

The column partition has size n.

@[simp]

theorem NPartition.colPartition_parts_lt (N n : ℕ) (hn : n ≤ N) (i : Fin N) (hi : ↑i < n) : (colPartition N n hn).parts i = 1

The first n parts of the column partition are 1.

@[simp]

theorem NPartition.colPartition_parts_ge (N n : ℕ) (hn : n ≤ N) (i : Fin N) (hi : n ≤ ↑i) : (colPartition N n hn).parts i = 0

Parts beyond n in the column partition are 0.

Transpose of a partition

The transpose of a partition λ is denoted λᵗ and satisfies: (λᵗ)ᵢ = |{j : λⱼ ≥ i+1}| for each i.

Since we work with fixed-length tuples, we define a predicate IsTranspose that captures when two tuples represent transpose partitions.

noncomputable def NPartition.transpose {N : ℕ} (μ : NPartition N) (hN : 0 < N) : NPartition (μ.parts ⟨0, hN⟩)

The transpose of a partition. See Exercise exe.pars.transpose in the source. The transpose λᵗ satisfies: (λᵗ)ᵢ = |{j : λⱼ ≥ i+1}| for each i. The length of the transpose equals the first (largest) part of λ.

Equations

• μ.transpose hN = { parts := fun (i : Fin (μ.parts ⟨0, hN⟩)) => {j : Fin N | ↑i + 1 ≤ μ.parts j}.card, antitone := ⋯ }

def NPartition.IsTranspose {N M : ℕ} (lam : Fin N → ℕ) (lamt : Fin M → ℕ) : Prop

Predicate asserting that lamt is the transpose of lam. The transpose λᵗ of a partition λ satisfies: (λᵗ)ᵢ = |{j : λⱼ ≥ i}| for each i.

Since we work with fixed-length tuples, this predicate captures when two tuples represent transpose partitions (possibly with trailing zeros).

Equations

• NPartition.IsTranspose lam lamt = ((∀ (i : Fin M), lamt i = {j : Fin N | ↑i + 1 ≤ lam j}.card) ∧ ∀ (j : Fin N), lam j = {i : Fin M | ↑j + 1 ≤ lamt i}.card)

theorem NPartition.zero_isTranspose {N : ℕ} : IsTranspose (fun (x : Fin N) => 0) fun (x : Fin N) => 0

The zero partition is its own transpose.

Namespace aliases for migration

NOTE: The aliases below are commented out because they conflict with existing local NPartition definitions in MonomialSymmetric.lean and PieriJacobiTrudi.lean. To migrate a file to use the shared definition:

1. Import this file
2. Remove the local structure NPartition definition
3. Uncomment the appropriate alias below, OR use open _root_.NPartition

-- namespace AlgComb.SymmetricFunctions -- abbrev NPartition := root.NPartition -- end AlgComb.SymmetricFunctions

-- Note: We don't create a SymmetricFunctions.NPartition alias here because -- PieriJacobiTrudi.lean already defines its own SymmetricFunctions.NPartition -- structure. Migration of PieriJacobiTrudi.lean is tracked separately.