Tutte polynomials of matroids

Stream: Is there code for X?

[Bernhard Reinke]

I saw that a lot of matroid theory has been recently added to mathlib by @Peter Nelson. Is there already a formalization of the Tutte polynomial? If not, I could try to do it, but I don't want to duplicate work if it is unnecessary.

[Peter Nelson]

I haven’t done this, and it is a good idea!

[Peter Nelson]

As of recently, mathlib should have all the needed machinery, with docs#Matroid.contract and docs#Matroid.delete . Any applications for graphs will need graphic matroids and multigraphs, neither of which are in mathlib or my repo yet.

[Peter Nelson]

But plenty of the material for Tutte polynomials will work at the generality of matroids, and will specialize routinely to graphs one the matroid/graph API is there.

I rode my bike past Tutte’s old house the other day!

[Bernhard Reinke]

Hmm, are you planning to add Matroid.Minor.Rank to mathlib soon? I think it makes sense to define the Tutte polynomial using eRelRk. My current attempt looks somewhat like this

import Mathlib

namespace Matroid
variable {α : Type*} {M : Matroid α} [M.Finite] {R : Type*} [CommRing R] (x y : R) {e : α}

variable (M) in
noncomputable def tutte.summand (s : Set α) : R :=
  (x - 1)^(M.eRank.toNat - (M.eRk s).toNat) * (y - 1)^(s.ncard - (M.eRk s).toNat)

variable (M) in
noncomputable def tutte : R := ∑ᶠ s ∈ M.E.powerset, tutte.summand M x y s
end Matroid

probably it is nicer to use

noncomputable def tutte.summand (s : Set α) : R :=
  (x - 1)^((M.eRelRk s M.E).toNat) * (y - 1)^((M✶.eRk s).toNat)

[Peter Nelson]

I can prioritize that. It is probably better to define relRk as (eRelRk _).toNat and to wrap it with sensible API to avoid working with toNat directly.

[Peter Nelson]

#23873 is in review, and there might be a need for another ENat rank PR, but I think Matroid.Minor.Rank can be next after that. @Bhavik Mehta , @Johan Commelin and @Kyle Miller are being very kind with their fast reviews at the moment!

[Peter Nelson]

I've just made #23951, which I think should contain all the eRk API needed to make eRelRk work.

[Bernhard Reinke]

I have created a WIP PR #23953 that deals with the manipulation of the sums in the Tutte polynomial, with 4 sorry lemmas where I would need to relate the summands of the Tutte polynomial to the deletion or contraction. Feel free to have a look already. I will attack those lemmas once we have eRelRk in mathlib.

[Bernhard Reinke]

Some basic sum manipulation is in #23926

[Peter Nelson]

That is looking very nice already!