The graphic matroid

The cycle (graphic) matroid of a finite multigraph: the matroid on the edge set whose independent sets are exactly the forests. See docs/fairest-edge-usage.md for why this connection matters: the paper's spanning-tree results are really matroid facts, so we route through Matroid.IsBase rather than reproving them directly.

def Multigraph.graphicMatroid {V : Type u_1} {E : Type u_2} [Finite E] (G : Multigraph V E) : Matroid E

The cycle (graphic) matroid of a finite multigraph G: the matroid on the edge set E whose independent sets are the forests of G.

Equations

• G.graphicMatroid = (Multigraph.indepMatroid✝ G).matroid

@[simp]

theorem Multigraph.graphicMatroid_indep {V : Type u_1} {E : Type u_2} [Finite E] (G : Multigraph V E) {I : Set E} : G.graphicMatroid.Indep I ↔ G.IsForest I

@[simp]

theorem Multigraph.graphicMatroid_E {V : Type u_1} {E : Type u_2} [Finite E] (G : Multigraph V E) : G.graphicMatroid.E = Set.univ

theorem Multigraph.isSpanningTree_iff_isBase {V : Type u_1} {E : Type u_2} [Finite E] (G : Multigraph V E) (hGconn : (G.toSimpleGraph Set.univ).Connected) {T : Set E} : G.IsSpanningTree T ↔ G.graphicMatroid.IsBase T

A spanning tree is exactly a base of the graphic matroid, provided G itself (using all of its edges) is connected.

theorem Multigraph.isBase_union_of_isBase_restrict_isBase_contract {V : Type u_1} {E : Type u_2} [Finite E] (G : Multigraph V E) {A I J : Set E} (hI : (G.graphicMatroid.restrict A).IsBase I) (hJ : (G.graphicMatroid.contract I).IsBase J) : G.graphicMatroid.IsBase (J ∪ I)

The gluing fact behind assembling a spanning tree of G out of a spanning tree of one vertex block plus a spanning tree of the rest of the graph with that block contracted to a point: given a spanning tree I of the induced subgraph on edge set A, and a spanning tree J of the contraction of G.graphicMatroid by I, the union J ∪ I is a spanning tree of the whole graph. This is just a specialization of Mathlib's general matroid restriction/contraction API (Matroid.Indep.union_isBasis_union_of_contract_isBasis).