Matroid Minors

For M : Matroid α and X : Set α, we can remove the elements of X from M to obtain a matroid with ground set M.E \ X in two different ways: 'deletion' and 'contraction'. The deletion of X from M, denoted M ＼ X, is the matroid whose independent sets are the independent sets of M that are disjoint from X. The contraction of X is the matroid M ／ X in which a set I is independent if and only if I ∪ J is independent in M, where J is an arbitrarily chosen basis for X.

We also have M ＼ X = M ↾ (M.E \ X) and (a little more cryptically) M ／ X = (M✶ ＼ X)✶. We use these as the definitions, and prove that the independent sets are the same as those just specified.

A matroid obtained from M by a sequence of deletions/contractions (or equivalently, by a single deletion and a single contraction) 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.

Main Declarations

• Matroid.delete M D, written M ＼ D, is the restriction of M to the set M.E \ D.
• Matroid.contract M C, written M ／ C, is the matroid on ground set M.E \ C in which a set I ⊆ M.E \ C is independent if and only if I ∪ J is independent in M, where J is an arbitrary basis for C.
• Matroid.contract_dual M C : (M ／ X)✶ = M✶ ＼ X; the dual of contraction is deletion.
• Matroid.delete_dual M C : (M ＼ X)✶ = M✶ ／ X; the dual of deletion is contraction.

Naming conventions

We use the abbreviations deleteElem and contractElem in lemma names to refer to the deletion M ＼ {e} or contraction M ／ {e} of a single element e : α from M : Matroid α.

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

The deletion M ＼ D is the restriction of a matroid M to M.E \ D. Its independent sets are the M-independent subsets of M.E \ D.

Equations

• M.delete D = M.restrict (M.E \ D)

def Matroid.«term_＼_» : Lean.TrailingParserDescr

M ＼ D refers to the deletion of a set D from the matroid M.

Equations

• Matroid.«term_＼_» = Lean.ParserDescr.trailingNode `Matroid.«term_＼_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ＼ ") (Lean.ParserDescr.cat `term 76))

theorem Matroid.delete_eq_restrict {α : Type u_1} (M : Matroid α) (D : Set α) : M.delete D = M.restrict (M.E \ D)

instance Matroid.delete_finite {α : Type u_1} {M : Matroid α} {D : Set α} [M.Finite] : (M.delete D).Finite

instance Matroid.delete_rankFinite {α : Type u_1} {M : Matroid α} {D : Set α} [M.RankFinite] : (M.delete D).RankFinite

theorem Matroid.restrict_compl {α : Type u_1} (M : Matroid α) (D : Set α) : M.restrict (M.E \ D) = M.delete D

@[simp]

theorem Matroid.delete_compl {α : Type u_1} {M : Matroid α} {R : Set α} (hR : R ⊆ M.E := by aesop_mat) : M.delete (M.E \ R) = M.restrict R

@[simp]

theorem Matroid.delete_isRestriction {α : Type u_1} (M : Matroid α) (D : Set α) : (M.delete D).IsRestriction M

theorem Matroid.IsRestriction.exists_eq_delete {α : Type u_1} {M N : Matroid α} (hNM : N.IsRestriction M) : ∃ D ⊆ M.E, N = M.delete D

theorem Matroid.isRestriction_iff_exists_eq_delete {α : Type u_1} {M N : Matroid α} : N.IsRestriction M ↔ ∃ D ⊆ M.E, N = M.delete D

@[simp]

theorem Matroid.delete_ground {α : Type u_1} (M : Matroid α) (D : Set α) : (M.delete D).E = M.E \ D

theorem Matroid.delete_subset_ground {α : Type u_1} (M : Matroid α) (D : Set α) : (M.delete D).E ⊆ M.E

@[simp]

theorem Matroid.delete_eq_self_iff {α : Type u_1} {M : Matroid α} {D : Set α} : M.delete D = M ↔ Disjoint D M.E

theorem Matroid.delete_eq_self {α : Type u_1} {M : Matroid α} {D : Set α} : Disjoint D M.E → M.delete D = M

Alias of the reverse direction of Matroid.delete_eq_self_iff.

theorem Matroid.deleteElem_eq_self {α : Type u_1} {M : Matroid α} {e : α} (he : e ∉ M.E) : M.delete {e} = M

@[simp]

