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.

• For f : α → β, Matroid.comap N f is the matroid on α with ground set f ⁻¹' N.E in which each I is independent if and only if f is injective on I and f '' I is independent in N. (For each nonloop x of N, the set f ⁻¹' {x} is a parallel class of N.comap f)

• Matroid.comapOn N f E is the restriction of N.comap f to E for some E : Set α.

• For an embedding f : M.E ↪ β defined on the subtype ↑M.E, Matroid.mapSetEmbedding M f is the matroid on β with ground set range f whose independent sets are the images of those in M. This matroid is isomorphic to M.

• For a function f : α → β and a proof hf that f is injective on M.E, Matroid.map f hf is the matroid on β with ground set f '' M.E whose independent sets are the images of those in M. This matroid is isomorphic to M, and does not depend on the values f takes outside M.E.

• Matroid.mapEmbedding f is a version of Matroid.map where f : α ↪ β is a bundled embedding. It is defined separately because the global injectivity of f gives some nicer simp lemmas.

• Matroid.mapEquiv f is a version of Matroid.map where f : α ≃ β is a bundled equivalence. It is defined separately because we get even nicer simp lemmas.

• Matroid.mapSetEquiv f is a version of Matroid.map where f : M.E ≃ E is an equivalence on subtypes. It gives a matroid on β with ground set E.

• For X : Set α, Matroid.restrictSubtype M X is the Matroid X with ground set univ : Set X that is isomorphic to M ↾ X.

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 [Per69] in which a matroid structure can be transported across an arbitrary bipartite graph that may not correspond to a function at all (See [Oxl11], 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 [AHCF12]. For this reason, Matroid.map requires injectivity to be well-defined in general.

TODO

• Bundled matroid isomorphisms.
• Maps of finite matroids across bipartite graphs.

References

• E. Aigner-Horev, J. Carmesin, J. Fröhlic, Infinite Matroid Union
• H. Perfect, Independence Spaces and Combinatorial Problems
• J. Oxley, Matroid Theory

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

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.

@[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 : α → β) : (Matroid.emptyOn β).comap f = Matroid.emptyOn α

@[simp]

theorem Matroid.comap_loopyOn {α : Type u_1} {β : Type u_2} (f : α → β) (E : Set β) : (Matroid.loopyOn E).comap f = Matroid.loopyOn (f ⁻¹' E)

@[simp]

theorem Matroid.comap_basis_iff {α : Type u_1} {β : Type u_2} {f : α → β} {N : Matroid β} {I 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 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

instance Matroid.comap_finiteRk {α : Type u_1} {β : Type u_2} (N : Matroid β) [N.FiniteRk] (f : α → β) : (N.comap f).FiniteRk

def Matroid.comapOn {α : Type u_1} {β : Type u_2} (N : Matroid β) (E : Set α) (f : α → β) : Matroid α

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

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 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 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 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 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

instance Matroid.comapOn_finiteRk {α : Type u_1} {β : Type u_2} {f : α → β} {N : Matroid β} {E : Set α} [N.FiniteRk] : (N.comapOn E f).FiniteRk

def Matroid.mapSetEmbedding {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : ↑M.E ↪ β) : Matroid β

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

Equations

• M.mapSetEmbedding f = Matroid.ofExistsMatroid (Set.range ⇑f) (fun (I : Set β) => M.Indep (Subtype.val '' (⇑f ⁻¹' I)) ∧ I ⊆ Set.range ⇑f) ⋯

@[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) : Matroid β

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

• M.map f hf = Matroid.ofExistsMatroid (f '' M.E) (fun (I : Set β) => ∃ (I₀ : Set α), M.Indep I₀ ∧ I = f '' I₀) ⋯

@[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 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 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 : α → β) : (Matroid.emptyOn α).map f ⋯ = Matroid.emptyOn β

@[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

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

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

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

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

def Matroid.mapSetEquiv {α : Type u_1} {β : Type u_2} (M : Matroid α) {E : Set β} (e : ↑M.E ≃ ↑E) : Matroid β

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

Equations

• M.mapSetEquiv e = Matroid.ofExistsMatroid E (fun (I : Set β) => M.Indep (Subtype.val '' (⇑e.symm '' (Subtype.val ⁻¹' I))) ∧ I ⊆ E) ⋯

@[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 : α ↪ β) : Matroid β

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

Equations

• M.mapEmbedding f = M.map ⇑f ⋯

@[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 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

instance Matroid.instFiniteMapEmbedding {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Finite] {f : α ↪ β} : (M.mapEmbedding f).Finite

instance Matroid.instFinitaryMapEmbedding {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Finitary] {f : α ↪ β} : (M.mapEmbedding f).Finitary

instance Matroid.instFiniteRkMapEmbedding {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.FiniteRk] {f : α ↪ β} : (M.mapEmbedding f).FiniteRk

instance Matroid.instRkPosMapEmbedding {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.RkPos] {f : α ↪ β} : (M.mapEmbedding f).RkPos

def Matroid.mapEquiv {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : α ≃ β) : Matroid β

Map M : Matroid α across an equivalence α ≃ β

Equations

• M.mapEquiv f = M.mapEmbedding f.toEmbedding

@[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 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

instance Matroid.instFiniteMapEquiv {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Finite] {f : α ≃ β} : (M.mapEquiv f).Finite

instance Matroid.instFinitaryMapEquiv {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.Finitary] {f : α ≃ β} : (M.mapEquiv f).Finitary

instance Matroid.instFiniteRkMapEquiv {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.FiniteRk] {f : α ≃ β} : (M.mapEquiv f).FiniteRk

instance Matroid.instRkPosMapEquiv {α : Type u_1} {β : Type u_2} {M : Matroid α} [M.RkPos] {f : α ≃ β} : (M.mapEquiv f).RkPos

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

@[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 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 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 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 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 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

instance Matroid.instFiniteRkElemRestrictSubtype {α : Type u_1} {M : Matroid α} [M.FiniteRk] {X : Set α} : (M.restrictSubtype X).FiniteRk

instance Matroid.instFiniteElemERestrictSubtype {α : Type u_1} {M : Matroid α} [M.Finite] : (M.restrictSubtype M.E).Finite

instance Matroid.instNonemptyElemERestrictSubtype {α : Type u_1} {M : Matroid α} [M.Nonempty] : (M.restrictSubtype M.E).Nonempty

instance Matroid.instRkPosElemERestrictSubtype {α : Type u_1} {M : Matroid α} [M.RkPos] : (M.restrictSubtype M.E).RkPos