Noncrossing partitions

Let s be a finite set of positions in a linear order. A finite partition P of s is noncrossing if there are no positions a < b < c < d with a and c in one part of P and b and d in a different part. For s = Finset.univ : Finset (Fin n) these are the noncrossing partitions of n ordered positions, which index the moment–cumulant formula of free probability.

The noncrossing partitions of s, ordered by refinement, form a finite lattice NC(s). Its meet is the common refinement of Finpartition, its bottom element is the partition into singletons and its top element is the partition with one part (no parts when s = ∅). Its join is the least noncrossing partition coarser than both arguments; mathematically it can be strictly coarser than their join among all partitions, which may cross. Mathlib's Finpartition s has only a meet, not a join, so the join in NC(s) is characterised by its universal property (le_sup_left, le_sup_right, sup_le) rather than by a comparison lemma.

Main definitions

• Finpartition.IsNoncrossing P — the finite partition P of s is noncrossing.
• TauCeti.NoncrossingPartition s — the noncrossing partitions of s, with the refinement order inherited from Finpartition s.
• TauCeti.NoncrossingPartition.singletonPartEquiv — the noncrossing partitions of s in which i forms a part on its own correspond to the noncrossing partitions of s.erase i.

Main results

• Finpartition.isNoncrossing_bot, Finpartition.isNoncrossing_top — the partitions into singletons and into one part are noncrossing.
• Finpartition.IsNoncrossing.part_eq_part — in a noncrossing partition, positions a < b < c < d with a, c in one part and b, d in one part all lie in one part.
• Finpartition.IsNoncrossing.inf — common refinements of noncrossing partitions are noncrossing.
• Finpartition.IsNoncrossing.restrict — restricting a noncrossing partition of s to a subset of s gives a noncrossing partition.
• Finpartition.IsNoncrossing.bind — juxtaposing noncrossing partitions of the parts of a noncrossing partition gives a noncrossing partition.
• Finpartition.IsNoncrossing.extend_singleton — adding a singleton part to a noncrossing partition gives a noncrossing partition.
• Finpartition.IsNoncrossing.exists_interval_mem_parts — a noncrossing partition of a nonempty set has a part containing every position between two of its elements; hence Finpartition.IsNoncrossing.exists_mem_parts_card_eq_one_or_adjacent — it has a singleton part or a part containing two positions that are adjacent in s.
• Finpartition.IsNoncrossing.le_and_lt_of_mem_part — for noncrossing P ≤ Q, the positions from the first position of a part B of P up to the next position after B of the part of Q containing B form a union of parts of P.
• Finpartition.IsNoncrossing.exists_part_eq_union — merging the parts through two adjacent positions of a noncrossing partition gives a noncrossing partition.
• Finpartition.isNoncrossing_pairPartition, Finpartition.isNoncrossing_splitPartition — the partition with one pair part and singletons elsewhere is noncrossing, and so is splitting off a part containing every position between two of its elements.
• TauCeti.NoncrossingPartition.instLattice — the noncrossing partitions of s form a lattice, with meets computed in Finpartition s; it is bounded, and locally finite so that its incidence algebra is available.
• TauCeti.NoncrossingPartition.univ_eq_bot_top_of_pair — a set with at most two elements has only the partitions into singletons and into one part, which differ by TauCeti.NoncrossingPartition.bot_ne_top_of_one_lt_card once it has two elements; a one-element set has a unique noncrossing partition, and TauCeti.NoncrossingPartition.bot_eq_top_iff_card_le_one says that these two partitions coincide exactly for sets with at most one element.
• TauCeti.NoncrossingPartition.sup_pairPartition_eq_top_iff — for positions i ≤ j adjacent in s, a noncrossing partition joins with the pair part {i, j} to the partition into one part exactly when its parts through i and j cover s; the converse direction, TauCeti.NoncrossingPartition.sup_pairPartition_eq_top_of_union_eq, needs no adjacency.
• TauCeti.NoncrossingPartition.part_union_eq_of_sup_pairPartition_eq_top and TauCeti.NoncrossingPartition.splitPartition_mem_erase_top_sup_pairPartition — for the two first positions m₁ < m₂ of s, the noncrossing partitions other than 1̂ joining with the pair part {m₁, m₂} to 1̂ have distinct parts through m₁ and m₂ covering s, and splitting off a convex set of positions containing m₂ but not m₁ gives such a partition.

