Matroids

A Matroid is a structure that combinatorially abstracts the notion of linear independence and dependence; matroids have connections with graph theory, discrete optimization, additive combinatorics and algebraic geometry. Mathematically, a matroid M is a structure on a set E comprising a collection of subsets of E called the bases of M, where the bases are required to obey certain axioms.

This file gives a definition of a matroid M in terms of its bases, and some API relating independent sets (subsets of bases) and the notion of a basis of a set X (a maximal independent subset of X).

Main definitions

• a Matroid α on a type α is a structure comprising a 'ground set' and a suitably behaved 'base' predicate.

Given M : Matroid α ...

• M.E denotes the ground set of M, which has type Set α

• For B : Set α, M.Base B means that B is a base of M.

• For I : Set α, M.Indep I means that I is independent in M (that is, I is contained in a base of M).

• For D : Set α, M.Dep D means that D is contained in the ground set of M but isn't independent.

• For I : Set α and X : Set α, M.Basis I X means that I is a maximal independent subset of X.

• M.Finite means that M has finite ground set.

• M.Nonempty means that the ground set of M is nonempty.

• FiniteRk M means that the bases of M are finite.

• InfiniteRk M means that the bases of M are infinite.

• RkPos M means that the bases of M are nonempty.

• Finitary M means that a set is independent if and only if all its finite subsets are independent.

• aesop_mat : a tactic designed to prove X ⊆ M.E for some set X and matroid M.

Implementation details

There are a few design decisions worth discussing.

Finiteness

The first is that our matroids are allowed to be infinite. Unlike with many mathematical structures, this isn't such an obvious choice. Finite matroids have been studied since the 1930's, and there was never controversy as to what is and isn't an example of a finite matroid - in fact, surprisingly many apparently different definitions of a matroid give rise to the same class of objects.

However, generalizing different definitions of a finite matroid to the infinite in the obvious way (i.e. by simply allowing the ground set to be infinite) gives a number of different notions of 'infinite matroid' that disagree with each other, and that all lack nice properties. Many different competing notions of infinite matroid were studied through the years; in fact, the problem of which definition is the best was only really solved in 2013, when Bruhn et al. [2] showed that there is a unique 'reasonable' notion of an infinite matroid (these objects had previously defined by Higgs under the name 'B-matroid'). These are defined by adding one carefully chosen axiom to the standard set, and adapting existing axioms to not mention set cardinalities; they enjoy nearly all the nice properties of standard finite matroids.

Even though at least 90% of the literature is on finite matroids, B-matroids are the definition we use, because they allow for additional generality, nearly all theorems are still true and just as easy to state, and (hopefully) the more general definition will prevent the need for a costly future refactor. The disadvantage is that developing API for the finite case is harder work (for instance, it is harder to prove that something is a matroid in the first place, and one must deal with ℕ∞ rather than ℕ). For serious work on finite matroids, we provide the typeclasses [M.Finite] and [FiniteRk M] and associated API.

Cardinality

Just as with bases of a vector space, all bases of a finite matroid M are finite and have the same cardinality; this cardinality is an important invariant known as the 'rank' of M. For infinite matroids, bases are not in general equicardinal; in fact the equicardinality of bases of infinite matroids is independent of ZFC [3]. What is still true is that either all bases are finite and equicardinal, or all bases are infinite. This means that the natural notion of 'size' for a set in matroid theory is given by the function Set.encard, which is the cardinality as a term in ℕ∞. We use this function extensively in building the API; it is preferable to both Set.ncard and Finset.card because it allows infinite sets to be handled without splitting into cases.

The ground Set

A last place where we make a consequential choice is making the ground set of a matroid a structure field of type Set α (where α is the type of 'possible matroid elements') rather than just having a type α of all the matroid elements. This is because of how common it is to simultaneously consider a number of matroids on different but related ground sets. For example, a matroid M on ground set E can have its structure 'restricted' to some subset R ⊆ E to give a smaller matroid M ↾ R with ground set R. A statement like (M ↾ R₁) ↾ R₂ = M ↾ R₂ is mathematically obvious. But if the ground set of a matroid is a type, this doesn't typecheck, and is only true up to canonical isomorphism. Restriction is just the tip of the iceberg here; one can also 'contract' and 'delete' elements and sets of elements in a matroid to give a smaller matroid, and in practice it is common to make statements like M₁.E = M₂.E ∩ M₃.E and ((M ⟋ e) ↾ R) ⟋ C = M ⟋ (C ∪ {e}) ↾ R. Such things are a nightmare to work with unless = is actually propositional equality (especially because the relevant coercions are usually between sets and not just elements).

So the solution is that the ground set M.E has type Set α, and there are elements of type α that aren't in the matroid. The tradeoff is that for many statements, one now has to add hypotheses of the form X ⊆ M.E to make sure than X is actually 'in the matroid', rather than letting a 'type of matroid elements' take care of this invisibly. It still seems that this is worth it. The tactic aesop_mat exists specifically to discharge such goals with minimal fuss (using default values). The tactic works fairly well, but has room for improvement. Even though the carrier set is written M.E,

