Matroid Circuits

A Circuit of a matroid M is a minimal set C that is dependent in M. A matroid is determined by its set of circuits, and often the circuits offer a more compact description of a matroid than the collection of independent sets or bases. In matroids arising from graphs, circuits correspond to graphical cycles.

Main Declarations

• Matroid.Circuit M C means that C is minimally dependent in M.
• For an Independent set I whose closure contains an element e ∉ I, Matroid.fundCircuit M e I is the unique circuit contained in insert e I.
• Matroid.Indep.fundCircuit_circuit states that Matroid.fundCircuit M e I is indeed a circuit.
• Circuit.eq_fundCircuit_of_subset states that Matroid.fundCircuit M e I is the unique circuit contained in insert e I.
• Matroid.dep_iff_superset_circuit states that the dependent subsets of the ground set are precisely those that contain a circuit.
• Matroid.ext_circuit : a matroid is determined by its collection of circuits.

Implementation Details

Since Matroid.fundCircuit M e I is only sensible if I is independent and e ∈ M.closure I \ I, to avoid hypotheses being explicitly included in the definition, junk values need to be chosen if either hypothesis fails. The definition is chosen so that the junk values satisfy M.fundCircuit e I = {e} for e ∈ I or e ∉ M.E and M.fundCircuit e I = insert e I if e ∈ M.E \ M.closure I. These make the useful statement e ∈ M.fundCircuit e I ⊆ insert e I true unconditionally.

def Matroid.Circuit {α : Type u_1} (M : Matroid α) (x : Set α) : Prop

A Circuit of M is a minimal dependent set in M

Equations

• M.Circuit = Minimal M.Dep

theorem Matroid.circuit_def {α : Type u_1} {M : Matroid α} {C : Set α} : M.Circuit C ↔ Minimal M.Dep C

theorem Matroid.Circuit.dep {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.Circuit C) : M.Dep C

theorem Matroid.Circuit.not_indep {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.Circuit C) : ¬M.Indep C

theorem Matroid.Circuit.minimal {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.Circuit C) : Minimal M.Dep C

theorem Matroid.Circuit.subset_ground {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.Circuit C) : C ⊆ M.E

theorem Matroid.Circuit.nonempty {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.Circuit C) : C.Nonempty

theorem Matroid.empty_not_circuit {α : Type u_1} (M : Matroid α) : ¬M.Circuit ∅

theorem Matroid.circuit_iff {α : Type u_1} {M : Matroid α} {C : Set α} : M.Circuit C ↔ M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C

theorem Matroid.Circuit.ssubset_indep {α : Type u_1} {M : Matroid α} {C X : Set α} (hC : M.Circuit C) (hXC : X ⊂ C) : M.Indep X

theorem Matroid.Circuit.minimal_not_indep {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.Circuit C) : Minimal (fun (x : Set α) => ¬M.Indep x) C

theorem Matroid.circuit_iff_minimal_not_indep {α : Type u_1} {M : Matroid α} {C : Set α} (hCE : C ⊆ M.E) : M.Circuit C ↔ Minimal (fun (x : Set α) => ¬M.Indep x) C

theorem Matroid.Circuit.diff_singleton_indep {α : Type u_1} {M : Matroid α} {C : Set α} {e : α} (hC : M.Circuit C) (he : e ∈ C) : M.Indep (C \ {e})

theorem Matroid.circuit_iff_forall_ssubset {α : Type u_1} {M : Matroid α} {C : Set α} : M.Circuit C ↔ M.Dep C ∧ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I

theorem Matroid.circuit_antichain {α : Type u_1} {M : Matroid α} : IsAntichain (fun (x1 x2 : Set α) => x1 ⊆ x2) (setOf M.Circuit)

theorem Matroid.Circuit.eq_of_not_indep_subset {α : Type u_1} {M : Matroid α} {C X : Set α} (hC : M.Circuit C) (hX : ¬M.Indep X) (hXC : X ⊆ C) : X = C

theorem Matroid.Circuit.eq_of_dep_subset {α : Type u_1} {M : Matroid α} {C X : Set α} (hC : M.Circuit C) (hX : M.Dep X) (hXC : X ⊆ C) : X = C

