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.
• Matroid.Circuit.strong_multi_elimination : the strong circuit elimination rule for an infinite collection of circuits.
• Matroid.Circuit.strong_elimination : the strong circuit elimination rule for two circuits.
• Matroid.finitary_iff_forall_circuit_finite : finitary matroids are precisely those whose circuits are all finite.

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

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) (hCs : 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

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

theorem Matroid.exists_circuit_of_mem_closure {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ M.closure X) (heX : e ∉ X) : ∃ C ⊆ insert e X, M.Circuit C ∧ e ∈ C

theorem Matroid.mem_closure_iff_exists_circuit {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (he : e ∉ X) : e ∈ M.closure X ↔ ∃ C ⊆ insert e X, M.Circuit C ∧ e ∈ 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

Circuit Elimination

theorem Matroid.Circuit.strong_multi_elimination_insert {α : Type u_1} {M : Matroid α} {ι : Type u_2} {J : Set α} (x : ι → α) (I : ι → Set α) (z : α) (hxI : ∀ (i : ι), x i ∉ I i) (hC : ∀ (i : ι), M.Circuit (insert (x i) (I i))) (hJx : M.Circuit (J ∪ Set.range x)) (hzJ : z ∈ J) (hzI : ∀ (i : ι), z ∉ I i) : ∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.Circuit C' ∧ z ∈ C'

A version of Matroid.Circuit.strong_multi_elimination that is phrased using insertion.

theorem Matroid.Circuit.strong_multi_elimination {α : Type u_1} {M : Matroid α} {ι : Type u_2} {C₀ : Set α} (hC₀ : M.Circuit C₀) (x : ι → α) (C : ι → Set α) (z : α) (hC : ∀ (i : ι), M.Circuit (C i)) (h_mem_C₀ : ∀ (i : ι), x i ∈ C₀) (h_mem : ∀ (i : ι), x i ∈ C i) (h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i') (hzC₀ : z ∈ C₀) (hzC : ∀ (i : ι), z ∉ C i) : ∃ C' ⊆ (C₀ ∪ ⋃ (i : ι), C i) \ Set.range x, M.Circuit C' ∧ z ∈ C'

A generalization of the strong circuit elimination axiom Matroid.Circuit.strong_elimination to an infinite collection of circuits.

It states that, given a circuit C₀, a arbitrary collection C : ι → Set α of circuits, an element x i of C₀ ∩ C i for each i, and an element z ∈ C₀ outside all the C i, the union of C₀ and the C i contains a circuit containing z but none of the x i.

This is one of the axioms when defining infinite matroids via circuits.

TODO : A similar statement will hold even when all mentions of z are removed.

theorem Matroid.Circuit.strong_multi_elimination_set {α : Type u_1} {M : Matroid α} {C₀ : Set α} (hC₀ : M.Circuit C₀) (X : Set α) (S : Set (Set α)) (z : α) (hCS : ∀ C ∈ S, M.Circuit C) (hXC₀ : X ⊆ C₀) (hX : ∀ x ∈ X, ∃ C ∈ S, C ∩ X = {x}) (hzC₀ : z ∈ C₀) (hz : ∀ C ∈ S, z ∉ C) : ∃ C' ⊆ (C₀ ∪ ⋃₀ S) \ X, M.Circuit C' ∧ z ∈ C'

A version of Circuit.strong_multi_elimination where the collection of circuits is a Set (Set α) and the distinguished elements are a Set α, rather than both being indexed.

theorem Matroid.Circuit.strong_elimination {α : Type u_1} {M : Matroid α} {e f : α} {C₁ C₂ : Set α} (hC₁ : M.Circuit C₁) (hC₂ : M.Circuit C₂) (heC₁ : e ∈ C₁) (heC₂ : e ∈ C₂) (hfC₁ : f ∈ C₁) (hfC₂ : f ∉ C₂) : ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.Circuit C ∧ f ∈ C

The strong circuit elimination axiom. For any pair of distinct circuits C₁, C₂ and all e ∈ C₁ ∩ C₂ and f ∈ C₁ \ C₂, there is a circuit C with f ∈ C ⊆ (C₁ ∪ C₂) \ {e}.

theorem Matroid.Circuit.elimination {α : Type u_1} {M : Matroid α} {C₁ C₂ : Set α} (hC₁ : M.Circuit C₁) (hC₂ : M.Circuit C₂) (h : C₁ ≠ C₂) (e : α) : ∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.Circuit C

The circuit elimination axiom : for any pair of distinct circuits C₁, C₂ and any e, some circuit is contained in (C₁ ∪ C₂) \ {e}.

This is one of the axioms when definining a finitary matroid via circuits; as an axiom, it is usually stated with the extra assumption that e ∈ C₁ ∩ C₂.

Finitary Matroids

theorem Matroid.Circuit.finite {α : Type u_1} {M : Matroid α} {C : Set α} [M.Finitary] (hC : M.Circuit C) : C.Finite

theorem Matroid.finitary_iff_forall_circuit_finite {α : Type u_1} {M : Matroid α} : M.Finitary ↔ ∀ (C : Set α), M.Circuit C → C.Finite

theorem Matroid.exists_mem_finite_closure_of_mem_closure {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} [M.Finitary] (he : e ∈ M.closure X) : ∃ I ⊆ X, I.Finite ∧ M.Indep I ∧ e ∈ M.closure I

In a finitary matroid, every element spanned by a set X is in fact spanned by a finite independent subset of X.

theorem Matroid.exists_subset_finite_closure_of_subset_closure {α : Type u_1} {M : Matroid α} {X Y : Set α} [M.Finitary] (hX : X.Finite) (hXY : X ⊆ M.closure Y) : ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I

In a finitary matroid, each finite set X spanned by a set Y is in fact spanned by a finite independent subset of Y.