A related decision is to not have matroids themselves be a typeclass. This would make things be notationally simpler (having Base in the presence of [Matroid α] rather than M.Base for a term M : Matroid α) but is again just too awkward when one has multiple matroids on the same type. In fact, in regular written mathematics, it is normal to explicitly indicate which matroid something is happening in, so our notation mirrors common practice.

Notation

We use a few nonstandard conventions in theorem names that are related to the above. First, we mirror common informal practice by referring explicitly to the ground set rather than the notation E. (Writing ground everywhere in a proof term would be unwieldy, and writing E in theorem names would be unnatural to read.)

Second, because we are typically interested in subsets of the ground set M.E, using Set.compl is inconvenient, since Xᶜ ⊆ M.E is typically false for X ⊆ M.E. On the other hand (especially when duals arise), it is common to complement a set X ⊆ M.E within the ground set, giving M.E \ X. For this reason, we use the term compl in theorem names to refer to taking a set difference with respect to the ground set, rather than a complement within a type. The lemma compl_base_dual is one of the many examples of this.

Finally, in theorem names, matroid predicates that apply to sets (such as Base, Indep, Basis) are typically used as suffixes rather than prefixes. For instance, we have ground_indep_iff_base rather than indep_ground_iff_base.

References

[1] The standard text on matroid theory [J. G. Oxley, Matroid Theory, Oxford University Press, New York, 2011.]

[2] The robust axiomatic definition of infinite matroids [H. Bruhn, R. Diestel, M. Kriesell, R. Pendavingh, P. Wollan, Axioms for infinite matroids, Adv. Math 239 (2013), 18-46]

[3] Equicardinality of matroid bases is independent of ZFC. [N. Bowler, S. Geschke, Self-dual uniform matroids on infinite sets, Proc. Amer. Math. Soc. 144 (2016), 459-471]

def Matroid.ExchangeProperty {α : Type u_1} (P : Set α → Prop) : Prop

A predicate P on sets satisfies the exchange property if, for all X and Y satisfying P and all a ∈ X \ Y, there exists b ∈ Y \ X so that swapping a for b in X maintains P.

Equations

• Matroid.ExchangeProperty P = ∀ (X Y : Set α), P X → P Y → ∀ a ∈ X \ Y, ∃ b ∈ Y \ X, P (insert b (X \ {a}))

def Matroid.ExistsMaximalSubsetProperty {α : Type u_1} (P : Set α → Prop) (X : Set α) : Prop

A set X has the maximal subset property for a predicate P if every subset of X satisfying P is contained in a maximal subset of X satisfying P.

Equations

• Matroid.ExistsMaximalSubsetProperty P X = ∀ (I : Set α), P I → I ⊆ X → ∃ (J : Set α), I ⊆ J ∧ Maximal (fun (K : Set α) => P K ∧ K ⊆ X) J

structure Matroid (α : Type u_1) : Type u_1

A Matroid α is a ground set E of type Set α, and a nonempty collection of its subsets satisfying the exchange property and the maximal subset property. Each such set is called a Base of M. An Independent set is just a set contained in a base, but we include this predicate as a structure field for better definitional properties.

In most cases, using this definition directly is not the best way to construct a matroid, since it requires specifying both the bases and independent sets. If the bases are known, use Matroid.ofBase or a variant. If just the independent sets are known, define an IndepMatroid, and then use IndepMatroid.matroid.

• E : Set α

  M has a ground set E.

• Base : Set α → Prop

  M has a predicate Base defining its bases.

• Indep : Set α → Prop

  M has a predicate Indep defining its independent sets.

• indep_iff' ⦃I : Set α⦄ : self.Indep I ↔ ∃ (B : Set α), self.Base B ∧ I ⊆ B

  The Independent sets are those contained in Bases.

• exists_base : ∃ (B : Set α), self.Base B

  There is at least one Base.

• base_exchange : Matroid.ExchangeProperty self.Base

  For any bases B, B' and e ∈ B \ B', there is some f ∈ B' \ B for which B-e+f is a base.

• maximality (X : Set α) : X ⊆ self.E → Matroid.ExistsMaximalSubsetProperty self.Indep X

  Every independent subset I of a set X for is contained in a maximal independent subset of X.

• subset_ground (B : Set α) : self.Base B → B ⊆ self.E

  Every base is contained in the ground set.

theorem Matroid.ext {α : Type u_1} {x y : Matroid α} (E : x.E = y.E) (Base : x.Base = y.Base) (Indep : x.Indep = y.Indep) : x = y

class Matroid.Finite {α : Type u_1} (M : Matroid α) : Prop

Typeclass for a matroid having finite ground set. Just a wrapper for M.E.Finite

• ground_finite : M.E.Finite

  The ground set is finite

class Matroid.Nonempty {α : Type u_1} (M : Matroid α) : Prop

Typeclass for a matroid having nonempty ground set. Just a wrapper for M.E.Nonempty

• ground_nonempty : M.E.Nonempty

  The ground set is nonempty

theorem Matroid.ground_nonempty {α : Type u_1} (M : Matroid α) [M.Nonempty] : M.E.Nonempty