theorem Matroid.Circuit.not_ssubset {α : Type u_1} {M : Matroid α} {C C' : Set α} (hC : M.Circuit C) (hC' : M.Circuit C') : ¬C' ⊂ C

theorem Matroid.Circuit.eq_of_subset_circuit {α : Type u_1} {M : Matroid α} {C C' : Set α} (hC : M.Circuit C) (hC' : M.Circuit C') (h : C ⊆ C') : C = C'

theorem Matroid.Circuit.eq_of_superset_circuit {α : Type u_1} {M : Matroid α} {C C' : Set α} (hC : M.Circuit C) (hC' : M.Circuit C') (h : C' ⊆ C) : C = C'

theorem Matroid.circuit_iff_dep_forall_diff_singleton_indep {α : Type u_1} {M : Matroid α} {C : Set α} : M.Circuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})

Independence and bases

theorem Matroid.Indep.insert_circuit_of_forall {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (hI : M.Indep I) (heI : e ∉ I) (he : e ∈ M.closure I) (h : ∀ f ∈ I, e ∉ M.closure (I \ {f})) : M.Circuit (insert e I)

theorem Matroid.Indep.insert_circuit_of_forall_of_nontrivial {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (hI : M.Indep I) (hInt : I.Nontrivial) (he : e ∈ M.closure I) (h : ∀ f ∈ I, e ∉ M.closure (I \ {f})) : M.Circuit (insert e I)

theorem Matroid.Circuit.diff_singleton_basis {α : Type u_1} {M : Matroid α} {C : Set α} {e : α} (hC : M.Circuit C) (he : e ∈ C) : M.Basis (C \ {e}) C

theorem Matroid.Circuit.basis_iff_eq_diff_singleton {α : Type u_1} {M : Matroid α} {C I : Set α} (hC : M.Circuit C) : M.Basis I C ↔ ∃ e ∈ C, I = C \ {e}

theorem Matroid.Circuit.basis_iff_insert_eq {α : Type u_1} {M : Matroid α} {C I : Set α} (hC : M.Circuit C) : M.Basis I C ↔ ∃ e ∈ C \ I, C = insert e I

Closure

theorem Matroid.Circuit.closure_diff_singleton_eq {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.Circuit C) (e : α) : M.closure (C \ {e}) = M.closure C

theorem Matroid.Circuit.subset_closure_diff_singleton {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.Circuit C) (e : α) : C ⊆ M.closure (C \ {e})

theorem Matroid.Circuit.mem_closure_diff_singleton_of_mem {α : Type u_1} {M : Matroid α} {C : Set α} {e : α} (hC : M.Circuit C) (heC : e ∈ C) : e ∈ M.closure (C \ {e})

Restriction

theorem Matroid.Circuit.circuit_restrict_of_subset {α : Type u_1} {M : Matroid α} {C R : Set α} (hC : M.Circuit C) (hCR : C ⊆ R) : (M.restrict R).Circuit C

theorem Matroid.restrict_circuit_iff {α : Type u_1} {M : Matroid α} {C R : Set α} (hR : R ⊆ M.E := by aesop_mat) : (M.restrict R).Circuit C ↔ M.Circuit C ∧ C ⊆ R

Fundamental Circuits

def Matroid.fundCircuit {α : Type u_1} (M : Matroid α) (e : α) (I : Set α) : Set α

For an independent set I and some e ∈ M.closure I \ I, M.fundCircuit e I is the unique circuit contained in insert e I. For the fact that this is a circuit, see Matroid.Indep.fundCircuit_circuit, and the fact that it is unique, see Matroid.Circuit.eq_fundCircuit_of_subset. Has the junk value {e} if e ∈ I or e ∉ M.E, and insert e I if e ∈ M.E \ M.closure I.

Equations

• M.fundCircuit e I = insert e (I ∩ ⋂₀ {J : Set α | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})

theorem Matroid.fundCircuit_eq_sInter {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (he : e ∈ M.closure I) : M.fundCircuit e I = insert e (⋂₀ {J : Set α | J ⊆ I ∧ e ∈ M.closure J})

theorem Matroid.fundCircuit_subset_insert {α : Type u_1} (M : Matroid α) (e : α) (I : Set α) : M.fundCircuit e I ⊆ insert e I

theorem Matroid.fundCircuit_subset_ground {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (he : e ∈ M.E) (hI : I ⊆ M.E := by aesop_mat) : M.fundCircuit e I ⊆ M.E

theorem Matroid.mem_fundCircuit {α : Type u_1} (M : Matroid α) (e : α) (I : Set α) : e ∈ M.fundCircuit e I

theorem Matroid.fundCircuit_diff_eq_inter {α : Type u_1} {I : Set α} {e : α} (M : Matroid α) (heI : e ∉ I) : M.fundCircuit e I \ {e} = M.fundCircuit e I ∩ I

theorem Matroid.fundCircuit_eq_of_mem {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (heX : e ∈ X) : M.fundCircuit e X = {e}

The fundamental circuit of e and X has the junk value {e} if e ∈ X

theorem Matroid.fundCircuit_eq_of_not_mem_ground {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (heX : e ∉ M.E) : M.fundCircuit e X = {e}

theorem Matroid.Indep.fundCircuit_circuit {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (hI : M.Indep I) (hecl : e ∈ M.closure I) (heI : e ∉ I) : M.Circuit (M.fundCircuit e I)

theorem Matroid.Indep.mem_fundCircuit_iff {α : Type u_1} {M : Matroid α} {I : Set α} {e x : α} (hI : M.Indep I) (hecl : e ∈ M.closure I) (heI : e ∉ I) : x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x})

theorem Matroid.Base.fundCircuit_circuit {α : Type u_1} {M : Matroid α} {x : α} {B : Set α} (hB : M.Base B) (hxE : x ∈ M.E) (hxB : x ∉ B) : M.Circuit (M.fundCircuit x B)

theorem Matroid.Circuit.eq_fundCircuit_of_subset {α : Type u_1} {M : Matroid α} {C I : Set α} {e : α} (hC : M.Circuit C) (hI : M.Indep I) (hCss : C ⊆ insert e I) : C = M.fundCircuit e I

For I independent, M.fundCircuit e I is the only circuit contained in insert e I.

theorem Matroid.fundCircuit_restrict {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} {R : Set α} (hIR : I ⊆ R) (heR : e ∈ R) (hR : R ⊆ M.E) : (M.restrict R).fundCircuit e I = M.fundCircuit e I

@[simp]

theorem Matroid.fundCircuit_restrict_univ {α : Type u_1} {I : Set α} {e : α} (M : Matroid α) : (M.restrict Set.univ).fundCircuit e I = M.fundCircuit e I

Dependence

theorem Matroid.Dep.exists_circuit_subset {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Dep X) : ∃ C ⊆ X, M.Circuit C

theorem Matroid.dep_iff_superset_circuit {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E := by aesop_mat) : M.Dep X ↔ ∃ C ⊆ X, M.Circuit C

theorem Matroid.dep_iff_superset_circuit' {α : Type u_1} {M : Matroid α} {X : Set α} : M.Dep X ↔ (∃ C ⊆ X, M.Circuit C) ∧ X ⊆ M.E

A version of Matroid.dep_iff_superset_circuit that has the supportedness hypothesis as part of the equivalence, rather than a hypothesis.

theorem Matroid.indep_iff_forall_subset_not_circuit' {α : Type u_1} {M : Matroid α} {I : Set α} : M.Indep I ↔ (∀ C ⊆ I, ¬M.Circuit C) ∧ I ⊆ M.E

A version of Matroid.indep_iff_forall_subset_not_circuit that has the supportedness hypothesis as part of the equivalence, rather than a hypothesis.

theorem Matroid.indep_iff_forall_subset_not_circuit {α : Type u_1} {M : Matroid α} {I : Set α} (hI : I ⊆ M.E := by aesop_mat) : M.Indep I ↔ ∀ C ⊆ I, ¬M.Circuit C

Extensionality

theorem Matroid.ext_circuit {α : Type u_1} {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (h : ∀ ⦃C : Set α⦄, C ⊆ M₁.E → (M₁.Circuit C ↔ M₂.Circuit C)) : M₁ = M₂

theorem Matroid.ext_circuit_not_indep {α : Type u_1} {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (h₁ : ∀ (C : Set α), M₁.Circuit C → ¬M₂.Indep C) (h₂ : ∀ (C : Set α), M₂.Circuit C → ¬M₁.Indep C) : M₁ = M₂

A stronger version of Matroid.ext_circuit: two matroids on the same ground set are equal if no circuit of one is independent in the other.

theorem Matroid.ext_iff_circuit {α : Type u_1} {M₁ M₂ : Matroid α} : M₁ = M₂ ↔ M₁.E = M₂.E ∧ ∀ (C : Set α), M₁.Circuit C ↔ M₂.Circuit C