References

• A. Nica, R. Speicher, Lectures on the Combinatorics of Free Probability, Lecture 9.
• G. Kreweras, Sur les partitions non croisées d'un cycle, Discrete Math. 1 (1972), 333–350.

def Finpartition.IsNoncrossing {α : Type u_1} [LinearOrder α] {s : Finset α} (P : Finpartition s) : Prop

A finite partition of a set of positions in a linear order is noncrossing if whenever a < b < c < d with a, c in a part B and b, d in a part C, the parts coincide.

theorem Finpartition.isNoncrossing_iff {α : Type u_1} [LinearOrder α] {s : Finset α} {P : Finpartition s} : P.IsNoncrossing ↔ ∀ B ∈ P.parts, ∀ C ∈ P.parts, ∀ a ∈ B, ∀ b ∈ C, ∀ c ∈ B, ∀ d ∈ C, a < b → b < c → c < d → B = C

@[instance_reducible]

instance Finpartition.instDecidablePredFinsetIsNoncrossing {α : Type u_1} [LinearOrder α] {s : Finset α} : DecidablePred IsNoncrossing

theorem Finpartition.isNoncrossing_iff_part {α : Type u_1} [LinearOrder α] {s : Finset α} {P : Finpartition s} : P.IsNoncrossing ↔ ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ P.part a, ∀ d ∈ P.part b, a < b → b < c → c < d → P.part a = P.part b

Noncrossingness in terms of the part P.part a containing each position: if a < b < c < d are positions of s with c in the part of a and d in the part of b, then a and b lie in the same part.

theorem Finpartition.IsNoncrossing.part_eq_part {α : Type u_1} [LinearOrder α] {s : Finset α} {P : Finpartition s} (hP : P.IsNoncrossing) {a b c d : α} (ha : a ∈ s) (hb : b ∈ s) (hac : P.part a = P.part c) (hbd : P.part b = P.part d) (hab : a < b) (hbc : b < c) (hcd : c < d) : P.part a = P.part b

In a noncrossing partition, positions a < b < c < d with a, c in a common part and b, d in a common part all lie in one part.

@[simp]

theorem Finpartition.isNoncrossing_bot {α : Type u_1} [LinearOrder α] {s : Finset α} : ⊥.IsNoncrossing

The partition into singletons is noncrossing.

@[simp]

theorem Finpartition.isNoncrossing_top {α : Type u_1} [LinearOrder α] {s : Finset α} : ⊤.IsNoncrossing

The partition with at most one part is noncrossing.

theorem Finpartition.IsNoncrossing.inf {α : Type u_1} [LinearOrder α] {s : Finset α} {P Q : Finpartition s} (hP : P.IsNoncrossing) (hQ : Q.IsNoncrossing) : (P ⊓ Q).IsNoncrossing

Common refinements of noncrossing partitions are noncrossing.

theorem Finpartition.IsNoncrossing.restrict {α : Type u_1} [LinearOrder α] {s t : Finset α} {P : Finpartition s} (hP : P.IsNoncrossing) (hts : t ⊆ s) : (P.restrict hts).IsNoncrossing

Restricting a noncrossing partition of s to a subset t ⊆ s, by intersecting each part with t, gives a noncrossing partition of t.

theorem Finpartition.IsNoncrossing.bind {α : Type u_1} [LinearOrder α] {s : Finset α} {P : Finpartition s} {Q : (B : Finset α) → B ∈ P.parts → Finpartition B} (hP : P.IsNoncrossing) (hQ : ∀ (B : Finset α) (hB : B ∈ P.parts), (Q B hB).IsNoncrossing) : (P.bind Q).IsNoncrossing

Juxtaposing noncrossing partitions of the parts of a noncrossing partition gives a noncrossing partition.

theorem Finpartition.IsNoncrossing.extend_singleton {α : Type u_1} [LinearOrder α] {s t : Finset α} {P : Finpartition t} (hP : P.IsNoncrossing) {i : α} (hi : {i} ≠ ⊥) (hti : Disjoint t {i}) (hts : t ∪ {i} = s) : (P.extend hi hti hts).IsNoncrossing

