Matroid Restriction

Given M : Matroid α and R : Set α, the independent sets of M that are contained in R are the independent sets of another matroid M ↾ R with ground set R, called the 'restriction' of M to R. For I, R ⊆ M.E, I is a basis of R in M if and only if I is a base of the restriction M ↾ R, so this construction relates Matroid.Basis to Matroid.Base.

If N M : Matroid α satisfy N = M ↾ R for some R ⊆ M.E, then we call N a 'restriction of M', and write N ≤r M. This is a partial order.

This file proves that the restriction is a matroid and that the ≤r order is a partial order, and gives related API. It also proves some Basis analogues of Base lemmas that, while they could be stated in Data.Matroid.Basic, are hard to prove without Matroid.restrict API.

Main Definitions

• M.restrict R, written M ↾ R, is the restriction of M : Matroid α to R : Set α: i.e. the matroid with ground set R whose independent sets are the M-independent subsets of R.

• Matroid.Restriction N M, written N ≤r M, means that N = M ↾ R for some R ⊆ M.E.

• Matroid.StrictRestriction N M, written N <r M, means that N = M ↾ R for some R ⊂ M.E.

• Matroidᵣ α is a type synonym for Matroid α, equipped with the PartialOrder ≤r.

Implementation Notes

Since R and M.E are both terms in Set α, to define the restriction M ↾ R, we need to either insist that R ⊆ M.E, or to say what happens when R contains the junk outside M.E.

It turns out that R ⊆ M.E is just an unnecessary hypothesis; if we say the restriction M ↾ R has ground set R and its independent sets are the M-independent subsets of R, we always get a matroid, in which the elements of R \ M.E aren't in any independent sets. We could instead define this matroid to always be 'smaller' than M by setting (M ↾ R).E := R ∩ M.E, but this is worse definitionally, and more generally less convenient.

This makes it possible to actually restrict a matroid 'upwards'; for instance, if M : Matroid α satisfies M.E = ∅, then M ↾ Set.univ is the matroid on α whose ground set is all of α, where the empty set is only the independent set. (Elements of R outside the ground set are all 'loops' of the matroid.) This is mathematically strange, but is useful for API building.

The cost of allowing a restriction of M to be 'bigger' than the M itself is that the statement M ↾ R ≤r M is only true with the hypothesis R ⊆ M.E (at least, if we want ≤r to be a partial order). But this isn't too inconvenient in practice. Indeed (· ⊆ M.E) proofs can often be automatically provided by aesop_mat.

We define the restriction order ≤r to give a PartialOrder instance on the type synonym Matroidᵣ α rather than Matroid α itself, because the PartialOrder (Matroid α) instance is reserved for the more mathematically important 'minor' order.

def Matroid.restrictIndepMatroid {α : Type u_1} (M : Matroid α) (R : Set α) : IndepMatroid α

The IndepMatroid whose independent sets are the independent subsets of R.

Equations

• M.restrictIndepMatroid R = { E := R, Indep := fun (I : Set α) => M.Indep I ∧ I ⊆ R, indep_empty := ⋯, indep_subset := ⋯, indep_aug := ⋯, indep_maximal := ⋯, subset_ground := ⋯ }

@[simp]

theorem Matroid.restrictIndepMatroid_E {α : Type u_1} (M : Matroid α) (R : Set α) : (M.restrictIndepMatroid R).E = R

@[simp]

theorem Matroid.restrictIndepMatroid_Indep {α : Type u_1} (M : Matroid α) (R I : Set α) : (M.restrictIndepMatroid R).Indep I = (M.Indep I ∧ I ⊆ R)

def Matroid.restrict {α : Type u_1} (M : Matroid α) (R : Set α) : Matroid α

Change the ground set of a matroid to some R : Set α. The independent sets of the restriction are the independent subsets of the new ground set. Most commonly used when R ⊆ M.E, but it is convenient not to require this. The elements of R \ M.E become 'loops'.

Equations

• M.restrict R = (M.restrictIndepMatroid R).matroid

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

M ↾ R means M.restrict R.

Equations

• Matroid.«term_↾_» = Lean.ParserDescr.trailingNode `Matroid.«term_↾_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↾ ") (Lean.ParserDescr.cat `term 66))

@[simp]

theorem Matroid.restrict_indep_iff {α : Type u_1} {M : Matroid α} {R I : Set α} : (M.restrict R).Indep I ↔ M.Indep I ∧ I ⊆ R

theorem Matroid.Indep.indep_restrict_of_subset {α : Type u_1} {M : Matroid α} {R I : Set α} (h : M.Indep I) (hIR : I ⊆ R) : (M.restrict R).Indep I

