Matroid Minors

A matroid N = M ／ C ＼ D obtained from a matroid M by a contraction then a delete, (or equivalently, by any number of contractions/deletions in any order) is a minor of M. This gives a partial order on Matroid α that is ubiquitous in matroid theory, and interacts nicely with duality and linear representations.

Although we provide a PartialOrder instance on Matroid α corresponding to the minor order, we do not use the M ≤ N / N < M notation directly, instead writing N ≤m M and N <m M for more convenient dot notation.

Main Declarations

• Matroid.IsMinor N M, written N ≤m M, means that N = M ／ C ＼ D for some subset C and D of M.E.
• Matroid.IsStrictMinor N M, written N <m M, means that N = M ／ C ＼ D for some subsets C and D of M.E that are not both nonempty.
• Matroid.IsMinor.exists_eq_contract_delete_disjoint : we can choose C and D disjoint.

Minors

def Matroid.IsMinor {α : Type u_1} (N M : Matroid α) : Prop

N is a minor of M if N = M ／ C ＼ D for some C and D. The definition itself does not require C and D to be disjoint, or even to be subsets of the ground set. See Matroid.IsMinor.exists_eq_contract_delete_disjoint for the fact that we can choose C and D with these properties.

Equations

• (N ≤m M) = ∃ (C : Set α) (D : Set α), N = (M.contract C).delete D

def Matroid.«term_≤m_» : Lean.TrailingParserDescr

≤m denotes the minor relation on matroids.

Equations

• Matroid.«term_≤m_» = Lean.ParserDescr.trailingNode `Matroid.«term_≤m_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤m ") (Lean.ParserDescr.cat `term 51))

@[simp]

theorem Matroid.contract_delete_isMinor {α : Type u_1} (M : Matroid α) (C D : Set α) : (M.contract C).delete D ≤m M

theorem Matroid.IsMinor.exists_eq_contract_delete_disjoint {α : Type u_1} {M N : Matroid α} (h : N ≤m M) : ∃ (C : Set α) (D : Set α), C ⊆ M.E ∧ D ⊆ M.E ∧ Disjoint C D ∧ N = (M.contract C).delete D

def Matroid.IsStrictMinor {α : Type u_1} (N M : Matroid α) : Prop

N is a strict minor of M if N is a minor of M and N ≠ M. Equivalently, N is obtained from M by deleting/contracting subsets of the ground set that are not both empty.

Equations

• (N <m M) = (N ≤m M ∧ ¬M ≤m N)

def Matroid.«term_<m_» : Lean.TrailingParserDescr

<m denotes the strict minor relation on matroids.

Equations

• Matroid.«term_<m_» = Lean.ParserDescr.trailingNode `Matroid.«term_<m_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <m ") (Lean.ParserDescr.cat `term 51))

theorem Matroid.IsMinor.subset {α : Type u_1} {M N : Matroid α} (h : N ≤m M) : N.E ⊆ M.E

theorem Matroid.IsMinor.refl {α : Type u_1} {M : Matroid α} : M ≤m M

theorem Matroid.IsMinor.trans {α : Type u_1} {M₁ M₂ M₃ : Matroid α} (h : M₁ ≤m M₂) (h' : M₂ ≤m M₃) : M₁ ≤m M₃

theorem Matroid.IsMinor.eq_of_ground_subset {α : Type u_1} {M N : Matroid α} (h : N ≤m M) (hE : M.E ⊆ N.E) : M = N

theorem Matroid.IsMinor.antisymm {α : Type u_1} {M N : Matroid α} (h : N ≤m M) (h' : M ≤m N) : N = M

instance Matroid.instPartialOrder (α : Type u_2) : PartialOrder (Matroid α)

The minor order is a PartialOrder on Matroid α. We prefer the spelling N ≤m M over N ≤ M for the dot notation.

Equations

• Matroid.instPartialOrder α = { le := fun (N M : Matroid α) => N ≤m M, lt := fun (N M : Matroid α) => N <m M, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

theorem Matroid.IsMinor.le {α : Type u_1} {M N : Matroid α} (h : N ≤m M) : N ≤ M

theorem Matroid.IsStrictMinor.lt {α : Type u_1} {M N : Matroid α} (h : N <m M) : N < M

@[simp]

theorem Matroid.le_eq_isMinor {α : Type u_1} : (fun (M M' : Matroid α) => M ≤ M') = IsMinor

@[simp]

theorem Matroid.lt_eq_isStrictMinor {α : Type u_1} : (fun (M M' : Matroid α) => M < M') = IsStrictMinor

theorem Matroid.isStrictMinor_iff_isMinor_ne {α : Type u_1} {M N : Matroid α} : N <m M ↔ N ≤m M ∧ N ≠ M

theorem Matroid.IsStrictMinor.ne {α : Type u_1} {M N : Matroid α} (h : N <m M) : N ≠ M

theorem Matroid.isStrictMinor_irrefl {α : Type u_1} (M : Matroid α) : ¬M <m M

theorem Matroid.IsStrictMinor.isMinor {α : Type u_1} {M N : Matroid α} (h : N <m M) : N ≤m M

theorem Matroid.IsStrictMinor.not_isMinor {α : Type u_1} {M N : Matroid α} (h : N <m M) : ¬M ≤m N

theorem Matroid.IsStrictMinor.ssubset {α : Type u_1} {M N : Matroid α} (h : N <m M) : N.E ⊂ M.E

theorem Matroid.isStrictMinor_iff_isMinor_ssubset {α : Type u_1} {M N : Matroid α} : N <m M ↔ N ≤m M ∧ N.E ⊂ M.E

theorem Matroid.IsStrictMinor.trans_isMinor {α : Type u_1} {M M' N : Matroid α} (h : N <m M) (h' : M ≤m M') : N <m M'

theorem Matroid.IsMinor.trans_isStrictMinor {α : Type u_1} {M M' N : Matroid α} (h : N ≤m M) (h' : M <m M') : N <m M'

theorem Matroid.IsStrictMinor.trans {α : Type u_1} {M M' N : Matroid α} (h : N <m M) (h' : M <m M') : N <m M'

theorem Matroid.Indep.of_isMinor {α : Type u_1} {M N : Matroid α} {I : Set α} (hI : N.Indep I) (hNM : N ≤m M) : M.Indep I

theorem Matroid.IsNonloop.of_isMinor {α : Type u_1} {M N : Matroid α} {e : α} (h : N.IsNonloop e) (hNM : N ≤m M) : M.IsNonloop e

theorem Matroid.Dep.of_isMinor {α : Type u_1} {M N : Matroid α} {D : Set α} (hD : M.Dep D) (hDN : D ⊆ N.E) (hNM : N ≤m M) : N.Dep D

theorem Matroid.IsLoop.of_isMinor {α : Type u_1} {M N : Matroid α} {e : α} (he : M.IsLoop e) (heN : e ∈ N.E) (hNM : N ≤m M) : N.IsLoop e