Lower intervals of the lattice of noncrossing partitions

Let π be a noncrossing partition of a finite set s of positions in a linear order. A noncrossing partition σ ≤ π is the same as a choice of a noncrossing partition of each part B of π: restricting σ to the parts of π and juxtaposing noncrossing partitions of the parts (Finpartition.bind) are inverse to each other, and both preserve refinement. Hence the lower interval [0_s, π] of NC(s) is isomorphic, as an order, to the product of the lattices NC(B) over the parts B of π.

Consequently, summing a multiplicative function σ ↦ ∏_{C ∈ σ} g C over σ ≤ π factors as the product over the parts B of π of its sums over NC(B). This factorisation is what makes the free cumulant of a noncrossing partition the product of the free cumulants of its parts.

Main definitions

• TauCeti.NoncrossingPartition.iicOrderIso π — the order isomorphism between the noncrossing partitions σ ≤ π and the families of noncrossing partitions of the parts of π.

Main results

• TauCeti.NoncrossingPartition.sum_Iic_prod_parts_eq_prod_sum — ∑_{σ ≤ π} ∏_{C ∈ σ} g C = ∏_{B ∈ π} ∑_{τ ∈ NC(B)} ∏_{C ∈ τ} g C.

References

• A. Nica, R. Speicher, Lectures on the Combinatorics of Free Probability, Lecture 9.
• R. Speicher, Multiplicative functions on the lattice of non-crossing partitions and free convolution, Math. Ann. 298 (1994), 611–628.

noncomputable def TauCeti.NoncrossingPartition.iicOrderIso {α : Type u_1} [LinearOrder α] {s : Finset α} (π : NoncrossingPartition s) : ↑(Set.Iic π) ≃o ((B : ↥(↑π).parts) → NoncrossingPartition ↑B)

The lower interval [0_s, π] of the lattice of noncrossing partitions of s is isomorphic to the product of the lattices of noncrossing partitions of the parts of π: a noncrossing partition σ ≤ π corresponds to its restrictions to the parts of π, and a family of noncrossing partitions of the parts corresponds to their juxtaposition.

@[simp]

theorem TauCeti.NoncrossingPartition.coe_iicOrderIso_apply {α : Type u_1} [LinearOrder α] {s : Finset α} (π : NoncrossingPartition s) (σ : ↑(Set.Iic π)) (B : ↥(↑π).parts) : ↑(π.iicOrderIso σ B) = (↑↑σ).restrict ⋯

@[simp]

theorem TauCeti.NoncrossingPartition.coe_iicOrderIso_symm_apply {α : Type u_1} [LinearOrder α] {s : Finset α} (π : NoncrossingPartition s) (Q : (B : ↥(↑π).parts) → NoncrossingPartition ↑B) : ↑↑(π.iicOrderIso.symm Q) = (↑π).bind fun (B : Finset α) (hB : B ∈ (↑π).parts) => ↑(Q ⟨B, hB⟩)

theorem TauCeti.NoncrossingPartition.sum_Iic_prod_parts_eq_prod_sum {α : Type u_1} [LinearOrder α] {s : Finset α} {M : Type u_2} [CommSemiring M] (π : NoncrossingPartition s) (g : Finset α → M) : ∑ σ ≤ π, ∏ C ∈ (↑σ).parts, g C = ∏ B ∈ (↑π).parts, ∑ τ : NoncrossingPartition B, ∏ C ∈ (↑τ).parts, g C

Summing a multiplicative function of the noncrossing partitions over the lower interval of a noncrossing partition π factors over the parts of π: ∑_{σ ≤ π} ∏_{C ∈ σ} g C = ∏_{B ∈ π} ∑_{τ ∈ NC(B)} ∏_{C ∈ τ} g C.