theorem Matroid.Indep.of_restrict {α : Type u_1} {M : Matroid α} {R I : Set α} (hI : (M.restrict R).Indep I) : M.Indep I

@[simp]

theorem Matroid.restrict_ground_eq {α : Type u_1} {M : Matroid α} {R : Set α} : (M.restrict R).E = R

theorem Matroid.restrict_finite {α : Type u_1} {M : Matroid α} {R : Set α} (hR : R.Finite) : (M.restrict R).Finite

@[simp]

theorem Matroid.restrict_dep_iff {α : Type u_1} {M : Matroid α} {R X : Set α} : (M.restrict R).Dep X ↔ ¬M.Indep X ∧ X ⊆ R

@[simp]

theorem Matroid.restrict_ground_eq_self {α : Type u_1} (M : Matroid α) : M.restrict M.E = M

theorem Matroid.restrict_restrict_eq {α : Type u_1} {R₁ R₂ : Set α} (M : Matroid α) (hR : R₂ ⊆ R₁) : (M.restrict R₁).restrict R₂ = M.restrict R₂

@[simp]

theorem Matroid.restrict_idem {α : Type u_1} (M : Matroid α) (R : Set α) : (M.restrict R).restrict R = M.restrict R

@[simp]

theorem Matroid.base_restrict_iff {α : Type u_1} {M : Matroid α} {I X : Set α} (hX : X ⊆ M.E := by aesop_mat) : (M.restrict X).Base I ↔ M.Basis I X

theorem Matroid.base_restrict_iff' {α : Type u_1} {M : Matroid α} {I X : Set α} : (M.restrict X).Base I ↔ M.Basis' I X

theorem Matroid.Basis.restrict_base {α : Type u_1} {M : Matroid α} {I X : Set α} (h : M.Basis I X) : (M.restrict X).Base I

instance Matroid.restrict_finiteRk {α : Type u_1} {M : Matroid α} [M.FiniteRk] (R : Set α) : (M.restrict R).FiniteRk

Equations

• ⋯ = ⋯

instance Matroid.restrict_finitary {α : Type u_1} {M : Matroid α} [M.Finitary] (R : Set α) : (M.restrict R).Finitary

Equations

• ⋯ = ⋯

@[simp]

theorem Matroid.Basis.base_restrict {α : Type u_1} {M : Matroid α} {I X : Set α} (h : M.Basis I X) : (M.restrict X).Base I

theorem Matroid.Basis.basis_restrict_of_subset {α : Type u_1} {M : Matroid α} {I X Y : Set α} (hI : M.Basis I X) (hXY : X ⊆ Y) : (M.restrict Y).Basis I X

theorem Matroid.basis'_restrict_iff {α : Type u_1} {M : Matroid α} {R I X : Set α} : (M.restrict R).Basis' I X ↔ M.Basis' I (X ∩ R) ∧ I ⊆ R

theorem Matroid.basis_restrict_iff' {α : Type u_1} {M : Matroid α} {R I X : Set α} : (M.restrict R).Basis I X ↔ M.Basis I (X ∩ M.E) ∧ X ⊆ R

theorem Matroid.basis_restrict_iff {α : Type u_1} {M : Matroid α} {R I X : Set α} (hR : R ⊆ M.E := by aesop_mat) : (M.restrict R).Basis I X ↔ M.Basis I X ∧ X ⊆ R

