structure Matroid.Iso {α : Type u_1} {β : Type u_2} (M : Matroid α) (N : Matroid β) : Type (max u_1 u_2)

An isomorphism between two matroids.

• toEquiv : ↑M.E ≃ ↑N.E
• indep_image_iff' (I : Set ↑M.E) : M.Indep (Subtype.val '' I) ↔ N.Indep (Subtype.val '' ⇑self.toEquiv '' I)

def Matroid.«term_≂_» : Lean.TrailingParserDescr

Equations

• Matroid.«term_≂_» = Lean.ParserDescr.trailingNode `Matroid.«term_≂_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≂ ") (Lean.ParserDescr.cat `term 66))

@[instance_reducible]

instance Matroid.instEquivLikeIsoElemE {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} : EquivLike (M ≂ N) ↑M.E ↑N.E

Equations

• Matroid.instEquivLikeIsoElemE = { coe := fun (f : M ≂ N) => ⇑f.toEquiv, inv := fun (f : M ≂ N) => ⇑f.toEquiv.symm, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

theorem Matroid.Iso.indep_image_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) {I : Set ↑M.E} : M.Indep (Subtype.val '' I) ↔ N.Indep (Subtype.val '' ⇑e '' I)

theorem Matroid.Iso.image_indep {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) {I : Set ↑M.E} (hI : M.Indep (Subtype.val '' I)) : N.Indep (Subtype.val '' ⇑e '' I)

theorem Matroid.Iso.dep_image_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) {D : Set ↑M.E} : M.Dep (Subtype.val '' D) ↔ N.Dep (Subtype.val '' ⇑e '' D)

theorem Matroid.Iso.image_dep {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) {D : Set ↑M.E} (hD : M.Dep (Subtype.val '' D)) : N.Dep (Subtype.val '' ⇑e '' D)

def Matroid.Iso.refl {α : Type u_1} {M : Matroid α} : M ≂ M

Equations

• Matroid.Iso.refl = { toEquiv := Equiv.refl ↑M.E, indep_image_iff' := ⋯ }

@[simp]

theorem Matroid.Iso.refl_toEquiv {α : Type u_1} {M : Matroid α} : refl.toEquiv = Equiv.refl ↑M.E

def Matroid.Iso.symm {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) : N ≂ M

Equations

• e.symm = { toEquiv := e.toEquiv.symm, indep_image_iff' := ⋯ }

@[simp]

theorem Matroid.Iso.symm_toEquiv {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) : e.symm.toEquiv = e.toEquiv.symm

@[simp]

theorem Matroid.Iso.apply_symm_apply {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) (x : ↑N.E) : e (e.symm x) = x

@[simp]

theorem Matroid.Iso.symm_apply_apply {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) (x : ↑M.E) : e.symm (e x) = x

theorem Matroid.Iso.symm_image_image {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) (X : Set ↑M.E) : ⇑e.symm '' ⇑e '' X = X

theorem Matroid.Iso.image_symm_image {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) (X : Set ↑N.E) : ⇑e '' ⇑e.symm '' X = X

@[simp]

theorem Matroid.Iso.image_symm_eq_preimage {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) (X : Set ↑N.E) : ⇑e.symm '' X = ⇑e ⁻¹' X

@[simp]

theorem Matroid.Iso.preimage_symm_eq_image {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) (X : Set ↑M.E) : ⇑e.symm ⁻¹' X = ⇑e '' X

@[simp]

theorem Matroid.Iso.preimage_image {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) (X : Set ↑M.E) : ⇑e ⁻¹' ⇑e '' X = X

@[simp]

theorem Matroid.Iso.image_preimage {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) (X : Set ↑N.E) : ⇑e '' ⇑e ⁻¹' X = X

@[simp]

theorem Matroid.Iso.preimage_subset_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) {X : Set ↑N.E} {Y : Set ↑M.E} : ⇑e ⁻¹' X ⊆ Y ↔ X ⊆ ⇑e '' Y

@[simp]

theorem Matroid.Iso.range_eq {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) : Set.range ⇑e = Set.univ

def Matroid.Iso.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Matroid α} {N : Matroid β} {R : Matroid γ} (e : M ≂ N) (f : N ≂ R) : M ≂ R

Equations

• e.trans f = { toEquiv := (↑e).trans ↑f, indep_image_iff' := ⋯ }

@[simp]

theorem Matroid.Iso.trans_toEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Matroid α} {N : Matroid β} {R : Matroid γ} (e : M ≂ N) (f : N ≂ R) : (e.trans f).toEquiv = (↑e).trans ↑f

def Matroid.Iso.ofEq {α : Type u_1} {M N : Matroid α} (hMN : M = N) : M ≂ N

Equations

