class Matroid.Simple {α : Type u_1} (M : Matroid α) : Prop

A matroid is Simple if it has no loops or nontrivial parallel pairs.

• parallel_iff_eq {e f : α} : e ∈ M.E → (M.Parallel e f ↔ e = f)

theorem Matroid.Parallel.eq {α : Type u_1} {M : Matroid α} {e f : α} [M.Simple] (h : M.Parallel e f) : e = f

theorem Matroid.parallel_iff_eq {α : Type u_1} {M : Matroid α} {e f : α} [M.Simple] (he : e ∈ M.E := by aesop_mat) : M.Parallel e f ↔ e = f

theorem Matroid.not_parallel_of_ne {α : Type u_1} {e f : α} (M : Matroid α) [M.Simple] (hef : e ≠ f) : ¬M.Parallel e f

instance Matroid.instLooplessOfSimple {α : Type u_1} {M : Matroid α} [M.Simple] : M.Loopless

instance Matroid.instSimpleEmptyOn {α : Type u_2} : (emptyOn α).Simple

instance Matroid.simple_dual_dual {α : Type u_1} {M : Matroid α} [M.Simple] : M✶✶.Simple

theorem Matroid.Simple.loopless {α : Type u_1} {M : Matroid α} (hM : M.Simple) : M.Loopless

theorem Matroid.Simple.isNonloop_of_mem {α : Type u_1} {M : Matroid α} {e : α} : M.Simple → ∀ (he : e ∈ M.E), M.IsNonloop e

theorem Matroid.Parallel'.eq {α : Type u_1} {M : Matroid α} {e f : α} [M.Simple] (h : M.Parallel' e f) : e = f

theorem Matroid.simple_iff_loopless_eq_of_parallel_forall {α : Type u_1} {M : Matroid α} : M.Simple ↔ M.Loopless ∧ ∀ (e f : α), M.Parallel e f → e = f

theorem Matroid.parallel_class_eq {α : Type u_1} {M : Matroid α} {e : α} [M.Simple] (he : e ∈ M.E := by aesop_mat) : {f : α | M.Parallel e f} = {e}

@[simp]

theorem Matroid.closure_singleton_eq {α : Type u_1} {M : Matroid α} {e : α} [M.Simple] (he : e ∈ M.E := by aesop_mat) : M.closure {e} = {e}

theorem Matroid.simple_iff_closure_subset_self_forall {α : Type u_1} {M : Matroid α} [M.RankPos] : M.Simple ↔ ∀ (e : α), M.IsNonloop e → M.closure {e} ⊆ {e}

We need RankPos or something similar here, since otherwise the matroid whose only element is a loop is a counterexample.

theorem Matroid.closure_eq_self_of_subset_singleton {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} [M.Simple] (he : e ∈ M.E) (hX : X ⊆ {e}) : M.closure X = X

theorem Matroid.singleton_isFlat {α : Type u_1} {M : Matroid α} {e : α} [M.Simple] (he : e ∈ M.E := by aesop_mat) : M.IsFlat {e}

theorem Matroid.pair_indep {α : Type u_1} {M : Matroid α} {e f : α} [M.Simple] (he : e ∈ M.E := by aesop_mat) (hf : f ∈ M.E := by aesop_mat) : M.Indep {e, f}

theorem Matroid.pair_closure_isLine {α : Type u_1} {M : Matroid α} {e f : α} [M.Simple] (hne : e ≠ f) (he : e ∈ M.E := by aesop_mat) (hf : f ∈ M.E := by aesop_mat) : M.IsLine (M.closure {e, f})

theorem Matroid.indep_of_encard_le_two {α : Type u_1} {M : Matroid α} {I : Set α} [M.Simple] (h : I.encard ≤ 2) (hI : I ⊆ M.E := by aesop_mat) : M.Indep I

theorem Matroid.eRk_pair_eq {α : Type u_1} {M : Matroid α} {e f : α} [M.Simple] (hef : e ≠ f) (he : e ∈ M.E := by aesop_mat) (hf : f ∈ M.E := by aesop_mat) : M.eRk {e, f} = 2

theorem Matroid.Dep.two_lt_encard {α : Type u_1} {M : Matroid α} {D : Set α} [M.Simple] (hD : M.Dep D) : 2 < D.encard