Adding a singleton part to a noncrossing partition gives a noncrossing partition.

theorem Finpartition.IsNoncrossing.exists_interval_mem_parts {α : Type u_1} [LinearOrder α] {s : Finset α} {P : Finpartition s} (hP : P.IsNoncrossing) (hs : s.Nonempty) : ∃ B ∈ P.parts, ∀ x ∈ B, ∀ y ∈ B, ∀ z ∈ s, x < z → z < y → z ∈ B

A noncrossing partition of a nonempty set has an interval part: a part containing every position of s that lies between two of its elements.

theorem Finpartition.IsNoncrossing.exists_mem_parts_card_eq_one_or_adjacent {α : Type u_1} [LinearOrder α] {s : Finset α} {P : Finpartition s} (hP : P.IsNoncrossing) (hs : s.Nonempty) : ∃ B ∈ P.parts, B.card = 1 ∨ ∃ x ∈ B, ∃ y ∈ B, x < y ∧ ∀ z ∈ s, z ≤ x ∨ y ≤ z

A noncrossing partition of a nonempty set has a part that is a singleton or that contains two positions with no position of s strictly between them.

theorem Finpartition.IsNoncrossing.le_and_lt_of_mem_part {α : Type u_1} [LinearOrder α] {s : Finset α} {P Q : Finpartition s} (hP : P.IsNoncrossing) (hQ : Q.IsNoncrossing) (hPQ : P ≤ Q) {m M t : α} (hM : M ∈ P.part m) (hmin : ∀ z ∈ P.part m, m ≤ z) (hmax : ∀ z ∈ P.part m, z ≤ M) (ht : t ∈ Q.part m) (hMt : M < t) (htmin : ∀ z ∈ Q.part m, M < z → t ≤ z) {a b : α} (hb : b ∈ P.part a) (hma : m ≤ a) (hat : a < t) : m ≤ b ∧ b < t

Let P ≤ Q be noncrossing partitions, let m and M be the first and the last position of the part of P through m, and let t be the first position after M of the part of Q through m. Then [m, t) is a union of parts of P: a part of P leaving it would cross the part of P through m or the part of Q through m.

theorem Finpartition.IsNoncrossing.exists_part_eq_union {α : Type u_1} [LinearOrder α] {s : Finset α} {P : Finpartition s} (hP : P.IsNoncrossing) {i j : α} (hi : i ∈ s) (hij : i ≤ j) (hadj : ∀ z ∈ s, z ≤ i ∨ j ≤ z) : ∃ (Q : Finpartition s), Q.IsNoncrossing ∧ P ≤ Q ∧ Q.part i = P.part i ∪ P.part j

Merging the parts through two positions i ≤ j of s with no position of s strictly between them keeps a noncrossing partition noncrossing: there is a coarser noncrossing partition whose part through i is the union of the parts through i and j. (If j ∉ s, its part is empty and P itself works.)

theorem Finpartition.isNoncrossing_pairPartition {α : Type u_1} [LinearOrder α] {s : Finset α} {i j : α} (hij : {i, j} ⊆ s) : (pairPartition s i j hij).IsNoncrossing

The partition with one pair part {i, j} and singletons elsewhere is noncrossing.

theorem Finpartition.isNoncrossing_splitPartition {α : Type u_1} [LinearOrder α] {s C : Finset α} {hC : C.Nonempty} {hCs : C ⊆ s} (hconv : ∀ a ∈ C, ∀ c ∈ C, ∀ b ∈ s, a < b → b < c → b ∈ C) : (splitPartition s C hC hCs).IsNoncrossing

Splitting off a part C that contains every position of s between two of its elements gives a noncrossing partition.

@[reducible, inline]

abbrev TauCeti.NoncrossingPartition {α : Type u_1} [LinearOrder α] (s : Finset α) : Type u_1

The noncrossing partitions of a finite set s of positions in a linear order, ordered by refinement. For s = Finset.univ : Finset (Fin n) this is the lattice NC(n) of noncrossing partitions of n ordered positions.

@[instance_reducible]

noncomputable instance TauCeti.NoncrossingPartition.instLattice {α : Type u_1} [LinearOrder α] {s : Finset α} : Lattice (NoncrossingPartition s)

