# Matroid IsCircuits #

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.IsCircuit M C` means that `C` is minimally dependent in `M`.
- For an `Indep`endent 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_isCircuit` states that `Matroid.fundCircuit M e I` is indeed a circuit.
- `Matroid.IsCircuit.eq_fundCircuit_of_subset` states that `Matroid.fundCircuit M e I` is the unique circuit contained in `insert e I`.
- `Matroid.dep_iff_superset_isCircuit` states that the dependent subsets of the ground set are precisely those that contain a circuit.
- `Matroid.ext_isCircuit` : a matroid is determined by its collection of circuits.
- `Matroid.IsCircuit.strong_multi_elimination` : the strong circuit elimination rule for an infinite collection of circuits.
- `Matroid.IsCircuit.strong_elimination` : the strong circuit elimination rule for two circuits.
- `Matroid.finitary_iff_forall_isCircuit_finite` : finitary matroids are precisely those whose circuits are all finite.
- `Matroid.IsCocircuit M C` means that `C` is minimally dependent in `M✶`, or equivalently that `M.E \ C` is a hyperplane of `M`.
- `Matroid.fundCocircuit M B e` is the unique cocircuit that intersects the base `B` precisely in the element `e`.
- `Matroid.IsBase.mem_fundCocircuit_iff_mem_fundCircuit` : `e` is in the fundamental circuit for `B` and `f` iff `f` is in the fundamental cocircuit for `B` and `e`.

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

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

`M.IsCircuit C` means that `C` is a minimal dependent set in `M`.

Equations

- M.IsCircuit = Minimal M.Dep

Instances For

source
theorem Matroid.isCircuit_def {α : Type u_1} {M : Matroid α} {C : Set α} :
M.IsCircuit C ↔ Minimal M.Dep C
source
theorem Matroid.IsCircuit.dep {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) :
M.Dep C
source
theorem Matroid.IsCircuit.not_indep {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) :
¬M.Indep C
source
theorem Matroid.IsCircuit.minimal {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) :
Minimal M.Dep C
source
theorem Matroid.IsCircuit.subset_ground {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) :
C ⊆ M.E
source
theorem Matroid.IsCircuit.nonempty {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) :
C.Nonempty
source
theorem Matroid.empty_not_isCircuit {α : Type u_1} (M : Matroid α) :
¬M.IsCircuit ∅
source
theorem Matroid.isCircuit_iff {α : Type u_1} {M : Matroid α} {C : Set α} :
M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C
source
theorem Matroid.IsCircuit.ssubset_indep {α : Type u_1} {M : Matroid α} {C X : Set α} (hC : M.IsCircuit C) (hXC : X ⊂ C) :
M.Indep X
source
theorem Matroid.IsCircuit.minimal_not_indep {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) :
Minimal (fun (x : Set α) => ¬M.Indep x) C
source
theorem Matroid.isCircuit_iff_minimal_not_indep {α : Type u_1} {M : Matroid α} {C : Set α} (hCE : C ⊆ M.E) :
M.IsCircuit C ↔ Minimal (fun (x : Set α) => ¬M.Indep x) C
source
theorem Matroid.IsCircuit.diff_singleton_indep {α : Type u_1} {M : Matroid α} {C : Set α} {e : α} (hC : M.IsCircuit C) (he : e ∈ C) :
M.Indep (C \ {e})
source
theorem Matroid.isCircuit_iff_forall_ssubset {α : Type u_1} {M : Matroid α} {C : Set α} :
M.IsCircuit C ↔ M.Dep C ∧ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I
source
theorem Matroid.isCircuit_antichain {α : Type u_1} {M : Matroid α} :
IsAntichain (fun (x1 x2 : Set α) => x1 ⊆ x2) (setOf M.IsCircuit)
source
theorem Matroid.IsCircuit.eq_of_not_indep_subset {α : Type u_1} {M : Matroid α} {C X : Set α} (hC : M.IsCircuit C) (hX : ¬M.Indep X) (hXC : X ⊆ C) :
X = C
source
theorem Matroid.IsCircuit.eq_of_dep_subset {α : Type u_1} {M : Matroid α} {C X : Set α} (hC : M.IsCircuit C) (hX : M.Dep X) (hXC : X ⊆ C) :
X = C
source
theorem Matroid.IsCircuit.not_ssubset {α : Type u_1} {M : Matroid α} {C C' : Set α} (hC : M.IsCircuit C) (hC' : M.IsCircuit C') :
¬C' ⊂ C
source
theorem Matroid.IsCircuit.eq_of_subset_isCircuit {α : Type u_1} {M : Matroid α} {C C' : Set α} (hC : M.IsCircuit C) (hC' : M.IsCircuit C') (h : C ⊆ C') :
C = C'
source
theorem Matroid.IsCircuit.eq_of_superset_isCircuit {α : Type u_1} {M : Matroid α} {C C' : Set α} (hC : M.IsCircuit C) (hC' : M.IsCircuit C') (h : C' ⊆ C) :
C = C'
source
theorem Matroid.isCircuit_iff_dep_forall_diff_singleton_indep {α : Type u_1} {M : Matroid α} {C : Set α} :
M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})