theorem Matroid.three_le_girth_iff {α : Type u_1} {M : Matroid α} : 3 ≤ M.girth ↔ M.Simple

theorem Matroid.three_le_girth {α : Type u_1} (M : Matroid α) [M.Simple] : 3 ≤ M.girth

theorem Matroid.two_lt_girth {α : Type u_1} (M : Matroid α) [M.Simple] : 2 < M.girth

theorem Matroid.Simple.three_le_girth {α : Type u_1} {M : Matroid α} (hM : M.Simple) : 3 ≤ M.girth

theorem Matroid.simple_iff_forall_isCircuit {α : Type u_1} {M : Matroid α} : M.Simple ↔ ∀ (C : Set α), M.IsCircuit C → 2 < C.encard

theorem Matroid.simple_iff_forall_pair_indep {α : Type u_1} {M : Matroid α} : M.Simple ↔ ∀ ⦃e f : α⦄, e ∈ M.E → f ∈ M.E → M.Indep {e, f}

@[simp]

theorem Matroid.simple_uniqueBaseOn_iff {α : Type u_1} {I E : Set α} : (uniqueBaseOn I E).Simple ↔ E ⊆ I

instance Matroid.simple_freeOn {α : Type u_1} {E : Set α} : (freeOn E).Simple

instance Matroid.simple_emptyOn {α : Type u_2} : (emptyOn α).Simple

theorem Matroid.Simple.map {α : Type u_1} {M : Matroid α} {β : Type u_2} (hM : M.Simple) {f : α → β} (hf : Set.InjOn f M.E) : (M.map f hf).Simple

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

theorem Matroid.Simple.delete {α : Type u_1} {M : Matroid α} (hM : M.Simple) (D : Set α) : (M.delete D).Simple

instance Matroid.simple_delete {α : Type u_1} {M : Matroid α} [M.Simple] (D : Set α) : (M.delete D).Simple

theorem Matroid.Simple.contractElem_loopless {α : Type u_1} {M : Matroid α} (hM : M.Simple) (e : α) : (M.contract {e}).Loopless

instance Matroid.contractElem_loopless {α : Type u_1} {M : Matroid α} [M.Simple] (e : α) : (M.contract {e}).Loopless

theorem Matroid.simple_iff_forall_parallel_class {α : Type u_1} {M : Matroid α} [M.Loopless] : M.Simple ↔ ∀ P ∈ M.parallelClasses, P.encard = 1

theorem Matroid.simple_iff_parallelClasses_eq_discrete' {α : Type u_1} {M : Matroid α} : M.Simple ↔ M.Loopless ∧ M.parallelClasses = Partition.discrete {e : α | M.IsNonloop e}

theorem Matroid.simple_iff_parallelClasses_eq_discrete {α : Type u_1} {M : Matroid α} [M.Loopless] : M.Simple ↔ M.parallelClasses = Partition.discrete {e : α | M.IsNonloop e}

theorem Matroid.parallelClasses_eq_discrete {α : Type u_1} {M : Matroid α} [M.Simple] : M.parallelClasses = Partition.discrete {e : α | M.IsNonloop e}

theorem Matroid.Simple.eq_of_parallel_of_mem {α : Type u_1} {M : Matroid α} {e f : α} {X : Set α} (h : (M.restrict X).Simple) (he : e ∈ X) (hf : f ∈ X) (hef : M.Parallel e f) : e = f

theorem Matroid.exists_isLoop_or_para_of_not_simple {α : Type u_1} {M : Matroid α} (hM : ¬M.Simple) : (∃ (e : α), M.IsLoop e) ∨ ∃ (e : α) (f : α), M.Parallel e f ∧ e ≠ f