The noncrossing partitions of s form a lattice. The meet is the common refinement, and the join of P and Q is the meet of all noncrossing partitions coarser than both.

@[instance_reducible]

instance TauCeti.NoncrossingPartition.instBoundedOrder {α : Type u_1} [LinearOrder α] {s : Finset α} : BoundedOrder (NoncrossingPartition s)

@[simp]

theorem TauCeti.NoncrossingPartition.coe_inf {α : Type u_1} [LinearOrder α] {s : Finset α} (P Q : NoncrossingPartition s) : ↑(P ⊓ Q) = ↑P ⊓ ↑Q

@[simp]

theorem TauCeti.NoncrossingPartition.coe_bot {α : Type u_1} [LinearOrder α] {s : Finset α} : ↑⊥ = ⊥

@[simp]

theorem TauCeti.NoncrossingPartition.coe_top {α : Type u_1} [LinearOrder α] {s : Finset α} : ↑⊤ = ⊤

@[instance_reducible]

instance TauCeti.NoncrossingPartition.instLocallyFiniteOrder {α : Type u_1} [LinearOrder α] {s : Finset α} : LocallyFiniteOrder (NoncrossingPartition s)

The noncrossing partitions of s form a finite poset with decidable order, hence a locally finite order; this makes its incidence algebra, with its zeta and Möbius functions, available.

theorem TauCeti.NoncrossingPartition.eq_bot_of_eq_empty {α : Type u_1} [LinearOrder α] {s : Finset α} (hs : s = ∅) (P : NoncrossingPartition s) : P = ⊥

A noncrossing partition of the empty set is the partition into no parts.

@[instance_reducible]

instance TauCeti.NoncrossingPartition.instUniqueEmptyCollectionFinset {α : Type u_1} [LinearOrder α] : Unique (NoncrossingPartition ∅)

The partition of the empty set into no parts is its only noncrossing partition.

@[instance_reducible]

instance TauCeti.NoncrossingPartition.instUniqueOfIsEmpty {α : Type u_1} [LinearOrder α] {s : Finset α} [IsEmpty α] : Unique (NoncrossingPartition s)

Over an empty type of positions, such as Fin 0, the partition into no parts is the only noncrossing partition; in particular NC(0) has a single element.

@[instance_reducible]

instance TauCeti.NoncrossingPartition.instUniqueSingletonFinset {α : Type u_1} [LinearOrder α] (i : α) : Unique (NoncrossingPartition {i})

The partition of a one-element set into its single part is its only noncrossing partition.

theorem TauCeti.NoncrossingPartition.bot_ne_top_of_one_lt_card {α : Type u_1} [LinearOrder α] {s : Finset α} (hs : 1 < s.card) : ⊥ ≠ ⊤

If s has at least two elements, the partition into singletons and the partition into one part are different noncrossing partitions of s.

theorem TauCeti.NoncrossingPartition.bot_eq_top_iff_card_le_one {α : Type u_1} [LinearOrder α] {s : Finset α} : ⊥ = ⊤ ↔ s.card ≤ 1

The partition into singletons and the partition into one part are the same noncrossing partition of s exactly when s has at most one element.

theorem TauCeti.NoncrossingPartition.eq_bot_or_eq_top_of_pair {α : Type u_1} [LinearOrder α] {i j : α} (P : NoncrossingPartition {i, j}) : P = ⊥ ∨ P = ⊤

A noncrossing partition of a set with at most two elements is either the partition into singletons or the partition into one part.

theorem TauCeti.NoncrossingPartition.univ_eq_bot_top_of_pair {α : Type u_1} [LinearOrder α] {i j : α} : Finset.univ = {⊥, ⊤}

The noncrossing partitions of a set with at most two elements are the partition into singletons and the partition into one part.

theorem TauCeti.NoncrossingPartition.sup_pairPartition_eq_top_of_union_eq {α : Type u_1} [LinearOrder α] {s : Finset α} {i j : α} (hij : {i, j} ⊆ s) (x : NoncrossingPartition s) (hx : (↑x).part i ∪ (↑x).part j = s) : x ⊔ ⟨Finpartition.pairPartition s i j hij, ⋯⟩ = ⊤

