Documentation

Mathlib.Data.Matroid.Restrict

Matroid IsRestriction #

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 'isRestriction' of M to R. For I, R ⊆ M.E, I is a isBasis of R in M if and only if I is a base of the isRestriction M ↾ R, so this construction relates Matroid.IsBasis to Matroid.Base.

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

This file proves that the isRestriction is a matroid and that the ≤r order is a partial order, and gives related API. It also proves some IsBasis 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 isRestriction 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 isRestriction 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 isRestriction 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 isRestriction 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 α) :

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
    @[simp]
    theorem Matroid.restrictIndepMatroid_E {α : Type u_1} (M : Matroid α) (R : Set α) :
    @[simp]
    theorem Matroid.restrictIndepMatroid_Indep {α : Type u_1} (M : Matroid α) (R I : Set α) :
    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
    Instances For
      @[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) :
      @[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 α) :
      @[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) :
      theorem Matroid.IsBasis.restrict_isBase {α : Type u_1} {M : Matroid α} {I X : Set α} (h : M.IsBasis I X) :
      instance Matroid.restrict_rankFinite {α : Type u_1} {M : Matroid α} [M.RankFinite] (R : Set α) :
      instance Matroid.restrict_finitary {α : Type u_1} {M : Matroid α} [M.Finitary] (R : Set α) :
      @[simp]
      theorem Matroid.IsBasis.isBase_restrict {α : Type u_1} {M : Matroid α} {I X : Set α} (h : M.IsBasis I X) :
      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.restrict_eq_restrict_iff {α : Type u_1} (M 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.IsRestriction {α : Type u_1} (N M : Matroid α) :

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

      Equations
      Instances For
        @[deprecated Matroid.IsRestriction (since := "2025-02-14")]
        def Matroid.Restriction {α : Type u_1} (N M : Matroid α) :

        Alias of Matroid.IsRestriction.


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

        Equations
        Instances For
          def Matroid.IsStrictRestriction {α : Type u_1} (N M : Matroid α) :

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

          Equations
          Instances For
            @[deprecated Matroid.IsStrictRestriction (since := "2025-02-14")]
            def Matroid.StrictRestriction {α : Type u_1} (N M : Matroid α) :

            Alias of Matroid.IsStrictRestriction.


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

            Equations
            Instances For

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

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

                Instances For
                  theorem Matroid.Matroidᵣ.ext {α : Type u_2} {x y : Matroidᵣ α} (toMatroid : x.toMatroid = y.toMatroid) :
                  x = y
                  @[simp]
                  theorem Matroid.Matroidᵣ.coe_inj {α : Type u_1} {M₁ M₂ : Matroidᵣ α} :
                  M₁.toMatroid = M₂.toMatroid M₁ = M₂
                  @[simp]
                  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.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) :
                  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) :
                  RM.E, N = M.restrict R
                  theorem Matroid.IsRestriction.of_subset {α : Type u_1} {R R' : Set α} (M : Matroid α) (h : R R') :
                  theorem Matroid.isRestriction_iff_exists {α : Type u_1} {M N : Matroid α} :
                  N.IsRestriction M RM.E, N = M.restrict R
                  theorem Matroid.IsStrictRestriction.ne {α : Type u_1} {M N : Matroid α} (h : N.IsStrictRestriction M) :
                  N M
                  theorem Matroid.IsStrictRestriction.ssubset {α : Type u_1} {M N : Matroid α} (h : N.IsStrictRestriction M) :
                  N.E M.E
                  theorem Matroid.IsStrictRestriction.exists_eq_restrict {α : Type u_1} {M N : Matroid α} (h : N.IsStrictRestriction M) :
                  RM.E, N = M.restrict R
                  theorem Matroid.restrict_isStrictRestriction {α : Type u_1} {R : Set α} {M : Matroid α} (hR : R M.E) :
                  theorem Matroid.IsStrictRestriction.of_ssubset {α : Type u_1} {R R' : Set α} (M : Matroid α) (h : R R') :
                  theorem Matroid.IsRestriction.finite {α : Type u_1} {N M : Matroid α} [M.Finite] (h : N.IsRestriction M) :
                  theorem Matroid.IsRestriction.finitary {α : Type u_1} {N M : Matroid α} [M.Finitary] (h : N.IsRestriction M) :
                  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) :
                  eJ \ 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) :
                  fJ \ 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}) :
                  fJ \ 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) :
                  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) :
                  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) :
                  eJ \ 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) :
                  eJ, eI M.Indep (insert e I)