theorem Matroid.Indep.restr_simple {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : (M.restrict I).Simple

theorem Matroid.Simple.subset_isNonloops {α : Type u_1} {M : Matroid α} {X : Set α} : (M.restrict X).Simple → X ⊆ {e : α | M.IsNonloop e}

theorem Matroid.Simple.repFun_injOn {α : Type u_1} {M : Matroid α} {X : Set α} (h : (M.restrict X).Simple) (f : M.parallelClasses.RepFun) : Set.InjOn (⇑f) X

theorem Matroid.Simple.subset_ground {α : Type u_1} {M : Matroid α} {X : Set α} (h : (M.restrict X).Simple) : X ⊆ M.E

theorem Matroid.Simple.subset {α : Type u_1} {M : Matroid α} {X Y : Set α} (hY : (M.restrict Y).Simple) (hXY : X ⊆ Y) : (M.restrict X).Simple

theorem Matroid.Loopless.of_restrict_contract {α : Type u_1} {M : Matroid α} {C : Set α} (hC : (M.restrict C).Loopless) (h : (M.contract C).Loopless) : M.Loopless

theorem Matroid.Simple.of_restrict_contract {α : Type u_1} {M : Matroid α} {C : Set α} (hC : (M.restrict C).Simple) (h : (M.contract C).Simple) : M.Simple

theorem Matroid.Indep.simple_of_contract_simple {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (h : (M.contract I).Simple) : M.Simple

@[simp]

theorem Matroid.simple_loopyOn_iff {α : Type u_1} {E : Set α} : (loopyOn E).Simple ↔ E = ∅

structure Matroid.Simplifies {α : Type u_1} (N M : Matroid α) : Prop

N simplifies M if N is a restriction of M, and every nonloop of M is parallel to an element of M. Equivalently, N is a restriction of M that has some simplification of M as a restriction.

• isRestriction : N.IsRestriction M
• exists_of_isNonloop ⦃e : α⦄ : M.IsNonloop e → ∃ f ∈ N.E, M.Parallel e f

theorem Matroid.simplifies_iff {α : Type u_1} (N M : Matroid α) : N.Simplifies M ↔ N.IsRestriction M ∧ ∀ ⦃e : α⦄, M.IsNonloop e → ∃ f ∈ N.E, M.Parallel e f

def Matroid.«term_≤si_» : Lean.TrailingParserDescr

Equations

• Matroid.«term_≤si_» = Lean.ParserDescr.trailingNode `Matroid.«term_≤si_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤si ") (Lean.ParserDescr.cat `term 51))

theorem Matroid.Simplifies.refl {α : Type u_1} {M : Matroid α} : M.Simplifies M

theorem Matroid.Simplifies.trans {α : Type u_1} {M N R : Matroid α} (hNM : N.Simplifies M) (hMR : M.Simplifies R) : N.Simplifies R

theorem Matroid.Simplifies.antisymm {α : Type u_1} {M N : Matroid α} (hNM : N.Simplifies M) (hMN : M.Simplifies N) : N = M

theorem Matroid.Simplifies.exists_imp_eq_of_isNonloop {α : Type u_1} {M N : Matroid α} {e : α} (h : N.Simplifies M) (he : M.IsNonloop e) : ∃ f ∈ N.E, M.Parallel e f ∧ (e ∈ N.E → f = e)

theorem Matroid.Simplifies.exists_mem_closure {α : Type u_1} {M N : Matroid α} {e : α} [N.Nonempty] (hM : N.Simplifies M) (he : e ∈ M.E) : ∃ f ∈ N.E, e ∈ M.closure {f}

theorem Matroid.Simplifies.exists_mem_closure_subsingleton {α : Type u_1} {M N : Matroid α} {e : α} (hM : N.Simplifies M) (he : e ∈ M.E) : ∃ X ⊆ N.E, X.Subsingleton ∧ e ∈ M.closure X

theorem Matroid.Simplifies.isSpanningRestriction {α : Type u_1} {M N : Matroid α} (h : N.Simplifies M) : N.IsSpanningRestriction M

theorem Matroid.Simplifies.simplifies_of_isRestriction {α : Type u_1} {M N R : Matroid α} (h : N.Simplifies M) (hNR : N.IsRestriction R) (hRM : R.IsRestriction M) : N.Simplifies R

theorem Matroid.Simplifies.simplifies_of_isRestriction_right {α : Type u_1} {M N R : Matroid α} (h : N.Simplifies M) (hNR : N.IsRestriction R) (hRM : R.IsRestriction M) : R.Simplifies M

theorem Matroid.delete_simplifies_of_subset_loops {α : Type u_1} {M : Matroid α} {X : Set α} (h : X ⊆ M.loops) : (M.delete X).Simplifies M

theorem Matroid.removeLoops_simplifies {α : Type u_1} (M : Matroid α) : M.removeLoops.Simplifies M

