Incidence Algebra in Mathlib4?

Stream: general

[Sina]

Is the notion of incidence algebra (and reduced incidence algebra) for a locally finite poset somewhere on Mathlib4? (I could not find it using mathlib4 docs, but it might be there and i might have missed it). And, if not on Mathlib4, is there a Lean4 formalization off Mathlib4?

[Eric Wieser]

!3#11656 apparently has some work in this direction

[Eric Wieser]

@Yaël Dillies

[Alex J. Best]

Looks like Yaël has ported it here https://github.com/YaelDillies/LeanCamCombi/blob/mathport/LeanCamCombi/Incidence.lean, I haven't tried the lean 4 version but the lean 3 one was in write usable shape I think

[Yaël Dillies]

Yes, I ported it two days ago and am currently fixing the errors. I will then move the prereqs to the correct place inside LeanCamCombi.Mathlib and PR the prereqs that have no other prereqs.

[Alex J. Best]

@Sina do you know more specifically what sort of results you wanted about incidence algebras? We had some future plans but as you see this has been left dormant for a couple of years!

[Sina]

Nothing too deep, but I am mentoring two undergraduate students who would like to formalize inlcusion-exclusion principle in combinatorics using the incidence algebra and convolution with the Möbius function. Do you know if this is done somewhere with Lean4 or Lean3?

[Sina]

We are following the notes by P.Bartlett here: https://github.com/sinhp/Proofs-F23-Projects/blob/master/resources/math_116_s2015_lecture4.pdf

[Sina]

Yaël Dillies said:

Yes, I ported it two days ago and am currently fixing the errors. I will then move the prereqs to the correct place inside LeanCamCombi.Mathlib and PR the prereqs that have no other prereqs.

OK, I just found time to look at this! Lots of stuff in here are very useful for us! Looks great!

[Sina]

Also, the students I am mentoring are not math students so their background is limited. It is quite likely the formalization end up "reinventing the wheel" and not do it any the level of generality suitable for Mathlib4, but i still think it is very worthwhile for them to do so.

[Sina]

@Alex J. Best
I now see that you mention inclusion-exclusion type principles in file you and @Yaël Dillies shared.

[Alex J. Best]

Yeah I think that was about as far as we got, proving moebius inversion. We were hoping to do some applications like PIE and classical mobius inversion but never got around to it

[Alex J. Best]

So sounds like a good project!

[Yaël Dillies]

Update: I've now finished fixing most of it, until the definition of mu actually, so I've pushed it to main and it will appear on https://yaeldillies.github.io/LeanCamCombi shortly.