theorem Matroid.ground_nonempty_iff {α : Type u_1} (M : Matroid α) : M.E.Nonempty ↔ M.Nonempty

theorem Matroid.ground_finite {α : Type u_1} (M : Matroid α) [M.Finite] : M.E.Finite

theorem Matroid.set_finite {α : Type u_1} (M : Matroid α) [M.Finite] (X : Set α) (hX : X ⊆ M.E := by aesop) : X.Finite

instance Matroid.finite_of_finite {α : Type u_1} [Finite α] {M : Matroid α} : M.Finite

class Matroid.FiniteRk {α : Type u_1} (M : Matroid α) : Prop

A FiniteRk matroid is one whose bases are finite

• exists_finite_base : ∃ (B : Set α), M.Base B ∧ B.Finite

  There is a finite base

instance Matroid.finiteRk_of_finite {α : Type u_1} (M : Matroid α) [M.Finite] : M.FiniteRk

class Matroid.InfiniteRk {α : Type u_1} (M : Matroid α) : Prop

An InfiniteRk matroid is one whose bases are infinite.

• exists_infinite_base : ∃ (B : Set α), M.Base B ∧ B.Infinite

  There is an infinite base

class Matroid.RkPos {α : Type u_1} (M : Matroid α) : Prop

A RkPos matroid is one whose bases are nonempty.

• empty_not_base : ¬M.Base ∅

  The empty set isn't a base

theorem Matroid.rkPos_iff_empty_not_base {α : Type u_1} {M : Matroid α} : M.RkPos ↔ ¬M.Base ∅

theorem Matroid.ExchangeProperty.antichain {α : Type u_1} {Base : Set α → Prop} {B B' : Set α} (exch : Matroid.ExchangeProperty Base) (hB : Base B) (hB' : Base B') (h : B ⊆ B') : B = B'

A family of sets with the exchange property is an antichain.

@[irreducible]

theorem Matroid.ExchangeProperty.encard_diff_le_aux {α : Type u_1} {Base : Set α → Prop} {B₁ B₂ : Set α} (exch : Matroid.ExchangeProperty Base) (hB₁ : Base B₁) (hB₂ : Base B₂) : (B₁ \ B₂).encard ≤ (B₂ \ B₁).encard

theorem Matroid.ExchangeProperty.encard_diff_eq {α : Type u_1} {Base : Set α → Prop} {B₁ B₂ : Set α} (exch : Matroid.ExchangeProperty Base) (hB₁ : Base B₁) (hB₂ : Base B₂) : (B₁ \ B₂).encard = (B₂ \ B₁).encard

For any two sets B₁, B₂ in a family with the exchange property, the differences B₁ \ B₂ and B₂ \ B₁ have the same ℕ∞-cardinality.

theorem Matroid.ExchangeProperty.encard_base_eq {α : Type u_1} {Base : Set α → Prop} {B₁ B₂ : Set α} (exch : Matroid.ExchangeProperty Base) (hB₁ : Base B₁) (hB₂ : Base B₂) : B₁.encard = B₂.encard

Any two sets B₁, B₂ in a family with the exchange property have the same ℕ∞-cardinality.

def Matroid.aesop_mat : Lean.ParserDescr

The aesop_mat tactic attempts to prove a set is contained in the ground set of a matroid. It uses a [Matroid] ruleset, and is allowed to fail.

Equations

• One or more equations did not get rendered due to their size.

theorem Matroid.Base.subset_ground {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.Base B) : B ⊆ M.E

theorem Matroid.Base.exchange {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} {e : α} (hB₁ : M.Base B₁) (hB₂ : M.Base B₂) (hx : e ∈ B₁ \ B₂) : ∃ y ∈ B₂ \ B₁, M.Base (insert y (B₁ \ {e}))

theorem Matroid.Base.exchange_mem {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} {e : α} (hB₁ : M.Base B₁) (hB₂ : M.Base B₂) (hxB₁ : e ∈ B₁) (hxB₂ : e ∉ B₂) : ∃ (y : α), (y ∈ B₂ ∧ y ∉ B₁) ∧ M.Base (insert y (B₁ \ {e}))

theorem Matroid.Base.eq_of_subset_base {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} (hB₁ : M.Base B₁) (hB₂ : M.Base B₂) (hB₁B₂ : B₁ ⊆ B₂) : B₁ = B₂

theorem Matroid.Base.not_base_of_ssubset {α : Type u_1} {M : Matroid α} {B X : Set α} (hB : M.Base B) (hX : X ⊂ B) : ¬M.Base X

theorem Matroid.Base.insert_not_base {α : Type u_1} {M : Matroid α} {B : Set α} {e : α} (hB : M.Base B) (heB : e ∉ B) : ¬M.Base (insert e B)

theorem Matroid.Base.encard_diff_comm {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} (hB₁ : M.Base B₁) (hB₂ : M.Base B₂) : (B₁ \ B₂).encard = (B₂ \ B₁).encard

theorem Matroid.Base.ncard_diff_comm {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} (hB₁ : M.Base B₁) (hB₂ : M.Base B₂) : (B₁ \ B₂).ncard = (B₂ \ B₁).ncard