theorem Matroid.IsLoop.delete_simplifies {α : Type u_1} {M : Matroid α} {e : α} (h : M.IsLoop e) : (M.delete {e}).Simplifies M

theorem Matroid.Parallel.delete_left_simplifies {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel e f) (hne : e ≠ f) : (M.delete {e}).Simplifies M

theorem Matroid.Parallel.delete_right_simplifies {α : Type u_1} {M : Matroid α} {e f : α} (h : M.Parallel e f) (hne : e ≠ f) : (M.delete {f}).Simplifies M

theorem Matroid.Simple.eq_of_simplifies {α : Type u_1} {M N : Matroid α} (h : M.Simple) (hNM : N.Simplifies M) : N = M

@[simp]

theorem Matroid.simplifies_iff_eq {α : Type u_1} {M N : Matroid α} [M.Simple] : N.Simplifies M ↔ N = M

theorem Matroid.Simple.simplifies_iff_eq {α : Type u_1} {M N : Matroid α} (h : M.Simple) : N.Simplifies M ↔ N = M

theorem Matroid.Simplifies.contract {α : Type u_1} {M N : Matroid α} {C : Set α} (h : N.Simplifies M) (hC : C ⊆ N.E) : (N.contract C).Simplifies (M.contract C)

theorem Matroid.Simplifies.eRank_eq {α : Type u_1} {M N : Matroid α} (h : N.Simplifies M) : N.eRank = M.eRank

@[simp]

theorem Matroid.loopyOn_simplifies_iff {α : Type u_1} {M : Matroid α} {X : Set α} : (loopyOn X).Simplifies M ↔ X ⊆ M.E ∧ M.eRank = 0

@[simp]

theorem Matroid.emptyOn_simplifies_iff {α : Type u_1} {M : Matroid α} : (emptyOn α).Simplifies M ↔ M.eRank = 0

@[simp]

theorem Matroid.removeLoops_eRank_eq {α : Type u_1} (M : Matroid α) : M.removeLoops.eRank = M.eRank

theorem Matroid.Simplifies.exists_eq_delete {α : Type u_1} {M N : Matroid α} (h : N.Simplifies M) : ∃ (D : Set α), N = M.delete D ∧ M.Coindep D ∧ ∀ (e : α), M.IsNonloop e → ∃ f ∉ D, M.Parallel e f

theorem Matroid.delete_simplifies_iff {α : Type u_1} {M : Matroid α} {D : Set α} : (M.delete D).Simplifies M ↔ ∀ e ∈ D, M.IsNonloop e → ∃ f ∉ D, M.Parallel e f

theorem Matroid.Simplifies.exists_eq_comapOn {α : Type u_1} {M N : Matroid α} (h : N.Simplifies M) : ∃ (φ : α → α), M = N.comapOn M.E φ ∧ Set.EqOn id φ N.E ∧ Set.EqOn id φ {e : α | ¬M.IsNonloop e} ∧ φ '' {e : α | M.IsNonloop e} = {e : α | N.IsNonloop e} ∧ ∀ (e : α), φ (φ e) = φ e

If N simplifies M, then M is a comap of N under some function that is the identity outside the nonloops of M, is the identity on N, and maps the nonloops of M to the nonloops of M.

theorem Matroid.Simplifies.exists_eq_comap {α : Type u_1} {M N : Matroid α} [M.Loopless] (h : N.Simplifies M) : ∃ (φ : α → α), M = N.comap φ ∧ Set.EqOn id φ N.E ∧ φ '' M.E = N.E ∧ φ ⁻¹' N.E = M.E ∧ ∀ (e : α), φ (φ e) = φ e

theorem Matroid.Simplifies.simplifies_right_iff_of_subset {α : Type u_1} {M N M₀ : Matroid α} (h : N.Simplifies M) (hM₀ : M₀.E ⊆ N.E) : M₀.Simplifies N ↔ M₀.Simplifies M

def Matroid.IsSimplification {α : Type u_1} (N M : Matroid α) : Prop

N.IsSimplification M means that N is obtained from M by deleting all loops and all but one element from each parallel class.

Equations

• N.IsSimplification M = ∃ (f : M.parallelClasses.RepFun), N = M.restrict (⇑f '' {e : α | M.IsNonloop e})

