Abstract Möbius inversion in mathlib?

Stream: maths

[Bob Jefferson]

I’m working on formalising a fairly abstract Möbius inversion framework in Lean, aiming to unify Dirichlet inversion and inclusion–exclusion as instances of a single algebraic statement.

Before duplicating work, I wanted to ask: is there already a general “abstract Möbius inversion” result in mathlib (e.g. phrased in terms of convolution algebras / incidence algebras), or is the existing coverage intentionally specialised to concrete settings like ℕ and Finset?

For context, I’ve written up the mathematics in a short note here :
[link]

I’m mainly interested in whether this abstraction aligns with current mathlib design, or whether it would be considered out of scope.

[Aaron Liu]

I see docs#IncidenceAlgebra.moebius_inversion_bot

[Bob Jefferson]

Thanks, that’s very helpful — I wasn’t aware of IncidenceAlgebra.moebius_inversion_bot, and this looks like exactly the right level of abstraction.

My interest here is less in reproving Möbius inversion per se, and more in understanding and explaining why Dirichlet inversion on ℕ and inclusion–exclusion on finite sets are instances of the same underlying mechanism, and how that perspective should guide formalisation choices.

I’ve attempted to lay out that conceptual unification for human readers, with those two cases as motivating examples, and it’s reassuring to see that the abstraction mathlib uses lines up with that viewpoint.

As a follow-up question: are there existing examples in mathlib that explicitly specialise IncidenceAlgebra to recover Dirichlet convolution or inclusion–exclusion, or would those be reasonable illustrative additions?

[Yaël Dillies]

No, currently nothing uses docs#IncidenceAlgebra

[Bob Jefferson]

Ah, so in that case, would it be considered reasonable to add illustrative specialisations (e.g. Dirichlet convolution on ℕ, or inclusion–exclusion on finite sets) as documentation or examples for IncidenceAlgebra, or is the intention that it remain a purely abstract interface?

[Yaël Dillies]

Sure, we need applications!

[Bob Jefferson]

Makes sense. By “applications”, do you mean small illustrative specialisations (Dirichlet, IE), or something more substantial?

[Yaël Dillies]

The ones you mentioned are good first ones. I'm sure there are more, but I'm not aware of them

[Bob Jefferson]

That’s helpful to know. I might explore a small illustrative example at some point.