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.IsBasis to Matroid.IsBase.

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 Matroid.IsBasis analogues of Matroid.IsBase 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.IsStrictRestriction 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 the only independent set. (In general, elements of R \ M.E are all 'loops' of the matroid M ↾ R; see Matroid.loops and Matroid.restrict_loops_eq' for a precise version of this statement.) This is mathematically strange, but is useful for API building.

The cost of allowing a restriction of M to be 'bigger' than 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; see Matroid.IsMinor.

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.isBase_restrict_iff {α : Type u_1} {M : Matroid α} {I X : Set α} (hX : X ⊆ M.E := by aesop_mat) : (M.restrict X).IsBase I ↔ M.IsBasis I X

theorem Matroid.isBase_restrict_iff' {α : Type u_1} {M : Matroid α} {I X : Set α} : (M.restrict X).IsBase I ↔ M.IsBasis' I X

theorem Matroid.IsBasis'.isBase_restrict {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis' I X) : (M.restrict X).IsBase I

theorem Matroid.IsBasis.restrict_isBase {α : Type u_1} {M : Matroid α} {I X : Set α} (h : M.IsBasis I X) : (M.restrict X).IsBase I

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

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

@[simp]

theorem Matroid.IsBasis.isBase_restrict {α : Type u_1} {M : Matroid α} {I X : Set α} (h : M.IsBasis I X) : (M.restrict X).IsBase I

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

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

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

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

theorem Matroid.isBasis'_iff_isBasis_restrict_univ {α : Type u_1} {M : Matroid α} {I X : Set α} : M.IsBasis' I X ↔ (M.restrict Set.univ).IsBasis I X

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.IsRestriction {α : Type u_1} (N M : Matroid α) : Prop

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

Equations

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

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

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

Equations

• N.IsStrictRestriction M = (N.IsRestriction M ∧ ¬M.IsRestriction 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 IsStrictRestriction 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 isRestriction order. (The PartialOrder on Matroid α is reserved for the minor order)

• ofMatroid :: (
• toMatroid : Matroid α

  The underlying Matroid

• )

theorem Matroid.Matroidᵣ.ext_iff {α : Type u_2} {x y : Matroidᵣ α} : x = y ↔ x.toMatroid = y.toMatroid

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

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

Equations

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

@[simp]

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

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

Equations

• Matroid.instPartialOrderMatroidᵣ = { le := fun (x1 x2 : Matroid.Matroidᵣ α) => x1.toMatroid.IsRestriction x2.toMatroid, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

theorem Matroid.IsStrictRestriction.isRestriction {α : Type u_1} {M N : Matroid α} (h : N.IsStrictRestriction M) : N.IsRestriction M

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

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

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

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

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

theorem Matroid.IsRestriction.isStrictRestriction_of_ne {α : Type u_1} {M N : Matroid α} (h : N.IsRestriction M) (hne : N ≠ M) : N.IsStrictRestriction M

theorem Matroid.IsRestriction.eq_or_isStrictRestriction {α : Type u_1} {M N : Matroid α} (h : N.IsRestriction M) : N = M ∨ N.IsStrictRestriction M

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

theorem Matroid.IsRestriction.isStrictRestriction_of_ground_ne {α : Type u_1} {M N : Matroid α} (h : N.IsRestriction M) (hne : N.E ≠ M.E) : N.IsStrictRestriction M

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

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

theorem Matroid.IsRestriction.rankFinite {α : Type u_1} {N M : Matroid α} [M.RankFinite] (h : N.IsRestriction M) : N.RankFinite

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

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

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

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

theorem Matroid.IsRestriction.indep_iff {α : Type u_1} {M : Matroid α} {I : Set α} {N : Matroid α} (hMN : N.IsRestriction M) : N.Indep I ↔ M.Indep I ∧ I ⊆ N.E

theorem Matroid.IsBasis.isBasis_isRestriction {α : Type u_1} {M : Matroid α} {I X : Set α} {N : Matroid α} (hI : M.IsBasis I X) (hNM : N.IsRestriction M) (hX : X ⊆ N.E) : N.IsBasis I X

theorem Matroid.IsBasis.of_isRestriction {α : Type u_1} {M : Matroid α} {I X : Set α} {N : Matroid α} (hI : N.IsBasis I X) (hNM : N.IsRestriction M) : M.IsBasis I X

theorem Matroid.IsBase.isBasis_of_isRestriction {α : Type u_1} {M : Matroid α} {I : Set α} {N : Matroid α} (hI : N.IsBase I) (hNM : N.IsRestriction M) : M.IsBasis I N.E

theorem Matroid.IsRestriction.base_iff {α : Type u_1} {M N : Matroid α} (hMN : N.IsRestriction M) {B : Set α} : N.IsBase B ↔ M.IsBasis B N.E

theorem Matroid.IsRestriction.isBasis_iff {α : Type u_1} {M : Matroid α} {I X : Set α} {N : Matroid α} (hMN : N.IsRestriction M) : N.IsBasis I X ↔ M.IsBasis I X ∧ X ⊆ N.E

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

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

theorem Matroid.IsRestriction.dep_iff {α : Type u_1} {M : Matroid α} {X : Set α} {N : Matroid α} (hMN : N.IsRestriction M) : N.Dep X ↔ M.Dep X ∧ X ⊆ N.E

IsBasis and Base

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

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

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

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

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

theorem Matroid.IsBasis.isBase_of_isBase_subset {α : Type u_1} {M : Matroid α} {I X B : Set α} (hIX : M.IsBasis I X) (hB : M.IsBase B) (hBX : B ⊆ X) : M.IsBase I

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

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

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

theorem Matroid.IsBasis.encard_eq_encard {α : Type u_1} {M : Matroid α} {I X J : Set α} (hI : M.IsBasis I X) (hJ : M.IsBasis 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.

theorem Matroid.Indep.augment_finset {α : Type u_1} {M : Matroid α} {I J : Finset α} (hI : M.Indep ↑I) (hJ : M.Indep ↑J) (hIJ : I.card < J.card) : ∃ e ∈ J, e ∉ I ∧ M.Indep (insert e ↑I)