If the parts of a noncrossing partition x through two positions i and j of s cover s, then x joins with pairPartition s i j to the partition into one part. This direction of sup_pairPartition_eq_top_iff needs no adjacency of i and j.

theorem TauCeti.NoncrossingPartition.sup_pairPartition_eq_top_iff {α : Type u_1} [LinearOrder α] {s : Finset α} {i j : α} (hij : {i, j} ⊆ s) (hle : i ≤ j) (hadj : ∀ z ∈ s, z ≤ i ∨ j ≤ z) (x : NoncrossingPartition s) : x ⊔ ⟨Finpartition.pairPartition s i j hij, ⋯⟩ = ⊤ ↔ (↑x).part i ∪ (↑x).part j = s

Let i ≤ j be positions of s with no position of s strictly between them. A noncrossing partition x joins with pairPartition s i j to the partition into one part exactly when the parts of x through i and j cover s.

noncomputable def TauCeti.NoncrossingPartition.singletonPartEquiv {α : Type u_1} [LinearOrder α] {s : Finset α} {i : α} (hi : i ∈ s) : { π : NoncrossingPartition s // {i} ∈ (↑π).parts } ≃ NoncrossingPartition (s.erase i)

The noncrossing partitions of s in which i forms a part on its own correspond to the noncrossing partitions of s.erase i: delete the part {i}, or insert it back.

@[simp]

theorem TauCeti.NoncrossingPartition.parts_singletonPartEquiv_apply {α : Type u_1} [LinearOrder α] {s : Finset α} {i : α} (hi : i ∈ s) (π : { π : NoncrossingPartition s // {i} ∈ (↑π).parts }) : (↑((singletonPartEquiv hi) π)).parts = (↑↑π).parts.erase {i}

Deleting the singleton part {i} leaves the other parts.

@[simp]

theorem TauCeti.NoncrossingPartition.parts_singletonPartEquiv_symm_apply {α : Type u_1} [LinearOrder α] {s : Finset α} {i : α} (hi : i ∈ s) (τ : NoncrossingPartition (s.erase i)) : (↑↑((singletonPartEquiv hi).symm τ)).parts = insert {i} (↑τ).parts

Inserting the singleton part {i} adds it to the parts.

theorem TauCeti.NoncrossingPartition.part_union_eq_of_sup_pairPartition_eq_top {α : Type u_1} [LinearOrder α] {s : Finset α} {m₁ m₂ : α} (hpair : {m₁, m₂} ⊆ s) (hle : m₁ ≤ m₂) (hadj : ∀ z ∈ s, z ≤ m₁ ∨ m₂ ≤ z) {x : NoncrossingPartition s} (hxtop : x ≠ ⊤) (hx : x ⊔ ⟨Finpartition.pairPartition s m₁ m₂ hpair, ⋯⟩ = ⊤) : (↑x).part m₁ ∪ (↑x).part m₂ = s ∧ (↑x).part m₁ ≠ (↑x).part m₂

For positions m₁ ≤ m₂ adjacent in s (every position of s is ≤ m₁ or ≥ m₂), a noncrossing partition other than the partition into one part, whose join with the part {m₁, m₂} is the partition into one part, has distinct parts through m₁ and m₂ that cover s.

theorem TauCeti.NoncrossingPartition.splitPartition_mem_erase_top_sup_pairPartition {α : Type u_1} [LinearOrder α] {s : Finset α} {m₁ m₂ : α} (hpair : {m₁, m₂} ⊆ s) {T : Finset α} (hT : T.Nonempty) (hTs : T ⊆ s) (hconv : ∀ a ∈ T, ∀ c ∈ T, ∀ b ∈ s, a < b → b < c → b ∈ T) (hm₂T : m₂ ∈ T) (hm₁T : m₁ ∉ T) : ⟨Finpartition.splitPartition s T hT hTs, ⋯⟩ ∈ {x : NoncrossingPartition s | x ⊔ ⟨Finpartition.pairPartition s m₁ m₂ hpair, ⋯⟩ = ⊤}.erase ⊤

Splitting off a nonempty subset T of s that is convex relative to s (every position of s strictly between two elements of T lies in T), contains m₂ and omits m₁, gives a noncrossing partition other than the partition into one part, whose join with the part {m₁, m₂} is the partition into one part.