noncomputable def Matroid.IsSimplification.repFun {α : Type u_1} {M N : Matroid α} (h : N.IsSimplification M) : M.parallelClasses.RepFun

Each simplification of M corresponds to a function that picks a representative from each parallel class. Even though the choice is unique, this is noncomputable.

Equations

• h.repFun = Exists.choose h

@[simp]

theorem Matroid.IsSimplification.image_restrict_repFun {α : Type u_1} {M N : Matroid α} (h : N.IsSimplification M) : M.restrict (⇑h.repFun '' {e : α | M.IsNonloop e}) = N

theorem Matroid.IsSimplification.ground_eq_image_repFun {α : Type u_1} {M N : Matroid α} (h : N.IsSimplification M) : N.E = ⇑h.repFun '' {e : α | M.IsNonloop e}

theorem Matroid.IsSimplification.parallel_repFun {α : Type u_1} {M N : Matroid α} {e : α} (h : N.IsSimplification M) (he : M.IsNonloop e) : M.Parallel e (h.repFun e)

theorem Matroid.IsSimplification.repFun_apply_mem_ground {α : Type u_1} {M N : Matroid α} {e : α} (h : N.IsSimplification M) (he : M.IsNonloop e) : h.repFun e ∈ N.E

theorem Matroid.IsSimplification.simple {α : Type u_1} {M N : Matroid α} (h : N.IsSimplification M) : N.Simple

theorem Matroid.Simple.exists_subset_isSimplification {α : Type u_1} {M : Matroid α} {X : Set α} (hX : (M.restrict X).Simple) : ∃ (N : Matroid α), N.IsSimplification M ∧ X ⊆ N.E

theorem Matroid.IsSimplification.isRestriction {α : Type u_1} {M N : Matroid α} (h : N.IsSimplification M) : N.IsRestriction M