theorem Matroid.delete_delete {α : Type u_1} (M : Matroid α) (D₁ D₂ : Set α) : (M.delete D₁).delete D₂ = M.delete (D₁ ∪ D₂)

theorem Matroid.delete_comm {α : Type u_1} (M : Matroid α) (D₁ D₂ : Set α) : (M.delete D₁).delete D₂ = (M.delete D₂).delete D₁

theorem Matroid.delete_inter_ground_eq {α : Type u_1} (M : Matroid α) (D : Set α) : M.delete (D ∩ M.E) = M.delete D

theorem Matroid.delete_eq_delete_iff {α : Type u_1} {M : Matroid α} {D₁ D₂ : Set α} : M.delete D₁ = M.delete D₂ ↔ D₁ ∩ M.E = D₂ ∩ M.E

theorem Matroid.IsRestriction.restrict_delete_of_disjoint {α : Type u_1} {M N : Matroid α} {X : Set α} (h : N.IsRestriction M) (hX : Disjoint X N.E) : N.IsRestriction (M.delete X)

theorem Matroid.IsRestriction.isRestriction_deleteElem {α : Type u_1} {M N : Matroid α} {e : α} (h : N.IsRestriction M) (he : e ∉ N.E) : N.IsRestriction (M.delete {e})

@[simp]

theorem Matroid.delete_indep_iff {α : Type u_1} {M : Matroid α} {I D : Set α} : (M.delete D).Indep I ↔ M.Indep I ∧ Disjoint I D

theorem Matroid.deleteElem_indep_iff {α : Type u_1} {M : Matroid α} {e : α} {I : Set α} : (M.delete {e}).Indep I ↔ M.Indep I ∧ e ∉ I

theorem Matroid.Indep.of_delete {α : Type u_1} {M : Matroid α} {I D : Set α} (h : (M.delete D).Indep I) : M.Indep I

theorem Matroid.Indep.indep_delete_of_disjoint {α : Type u_1} {M : Matroid α} {I D : Set α} (h : M.Indep I) (hID : Disjoint I D) : (M.delete D).Indep I

theorem Matroid.indep_iff_delete_of_disjoint {α : Type u_1} {M : Matroid α} {I D : Set α} (hID : Disjoint I D) : M.Indep I ↔ (M.delete D).Indep I

@[simp]

theorem Matroid.delete_dep_iff {α : Type u_1} {M : Matroid α} {X D : Set α} : (M.delete D).Dep X ↔ M.Dep X ∧ Disjoint X D

@[simp]

theorem Matroid.delete_isBase_iff {α : Type u_1} {M : Matroid α} {B D : Set α} : (M.delete D).IsBase B ↔ M.IsBasis B (M.E \ D)

@[simp]

theorem Matroid.delete_isBasis_iff {α : Type u_1} {M : Matroid α} {I X D : Set α} : (M.delete D).IsBasis I X ↔ M.IsBasis I X ∧ Disjoint X D

@[simp]

theorem Matroid.delete_isBasis'_iff {α : Type u_1} {M : Matroid α} {I X D : Set α} : (M.delete D).IsBasis' I X ↔ M.IsBasis' I (X \ D)

theorem Matroid.IsBasis.of_delete {α : Type u_1} {M : Matroid α} {I X D : Set α} (h : (M.delete D).IsBasis I X) : M.IsBasis I X

theorem Matroid.IsBasis.delete {α : Type u_1} {M : Matroid α} {I X D : Set α} (h : M.IsBasis I X) (hX : Disjoint X D) : (M.delete D).IsBasis I X

@[simp]

theorem Matroid.delete_isLoop_iff {α : Type u_1} {M : Matroid α} {e : α} {D : Set α} : (M.delete D).IsLoop e ↔ M.IsLoop e ∧ e ∉ D

@[simp]

theorem Matroid.delete_isNonloop_iff {α : Type u_1} {M : Matroid α} {e : α} {D : Set α} : (M.delete D).IsNonloop e ↔ M.IsNonloop e ∧ e ∉ D

theorem Matroid.IsNonloop.of_delete {α : Type u_1} {M : Matroid α} {e : α} {D : Set α} (h : (M.delete D).IsNonloop e) : M.IsNonloop e

theorem Matroid.isNonloop_iff_delete_of_not_mem {α : Type u_1} {M : Matroid α} {e : α} {D : Set α} (he : e ∉ D) : M.IsNonloop e ↔ (M.delete D).IsNonloop e

@[simp]

