Pulling back noncrossing partitions along monotone maps

Let f : α → β be a map between linear orders that is monotone on a finite set s of positions. Its fibres cut s into consecutive intervals, and they form the partition σ_f of s into the fibres of f. Pulling back a partition of the image f '' s along f (Finpartition.comap) preserves and reflects noncrossingness, so it is an order embedding NC(f '' s) ↪o NC(s), and its image is the upper interval [σ_f, 1_s] of NC(s).

For s = Finset.univ : Finset (Fin n) and a monotone surjection f : Fin n → Fin m, the partition σ_f is the interval partition grouping the positions 1, …, n into m consecutive blocks, and the embedding is the lift NC(m) ↪o NC(n) of noncrossing partitions of the blocks. This is the combinatorial input of the formula for free cumulants whose arguments are products of consecutive letters.

Main definitions

• TauCeti.NoncrossingPartition.comap hf — the order embedding NC(f '' s) ↪o NC(s) given by pulling back along a map f that is monotone on s.

Main results

• Finpartition.isNoncrossing_comap_iff — the pullback of a partition of f '' s along a map that is monotone on s is noncrossing exactly when the partition is.
• TauCeti.NoncrossingPartition.exists_comap_eq_iff — a noncrossing partition of s is a pullback exactly when it is coarser than the partition σ_f of s into the fibres of f.
• TauCeti.NoncrossingPartition.mem_part_union_part_of_sup_comap_bot_eq_top — if f identifies only two adjacent positions i ≤ j of s and π ⊔ σ_f = 1, then s is the union of the parts of π through i and j.

References

• A. Nica, R. Speicher, Lectures on the Combinatorics of Free Probability, Lecture 9 and Notation 11.9.

theorem Finpartition.isNoncrossing_comap_iff {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {s : Finset α} {f : α → β} {P : Finpartition (Finset.image f s)} (hf : MonotoneOn f ↑s) : (comap f P).IsNoncrossing ↔ P.IsNoncrossing

The pullback of a partition of f '' s along a map f that is monotone on s is noncrossing exactly when the partition is.

theorem Finpartition.IsNoncrossing.comap {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {s : Finset α} {f : α → β} {P : Finpartition (Finset.image f s)} (hf : MonotoneOn f ↑s) (hP : P.IsNoncrossing) : (Finpartition.comap f P).IsNoncrossing

The pullback of a noncrossing partition of f '' s along a map f that is monotone on s is noncrossing.

def TauCeti.NoncrossingPartition.comap {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {s : Finset α} {f : α → β} (hf : MonotoneOn f ↑s) : NoncrossingPartition (Finset.image f s) ↪o NoncrossingPartition s

Pulling back along a map f that is monotone on s embeds the noncrossing partitions of the image f '' s into the noncrossing partitions of s, as the partitions coarser than the partition of s into the fibres of f (TauCeti.NoncrossingPartition.exists_comap_eq_iff).

@[simp]

theorem TauCeti.NoncrossingPartition.coe_comap {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {s : Finset α} {f : α → β} (hf : MonotoneOn f ↑s) (ρ : NoncrossingPartition (Finset.image f s)) : ↑((comap hf) ρ) = Finpartition.comap f ↑ρ

@[simp]

theorem TauCeti.NoncrossingPartition.comap_top {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {s : Finset α} {f : α → β} (hf : MonotoneOn f ↑s) : (comap hf) ⊤ = ⊤

theorem TauCeti.NoncrossingPartition.exists_comap_eq_iff {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {s : Finset α} {f : α → β} {hf : MonotoneOn f ↑s} {π : NoncrossingPartition s} : (∃ (ρ : NoncrossingPartition (Finset.image f s)), (comap hf) ρ = π) ↔ (comap hf) ⊥ ≤ π

A noncrossing partition of s is the pullback of a noncrossing partition of f '' s along a map f that is monotone on s exactly when it is coarser than the partition of s into the fibres of f.

theorem TauCeti.NoncrossingPartition.mem_part_union_part_of_sup_comap_bot_eq_top {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {s : Finset α} {f : α → β} (hf : MonotoneOn f ↑s) {i j : α} (hi : i ∈ s) (hj : j ∈ s) (hij : i ≤ j) (hadj : ∀ z ∈ s, z ≤ i ∨ j ≤ z) (hfeq : ∀ {u v : α}, u ∈ s → v ∈ s → f u = f v → u ≠ v → (u = i ∨ u = j) ∧ (v = i ∨ v = j)) {π : NoncrossingPartition s} (hπ : π ⊔ (comap hf) ⊥ = ⊤) {z : α} (hz : z ∈ s) : z ∈ (↑π).part i ∪ (↑π).part j

Let f be monotone on s and identify no two positions other than i ≤ j, which are adjacent in s. If the join in NC(s) of π with the partition σ_f into the fibres of f is 1, then s is the union of the parts of π through i and j: merging these two parts gives a noncrossing partition above π and σ_f.