Documentation

Mathlib.Data.Matroid.Map

Maps between matroids #

This file defines maps and comaps, which move a matroid on one type to a matroid on another using a function between the types. The constructions are (up to isomorphism) just combinations of restrictions and parallel extensions, so are not mathematically difficult.

Because a matroid M : Matroid α is defined with am embedded ground set M.E : Set α which contains all the structure of M, there are several types of map and comap one could reasonably ask for; for instance, we could map M : Matroid α to a Matroid β using either a function f : α → β, a function f : ↑M.E → β or indeed a function f : ↑M.E → ↑E for some E : Set β. We attempt to give definitions that capture most reasonable use cases.

Matroid.map and Matroid.comap are defined in terms of bare functions rather than functions defined on subtypes, so are often easier to work in practice than the subtype variants. In fact, the statement that N = Matroid.map M f _ for some f : α → β is equivalent to the existence of an isomorphism from M to N, except in the trivial degenerate case where M is an empty matroid on a nonempty type and N is an empty matroid on an empty type. This can be simpler to use than an actual formal isomorphism, which requires subtypes.

Main definitions #

In the definitions below, M and N are matroids on α and β respectively.

Implementation details #

The definition of comap is the only place where we need to actually define a matroid from scratch. After comap is defined, we can define map and its variants indirectly in terms of comap.