theorem Matroid.delete_isCircuit_iff {α : Type u_1} {M : Matroid α} {D C : Set α} : (M.delete D).IsCircuit C ↔ M.IsCircuit C ∧ Disjoint C D

theorem Matroid.IsCircuit.of_delete {α : Type u_1} {M : Matroid α} {D C : Set α} (h : (M.delete D).IsCircuit C) : M.IsCircuit C

theorem Matroid.circuit_iff_delete_of_disjoint {α : Type u_1} {M : Matroid α} {D C : Set α} (hCD : Disjoint C D) : M.IsCircuit C ↔ (M.delete D).IsCircuit C

@[simp]

theorem Matroid.delete_closure_eq {α : Type u_1} (M : Matroid α) (D X : Set α) : (M.delete D).closure X = M.closure (X \ D) \ D

@[simp]

theorem Matroid.delete_loops_eq {α : Type u_1} (M : Matroid α) (D : Set α) : (M.delete D).loops = M.loops \ D

@[simp]

theorem Matroid.delete_empty {α : Type u_1} (M : Matroid α) : M.delete ∅ = M

theorem Matroid.delete_delete_eq_delete_diff {α : Type u_1} (M : Matroid α) (D₁ D₂ : Set α) : (M.delete D₁).delete D₂ = (M.delete D₁).delete (D₂ \ D₁)

instance Matroid.delete_finitary {α : Type u_1} (M : Matroid α) [M.Finitary] (D : Set α) : (M.delete D).Finitary

theorem Matroid.Coindep.delete_isBase_iff {α : Type u_1} {M : Matroid α} {B D : Set α} (hD : M.Coindep D) : (M.delete D).IsBase B ↔ M.IsBase B ∧ Disjoint B D

theorem Matroid.Coindep.delete_rankPos {α : Type u_1} {M : Matroid α} {D : Set α} [M.RankPos] (hD : M.Coindep D) : (M.delete D).RankPos

theorem Matroid.Coindep.delete_spanning_iff {α : Type u_1} {M : Matroid α} {S D : Set α} (hD : M.Coindep D) : (M.delete D).Spanning S ↔ M.Spanning S ∧ Disjoint S D

def Matroid.contract {α : Type u_1} (M : Matroid α) (C : Set α) : Matroid α

The contraction M ／ C is the matroid on M.E \ C in which a set I ⊆ M.E \ C is independent if and only if I ∪ J is independent, where J is an arbitrarily chosen basis for C. It is also equal to (M✶ ＼ C)✶, and is defined this way so we don't have to give a separate proof that it is actually a matroid. (Currently the proof it has the correct independent sets is TODO. )

Equations

• M ／ C = (M✶.delete C)✶

def Matroid.«term_／_» : Lean.TrailingParserDescr

M ／ C refers to the contraction of a set C from the matroid M.

Equations

• Matroid.«term_／_» = Lean.ParserDescr.trailingNode `Matroid.«term_／_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ／ ") (Lean.ParserDescr.cat `term 76))

theorem Matroid.dual_delete_dual {α : Type u_1} (M : Matroid α) (X : Set α) : (M✶.delete X)✶ = M ／ X

@[simp]

theorem Matroid.dual_delete {α : Type u_1} (M : Matroid α) (X : Set α) : (M.delete X)✶ = M✶ ／ X

@[simp]

theorem Matroid.dual_contract {α : Type u_1} (M : Matroid α) (X : Set α) : (M ／ X)✶ = M✶.delete X

theorem Matroid.dual_contract_dual {α : Type u_1} (M : Matroid α) (X : Set α) : (M✶ ／ X)✶ = M.delete X

@[simp]

theorem Matroid.contract_contract {α : Type u_1} (M : Matroid α) (C₁ C₂ : Set α) : M ／ C₁ ／ C₂ = M ／ (C₁ ∪ C₂)

theorem Matroid.contract_comm {α : Type u_1} (M : Matroid α) (C₁ C₂ : Set α) : M ／ C₁ ／ C₂ = M ／ C₂ ／ C₁

theorem Matroid.dual_contract_delete {α : Type u_1} (M : Matroid α) (X Y : Set α) : ((M ／ X).delete Y)✶ = M✶.delete X ／ Y

theorem Matroid.dual_delete_contract {α : Type u_1} (M : Matroid α) (X Y : Set α) : (M.delete X ／ Y)✶ = (M✶ ／ X).delete Y