Documentation

Mathlib.Data.Matroid.Restrict

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 #

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.

@[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 : Set α) (I : Set α) :
(M.restrictIndepMatroid R).Indep I = (M.Indep I I R)
def Matroid.restrictIndepMatroid {α : Type u_1} (M : Matroid α) (R : Set α) :

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 := }
Instances For
    def Matroid.restrict {α : Type u_1} (M : Matroid α) (R : Set α) :

    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
    Instances For
      @[simp]
      theorem Matroid.restrict_indep_iff {α : Type u_1} {M : Matroid α} {R : Set α} {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 : Set α} {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 : Set α} {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 : Set α} {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₁ : Set α} {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 : Set α} {X : Set α} (hX : autoParam (X M.E) _auto✝) :
      (M.restrict X).Base I M.Basis I X
      theorem Matroid.base_restrict_iff' {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} :
      (M.restrict X).Base I M.Basis' I X
      theorem Matroid.Basis.restrict_base {α : Type u_1} {M : Matroid α} {I : Set α} {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 : Set α} {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 : Set α} {X : Set α} {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 : Set α} {I : Set α} {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 : Set α} {I : Set α} {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 : Set α} {I : Set α} {X : Set α} (hR : autoParam (R M.E) _auto✝) :
      (M.restrict R).Basis I X M.Basis I X X R
      theorem Matroid.restrict_eq_restrict_iff {α : Type u_1} (M : Matroid α) (M' : Matroid α) (X : Set α) :
      M.restrict X = M'.restrict X IX, 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 : Matroid α) (M : Matroid α) :

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

      Equations
      • N.Restriction M = RM.E, N = M.restrict R
      Instances For
        def Matroid.StrictRestriction {α : Type u_1} (N : Matroid α) (M : Matroid α) :

        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)
        Instances For

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

          Equations
          Instances For
            theorem Matroid.Matroidᵣ.ext_iff {α : Type u_2} {x : Matroid.Matroidᵣ α} {y : Matroid.Matroidᵣ α} :
            x = y x.toMatroid = y.toMatroid
            theorem Matroid.Matroidᵣ.ext {α : Type u_2} {x : Matroid.Matroidᵣ α} {y : Matroid.Matroidᵣ α} (toMatroid : x.toMatroid = y.toMatroid) :
            x = y
            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)

            Instances For
              Equations
              • Matroid.instCoeOutMatroidᵣ = { coe := Matroid.Matroidᵣ.toMatroid }
              @[simp]
              theorem Matroid.Matroidᵣ.coe_inj {α : Type u_1} {M₁ : Matroid.Matroidᵣ α} {M₂ : Matroid.Matroidᵣ α} :
              M₁.toMatroid = M₂.toMatroid M₁ = M₂
              Equations
              @[simp]
              theorem Matroid.Matroidᵣ.le_iff {α : Type u_1} {M : Matroid.Matroidᵣ α} {M' : Matroid.Matroidᵣ α} :
              M M' M.toMatroid.Restriction M'.toMatroid
              @[simp]
              theorem Matroid.Matroidᵣ.lt_iff {α : Type u_1} {M : Matroid.Matroidᵣ α} {M' : Matroid.Matroidᵣ α} :
              M < M' M.toMatroid.StrictRestriction M'.toMatroid
              theorem Matroid.ofMatroid_le_iff {α : Type u_1} {M : Matroid α} {M' : Matroid α} :
              { toMatroid := M } { toMatroid := M' } M.Restriction M'
              theorem Matroid.ofMatroid_lt_iff {α : Type u_1} {M : Matroid α} {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 : Matroid α} {M' : Matroid α} (h : M.Restriction M') (h' : M'.Restriction M) :
              M = M'
              theorem Matroid.Restriction.trans {α : Type u_1} {M₁ : Matroid α} {M₂ : Matroid α} {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 : autoParam (R M.E) _auto✝) :
              (M.restrict R).Restriction M
              theorem Matroid.Restriction.eq_restrict {α : Type u_1} {M : Matroid α} {N : Matroid α} (h : N.Restriction M) :
              M.restrict N.E = N
              theorem Matroid.Restriction.subset {α : Type u_1} {M : Matroid α} {N : Matroid α} (h : N.Restriction M) :
              N.E M.E
              theorem Matroid.Restriction.exists_eq_restrict {α : Type u_1} {M : Matroid α} {N : Matroid α} (h : N.Restriction M) :
              RM.E, N = M.restrict R
              theorem Matroid.Restriction.of_subset {α : Type u_1} {R : Set α} {R' : Set α} (M : Matroid α) (h : R R') :
              (M.restrict R).Restriction (M.restrict R')
              theorem Matroid.restriction_iff_exists {α : Type u_1} {M : Matroid α} {N : Matroid α} :
              N.Restriction M RM.E, N = M.restrict R
              theorem Matroid.StrictRestriction.restriction {α : Type u_1} {M : Matroid α} {N : Matroid α} (h : N.StrictRestriction M) :
              N.Restriction M
              theorem Matroid.StrictRestriction.ne {α : Type u_1} {M : Matroid α} {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 : Matroid α} {N : Matroid α} (h : N.StrictRestriction M) :
              N.E M.E
              theorem Matroid.StrictRestriction.eq_restrict {α : Type u_1} {M : Matroid α} {N : Matroid α} (h : N.StrictRestriction M) :
              M.restrict N.E = N
              theorem Matroid.StrictRestriction.exists_eq_restrict {α : Type u_1} {M : Matroid α} {N : Matroid α} (h : N.StrictRestriction M) :
              RM.E, N = M.restrict R
              theorem Matroid.Restriction.strictRestriction_of_ne {α : Type u_1} {M : Matroid α} {N : Matroid α} (h : N.Restriction M) (hne : N M) :
              N.StrictRestriction M
              theorem Matroid.Restriction.eq_or_strictRestriction {α : Type u_1} {M : Matroid α} {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 : Matroid α} {N : Matroid α} (h : N.Restriction M) (hne : N.E M.E) :
              N.StrictRestriction M
              theorem Matroid.StrictRestriction.of_ssubset {α : Type u_1} {R : Set α} {R' : Set α} (M : Matroid α) (h : R R') :
              (M.restrict R).StrictRestriction (M.restrict R')
              theorem Matroid.Restriction.finite {α : Type u_1} {N : Matroid α} {M : Matroid α} [M.Finite] (h : N.Restriction M) :
              N.Finite
              theorem Matroid.Restriction.finiteRk {α : Type u_1} {N : Matroid α} {M : Matroid α} [M.FiniteRk] (h : N.Restriction M) :
              N.FiniteRk
              theorem Matroid.Restriction.finitary {α : Type u_1} {N : Matroid α} {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 : Set α} {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 : Set α} {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 : autoParam (X N.E) _auto✝) :
              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 : Set α} {X : Set α} {Y : Set α} {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 : Set α} {X : Set α} {Y : Set α} {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 : Set α} {X : Set α} {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 : Set α} {X : Set α} {J : Set α} (hI : M.Indep I) (hIX : I X) (hI' : ¬M.Basis I X) (hJ : M.Basis J X) :
              eJ \ I, M.Indep (insert e I)
              theorem Matroid.Basis.base_of_base_subset {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} {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 : Set α} {X : Set α} {J : Set α} {e : α} (hIX : M.Basis I X) (hJX : M.Basis J X) (he : e I \ J) :
              fJ \ I, M.Basis (insert f (I \ {e})) X
              theorem Matroid.Basis.eq_exchange_of_diff_eq_singleton {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} {J : Set α} {e : α} (hI : M.Basis I X) (hJ : M.Basis J X) (hIJ : I \ J = {e}) :
              fJ \ I, J = insert f I \ {e}
              theorem Matroid.Basis'.encard_eq_encard {α : Type u_1} {M : Matroid α} {I : Set α} {X : Set α} {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 : Set α} {X : Set α} {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 : Set α} {J : Set α} (hI : M.Indep I) (hJ : M.Indep J) (hIJ : I.encard < J.encard) :
              eJ \ I, M.Indep (insert e I)

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