• Matroid.Iso.ofEq hMN = { toEquiv := Set.equivOfEq ⋯, indep_image_iff' := ⋯ }

@[simp]

theorem Matroid.Iso.ofEq_toEquiv {α : Type u_1} {M N : Matroid α} (hMN : M = N) : (ofEq hMN).toEquiv = Set.equivOfEq ⋯

def Matroid.Iso.ofForallDep {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : ↑M.E ≃ ↑N.E) (he : ∀ (D : Set ↑M.E), M.Dep (Subtype.val '' D) ↔ N.Dep (Subtype.val '' ⇑e '' D)) : M ≂ N

Equations

• Matroid.Iso.ofForallDep e he = { toEquiv := e, indep_image_iff' := ⋯ }

@[simp]

theorem Matroid.Iso.ofForallDep_toEquiv {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : ↑M.E ≃ ↑N.E) (he : ∀ (D : Set ↑M.E), M.Dep (Subtype.val '' D) ↔ N.Dep (Subtype.val '' ⇑e '' D)) : (ofForallDep e he).toEquiv = e

def Matroid.Iso.ofForallBase {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : ↑M.E ≃ ↑N.E) (he : ∀ (B : Set ↑M.E), M.IsBase (Subtype.val '' B) ↔ N.IsBase (Subtype.val '' ⇑e '' B)) : M ≂ N

Equations

• Matroid.Iso.ofForallBase e he = { toEquiv := e, indep_image_iff' := ⋯ }

@[simp]

theorem Matroid.Iso.ofForallBase_toEquiv {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : ↑M.E ≃ ↑N.E) (he : ∀ (B : Set ↑M.E), M.IsBase (Subtype.val '' B) ↔ N.IsBase (Subtype.val '' ⇑e '' B)) : (ofForallBase e he).toEquiv = e

theorem Matroid.Iso.isBase_image {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) {B : Set ↑M.E} (hB : M.IsBase (Subtype.val '' B)) : N.IsBase (Subtype.val '' ⇑e '' B)

theorem Matroid.Iso.isBase_image_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) {B : Set ↑M.E} : M.IsBase (Subtype.val '' B) ↔ N.IsBase (Subtype.val '' ⇑e '' B)

theorem Matroid.Iso.nonempty_right {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) [M.Nonempty] : N.Nonempty

theorem Matroid.Iso.right_eq_empty {α : Type u_1} {β : Type u_2} {N : Matroid β} (e : emptyOn α ≂ N) : N = emptyOn β

def Matroid.empty_iso_empty (α : Type u_3) (β : Type u_4) : emptyOn α ≂ emptyOn β

Equations

• Matroid.empty_iso_empty α β = { toEquiv := Equiv.equivOfIsEmpty ↑(Matroid.emptyOn α).E ↑(Matroid.emptyOn β).E, indep_image_iff' := ⋯ }

theorem Matroid.Iso.isBasis_image_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) {I X : Set ↑M.E} : M.IsBasis (Subtype.val '' I) (Subtype.val '' X) ↔ N.IsBasis (Subtype.val '' ⇑e '' I) (Subtype.val '' ⇑e '' X)

noncomputable def Matroid.isoMap {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : α → β) (hf : Set.InjOn f M.E) : M ≂ M.map f hf

Equations

• M.isoMap f hf = { toEquiv := Equiv.Set.imageOfInjOn f M.E hf, indep_image_iff' := ⋯ }

@[simp]

theorem Matroid.isoMap_toEquiv {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : α → β) (hf : Set.InjOn f M.E) : (M.isoMap f hf).toEquiv = Equiv.Set.imageOfInjOn f M.E hf

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

Equations

• M.isoMapEquiv f = { toEquiv := Equiv.Set.image (⇑f) M.E ⋯, indep_image_iff' := ⋯ }

@[simp]

theorem Matroid.isoMapEquiv_toEquiv {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : α ≃ β) : (M.isoMapEquiv f).toEquiv = Equiv.Set.image (⇑f) M.E ⋯

noncomputable def Matroid.isoComapOn {α : Type u_1} {β : Type u_2} (M : Matroid β) (f : α → β) {E : Set α} (hf : Set.BijOn f E M.E) : M.comapOn E f ≂ M

Equations

• M.isoComapOn f hf = { toEquiv := Set.BijOn.equiv f hf, indep_image_iff' := ⋯ }

noncomputable def Matroid.isoComap {α : Type u_1} {β : Type u_2} (M : Matroid β) (f : α → β) (hf : Set.BijOn f (f ⁻¹' M.E) M.E) : M.comap f ≂ M

Equations

• M.isoComap f hf = (Matroid.Iso.ofEq ⋯).trans (M.isoComapOn f hf)

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

Equations

• M.isoMapSetEmbedding f = { toEquiv := Equiv.ofInjective ⇑f ⋯, indep_image_iff' := ⋯ }

theorem Matroid.Iso.exists_eq_map {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) [Nonempty (α → β)] : ∃ (f : α → β) (h : Set.InjOn f M.E), N = M.map f h

If M and N are isomorphic and α → β is nonempty, then N is a map of M. Useful for getting out of subtype hell.

theorem Matroid.Iso.exists_eq_map' {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) [M.Nonempty] : ∃ (f : α → β) (hf : Set.InjOn f M.E), N = M.map f hf

theorem Matroid.Iso.empty_empty_or_exists_eq_map {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) : M = emptyOn α ∧ N = emptyOn β ∨ ∃ (f : α → β) (hf : Set.InjOn f M.E), N = M.map f hf

theorem Matroid.Finite.of_iso {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (hM : M.Finite) (e : M ≂ N) : N.Finite

theorem Matroid.Finitary.of_iso {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (hM : M.Finitary) (e : M ≂ N) : N.Finitary

theorem Matroid.Iso.finite_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) : M.Finite ↔ N.Finite

theorem Matroid.Iso.finitary_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) : M.Finitary ↔ N.Finitary

theorem Matroid.nonempty_iso_comm {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} : Nonempty (M ≂ N) ↔ Nonempty (N ≂ M)

def Matroid.Iso.dual {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) : M✶ ≂ N✶

Equations

• e.dual = Matroid.Iso.ofForallBase (((Set.equivOfEq ⋯).trans ↑e).trans (Set.equivOfEq ⋯)) ⋯

@[simp]

theorem Matroid.Iso.dual_image {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) (X : Set α) : Subtype.val '' ⇑e.dual '' Subtype.val ⁻¹' X = Subtype.val '' ⇑e '' Subtype.val ⁻¹' X

@[simp]

theorem Matroid.Iso.dual_image' {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) (X : Set ↑M.E) : ⇑e.dual '' X = ⇑e '' X

@[simp]

theorem Matroid.Iso.dual_image'' {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) (X : Set ↑M✶.E) : ⇑e.dual '' X = ⇑e '' X

@[simp]

theorem Matroid.Iso.dual_apply {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) (x : ↑M.E) : e.dual x = e x

@[simp]

theorem Matroid.Iso.dual_apply' {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) (x : ↑M✶.E) : e.dual x = e x

def Matroid.Iso.dual_comm {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N✶) : M✶ ≂ N

Equations

• e.dual_comm = e.dual.trans (Matroid.Iso.ofEq ⋯)

def Matroid.Iso.restrict {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) {R : Set α} {S : Set β} (hR : R ⊆ M.E) (hS : S ⊆ N.E) (hRS : ∀ (x : ↑M.E), ↑(e x) ∈ S ↔ ↑x ∈ R) : M.restrict R ≂ N.restrict S

Equations

• e.restrict hR hS hRS = { toEquiv := (↑e).subsetEquivSubset hR hS hRS, indep_image_iff' := ⋯ }

def Matroid.isoOfForallImageclosure {α : Type u_1} {M : Matroid α} {β : Type u_3} {N : Matroid β} (e : ↑M.E ≃ ↑N.E) (h : ∀ (X : Set ↑M.E), N.closure (Subtype.val '' ⇑e '' X) = Subtype.val '' ⇑e '' Subtype.val ⁻¹' M.closure (Subtype.val '' X)) : M ≂ N

If an equivalence between M.E and N.E respects the closure function, it is an isomorphism

Equations

• Matroid.isoOfForallImageclosure e h = { toEquiv := e, indep_image_iff' := ⋯ }

@[simp]

theorem Matroid.isoOfForallImageclosure_apply {α : Type u_1} {M : Matroid α} {β : Type u_3} {N : Matroid β} (e : ↑M.E ≃ ↑N.E) (h : ∀ (X : Set ↑M.E), N.closure (Subtype.val '' ⇑e '' X) = Subtype.val '' ⇑e '' Subtype.val ⁻¹' M.closure (Subtype.val '' X)) (x : ↑M.E) : (isoOfForallImageclosure e h) x = e x

theorem Matroid.Iso.isCircuit_image {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : M ≂ N) {C : Set ↑M.E} (hC : M.IsCircuit (Subtype.val '' C)) : N.IsCircuit (Subtype.val '' ⇑e '' C)

def Matroid.Iso.ofForallIsCircuit {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (e : ↑M.E ≃ ↑N.E) (h : ∀ (C : Set ↑M.E), M.IsCircuit (Subtype.val '' C) ↔ N.IsCircuit (Subtype.val '' ⇑e '' C)) : M ≂ N

Equations

• Matroid.Iso.ofForallIsCircuit e h = Matroid.Iso.ofForallDep e ⋯

theorem Matroid.Iso.eRank_eq {α : Type u_1} {M : Matroid α} {β : Type u_3} {N : Matroid β} (e : M ≂ N) : M.eRank = N.eRank

theorem Matroid.Iso.rank_eq {α : Type u_1} {M : Matroid α} {β : Type u_3} {N : Matroid β} (e : M ≂ N) : M.rank = N.rank

theorem Matroid.exists_iso_onUniv {α : Type u} (M : Matroid α) : ∃ (β : Type u) (N : Matroid β), N.OnUniv ∧ Nonempty (M ≂ N)

Every matroid is isomorphic to an OnUniv matroid.

theorem Matroid.Iso.spanning_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {N : Matroid β} (i : M ≂ N) (X : Set ↑M.E) : M.Spanning (Subtype.val '' X) ↔ N.Spanning (Subtype.val '' ⇑i '' X)