Order invariance, converse Möbius inversion and Weisner's theorem

The Möbius function is invariant under order isomorphisms (OrderIso.mu_map).

Mathlib's IncidenceAlgebra.moebius_inversion_bot recovers f from its lower sums g x = ∑_{y ≤ x} f y as f x = ∑_{y ≤ x} μ(y, x) g y. This file proves the converse direction: summing the Möbius transform x ↦ ∑_{z ≤ x} μ(z, x) g z over the lower set of x gives back g x.

It also proves Weisner's theorem: in a finite lattice, the values μ(⊥, x) summed over the elements x whose join with a fixed a ≠ ⊥ is ⊤ cancel. Choosing a to be an atom turns this into a recurrence for μ(⊥, ⊤) in terms of the Möbius function on smaller intervals; this is how the Möbius function of the lattice of noncrossing partitions is computed.

Main results

• IncidenceAlgebra.sum_Iic_sum_Iic_mu_mul — ∑_{y ≤ x} ∑_{z ≤ y} μ(z, y) g z = g x.
• IncidenceAlgebra.sum_filter_sup_eq_top_mu_bot_eq_zero — Weisner's theorem: for a ≠ ⊥, ∑_{x ⊔ a = ⊤} μ(⊥, x) = 0.

References

• L. Weisner, Abstract theory of inversion of finite series, Trans. Amer. Math. Soc. 38 (1935), 474–484.
• R. P. Stanley, Enumerative Combinatorics, Volume 1, 2nd ed., Corollary 3.9.3.

@[simp]

theorem OrderIso.mu_map {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommGroup 𝕜] [One 𝕜] [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] [PartialOrder β] [LocallyFiniteOrder β] [DecidableEq β] (e : α ≃o β) (a b : α) : (IncidenceAlgebra.mu 𝕜) (e a) (e b) = (IncidenceAlgebra.mu 𝕜) a b

The Möbius function is invariant under order isomorphisms.

theorem IncidenceAlgebra.sum_Iic_sum_Iic_mu_mul {𝕜 : Type u_1} {α : Type u_2} [NonAssocRing 𝕜] [PartialOrder α] [LocallyFiniteOrder α] [LocallyFiniteOrderBot α] [DecidableEq α] (g : α → 𝕜) (x : α) : ∑ y ≤ x, ∑ z ≤ y, (mu 𝕜) z y * g z = g x

Converse Möbius inversion: the lower sums of the Möbius transform y ↦ ∑_{z ≤ y} μ(z, y) g z of g recover g, ∑_{y ≤ x} ∑_{z ≤ y} μ(z, y) g z = g x.

theorem IncidenceAlgebra.sum_filter_sup_eq_top_mu_bot_eq_zero {𝕜 : Type u_1} {α : Type u_2} [Ring 𝕜] [Lattice α] [BoundedOrder α] [LocallyFiniteOrder α] [DecidableEq α] {a : α} (ha : a ≠ ⊥) : ∑ x ∈ Finset.Icc ⊥ ⊤ with x ⊔ a = ⊤, (mu 𝕜) ⊥ x = 0

Weisner's theorem: in a finite lattice, for every a ≠ ⊥ the Möbius function μ(⊥, x) sums to zero over the elements x with x ⊔ a = ⊤.