### Independence and bases #

source
theorem Matroid.Indep.insert_isCircuit_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.IsCircuit (insert e I)
source
theorem Matroid.Indep.insert_isCircuit_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.IsCircuit (insert e I)
source
theorem Matroid.IsCircuit.diff_singleton_isBasis {α : Type u_1} {M : Matroid α} {C : Set α} {e : α} (hC : M.IsCircuit C) (he : e ∈ C) :
M.IsBasis (C \ {e}) C
source
theorem Matroid.IsCircuit.isBasis_iff_eq_diff_singleton {α : Type u_1} {M : Matroid α} {C I : Set α} (hC : M.IsCircuit C) :
M.IsBasis I C ↔ ∃ e ∈ C, I = C \ {e}
source
theorem Matroid.IsCircuit.isBasis_iff_insert_eq {α : Type u_1} {M : Matroid α} {C I : Set α} (hC : M.IsCircuit C) :
M.IsBasis I C ↔ ∃ e ∈ C \ I, C = insert e I

### Restriction #

source
theorem Matroid.IsCircuit.isCircuit_restrict_of_subset {α : Type u_1} {M : Matroid α} {C R : Set α} (hC : M.IsCircuit C) (hCR : C ⊆ R) :
(M.restrict R).IsCircuit C
source
theorem Matroid.restrict_isCircuit_iff {α : Type u_1} {M : Matroid α} {C R : Set α} (hR : R ⊆ M.E := by aesop_mat) :
(M.restrict R).IsCircuit C ↔ M.IsCircuit C ∧ C ⊆ R

### Fundamental IsCircuits #

source
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_isCircuit`, and the fact that it is unique, see `Matroid.IsCircuit.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})

Instances For