theorem Matroid.Simple.exists_isRestriction_isSimplification_of_isRestriction {α : Type u_1} {M N : Matroid α} (hN : N.Simple) (h : N.IsRestriction M) : ∃ (M' : Matroid α), M'.IsSimplification M ∧ N.IsRestriction M'

theorem Matroid.IsSimplification.repFun_injOn {α : Type u_1} {M N : Matroid α} (h : N.IsSimplification M) : Set.InjOn (⇑h.repFun) N.E

theorem Matroid.IsSimplification.eq_self_iff {α : Type u_1} {M N : Matroid α} (h : N.IsSimplification M) : N = M ↔ M.Simple

theorem Matroid.IsSimplification.isNonloop_of_mem {α : Type u_1} {M N : Matroid α} {e : α} (h : N.IsSimplification M) (heN : e ∈ N.E) : M.IsNonloop e

theorem Matroid.IsSimplification.exists_unique {α : Type u_1} {M N : Matroid α} {e : α} (h : N.IsSimplification M) (he : M.IsNonloop e) : ∃! f : α, f ∈ N.E ∧ M.Parallel e f

theorem Matroid.IsSimplification.simplifies {α : Type u_1} {M N : Matroid α} (h : N.IsSimplification M) : N.Simplifies M

theorem Matroid.IsSimplification.eq_of_parallel {α : Type u_1} {M N : Matroid α} {e f : α} (h : N.IsSimplification M) (he : e ∈ N.E) (hf : f ∈ N.E) (hef : M.Parallel e f) : e = f

theorem Matroid.IsSimplification.eq_of_simplifies_ge {α : Type u_1} {M N N₀ : Matroid α} (h : N.IsSimplification M) (hN₀ : N₀.Simplifies M) (hN₀N : N₀.IsRestriction N) : N₀ = N

theorem Matroid.isSimplification_iff {α : Type u_1} {M N : Matroid α} : N.IsSimplification M ↔ N.Loopless ∧ N.IsRestriction M ∧ ∀ ⦃e : α⦄, M.IsNonloop e → ∃! f : α, f ∈ N.E ∧ M.Parallel e f

A simplification of M is the restriction of M to a transversal of its parallel classes.

theorem Matroid.isSimplification_iff_minimal_simplifies {α : Type u_1} {M N : Matroid α} : N.IsSimplification M ↔ N.Simplifies M ∧ ∀ ⦃N₀ : Matroid α⦄, N₀.IsRestriction N → N₀.Simplifies M → N₀ = N

N is a simplification of M if N is minimal in the restriction order simplifying M.

theorem Matroid.Simple.isSimplification_of_simplifies {α : Type u_1} {M N : Matroid α} (hN : N.Simple) (hNM : N.Simplifies M) : N.IsSimplification M

theorem Matroid.IsSimplification.isSimplification_of_simplifies {α : Type u_1} {M N N₀ : Matroid α} (hN₀N : N₀.IsSimplification N) (hNM : N.Simplifies M) : N₀.IsSimplification M

theorem Matroid.IsSimplification.of_isRestriction {α : Type u_1} {M N M' : Matroid α} (h : N.IsSimplification M) (hNM' : N.IsRestriction M') (hM'M : M'.IsRestriction M) : N.IsSimplification M'

theorem Matroid.IsPoint.mem_simplification {α : Type u_1} {M N : Matroid α} {e : α} (he : M.IsPoint {e}) (hN : N.IsSimplification M) : e ∈ N.E

theorem Matroid.IsPoint.exists_unique_of_isSimplification {α : Type u_1} {M N : Matroid α} {P : Set α} (h : M.IsPoint P) (hNM : N.IsSimplification M) : ∃! f : α, f ∈ P ∧ f ∈ N.E

theorem Matroid.IsSimplification.delete {α : Type u_1} {M N : Matroid α} {D : Set α} (hN : N.IsSimplification M) (hD : D ⊆ N.E) : (N.delete D).IsSimplification (M.delete (⋃ e ∈ D, {f : α | M.Parallel e f}))

noncomputable def Matroid.IsSimplification.iso {α : Type u_1} {M N N' : Matroid α} (hN : N.IsSimplification M) (hN' : N'.IsSimplification M) : N ≂ N'

Any two simplifications of M are isomorphic.

Equations

• One or more equations did not get rendered due to their size.

theorem Matroid.IsSimplification.exists_of_isStrictRestriction {α : Type u_1} {M N : Matroid α} (hN : N.IsSimplification M) (hNM : N.IsStrictRestriction M) : (∃ (e : α), M.IsLoop e ∧ e ∉ N.E) ∨ ∃ (e : α) (f : α), M.Parallel e f ∧ e ∈ M.E ∧ e ∉ N.E ∧ f ∈ N.E

theorem Matroid.IsSimplification.isSpanningRestriction {α : Type u_1} {M N : Matroid α} (hN : N.IsSimplification M) : N.IsSpanningRestriction M

theorem Matroid.IsSimplification.isSimplification_removeLoops {α : Type u_1} {M N : Matroid α} (hN : N.IsSimplification M) : N.IsSimplification M.removeLoops

theorem Matroid.IsSimplification.isBase_of_isBase {α : Type u_1} {M N : Matroid α} {B : Set α} (hN : N.IsSimplification M) (hB : N.IsBase B) : M.IsBase B

theorem Matroid.IsSimplification.eRank_eq {α : Type u_1} {M N : Matroid α} (hN : N.IsSimplification M) : N.eRank = M.eRank

theorem Matroid.IsSimplification.ground_eq_biUnion_setOf_parallel {α : Type u_1} {M N : Matroid α} [M.Loopless] (hNM : N.IsSimplification M) : M.E = ⋃ e ∈ N.E, {x : α | M.Parallel e x}

theorem Matroid.IsSimplification.ground_eq_biUnion_setOf_parallel_union_loops {α : Type u_1} {M N : Matroid α} (hNM : N.IsSimplification M) : M.E = (⋃ e ∈ N.E, {x : α | M.Parallel e x}) ∪ M.loops

theorem Matroid.IsSimplification.ground_eq_biUnion_closure {α : Type u_1} {M N : Matroid α} [M.RankPos] (hNM : N.IsSimplification M) : M.E = ⋃ e ∈ N.E, M.closure {e}

theorem Matroid.IsSimplification.setOf_parallel_pairwiseDisjoint {α : Type u_1} {M N : Matroid α} (hNM : N.IsSimplification M) : N.E.PairwiseDisjoint fun (e : α) => {x : α | M.Parallel e x}

theorem Matroid.IsSimplification.setOf_parallel_injOn {α : Type u_1} {M N : Matroid α} (hNM : N.IsSimplification M) : Set.InjOn (fun (e : α) => {x : α | M.Parallel e x}) N.E

theorem Matroid.IsSimplification.image_setOf_parallel_pairwiseDisjoint {α : Type u_1} {M N : Matroid α} (hNM : N.IsSimplification M) : ((fun (e : α) => {f : α | M.Parallel e f}) '' N.E).PairwiseDisjoint id

theorem Matroid.IsSimplification.closure_pairwiseDisjoint {α : Type u_1} {M N : Matroid α} [M.Loopless] (hNM : N.IsSimplification M) : N.E.PairwiseDisjoint fun (e : α) => M.closure {e}

noncomputable def Matroid.IsSimplification.pointEquiv {α : Type u_1} {M N : Matroid α} (h : N.IsSimplification M) : ↑N.E ≃ { P : Set α // M.IsPoint P }

The elements of a simplification of M correspond to the points of M.

Equations

• h.pointEquiv = { toFun := fun (e : ↑N.E) => ⟨M.closure {↑e}, ⋯⟩, invFun := fun (P : { P : Set α // M.IsPoint P }) => ⟨⋯.some, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem Matroid.IsSimplification.encard_ground_eq {α : Type u_1} {M N : Matroid α} (h : N.IsSimplification M) : N.E.encard = {P : Set α | M.IsPoint P}.encard

noncomputable def Matroid.simplification {α : Type u_1} (M : Matroid α) : Matroid α

A classically chosen simplification of M. The definition depends on M.removeLoops rather than M, so the choice is a bit more stable; deleting a subset of the loops does not change the choice of simplification.

Equations

• M.simplification = (fun (M : Matroid α) => M.restrict (⇑⋯.some '' {e : α | M.IsNonloop e})) M.removeLoops

theorem Matroid.simplification_isSimplification {α : Type u_1} (M : Matroid α) : M.simplification.IsSimplification M

theorem Matroid.exists_isSimplification {α : Type u_1} (M : Matroid α) : ∃ (N : Matroid α), N.IsSimplification M

@[simp]

theorem Matroid.simplification_eq_self {α : Type u_1} {M : Matroid α} [M.Simple] : M.simplification = M

theorem Matroid.Simple.simplification_eq_self {α : Type u_1} {M : Matroid α} (h : M.Simple) : M.simplification = M

instance Matroid.simplification_simple {α : Type u_1} (M : Matroid α) : M.simplification.Simple

theorem Matroid.simplification_eq_self_iff {α : Type u_1} {M : Matroid α} : M.simplification = M ↔ M.Simple

theorem Matroid.isSimplification_self {α : Type u_1} {M : Matroid α} [M.Simple] : M.IsSimplification M

theorem Matroid.simplification_factorsThrough_removeLoops {α : Type u_1} : Function.FactorsThrough simplification removeLoops

theorem Matroid.simplification_delete_eq_of_subset_loops {α : Type u_1} {X : Set α} (M : Matroid α) (hX : X ⊆ M.loops) : (M.delete X).simplification = M.simplification

@[simp]

theorem Matroid.simplification_removeLoops_eq {α : Type u_1} (M : Matroid α) : M.removeLoops.simplification = M.simplification

@[simp]

theorem Matroid.simplification_idem {α : Type u_1} (M : Matroid α) : M.simplification.simplification = M.simplification

theorem Matroid.simplification_isRestriction {α : Type u_1} (M : Matroid α) : M.simplification.IsRestriction M

@[simp]

theorem Matroid.simplification_eRank_eq {α : Type u_1} (M : Matroid α) : M.simplification.eRank = M.eRank

theorem Matroid.IsMinor.exists_isMinor_isSimplification {α : Type u_1} {M N : Matroid α} (hNM : N ≤m M) (hN : N.Simple) : ∃ (M₀ : Matroid α), N ≤m M₀ ∧ M₀.IsSimplification M

theorem Matroid.Simple.isMinor_iff_isMinor_simplification {α : Type u_1} {N : Matroid α} {β : Type u_2} (hN : N.Simple) {M : Matroid β} : Nonempty (IsoMinor N M) ↔ Nonempty (IsoMinor N M.simplification)