theorem Matroid.Base.card_eq_card_of_base {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} (hB₁ : M.Base B₁) (hB₂ : M.Base B₂) : B₁.encard = B₂.encard

theorem Matroid.Base.ncard_eq_ncard_of_base {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} (hB₁ : M.Base B₁) (hB₂ : M.Base B₂) : B₁.ncard = B₂.ncard

theorem Matroid.Base.finite_of_finite {α : Type u_1} {M : Matroid α} {B B' : Set α} (hB : M.Base B) (h : B.Finite) (hB' : M.Base B') : B'.Finite

theorem Matroid.Base.infinite_of_infinite {α : Type u_1} {M : Matroid α} {B B₁ : Set α} (hB : M.Base B) (h : B.Infinite) (hB₁ : M.Base B₁) : B₁.Infinite

theorem Matroid.Base.finite {α : Type u_1} {M : Matroid α} {B : Set α} [M.FiniteRk] (hB : M.Base B) : B.Finite

theorem Matroid.Base.infinite {α : Type u_1} {M : Matroid α} {B : Set α} [M.InfiniteRk] (hB : M.Base B) : B.Infinite

theorem Matroid.empty_not_base {α : Type u_1} {M : Matroid α} [h : M.RkPos] : ¬M.Base ∅

theorem Matroid.Base.nonempty {α : Type u_1} {M : Matroid α} {B : Set α} [M.RkPos] (hB : M.Base B) : B.Nonempty

theorem Matroid.Base.rkPos_of_nonempty {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.Base B) (h : B.Nonempty) : M.RkPos

theorem Matroid.Base.finiteRk_of_finite {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.Base B) (hfin : B.Finite) : M.FiniteRk

theorem Matroid.Base.infiniteRk_of_infinite {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.Base B) (h : B.Infinite) : M.InfiniteRk

theorem Matroid.not_finiteRk {α : Type u_1} (M : Matroid α) [M.InfiniteRk] : ¬M.FiniteRk

theorem Matroid.not_infiniteRk {α : Type u_1} (M : Matroid α) [M.FiniteRk] : ¬M.InfiniteRk

theorem Matroid.finite_or_infiniteRk {α : Type u_1} (M : Matroid α) : M.FiniteRk ∨ M.InfiniteRk

theorem Matroid.Base.diff_finite_comm {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} (hB₁ : M.Base B₁) (hB₂ : M.Base B₂) : (B₁ \ B₂).Finite ↔ (B₂ \ B₁).Finite

theorem Matroid.Base.diff_infinite_comm {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} (hB₁ : M.Base B₁) (hB₂ : M.Base B₂) : (B₁ \ B₂).Infinite ↔ (B₂ \ B₁).Infinite

theorem Matroid.eq_of_base_iff_base_forall {α : Type u_1} {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (h : ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.Base B ↔ M₂.Base B)) : M₁ = M₂

theorem Matroid.base_compl_iff_maximal_disjoint_base {α : Type u_1} {M : Matroid α} {B : Set α} (hB : B ⊆ M.E := by aesop_mat) : M.Base (M.E \ B) ↔ Maximal (fun (I : Set α) => I ⊆ M.E ∧ ∃ (B : Set α), M.Base B ∧ Disjoint I B) B

def Matroid.Dep {α : Type u_1} (M : Matroid α) (D : Set α) : Prop

A subset of M.E is Dependent if it is not Independent .

Equations

• M.Dep D = (¬M.Indep D ∧ D ⊆ M.E)

theorem Matroid.indep_iff {α : Type u_1} {M : Matroid α} {I : Set α} : M.Indep I ↔ ∃ (B : Set α), M.Base B ∧ I ⊆ B

theorem Matroid.setOf_indep_eq {α : Type u_1} (M : Matroid α) : {I : Set α | M.Indep I} = ↑(lowerClosure {B : Set α | M.Base B})

theorem Matroid.Indep.exists_base_superset {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : ∃ (B : Set α), M.Base B ∧ I ⊆ B

theorem Matroid.dep_iff {α : Type u_1} {M : Matroid α} {D : Set α} : M.Dep D ↔ ¬M.Indep D ∧ D ⊆ M.E

theorem Matroid.setOf_dep_eq {α : Type u_1} (M : Matroid α) : {D : Set α | M.Dep D} = {I : Set α | M.Indep I}ᶜ ∩ Set.Iic M.E

theorem Matroid.Indep.subset_ground {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : I ⊆ M.E

theorem Matroid.Dep.subset_ground {α : Type u_1} {M : Matroid α} {D : Set α} (hD : M.Dep D) : D ⊆ M.E

theorem Matroid.indep_or_dep {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E := by aesop_mat) : M.Indep X ∨ M.Dep X

theorem Matroid.Indep.not_dep {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : ¬M.Dep I

theorem Matroid.Dep.not_indep {α : Type u_1} {M : Matroid α} {D : Set α} (hD : M.Dep D) : ¬M.Indep D

theorem Matroid.dep_of_not_indep {α : Type u_1} {M : Matroid α} {D : Set α} (hD : ¬M.Indep D) (hDE : D ⊆ M.E := by aesop_mat) : M.Dep D

theorem Matroid.indep_of_not_dep {α : Type u_1} {M : Matroid α} {I : Set α} (hI : ¬M.Dep I) (hIE : I ⊆ M.E := by aesop_mat) : M.Indep I

@[simp]

theorem Matroid.not_dep_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E := by aesop_mat) : ¬M.Dep X ↔ M.Indep X

@[simp]

theorem Matroid.not_indep_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E := by aesop_mat) : ¬M.Indep X ↔ M.Dep X

theorem Matroid.indep_iff_not_dep {α : Type u_1} {M : Matroid α} {I : Set α} : M.Indep I ↔ ¬M.Dep I ∧ I ⊆ M.E

theorem Matroid.Indep.subset {α : Type u_1} {M : Matroid α} {I J : Set α} (hJ : M.Indep J) (hIJ : I ⊆ J) : M.Indep I

theorem Matroid.Dep.superset {α : Type u_1} {M : Matroid α} {D X : Set α} (hD : M.Dep D) (hDX : D ⊆ X) (hXE : X ⊆ M.E := by aesop_mat) : M.Dep X

theorem Matroid.Base.indep {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.Base B) : M.Indep B

@[simp]

theorem Matroid.empty_indep {α : Type u_1} (M : Matroid α) : M.Indep ∅

theorem Matroid.Dep.nonempty {α : Type u_1} {M : Matroid α} {D : Set α} (hD : M.Dep D) : D.Nonempty

theorem Matroid.Indep.finite {α : Type u_1} {M : Matroid α} {I : Set α} [M.FiniteRk] (hI : M.Indep I) : I.Finite

theorem Matroid.Indep.rkPos_of_nonempty {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (hne : I.Nonempty) : M.RkPos

theorem Matroid.Indep.inter_right {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (X : Set α) : M.Indep (I ∩ X)

theorem Matroid.Indep.inter_left {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (X : Set α) : M.Indep (X ∩ I)

theorem Matroid.Indep.diff {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (X : Set α) : M.Indep (I \ X)

theorem Matroid.Base.eq_of_subset_indep {α : Type u_1} {M : Matroid α} {B I : Set α} (hB : M.Base B) (hI : M.Indep I) (hBI : B ⊆ I) : B = I

theorem Matroid.base_iff_maximal_indep {α : Type u_1} {M : Matroid α} {B : Set α} : M.Base B ↔ Maximal M.Indep B

theorem Matroid.Indep.base_of_maximal {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (h : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → I = J) : M.Base I

theorem Matroid.Base.dep_of_ssubset {α : Type u_1} {M : Matroid α} {B X : Set α} (hB : M.Base B) (h : B ⊂ X) (hX : X ⊆ M.E := by aesop_mat) : M.Dep X

theorem Matroid.Base.dep_of_insert {α : Type u_1} {M : Matroid α} {B : Set α} {e : α} (hB : M.Base B) (heB : e ∉ B) (he : e ∈ M.E := by aesop_mat) : M.Dep (insert e B)

theorem Matroid.Base.mem_of_insert_indep {α : Type u_1} {M : Matroid α} {B : Set α} {e : α} (hB : M.Base B) (heB : M.Indep (insert e B)) : e ∈ B

theorem Matroid.Base.eq_exchange_of_diff_eq_singleton {α : Type u_1} {M : Matroid α} {B B' : Set α} {e : α} (hB : M.Base B) (hB' : M.Base B') (h : B \ B' = {e}) : ∃ f ∈ B' \ B, B' = insert f B \ {e}

If the difference of two Bases is a singleton, then they differ by an insertion/removal

theorem Matroid.Base.exchange_base_of_indep {α : Type u_1} {M : Matroid α} {B : Set α} {e f : α} (hB : M.Base B) (hf : f ∉ B) (hI : M.Indep (insert f (B \ {e}))) : M.Base (insert f (B \ {e}))

theorem Matroid.Base.exchange_base_of_indep' {α : Type u_1} {M : Matroid α} {B : Set α} {e f : α} (hB : M.Base B) (he : e ∈ B) (hf : f ∉ B) (hI : M.Indep (insert f B \ {e})) : M.Base (insert f B \ {e})

theorem Matroid.Base.insert_dep {α : Type u_1} {M : Matroid α} {B : Set α} {e : α} (hB : M.Base B) (h : e ∈ M.E \ B) : M.Dep (insert e B)

theorem Matroid.Indep.exists_insert_of_not_base {α : Type u_1} {M : Matroid α} {B I : Set α} (hI : M.Indep I) (hI' : ¬M.Base I) (hB : M.Base B) : ∃ e ∈ B \ I, M.Indep (insert e I)

theorem Matroid.Indep.exists_insert_of_not_maximal {α : Type u_1} (M : Matroid α) ⦃I B : Set α⦄ (hI : M.Indep I) (hInotmax : ¬Maximal M.Indep I) (hB : Maximal M.Indep B) : ∃ x ∈ B \ I, M.Indep (insert x I)

This is the same as Indep.exists_insert_of_not_base, but phrased so that it is defeq to the augmentation axiom for independent sets.

theorem Matroid.Indep.base_of_forall_insert {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.Indep B) (hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)) : M.Base B

theorem Matroid.ground_indep_iff_base {α : Type u_1} {M : Matroid α} : M.Indep M.E ↔ M.Base M.E

theorem Matroid.Base.exists_insert_of_ssubset {α : Type u_1} {M : Matroid α} {B B' I : Set α} (hB : M.Base B) (hIB : I ⊂ B) (hB' : M.Base B') : ∃ e ∈ B' \ I, M.Indep (insert e I)

theorem Matroid.eq_of_indep_iff_indep_forall {α : Type u_1} {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (h : ∀ I ⊆ M₁.E, M₁.Indep I ↔ M₂.Indep I) : M₁ = M₂

theorem Matroid.eq_iff_indep_iff_indep_forall {α : Type u_1} {M₁ M₂ : Matroid α} : M₁ = M₂ ↔ M₁.E = M₂.E ∧ ∀ I ⊆ M₁.E, M₁.Indep I ↔ M₂.Indep I

class Matroid.Finitary {α : Type u_1} (M : Matroid α) : Prop

A Finitary matroid is one where a set is independent if and only if it all its finite subsets are independent, or equivalently a matroid whose circuits are finite.

• indep_of_forall_finite (I : Set α) : (∀ J ⊆ I, J.Finite → M.Indep J) → M.Indep I

  I is independent if all its finite subsets are independent.

theorem Matroid.indep_of_forall_finite_subset_indep {α : Type u_1} {M : Matroid α} [M.Finitary] (I : Set α) (h : ∀ J ⊆ I, J.Finite → M.Indep J) : M.Indep I

theorem Matroid.indep_iff_forall_finite_subset_indep {α : Type u_1} {I : Set α} {M : Matroid α} [M.Finitary] : M.Indep I ↔ ∀ J ⊆ I, J.Finite → M.Indep J

instance Matroid.finitary_of_finiteRk {α : Type u_1} {M : Matroid α} [M.FiniteRk] : M.Finitary

theorem Matroid.existsMaximalSubsetProperty_indep {α : Type u_1} (M : Matroid α) (X : Set α) : X ⊆ M.E → Matroid.ExistsMaximalSubsetProperty M.Indep X

Matroids obey the maximality axiom

def Matroid.Basis {α : Type u_1} (M : Matroid α) (I X : Set α) : Prop

A Basis for a set X ⊆ M.E is a maximal independent subset of X (Often in the literature, the word 'Basis' is used to refer to what we call a 'Base').

Equations

• M.Basis I X = (Maximal (fun (A : Set α) => M.Indep A ∧ A ⊆ X) I ∧ X ⊆ M.E)

def Matroid.Basis' {α : Type u_1} (M : Matroid α) (I X : Set α) : Prop

A Basis' is a basis without the requirement that X ⊆ M.E. This is convenient for some API building, especially when working with rank and closure.

Equations

• M.Basis' I X = Maximal (fun (A : Set α) => M.Indep A ∧ A ⊆ X) I

theorem Matroid.Basis'.indep {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Basis' I X) : M.Indep I

theorem Matroid.Basis.indep {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Basis I X) : M.Indep I

theorem Matroid.Basis.subset {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Basis I X) : I ⊆ X

theorem Matroid.Basis.basis' {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Basis I X) : M.Basis' I X

theorem Matroid.Basis'.basis {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Basis' I X) (hX : X ⊆ M.E := by aesop_mat) : M.Basis I X

theorem Matroid.Basis'.subset {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Basis' I X) : I ⊆ X

theorem Matroid.Basis.subset_ground {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Basis I X) : X ⊆ M.E

theorem Matroid.Basis.basis_inter_ground {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Basis I X) : M.Basis I (X ∩ M.E)

theorem Matroid.Basis.left_subset_ground {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Basis I X) : I ⊆ M.E

theorem Matroid.Basis.eq_of_subset_indep {α : Type u_1} {M : Matroid α} {I J X : Set α} (hI : M.Basis I X) (hJ : M.Indep J) (hIJ : I ⊆ J) (hJX : J ⊆ X) : I = J

theorem Matroid.Basis.Finite {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Basis I X) [M.FiniteRk] : I.Finite

theorem Matroid.basis_iff' {α : Type u_1} {M : Matroid α} {I X : Set α} : M.Basis I X ↔ (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E

theorem Matroid.basis_iff {α : Type u_1} {M : Matroid α} {I X : Set α} (hX : X ⊆ M.E := by aesop_mat) : M.Basis I X ↔ M.Indep I ∧ I ⊆ X ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ X → I = J

theorem Matroid.basis'_iff_basis_inter_ground {α : Type u_1} {M : Matroid α} {I X : Set α} : M.Basis' I X ↔ M.Basis I (X ∩ M.E)

theorem Matroid.basis'_iff_basis {α : Type u_1} {M : Matroid α} {I X : Set α} (hX : X ⊆ M.E := by aesop_mat) : M.Basis' I X ↔ M.Basis I X

theorem Matroid.basis_iff_basis'_subset_ground {α : Type u_1} {M : Matroid α} {I X : Set α} : M.Basis I X ↔ M.Basis' I X ∧ X ⊆ M.E

theorem Matroid.Basis'.basis_inter_ground {α : Type u_1} {M : Matroid α} {I X : Set α} (hIX : M.Basis' I X) : M.Basis I (X ∩ M.E)

theorem Matroid.Basis'.eq_of_subset_indep {α : Type u_1} {M : Matroid α} {I J X : Set α} (hI : M.Basis' I X) (hJ : M.Indep J) (hIJ : I ⊆ J) (hJX : J ⊆ X) : I = J

theorem Matroid.Basis'.insert_not_indep {α : Type u_1} {M : Matroid α} {I X : Set α} {e : α} (hI : M.Basis' I X) (he : e ∈ X \ I) : ¬M.Indep (insert e I)

theorem Matroid.basis_iff_maximal {α : Type u_1} {M : Matroid α} {I X : Set α} (hX : X ⊆ M.E := by aesop_mat) : M.Basis I X ↔ Maximal (fun (I : Set α) => M.Indep I ∧ I ⊆ X) I

theorem Matroid.Indep.basis_of_maximal_subset {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Indep I) (hIX : I ⊆ X) (hmax : ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → J ⊆ I) (hX : X ⊆ M.E := by aesop_mat) : M.Basis I X

theorem Matroid.Basis.basis_subset {α : Type u_1} {M : Matroid α} {I X Y : Set α} (hI : M.Basis I X) (hIY : I ⊆ Y) (hYX : Y ⊆ X) : M.Basis I Y

@[simp]

theorem Matroid.basis_self_iff_indep {α : Type u_1} {M : Matroid α} {I : Set α} : M.Basis I I ↔ M.Indep I

theorem Matroid.Indep.basis_self {α : Type u_1} {M : Matroid α} {I : Set α} (h : M.Indep I) : M.Basis I I

@[simp]

theorem Matroid.basis_empty_iff {α : Type u_1} {I : Set α} (M : Matroid α) : M.Basis I ∅ ↔ I = ∅

theorem Matroid.Basis.dep_of_ssubset {α : Type u_1} {M : Matroid α} {I X Y : Set α} (hI : M.Basis I X) (hIY : I ⊂ Y) (hYX : Y ⊆ X) : M.Dep Y

theorem Matroid.Basis.insert_dep {α : Type u_1} {M : Matroid α} {I X : Set α} {e : α} (hI : M.Basis I X) (he : e ∈ X \ I) : M.Dep (insert e I)

theorem Matroid.Basis.mem_of_insert_indep {α : Type u_1} {M : Matroid α} {I X : Set α} {e : α} (hI : M.Basis I X) (he : e ∈ X) (hIe : M.Indep (insert e I)) : e ∈ I

theorem Matroid.Basis'.mem_of_insert_indep {α : Type u_1} {M : Matroid α} {I X : Set α} {e : α} (hI : M.Basis' I X) (he : e ∈ X) (hIe : M.Indep (insert e I)) : e ∈ I

theorem Matroid.Basis.not_basis_of_ssubset {α : Type u_1} {M : Matroid α} {I J X : Set α} (hI : M.Basis I X) (hJI : J ⊂ I) : ¬M.Basis J X

theorem Matroid.Indep.subset_basis_of_subset {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Indep I) (hIX : I ⊆ X) (hX : X ⊆ M.E := by aesop_mat) : ∃ (J : Set α), M.Basis J X ∧ I ⊆ J

theorem Matroid.Indep.subset_basis'_of_subset {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Indep I) (hIX : I ⊆ X) : ∃ (J : Set α), M.Basis' J X ∧ I ⊆ J

theorem Matroid.exists_basis {α : Type u_1} (M : Matroid α) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : ∃ (I : Set α), M.Basis I X

theorem Matroid.exists_basis' {α : Type u_1} (M : Matroid α) (X : Set α) : ∃ (I : Set α), M.Basis' I X

theorem Matroid.exists_basis_subset_basis {α : Type u_1} {X Y : Set α} (M : Matroid α) (hXY : X ⊆ Y) (hY : Y ⊆ M.E := by aesop_mat) : ∃ (I : Set α) (J : Set α), M.Basis I X ∧ M.Basis J Y ∧ I ⊆ J

theorem Matroid.Basis.exists_basis_inter_eq_of_superset {α : Type u_1} {M : Matroid α} {I X Y : Set α} (hI : M.Basis I X) (hXY : X ⊆ Y) (hY : Y ⊆ M.E := by aesop_mat) : ∃ (J : Set α), M.Basis J Y ∧ J ∩ X = I

theorem Matroid.exists_basis_union_inter_basis {α : Type u_1} (M : Matroid α) (X Y : Set α) (hX : X ⊆ M.E := by aesop_mat) (hY : Y ⊆ M.E := by aesop_mat) : ∃ (I : Set α), M.Basis I (X ∪ Y) ∧ M.Basis (I ∩ Y) Y

theorem Matroid.Indep.eq_of_basis {α : Type u_1} {M : Matroid α} {I J : Set α} (hI : M.Indep I) (hJ : M.Basis J I) : J = I

theorem Matroid.Basis.exists_base {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Basis I X) : ∃ (B : Set α), M.Base B ∧ I = B ∩ X

@[simp]

theorem Matroid.basis_ground_iff {α : Type u_1} {M : Matroid α} {B : Set α} : M.Basis B M.E ↔ M.Base B

theorem Matroid.Base.basis_ground {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.Base B) : M.Basis B M.E

theorem Matroid.Indep.basis_iff_forall_insert_dep {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Indep I) (hIX : I ⊆ X) : M.Basis I X ↔ ∀ e ∈ X \ I, M.Dep (insert e I)

theorem Matroid.Indep.basis_of_forall_insert {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Indep I) (hIX : I ⊆ X) (he : ∀ e ∈ X \ I, M.Dep (insert e I)) : M.Basis I X

theorem Matroid.Indep.basis_insert_iff {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (hI : M.Indep I) : M.Basis I (insert e I) ↔ M.Dep (insert e I) ∨ e ∈ I

theorem Matroid.Basis.iUnion_basis_iUnion {α : Type u_1} {M : Matroid α} {ι : Type u_2} (X I : ι → Set α) (hI : ∀ (i : ι), M.Basis (I i) (X i)) (h_ind : M.Indep (⋃ (i : ι), I i)) : M.Basis (⋃ (i : ι), I i) (⋃ (i : ι), X i)

theorem Matroid.Basis.basis_iUnion {α : Type u_1} {M : Matroid α} {I : Set α} {ι : Type u_2} [Nonempty ι] (X : ι → Set α) (hI : ∀ (i : ι), M.Basis I (X i)) : M.Basis I (⋃ (i : ι), X i)

theorem Matroid.Basis.basis_sUnion {α : Type u_1} {M : Matroid α} {I : Set α} {Xs : Set (Set α)} (hne : Xs.Nonempty) (h : ∀ X ∈ Xs, M.Basis I X) : M.Basis I (⋃₀ Xs)

theorem Matroid.Indep.basis_setOf_insert_basis {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : M.Basis I {x : α | M.Basis I (insert x I)}

theorem Matroid.Basis.union_basis_union {α : Type u_1} {M : Matroid α} {I J X Y : Set α} (hIX : M.Basis I X) (hJY : M.Basis J Y) (h : M.Indep (I ∪ J)) : M.Basis (I ∪ J) (X ∪ Y)

theorem Matroid.Basis.basis_union {α : Type u_1} {M : Matroid α} {I X Y : Set α} (hIX : M.Basis I X) (hIY : M.Basis I Y) : M.Basis I (X ∪ Y)

theorem Matroid.Basis.basis_union_of_subset {α : Type u_1} {M : Matroid α} {I J X : Set α} (hI : M.Basis I X) (hJ : M.Indep J) (hIJ : I ⊆ J) : M.Basis J (J ∪ X)

theorem Matroid.Basis.insert_basis_insert {α : Type u_1} {M : Matroid α} {I X : Set α} {e : α} (hI : M.Basis I X) (h : M.Indep (insert e I)) : M.Basis (insert e I) (insert e X)

theorem Matroid.Base.base_of_basis_superset {α : Type u_1} {M : Matroid α} {B I X : Set α} (hB : M.Base B) (hBX : B ⊆ X) (hIX : M.Basis I X) : M.Base I

theorem Matroid.Indep.exists_base_subset_union_base {α : Type u_1} {M : Matroid α} {B I : Set α} (hI : M.Indep I) (hB : M.Base B) : ∃ (B' : Set α), M.Base B' ∧ I ⊆ B' ∧ B' ⊆ I ∪ B

theorem Matroid.Basis.inter_eq_of_subset_indep {α : Type u_1} {M : Matroid α} {I J X : Set α} (hIX : M.Basis I X) (hIJ : I ⊆ J) (hJ : M.Indep J) : J ∩ X = I

theorem Matroid.Basis'.inter_eq_of_subset_indep {α : Type u_1} {M : Matroid α} {I J X : Set α} (hI : M.Basis' I X) (hIJ : I ⊆ J) (hJ : M.Indep J) : J ∩ X = I

theorem Matroid.Base.basis_of_subset {α : Type u_1} {M : Matroid α} {B X : Set α} (hX : X ⊆ M.E := by aesop_mat) (hB : M.Base B) (hBX : B ⊆ X) : M.Basis B X

theorem Matroid.exists_basis_disjoint_basis_of_subset {α : Type u_1} (M : Matroid α) {X Y : Set α} (hXY : X ⊆ Y) (hY : Y ⊆ M.E := by aesop_mat) : ∃ (I : Set α) (J : Set α), M.Basis I X ∧ M.Basis (I ∪ J) Y ∧ Disjoint X J

theorem Matroid.finite_setOf_matroid {α : Type u_1} {E : Set α} (hE : E.Finite) : {M : Matroid α | M.E ⊆ E}.Finite

For finite E, finitely many matroids have ground set contained in E.

theorem Matroid.finite_setOf_matroid' {α : Type u_1} {E : Set α} (hE : E.Finite) : {M : Matroid α | M.E = E}.Finite

For finite E, finitely many matroids have ground set E.