Preliminary "cographic matroids are regular" blueprint

Stream: Seymour

[Cameron Rampell]

Hi all, I've recently joined the project and I think I've written a somewhat lean4 compatible proof of the regularity of cographic matroids. I just needed to prove that the dual matroid of a regular matroid is also a regular matroid, and I tried to stay away from rank arguments as per @Martin Dvořák 's request. Most of the proofs I use involve relatively simple linear algebra.

Let me know if there's anything I can cut down on or I should add to improve the blueprint.

blueprint.pdf

[Cameron Rampell]

accidentally entered a new line :upside_down: new to zulip

[Byung-Hak Hwang]

Thank you for the blueprint. It looks great and well structured.

I have a couple of quick mathematical questions:

1. In the proof of Lemma 1.6, how do we take a matrix $B$ which is a standard $Z_2$-representation of $M$?
2. Is it necessary to work over the field $Z_2$? In other words, which parts of the blueprint specifically require that $char F=2$?

[Cameron Rampell]

1. AFAIK, by definition of regularity, a regular matroid $M$ is representable over the rationals, the reals, and all finite fields $F_p$, which includes $Z_2$. So we can write this regular matroid as some representation over $Z_2$. If we then choose a basis $X \subseteq E(M)$ and perform row operations so the basis columns become the identity matrix, the resulting matrix has block form $A = [1_X \mid B]$. And the submatrix $B$ is exactly the standard $Z_2$ representation of $M$. If you think I should, I can add some extra math clarifying this. Let me know if my reasoning is sound or not.
2. It's not necessary, but rather a matter of convenience. It just made the proof nicer.

[Cameron Rampell]

By the way, I uploaded an updated blueprint to Github: https://github.com/cappucher/Cographic-Matroids

[Byung-Hak Hwang]

Thank you for the comments.

The reason I asked the two questions is as follows. In our implementation, a matroid $M$ is regular if it is the vector matroid of a TU matrix $A$ over $Q$. So from the definition we can take a TU matrix $A$ over $Q$, but if one wants to use a standard $Z_2$-representation, then a bit more explanation may be needed. Since Lemmas 1.1, 1.2, and 1.3 also seem to hold over $Q$, I was wondering whether working with the TU matrix $A$ over $Q$ might make some parts of the proof simpler.

In any case, your argument looks sound, and the overall flow seems very reasonable and concise.

[Cameron Rampell]

Great. Aside from the minor explanations I might need to insert, are we ready to begin formalizing the blueprint?