Oriented Matroids

Stream: maths

[Jihoon Hyun]

Is anyone working on oriented matroids? I remember there was a repository for this, but I'm not sure if it aligns well with the current implementation of matroid.

[Floris van Doorn]

There is #16239

[Julian Berman]

(Those are oriented manifolds right? Not matroids?)

[Floris van Doorn]

Oops, I didn't read carefully :man_facepalming:

[Julian Berman]

@Jihoon Hyun I think if you're recalling something matroid-related that probably @Peter Nelson was involved and/or at least might know what the state of things are.

[Peter Nelson]

Nothing I know of has been done

[Jihoon Hyun]

Then, I might start working on this soon.

[Antoine Chambert-Loir]

For a generalization of matroids that encompasses oriented matroids and some more objects, see https://arxiv.org/abs/2402.09612

[Peter Nelson]

Arrived here after reading this: > Oriented matroids

Jihoon Hyun said:

Oriented matroids

I'm struggling on formalizing this. I need some research on how to define 'infinite' oriented matroids which is relatable with the current implementation of Matroid. However the most reliable definition of infinite oriented matroid I could find is as noted in 'Oriented Matroids' by Bjorner et al, which I don't think is relatable with B-matroids. If someone's interested, maybe we can talk about it in this thread

This paper probably contains the definitions you need.

That said, I don’t think there is any issues with just making them finite (i.e. making the ambient type finite in the definition). I don’t regret allowing mathlib matroids to be infinite, but it has been a massive amount of work which has required fleshing out a lot of the theory myself (I’m in the process of writing a paper with a bunch of new stuff on infinite matroids that has directly come out of formalization). And that was with the help of a somewhat robust literature of infinite matroids already existing.

To get something started on oriented matroids, I think finiteness is ok.

[Jihoon Hyun]

@Peter Nelson Thank you for the guidance, especially for pointing out the right reference!
However, I'd like to work on infinite oriented matroids: Simply defining it shouldn't be a lot of effort. Also it should be much less work to first define an infinite structure then restrict it to finite case to prove several theorems and later generalizing to infinite case, than to define the finite structure, work on that, and later refactor every theorem.