theorem Matroid.restrict_eq_restrict_iff {α : Type u_1} (M M' : Matroid α) (X : Set α) : M.restrict X = M'.restrict X ↔ ∀ I ⊆ X, M.Indep I ↔ M'.Indep I

@[simp]

theorem Matroid.restrict_eq_self_iff {α : Type u_1} {M : Matroid α} {R : Set α} : M.restrict R = M ↔ R = M.E

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

Restriction N M means that N = M ↾ R for some subset R of M.E

Equations

• N.Restriction M = ∃ R ⊆ M.E, N = M.restrict R

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

StrictRestriction N M means that N = M ↾ R for some strict subset R of M.E

Equations

• N.StrictRestriction M = (N.Restriction M ∧ ¬M.Restriction N)

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

N ≤r M means that N is a Restriction of M.

Equations

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

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

N <r M means that N is a StrictRestriction of M.

Equations

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

structure Matroid.Matroidᵣ (α : Type u_2) : Type u_2

A type synonym for matroids with the restriction order. (The PartialOrder on Matroid α is reserved for the minor order)

• ofMatroid :: (
• toMatroid : Matroid α

  The underlying Matroid.

• )

theorem Matroid.Matroidᵣ.ext {α : Type u_2} {x y : Matroid.Matroidᵣ α} (toMatroid : x.toMatroid = y.toMatroid) : x = y

instance Matroid.instCoeOutMatroidᵣ {α : Type u_2} : CoeOut (Matroid.Matroidᵣ α) (Matroid α)

Equations

• Matroid.instCoeOutMatroidᵣ = { coe := Matroid.Matroidᵣ.toMatroid }

@[simp]

theorem Matroid.Matroidᵣ.coe_inj {α : Type u_1} {M₁ M₂ : Matroid.Matroidᵣ α} : M₁.toMatroid = M₂.toMatroid ↔ M₁ = M₂

instance Matroid.instPartialOrderMatroidᵣ {α : Type u_2} : PartialOrder (Matroid.Matroidᵣ α)

Equations

• Matroid.instPartialOrderMatroidᵣ = PartialOrder.mk ⋯

@[simp]

theorem Matroid.Matroidᵣ.le_iff {α : Type u_1} {M M' : Matroid.Matroidᵣ α} : M ≤ M' ↔ M.toMatroid.Restriction M'.toMatroid

@[simp]

theorem Matroid.Matroidᵣ.lt_iff {α : Type u_1} {M M' : Matroid.Matroidᵣ α} : M < M' ↔ M.toMatroid.StrictRestriction M'.toMatroid

theorem Matroid.ofMatroid_le_iff {α : Type u_1} {M M' : Matroid α} : { toMatroid := M } ≤ { toMatroid := M' } ↔ M.Restriction M'

theorem Matroid.ofMatroid_lt_iff {α : Type u_1} {M M' : Matroid α} : { toMatroid := M } < { toMatroid := M' } ↔ M.StrictRestriction M'

theorem Matroid.Restriction.refl {α : Type u_1} {M : Matroid α} : M.Restriction M

theorem Matroid.Restriction.antisymm {α : Type u_1} {M M' : Matroid α} (h : M.Restriction M') (h' : M'.Restriction M) : M = M'

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

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

theorem Matroid.Restriction.eq_restrict {α : Type u_1} {M N : Matroid α} (h : N.Restriction M) : M.restrict N.E = N

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

theorem Matroid.Restriction.exists_eq_restrict {α : Type u_1} {M N : Matroid α} (h : N.Restriction M) : ∃ R ⊆ M.E, N = M.restrict R

theorem Matroid.Restriction.of_subset {α : Type u_1} {R R' : Set α} (M : Matroid α) (h : R ⊆ R') : (M.restrict R).Restriction (M.restrict R')

theorem Matroid.restriction_iff_exists {α : Type u_1} {M N : Matroid α} : N.Restriction M ↔ ∃ R ⊆ M.E, N = M.restrict R

theorem Matroid.StrictRestriction.restriction {α : Type u_1} {M N : Matroid α} (h : N.StrictRestriction M) : N.Restriction M

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

theorem Matroid.StrictRestriction.irrefl {α : Type u_1} (M : Matroid α) : ¬M.StrictRestriction M

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

theorem Matroid.StrictRestriction.eq_restrict {α : Type u_1} {M N : Matroid α} (h : N.StrictRestriction M) : M.restrict N.E = N

theorem Matroid.StrictRestriction.exists_eq_restrict {α : Type u_1} {M N : Matroid α} (h : N.StrictRestriction M) : ∃ R ⊂ M.E, N = M.restrict R

theorem Matroid.Restriction.strictRestriction_of_ne {α : Type u_1} {M N : Matroid α} (h : N.Restriction M) (hne : N ≠ M) : N.StrictRestriction M

theorem Matroid.Restriction.eq_or_strictRestriction {α : Type u_1} {M N : Matroid α} (h : N.Restriction M) : N = M ∨ N.StrictRestriction M

theorem Matroid.restrict_strictRestriction {α : Type u_1} {R : Set α} {M : Matroid α} (hR : R ⊂ M.E) : (M.restrict R).StrictRestriction M

theorem Matroid.Restriction.strictRestriction_of_ground_ne {α : Type u_1} {M N : Matroid α} (h : N.Restriction M) (hne : N.E ≠ M.E) : N.StrictRestriction M

theorem Matroid.StrictRestriction.of_ssubset {α : Type u_1} {R R' : Set α} (M : Matroid α) (h : R ⊂ R') : (M.restrict R).StrictRestriction (M.restrict R')

theorem Matroid.Restriction.finite {α : Type u_1} {N M : Matroid α} [M.Finite] (h : N.Restriction M) : N.Finite

theorem Matroid.Restriction.finiteRk {α : Type u_1} {N M : Matroid α} [M.FiniteRk] (h : N.Restriction M) : N.FiniteRk

theorem Matroid.Restriction.finitary {α : Type u_1} {N M : Matroid α} [M.Finitary] (h : N.Restriction M) : N.Finitary

theorem Matroid.finite_setOf_restriction {α : Type u_1} (M : Matroid α) [M.Finite] : {N : Matroid α | N.Restriction M}.Finite

theorem Matroid.Indep.of_restriction {α : Type u_1} {M : Matroid α} {I : Set α} {N : Matroid α} (hI : N.Indep I) (hNM : N.Restriction M) : M.Indep I

theorem Matroid.Indep.indep_restriction {α : Type u_1} {M : Matroid α} {I : Set α} {N : Matroid α} (hI : M.Indep I) (hNM : N.Restriction M) (hIN : I ⊆ N.E) : N.Indep I

theorem Matroid.Basis.basis_restriction {α : Type u_1} {M : Matroid α} {I X : Set α} {N : Matroid α} (hI : M.Basis I X) (hNM : N.Restriction M) (hX : X ⊆ N.E) : N.Basis I X

theorem Matroid.Basis.of_restriction {α : Type u_1} {M : Matroid α} {I X : Set α} {N : Matroid α} (hI : N.Basis I X) (hNM : N.Restriction M) : M.Basis I X

theorem Matroid.Base.basis_of_restriction {α : Type u_1} {M : Matroid α} {I : Set α} {N : Matroid α} (hI : N.Base I) (hNM : N.Restriction M) : M.Basis I N.E

theorem Matroid.Dep.of_restriction {α : Type u_1} {M : Matroid α} {X : Set α} {N : Matroid α} (hX : N.Dep X) (hNM : N.Restriction M) : M.Dep X

theorem Matroid.Dep.dep_restriction {α : Type u_1} {M : Matroid α} {X : Set α} {N : Matroid α} (hX : M.Dep X) (hNM : N.Restriction M) (hXE : X ⊆ N.E := by aesop_mat) : N.Dep X

Basis and Base

The lemmas below exploit the fact that (M ↾ X).Base I ↔ M.Basis I X to transfer facts about Matroid.Base to facts about Matroid.Basis. Their statements thematically belong in Data.Matroid.Basic, but they appear here because their proofs depend on the API for Matroid.restrict,

theorem Matroid.Basis.transfer {α : Type u_1} {M : Matroid α} {I X Y J : Set α} (hIX : M.Basis I X) (hJX : M.Basis J X) (hXY : X ⊆ Y) (hJY : M.Basis J Y) : M.Basis I Y

theorem Matroid.Basis.basis_of_basis_of_subset_of_subset {α : Type u_1} {M : Matroid α} {I X Y J : Set α} (hI : M.Basis I X) (hJ : M.Basis J Y) (hJX : J ⊆ X) (hIY : I ⊆ Y) : M.Basis I Y

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

theorem Matroid.Indep.exists_insert_of_not_basis {α : Type u_1} {M : Matroid α} {I X J : Set α} (hI : M.Indep I) (hIX : I ⊆ X) (hI' : ¬M.Basis I X) (hJ : M.Basis J X) : ∃ e ∈ J \ I, M.Indep (insert e I)

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

theorem Matroid.Basis.exchange {α : Type u_1} {M : Matroid α} {I X J : Set α} {e : α} (hIX : M.Basis I X) (hJX : M.Basis J X) (he : e ∈ I \ J) : ∃ f ∈ J \ I, M.Basis (insert f (I \ {e})) X

theorem Matroid.Basis.eq_exchange_of_diff_eq_singleton {α : Type u_1} {M : Matroid α} {I X J : Set α} {e : α} (hI : M.Basis I X) (hJ : M.Basis J X) (hIJ : I \ J = {e}) : ∃ f ∈ J \ I, J = insert f I \ {e}

theorem Matroid.Basis'.encard_eq_encard {α : Type u_1} {M : Matroid α} {I X J : Set α} (hI : M.Basis' I X) (hJ : M.Basis' J X) : I.encard = J.encard

theorem Matroid.Basis.encard_eq_encard {α : Type u_1} {M : Matroid α} {I X J : Set α} (hI : M.Basis I X) (hJ : M.Basis J X) : I.encard = J.encard

theorem Matroid.Indep.augment {α : Type u_1} {M : Matroid α} {I J : Set α} (hI : M.Indep I) (hJ : M.Indep J) (hIJ : I.encard < J.encard) : ∃ e ∈ J \ I, M.Indep (insert e I)

Any independent set can be extended into a larger independent set.