source
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})
source
theorem Matroid.fundCircuit_subset_insert {α : Type u_1} (M : Matroid α) (e : α) (I : Set α) :
M.fundCircuit e I ⊆ insert e I
source
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
source
theorem Matroid.mem_fundCircuit {α : Type u_1} (M : Matroid α) (e : α) (I : Set α) :
e ∈ M.fundCircuit e I
source
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
source
theorem Matroid.fundCircuit_eq_of_mem {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (heX : e ∈ X) :
M.fundCircuit e X = {e}

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

source
theorem Matroid.fundCircuit_eq_of_notMem_ground {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (heX : e ∉ M.E) :
M.fundCircuit e X = {e}
source
@[deprecated Matroid.fundCircuit_eq_of_notMem_ground (since := "2025-05-23")]
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}

Alias of `Matroid.fundCircuit_eq_of_notMem_ground`.

source
theorem Matroid.Indep.fundCircuit_isCircuit {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (hI : M.Indep I) (hecl : e ∈ M.closure I) (heI : e ∉ I) :
M.IsCircuit (M.fundCircuit e I)
source
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})
source
theorem Matroid.IsBase.fundCircuit_isCircuit {α : Type u_1} {M : Matroid α} {x : α} {B : Set α} (hB : M.IsBase B) (hxE : x ∈ M.E) (hxB : x ∉ B) :
M.IsCircuit (M.fundCircuit x B)
source
theorem Matroid.IsCircuit.eq_fundCircuit_of_subset {α : Type u_1} {M : Matroid α} {C I : Set α} {e : α} (hC : M.IsCircuit 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`.

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

source
theorem Matroid.Dep.exists_isCircuit_subset {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Dep X) :
∃ C ⊆ X, M.IsCircuit C
source
theorem Matroid.dep_iff_superset_isCircuit {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E := by aesop_mat) :
M.Dep X ↔ ∃ C ⊆ X, M.IsCircuit C
source
theorem Matroid.dep_iff_superset_isCircuit' {α : Type u_1} {M : Matroid α} {X : Set α} :
M.Dep X ↔ (∃ C ⊆ X, M.IsCircuit C) ∧ X ⊆ M.E

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

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

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

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

### Closure #

source
theorem Matroid.IsCircuit.closure_diff_singleton_eq {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) (e : α) :
M.closure (C \ {e}) = M.closure C
source
theorem Matroid.IsCircuit.subset_closure_diff_singleton {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) (e : α) :
C ⊆ M.closure (C \ {e})
source
theorem Matroid.IsCircuit.mem_closure_diff_singleton_of_mem {α : Type u_1} {M : Matroid α} {C : Set α} {e : α} (hC : M.IsCircuit C) (heC : e ∈ C) :
e ∈ M.closure (C \ {e})
source
theorem Matroid.exists_isCircuit_of_mem_closure {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ M.closure X) (heX : e ∉ X) :
∃ C ⊆ insert e X, M.IsCircuit C ∧ e ∈ C
source
theorem Matroid.mem_closure_iff_exists_isCircuit {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (he : e ∉ X) :
e ∈ M.closure X ↔ ∃ C ⊆ insert e X, M.IsCircuit C ∧ e ∈ C

### Extensionality #

source
theorem Matroid.ext_isCircuit {α : Type u_1} {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (h : ∀ ⦃C : Set α⦄, C ⊆ M₁.E → (M₁.IsCircuit C ↔ M₂.IsCircuit C)) :
M₁ = M₂
source
theorem Matroid.ext_isCircuit_not_indep {α : Type u_1} {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C) (h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C) :
M₁ = M₂

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

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

### Circuit Elimination #

source
theorem Matroid.IsCircuit.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.IsCircuit (insert (x i) (I i))) (hJx : M.IsCircuit (J ∪ Set.range x)) (hzJ : z ∈ J) (hzI : ∀ (i : ι), z ∉ I i) :
∃ C' ⊆ J ∪ ⋃ (i : ι), I i, M.IsCircuit C' ∧ z ∈ C'

A version of `Matroid.IsCircuit.strong_multi_elimination` that is phrased using insertion.

source
theorem Matroid.IsCircuit.strong_multi_elimination {α : Type u_1} {M : Matroid α} {ι : Type u_2} {C₀ : Set α} (hC₀ : M.IsCircuit C₀) (x : ι → α) (C : ι → Set α) (z : α) (hC : ∀ (i : ι), M.IsCircuit (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.IsCircuit C' ∧ z ∈ C'

A generalization of the strong circuit elimination axiom `Matroid.IsCircuit.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.

source
theorem Matroid.IsCircuit.strong_multi_elimination_set {α : Type u_1} {M : Matroid α} {C₀ : Set α} (hC₀ : M.IsCircuit C₀) (X : Set α) (S : Set (Set α)) (z : α) (hCS : ∀ C ∈ S, M.IsCircuit 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.IsCircuit 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.

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

The strong isCircuit 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}`.

source
theorem Matroid.IsCircuit.elimination {α : Type u_1} {M : Matroid α} {C₁ C₂ : Set α} (hC₁ : M.IsCircuit C₁) (hC₂ : M.IsCircuit C₂) (h : C₁ ≠ C₂) (e : α) :
∃ C ⊆ (C₁ ∪ C₂) \ {e}, M.IsCircuit 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 defining a finitary matroid via circuits; as an axiom, it is usually stated with the extra assumption that `e ∈ C₁ ∩ C₂`.

### Finitary Matroids #

source
theorem Matroid.IsCircuit.finite {α : Type u_1} {M : Matroid α} {C : Set α} [M.Finitary] (hC : M.IsCircuit C) :
C.Finite
source
theorem Matroid.finitary_iff_forall_isCircuit_finite {α : Type u_1} {M : Matroid α} :
M.Finitary ↔ ∀ (C : Set α), M.IsCircuit C → C.Finite
source
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`.

source
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`.

### IsCocircuits #

source
@[reducible, inline]
abbrev Matroid.IsCocircuit {α : Type u_1} (M : Matroid α) (K : Set α) :
Prop

A cocircuit is a circuit of the dual matroid, or equivalently the complement of a hyperplane.

Equations

- M.IsCocircuit K = M✶.IsCircuit K

Instances For

source
theorem Matroid.isCocircuit_def {α : Type u_1} {M : Matroid α} {K : Set α} :
M.IsCocircuit K ↔ M✶.IsCircuit K
source
theorem Matroid.IsCocircuit.isCircuit {α : Type u_1} {M : Matroid α} {K : Set α} (hK : M.IsCocircuit K) :
M✶.IsCircuit K
source
theorem Matroid.IsCircuit.isCocircuit {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) :
M✶.IsCocircuit C
source
theorem Matroid.IsCocircuit.nonempty {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCocircuit C) :
C.Nonempty
source
theorem Matroid.IsCocircuit.subset_ground {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCocircuit C) :
C ⊆ M.E
source
@[simp]
theorem Matroid.dual_isCocircuit_iff {α : Type u_1} {M : Matroid α} {C : Set α} :
M✶.IsCocircuit C ↔ M.IsCircuit C
source
theorem Matroid.coindep_iff_forall_subset_not_isCocircuit {α : Type u_1} {M : Matroid α} {X : Set α} :
M.Coindep X ↔ (∀ K ⊆ X, ¬M.IsCocircuit K) ∧ X ⊆ M.E
source
theorem Matroid.isCocircuit_iff_minimal {α : Type u_1} {M : Matroid α} {K : Set α} :
M.IsCocircuit K ↔ Minimal (fun (X : Set α) => ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K

A cocircuit is a minimal set that intersects every base.

source
theorem Matroid.isCocircuit_iff_minimal_compl_nonspanning {α : Type u_1} {M : Matroid α} {K : Set α} :
M.IsCocircuit K ↔ Minimal (fun (X : Set α) => ¬M.Spanning (M.E \ X)) K

A cocircuit is a minimal set whose complement is nonspanning.

source
theorem Matroid.IsBase.compl_closure_diff_singleton_isCocircuit {α : Type u_1} {M : Matroid α} {e : α} {B : Set α} (hB : M.IsBase B) (he : e ∈ B) :
M.IsCocircuit (M.E \ M.closure (B \ {e}))

For an element `e` of a base `B`, the complement of the closure of `B \ {e}` is a cocircuit.

source
theorem Matroid.isCocircuit_iff_minimal_compl_nonspanning' {α : Type u_1} {M : Matroid α} {K : Set α} :
M.IsCocircuit K ↔ Minimal (fun (X : Set α) => ¬M.Spanning (M.E \ X) ∧ X ⊆ M.E) K

A version of `Matroid.isCocircuit_iff_minimal_compl_nonspanning` with a support assumption in the minimality.

source
theorem Matroid.IsCircuit.inter_isCocircuit_ne_singleton {α : Type u_1} {M : Matroid α} {C : Set α} {e : α} {K : Set α} (hC : M.IsCircuit C) (hK : M.IsCocircuit K) :
C ∩ K ≠ {e}

A cocircuit and a circuit cannot meet in exactly one element.

source
theorem Matroid.IsCircuit.isCocircuit_inter_nontrivial {α : Type u_1} {M : Matroid α} {C K : Set α} (hC : M.IsCircuit C) (hK : M.IsCocircuit K) (hCK : (C ∩ K).Nonempty) :
(C ∩ K).Nontrivial
source
theorem Matroid.IsCircuit.isCocircuit_disjoint_or_nontrivial_inter {α : Type u_1} {M : Matroid α} {C K : Set α} (hC : M.IsCircuit C) (hK : M.IsCocircuit K) :
Disjoint C K ∨ (C ∩ K).Nontrivial
source
theorem Matroid.dual_rankPos_iff_exists_isCircuit {α : Type u_1} {M : Matroid α} :
M✶.RankPos ↔ ∃ (C : Set α), M.IsCircuit C
source
theorem Matroid.IsCircuit.dual_rankPos {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) :
M✶.RankPos
source
theorem Matroid.exists_isCircuit {α : Type u_1} {M : Matroid α} [M✶.RankPos] :
∃ (C : Set α), M.IsCircuit C
source
theorem Matroid.rankPos_iff_exists_isCocircuit {α : Type u_1} {M : Matroid α} :
M.RankPos ↔ ∃ (K : Set α), M.IsCocircuit K
source
def Matroid.fundCocircuit {α : Type u_1} (M : Matroid α) (e : α) (B : Set α) :
Set α

The fundamental cocircuit for `B` and `e`: that is, the unique cocircuit `K` of `M` for which `K ∩ B = {e}`. Should be used when `B` is a base and `e ∈ B`. Has the junk value `{e}` if `e ∉ B` or `e ∉ M.E`.

Equations

- M.fundCocircuit e B = M✶.fundCircuit e (M✶.E \ B)

Instances For

source
theorem Matroid.fundCocircuit_isCocircuit {α : Type u_1} {M : Matroid α} {e : α} {B : Set α} (he : e ∈ B) (hB : M.IsBase B) :
M.IsCocircuit (M.fundCocircuit e B)
source
theorem Matroid.mem_fundCocircuit {α : Type u_1} (M : Matroid α) (e : α) (B : Set α) :
e ∈ M.fundCocircuit e B
source
theorem Matroid.fundCocircuit_subset_insert_compl {α : Type u_1} (M : Matroid α) (e : α) (B : Set α) :
M.fundCocircuit e B ⊆ insert e (M.E \ B)
source
theorem Matroid.fundCocircuit_inter_eq {α : Type u_1} {e : α} (M : Matroid α) {B : Set α} (he : e ∈ B) :
M.fundCocircuit e B ∩ B = {e}
source
theorem Matroid.fundCocircuit_eq_of_notMem_ground {α : Type u_1} {M : Matroid α} {e : α} (X : Set α) (he : e ∉ M.E) :
M.fundCocircuit e X = {e}

The fundamental cocircuit of `X` and `e` has the junk value `{e}` if `e ∉ M.E`

source
@[deprecated Matroid.fundCocircuit_eq_of_notMem_ground (since := "2025-05-23")]
theorem Matroid.fundCocircuit_eq_of_not_mem_ground {α : Type u_1} {M : Matroid α} {e : α} (X : Set α) (he : e ∉ M.E) :
M.fundCocircuit e X = {e}

Alias of `Matroid.fundCocircuit_eq_of_notMem_ground`.

The fundamental cocircuit of `X` and `e` has the junk value `{e}` if `e ∉ M.E`

source
theorem Matroid.fundCocircuit_eq_of_notMem {α : Type u_1} {X : Set α} {e : α} (M : Matroid α) (heX : e ∉ X) :
M.fundCocircuit e X = {e}

The fundamental cocircuit of `X` and `e` has the junk value `{e}` if `e ∉ X`

source
@[deprecated Matroid.fundCocircuit_eq_of_notMem (since := "2025-05-23")]
theorem Matroid.fundCocircuit_eq_of_not_mem {α : Type u_1} {X : Set α} {e : α} (M : Matroid α) (heX : e ∉ X) :
M.fundCocircuit e X = {e}

Alias of `Matroid.fundCocircuit_eq_of_notMem`.

The fundamental cocircuit of `X` and `e` has the junk value `{e}` if `e ∉ X`

source
theorem Matroid.Indep.exists_isCocircuit_inter_eq_mem {α : Type u_1} {M : Matroid α} {I : Set α} {e : α} (hI : M.Indep I) (heI : e ∈ I) :
∃ (K : Set α), M.IsCocircuit K ∧ K ∩ I = {e}

For every element `e` of an independent set `I`, there is a cocircuit whose intersection with `I` is `{e}`.

source
theorem Matroid.IsBase.mem_fundCocircuit_iff_mem_fundCircuit {α : Type u_1} {M : Matroid α} {B : Set α} {e f : α} (hB : M.IsBase B) :
e ∈ M.fundCocircuit f B ↔ f ∈ M.fundCircuit e B

Fundamental circuits and cocircuits of a base `B` play dual roles; `e` belongs to the fundamental cocircuit for `B` and `f` if and only if `f` belongs to the fundamental circuit for `e` and `B`. This statement isn't so reasonable unless `f ∈ B` and `e ∉ B`, but holds due to junk values even without these assumptions.