If f : α → β is injective on M.E, the independent sets of M.map f hf are the images of the independent set of M; i.e. (M.map f hf).Indep I ↔ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀. But if f is globally injective, we can phrase this more directly; indeed, (M.map f _).Indep I ↔ M.Indep (f ⁻¹' I) ∧ I ⊆ range f. If f is an equivalence we have (M.map f _).Indep I ↔ M.Indep (f.symm '' I). In order that these stronger statements can be @[simp], we define mapEmbedding and mapEquiv separately from map.

Notes #

For finite matroids, both maps and comaps are a special case of a construction of Perfect [perfect1969matroid] in which a matroid structure can be transported across an arbitrary bipartite graph that may not correspond to a function at all (See [oxley2011], Theorem 11.2.12). It would have been nice to use this more general construction as a basis for the definition of both Matroid.map and Matroid.comap.

Unfortunately, we can't do this, because the construction doesn't extend to infinite matroids. Specifically, if M₁ and M₂ are matroids on the same type α, and f is the natural function from α ⊕ α to α, then the images under f of the independent sets of the direct sum M₁ ⊕ M₂ are the independent sets of a matroid if and only if the union of M₁ and M₂ is a matroid, and unions do not exist for some pairs of infinite matroids: see [aignerhorev2012infinite]. For this reason, Matroid.map requires injectivity to be well-defined in general.

TODO #

References #

def Matroid.comap {α : Type u_1} {β : Type u_2} (N : Matroid β) (f : αβ) :

The pullback of a matroid on β by a function f : α → β to a matroid on α. Elements with the same (nonloop) image are parallel and the ground set is f ⁻¹' M.E. The matroids M.comap f and M ↾ range f have isomorphic simplifications; the preimage of each nonloop of M ↾ range f is a parallel class.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Matroid.comap_indep_iff {α : Type u_1} {β : Type u_2} {f : αβ} {I : Set α} {N : Matroid β} :
    (N.comap f).Indep I N.Indep (f '' I) Set.InjOn f I
    @[simp]
    theorem Matroid.comap_ground_eq {α : Type u_1} {β : Type u_2} (N : Matroid β) (f : αβ) :
    (N.comap f).E = f ⁻¹' N.E
    @[simp]
    theorem Matroid.comap_dep_iff {α : Type u_1} {β : Type u_2} {f : αβ} {I : Set α} {N : Matroid β} :
    (N.comap f).Dep I N.Dep (f '' I) N.Indep (f '' I) ¬Set.InjOn f I
    @[simp]
    theorem Matroid.comap_id {β : Type u_2} (N : Matroid β) :
    N.comap id = N
    theorem Matroid.comap_indep_iff_of_injOn {α : Type u_1} {β : Type u_2} {f : αβ} {I : Set α} {N : Matroid β} (hf : Set.InjOn f (f ⁻¹' N.E)) :
    (N.comap f).Indep I N.Indep (f '' I)
    @[simp]
    theorem Matroid.comap_emptyOn {α : Type u_1} {β : Type u_2} (f : αβ) :
    @[simp]
    theorem Matroid.comap_loopyOn {α : Type u_1} {β : Type u_2} (f : αβ) (E : Set β) :
    @[simp]
    theorem Matroid.comap_basis_iff {α : Type u_1} {β : Type u_2} {f : αβ} {N : Matroid β} {I : Set α} {X : Set α} :
    (N.comap f).Basis I X N.Basis (f '' I) (f '' X) Set.InjOn f I I X
    @[simp]
    theorem Matroid.comap_base_iff {α : Type u_1} {β : Type u_2} {f : αβ} {N : Matroid β} {B : Set α} :
    (N.comap f).Base B N.Basis (f '' B) (f '' (f ⁻¹' N.E)) Set.InjOn f B B f ⁻¹' N.E
    @[simp]
    theorem Matroid.comap_basis'_iff {α : Type u_1} {β : Type u_2} {f : αβ} {N : Matroid β} {I : Set α} {X : Set α} :
    (N.comap f).Basis' I X N.Basis' (f '' I) (f '' X) Set.InjOn f I I X
    instance Matroid.comap_finitary {α : Type u_1} {β : Type u_2} (N : Matroid β) [N.Finitary] (f : αβ) :
    (N.comap f).Finitary
    Equations
    • =
    instance Matroid.comap_finiteRk {α : Type u_1} {β : Type u_2} (N : Matroid β) [N.FiniteRk] (f : αβ) :
    (N.comap f).FiniteRk
    Equations
    • =
    def Matroid.comapOn {α : Type u_1} {β : Type u_2} (N : Matroid β) (E : Set α) (f : αβ) :

    The pullback of a matroid on β by a function f : α → β to a matroid on α, restricted to a ground set E. The matroids M.comapOn f E and M ↾ (f '' E) have isomorphic simplifications; elements with the same nonloop image are parallel.

    Equations
    • N.comapOn E f = (N.comap f).restrict E
    Instances For
      theorem Matroid.comapOn_preimage_eq {α : Type u_1} {β : Type u_2} (N : Matroid β) (f : αβ) :
      N.comapOn (f ⁻¹' N.E) f = N.comap f
      @[simp]
      theorem Matroid.comapOn_indep_iff {α : Type u_1} {β : Type u_2} {f : αβ} {N : Matroid β} {E : Set α} {I : Set α} :
      (N.comapOn E f).Indep I N.Indep (f '' I) Set.InjOn f I I E
      @[simp]
      theorem Matroid.comapOn_ground_eq {α : Type u_1} {β : Type u_2} {f : αβ} {N : Matroid β} {E : Set α} :
      (N.comapOn E f).E = E
      theorem Matroid.comapOn_base_iff {α : Type u_1} {β : Type u_2} {f : αβ} {N : Matroid β} {E : Set α} {B : Set α} :
      (N.comapOn E f).Base B N.Basis' (f '' B) (f '' E) Set.InjOn f B B E
      theorem Matroid.comapOn_base_iff_of_surjOn {α : Type u_1} {β : Type u_2} {f : αβ} {N : Matroid β} {E : Set α} {B : Set α} (h : Set.SurjOn f E N.E) :
      (N.comapOn E f).Base B N.Base (f '' B) Set.InjOn f B B E
      theorem Matroid.comapOn_base_iff_of_bijOn {α : Type u_1} {β : Type u_2} {f : αβ} {N : Matroid β} {E : Set α} {B : Set α} (h : Set.BijOn f E N.E) :
      (N.comapOn E f).Base B N.Base (f '' B) B E
      theorem Matroid.comapOn_dual_eq_of_bijOn {α : Type u_1} {β : Type u_2} {f : αβ} {N : Matroid β} {E : Set α} (h : Set.BijOn f E N.E) :
      (N.comapOn E f) = N.comapOn E f
      instance Matroid.comapOn_finitary {α : Type u_1} {β : Type u_2} {f : αβ} {N : Matroid β} {E : Set α} [N.Finitary] :
      (N.comapOn E f).Finitary
      Equations
      • =
      instance Matroid.comapOn_finiteRk {α : Type u_1} {β : Type u_2} {f : αβ} {N : Matroid β} {E : Set α} [N.FiniteRk] :
      (N.comapOn E f).FiniteRk
      Equations
      • =
      def Matroid.mapSetEmbedding {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : M.E β) :

      Map a matroid M to an isomorphic copy in β using an embedding M.E ↪ β.

      Equations
      Instances For
        @[simp]
        theorem Matroid.mapSetEmbedding_ground {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : M.E β) :
        (M.mapSetEmbedding f).E = Set.range f
        @[simp]
        theorem Matroid.mapSetEmbedding_indep_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : M.E β} {I : Set β} :
        (M.mapSetEmbedding f).Indep I M.Indep (Subtype.val '' (f ⁻¹' I)) I Set.range f
        theorem Matroid.Indep.exists_eq_image_of_mapSetEmbedding {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : M.E β} {I : Set β} (hI : (M.mapSetEmbedding f).Indep I) :
        ∃ (I₀ : Set M.E), M.Indep (Subtype.val '' I₀) I = f '' I₀
        theorem Matroid.mapSetEmbedding_indep_iff' {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : M.E β} {I : Set β} :
        (M.mapSetEmbedding f).Indep I ∃ (I₀ : Set M.E), M.Indep (Subtype.val '' I₀) I = f '' I₀
        def Matroid.map {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : αβ) (hf : Set.InjOn f M.E) :

        Given a function f that is injective on M.E, the copy of M in β whose independent sets are the images of those in M. If β is a nonempty type, then N : Matroid β is a map of M if and only if M and N are isomorphic.

        Equations
        Instances For
          @[simp]
          theorem Matroid.map_ground {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : αβ) (hf : Set.InjOn f M.E) :
          (M.map f hf).E = f '' M.E
          @[simp]
          theorem Matroid.map_indep_iff {α : Type u_1} {β : Type u_2} {f : αβ} {M : Matroid α} {hf : Set.InjOn f M.E} {I : Set β} :
          (M.map f hf).Indep I ∃ (I₀ : Set α), M.Indep I₀ I = f '' I₀
          theorem Matroid.Indep.map {α : Type u_1} {β : Type u_2} {I : Set α} {M : Matroid α} (hI : M.Indep I) (f : αβ) (hf : Set.InjOn f M.E) :
          (M.map f hf).Indep (f '' I)
          theorem Matroid.Indep.exists_bijOn_of_map {α : Type u_1} {β : Type u_2} {f : αβ} {M : Matroid α} {I : Set β} (hf : Set.InjOn f M.E) (hI : (M.map f hf).Indep I) :
          ∃ (I₀ : Set α), M.Indep I₀ Set.BijOn f I₀ I
          theorem Matroid.map_image_indep_iff {α : Type u_1} {β : Type u_2} {f : αβ} {M : Matroid α} {hf : Set.InjOn f M.E} {I : Set α} (hI : I M.E) :
          (M.map f hf).Indep (f '' I) M.Indep I
          @[simp]
          theorem Matroid.map_base_iff {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : αβ) (hf : Set.InjOn f M.E) {B : Set β} :
          (M.map f hf).Base B ∃ (B₀ : Set α), M.Base B₀ B = f '' B₀
          theorem Matroid.Base.map {α : Type u_1} {β : Type u_2} {M : Matroid α} {B : Set α} (hB : M.Base B) {f : αβ} (hf : Set.InjOn f M.E) :
          (M.map f hf).Base (f '' B)
          theorem Matroid.map_dep_iff {α : Type u_1} {β : Type u_2} {f : αβ} {M : Matroid α} {hf : Set.InjOn f M.E} {D : Set β} :
          (M.map f hf).Dep D ∃ (D₀ : Set α), M.Dep D₀ D = f '' D₀
          theorem Matroid.map_image_base_iff {α : Type u_1} {β : Type u_2} {f : αβ} {M : Matroid α} {hf : Set.InjOn f M.E} {B : Set α} (hB : B M.E) :
          (M.map f hf).Base (f '' B) M.Base B
          theorem Matroid.Basis.map {α : Type u_1} {β : Type u_2} {I : Set α} {M : Matroid α} {X : Set α} (hIX : M.Basis I X) {f : αβ} (hf : Set.InjOn f M.E) :
          (M.map f hf).Basis (f '' I) (f '' X)
          theorem Matroid.map_basis_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {I : Set α} {X : Set α} (f : αβ) (hf : Set.InjOn f M.E) (hI : I M.E) (hX : X M.E) :
          (M.map f hf).Basis (f '' I) (f '' X) M.Basis I X
          theorem Matroid.map_basis_iff' {α : Type u_1} {β : Type u_2} {f : αβ} {M : Matroid α} {I : Set β} {X : Set β} {hf : Set.InjOn f M.E} :
          (M.map f hf).Basis I X ∃ (I₀ : Set α) (X₀ : Set α), M.Basis I₀ X₀ I = f '' I₀ X = f '' X₀
          @[simp]
          theorem Matroid.map_dual {α : Type u_1} {β : Type u_2} {f : αβ} {M : Matroid α} {hf : Set.InjOn f M.E} :
          (M.map f hf) = M.map f hf
          @[simp]
          theorem Matroid.map_emptyOn {α : Type u_1} {β : Type u_2} (f : αβ) :
          @[simp]
          theorem Matroid.map_loopyOn {α : Type u_1} {β : Type u_2} {E : Set α} (f : αβ) (hf : Set.InjOn f (Matroid.loopyOn E).E) :
          (Matroid.loopyOn E).map f hf = Matroid.loopyOn (f '' E)
          @[simp]
          theorem Matroid.map_freeOn {α : Type u_1} {β : Type u_2} {E : Set α} (f : αβ) (hf : Set.InjOn f (Matroid.freeOn E).E) :
          (Matroid.freeOn E).map f hf = Matroid.freeOn (f '' E)
          @[simp]
          theorem Matroid.map_id {α : Type u_1} {M : Matroid α} :
          M.map id = M
          theorem Matroid.map_comap {α : Type u_1} {β : Type u_2} {N : Matroid β} {f : αβ} (h_range : N.E Set.range f) (hf : Set.InjOn f (f ⁻¹' N.E)) :
          (N.comap f).map f hf = N
          theorem Matroid.comap_map {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : αβ} (hf : Function.Injective f) :
          (M.map f ).comap f = M
          instance Matroid.instNonemptyMap {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Nonempty] {f : αβ} (hf : Set.InjOn f M.E) :
          (M.map f hf).Nonempty
          Equations
          • =
          instance Matroid.instFiniteMap {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Finite] {f : αβ} (hf : Set.InjOn f M.E) :
          (M.map f hf).Finite
          Equations
          • =
          instance Matroid.instFinitaryMap {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Finitary] {f : αβ} (hf : Set.InjOn f M.E) :
          (M.map f hf).Finitary
          Equations
          • =
          instance Matroid.instFiniteRkMap {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.FiniteRk] {f : αβ} (hf : Set.InjOn f M.E) :
          (M.map f hf).FiniteRk
          Equations
          • =
          instance Matroid.instRkPosMap {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.RkPos] {f : αβ} (hf : Set.InjOn f M.E) :
          (M.map f hf).RkPos
          Equations
          • =
          def Matroid.mapSetEquiv {α : Type u_1} {β : Type u_2} (M : Matroid α) {E : Set β} (e : M.E E) :

          Map M : Matroid α to a Matroid β with ground set E using an equivalence M.E ≃ E. Defined using Matroid.ofExistsMatroid for better defeq.

          Equations
          Instances For
            @[simp]
            theorem Matroid.mapSetEquiv_indep_iff {α : Type u_1} {β : Type u_2} (M : Matroid α) {E : Set β} (e : M.E E) {I : Set β} :
            (M.mapSetEquiv e).Indep I M.Indep (Subtype.val '' (e.symm '' (Subtype.val ⁻¹' I))) I E
            @[simp]
            theorem Matroid.mapSetEquiv.ground {α : Type u_1} {β : Type u_2} (M : Matroid α) {E : Set β} (e : M.E E) :
            (M.mapSetEquiv e).E = E
            def Matroid.mapEmbedding {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : α β) :

            Map M : Matroid α across an embedding defined on all of α

            Equations
            • M.mapEmbedding f = M.map f
            Instances For
              @[simp]
              theorem Matroid.mapEmbedding_ground_eq {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : α β) :
              (M.mapEmbedding f).E = f '' M.E
              @[simp]
              theorem Matroid.mapEmbedding_indep_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : α β} {I : Set β} :
              (M.mapEmbedding f).Indep I M.Indep (f ⁻¹' I) I Set.range f
              theorem Matroid.Indep.mapEmbedding {α : Type u_1} {β : Type u_2} {I : Set α} {M : Matroid α} (hI : M.Indep I) (f : α β) :
              (M.mapEmbedding f).Indep (f '' I)
              theorem Matroid.Base.mapEmbedding {α : Type u_1} {β : Type u_2} {M : Matroid α} {B : Set α} (hB : M.Base B) (f : α β) :
              (M.mapEmbedding f).Base (f '' B)
              theorem Matroid.Basis.mapEmbedding {α : Type u_1} {β : Type u_2} {I : Set α} {M : Matroid α} {X : Set α} (hIX : M.Basis I X) (f : α β) :
              (M.mapEmbedding f).Basis (f '' I) (f '' X)
              @[simp]
              theorem Matroid.mapEmbedding_base_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : α β} {B : Set β} :
              (M.mapEmbedding f).Base B M.Base (f ⁻¹' B) B Set.range f
              @[simp]
              theorem Matroid.mapEmbedding_basis_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : α β} {I : Set β} {X : Set β} :
              (M.mapEmbedding f).Basis I X M.Basis (f ⁻¹' I) (f ⁻¹' X) I X X Set.range f
              instance Matroid.instNonemptyMapEmbedding {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Nonempty] {f : α β} :
              (M.mapEmbedding f).Nonempty
              Equations
              • =
              instance Matroid.instFiniteMapEmbedding {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Finite] {f : α β} :
              (M.mapEmbedding f).Finite
              Equations
              • =
              instance Matroid.instFinitaryMapEmbedding {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Finitary] {f : α β} :
              (M.mapEmbedding f).Finitary
              Equations
              • =
              instance Matroid.instFiniteRkMapEmbedding {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.FiniteRk] {f : α β} :
              (M.mapEmbedding f).FiniteRk
              Equations
              • =
              instance Matroid.instRkPosMapEmbedding {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.RkPos] {f : α β} :
              (M.mapEmbedding f).RkPos
              Equations
              • =
              def Matroid.mapEquiv {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : α β) :

              Map M : Matroid α across an equivalence α ≃ β

              Equations
              • M.mapEquiv f = M.mapEmbedding f.toEmbedding
              Instances For
                @[simp]
                theorem Matroid.mapEquiv_ground_eq {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : α β) :
                (M.mapEquiv f).E = f '' M.E
                theorem Matroid.mapEquiv_eq_map {α : Type u_1} {β : Type u_2} {M : Matroid α} (f : α β) :
                M.mapEquiv f = M.map f
                @[simp]
                theorem Matroid.mapEquiv_indep_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : α β} {I : Set β} :
                (M.mapEquiv f).Indep I M.Indep (f.symm '' I)
                @[simp]
                theorem Matroid.mapEquiv_dep_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : α β} {D : Set β} :
                (M.mapEquiv f).Dep D M.Dep (f.symm '' D)
                @[simp]
                theorem Matroid.mapEquiv_base_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : α β} {B : Set β} :
                (M.mapEquiv f).Base B M.Base (f.symm '' B)
                @[simp]
                theorem Matroid.mapEquiv_basis_iff {α : Type u_3} {β : Type u_4} {M : Matroid α} (f : α β) {I : Set β} {X : Set β} :
                (M.mapEquiv f).Basis I X M.Basis (f.symm '' I) (f.symm '' X)
                instance Matroid.instNonemptyMapEquiv {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Nonempty] {f : α β} :
                (M.mapEquiv f).Nonempty
                Equations
                • =
                instance Matroid.instFiniteMapEquiv {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Finite] {f : α β} :
                (M.mapEquiv f).Finite
                Equations
                • =
                instance Matroid.instFinitaryMapEquiv {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Finitary] {f : α β} :
                (M.mapEquiv f).Finitary
                Equations
                • =
                instance Matroid.instFiniteRkMapEquiv {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.FiniteRk] {f : α β} :
                (M.mapEquiv f).FiniteRk
                Equations
                • =
                instance Matroid.instRkPosMapEquiv {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.RkPos] {f : α β} :
                (M.mapEquiv f).RkPos
                Equations
                • =
                def Matroid.restrictSubtype {α : Type u_1} (M : Matroid α) (X : Set α) :
                Matroid X

                Given M : Matroid α and X : Set α, the restriction of M to X, viewed as a matroid on type X with ground set univ. Always isomorphic to M ↾ X. If X = M.E, then isomorphic to M.

                Equations
                • M.restrictSubtype X = (M.restrict X).comap Subtype.val
                Instances For
                  @[simp]
                  theorem Matroid.restrictSubtype_ground {α : Type u_1} {X : Set α} {M : Matroid α} :
                  (M.restrictSubtype X).E = Set.univ
                  @[simp]
                  theorem Matroid.restrictSubtype_indep_iff {α : Type u_1} {X : Set α} {M : Matroid α} {I : Set X} :
                  (M.restrictSubtype X).Indep I M.Indep (Subtype.val '' I)
                  theorem Matroid.restrictSubtype_indep_iff_of_subset {α : Type u_1} {X : Set α} {I : Set α} {M : Matroid α} (hIX : I X) :
                  (M.restrictSubtype X).Indep (Subtype.val ⁻¹' I) M.Indep I
                  theorem Matroid.restrictSubtype_inter_indep_iff {α : Type u_1} {X : Set α} {I : Set α} {M : Matroid α} :
                  (M.restrictSubtype X).Indep (Subtype.val ⁻¹' I) M.Indep (X I)
                  theorem Matroid.restrictSubtype_basis_iff {α : Type u_1} {M : Matroid α} {Y : Set α} {I : Set Y} {X : Set Y} :
                  (M.restrictSubtype Y).Basis I X M.Basis' (Subtype.val '' I) (Subtype.val '' X)
                  theorem Matroid.restrictSubtype_base_iff {α : Type u_1} {X : Set α} {M : Matroid α} {B : Set X} :
                  (M.restrictSubtype X).Base B M.Basis' (Subtype.val '' B) X
                  @[simp]
                  theorem Matroid.restrictSubtype_ground_base_iff {α : Type u_1} {M : Matroid α} {B : Set M.E} :
                  (M.restrictSubtype M.E).Base B M.Base (Subtype.val '' B)
                  @[simp]
                  theorem Matroid.restrictSubtype_ground_basis_iff {α : Type u_1} {M : Matroid α} {I : Set M.E} {X : Set M.E} :
                  (M.restrictSubtype M.E).Basis I X M.Basis (Subtype.val '' I) (Subtype.val '' X)
                  theorem Matroid.eq_of_restrictSubtype_eq {α : Type u_1} {E : Set α} {M : Matroid α} {N : Matroid α} (hM : M.E = E) (hN : N.E = E) (h : M.restrictSubtype E = N.restrictSubtype E) :
                  M = N
                  @[simp]
                  theorem Matroid.restrictSubtype_dual {α : Type u_1} {M : Matroid α} :
                  (M.restrictSubtype M.E) = M.restrictSubtype M.E
                  theorem Matroid.restrictSubtype_dual' {α : Type u_1} {E : Set α} {M : Matroid α} (hM : M.E = E) :
                  (M.restrictSubtype E) = M.restrictSubtype E
                  @[simp]
                  theorem Matroid.map_val_restrictSubtype_eq {α : Type u_1} (M : Matroid α) (X : Set α) :
                  (M.restrictSubtype X).map Subtype.val = M.restrict X

                  M.restrictSubtype X is isomorphic to M ↾ X.

                  theorem Matroid.map_val_restrictSubtype_ground_eq {α : Type u_1} (M : Matroid α) :
                  (M.restrictSubtype M.E).map Subtype.val = M

                  M.restrictSubtype M.E is isomorphic to M.

                  instance Matroid.instFinitaryElemRestrictSubtype {α : Type u_1} {M : Matroid α} [M.Finitary] {X : Set α} :
                  (M.restrictSubtype X).Finitary
                  Equations
                  • =
                  instance Matroid.instFiniteRkElemRestrictSubtype {α : Type u_1} {M : Matroid α} [M.FiniteRk] {X : Set α} :
                  (M.restrictSubtype X).FiniteRk
                  Equations
                  • =
                  instance Matroid.instFiniteElemERestrictSubtype {α : Type u_1} {M : Matroid α} [M.Finite] :
                  (M.restrictSubtype M.E).Finite
                  Equations
                  • =
                  instance Matroid.instNonemptyElemERestrictSubtype {α : Type u_1} {M : Matroid α} [M.Nonempty] :
                  (M.restrictSubtype M.E).Nonempty
                  Equations
                  • =
                  instance Matroid.instRkPosElemERestrictSubtype {α : Type u_1} {M : Matroid α} [M.RkPos] :
                  (M.restrictSubtype M.E).RkPos
                  Equations
                  • =