# Matroid loops and coloops #

## Loops #

A 'loop' of a matroid `M` is an element `e` satisfying one of the following equivalent conditions:

- `e ∈ M.closure ∅`;
- `{e}` is dependent in `M`;
- `{e}` is a circuit of `M`;
- no base of `M` contains `e`.

In many mathematical contexts, loops can be thought of as 'trivial' or 'zero' elements; For linearly representable matroids, they correspond to the zero vector, and for graphic matroids, they correspond to edges incident with just one vertex (aka 'loops'). As trivial as they are, loops can be created from matroids with no loops by taking minors or duals, so in many contexts it is unreasonable to simply forbid loops from appearing. For `M : Matroid α`, this file defines a set `Matroid.loops M : Set α`, as well as predicates `Matroid.IsLoop M : α → Prop` and `Matroid.IsNonloop M : α → Prop`, and provides API for interacting with them.

## Coloops #

The dual notion of a loop is a 'coloop'. Geometrically, these can be thought of elements that are skew to the remainder of the matroid. Coloops in graphic matroids are 'bridge' edges of the graph, and coloops in linearly representable matroids are vectors not spanned by the other vectors in the matroid. Coloops also have many equivalent definitions in abstract matroid language; a coloop is an element of `M.E` if any of the following equivalent conditions holds :

- `e` is a loop of `M✶`;
- `{e}` is a cocircuit of `M`;
- `e` is in no circuit of `M`;
- `e` is in every base of `M`;
- for all `X ⊆ M.E`, `e ∈ X ↔ e ∈ M.closure X`,
- `M.E \ {e}` is nonspanning.

## Main Declarations #

For `M` : Matroid `α`:

- `M.loops` is the set `M.closure ∅`.
- `M.IsLoop e` means that `e : α` is a loop of `M`, defined as the statement `e ∈ M.loops`.
- `M.isLoop_tfae` gives a number of properties that are equivalent to `IsLoop`.
- `M.IsNonloop e` means that `e ∈ M.E`, but `e` is not a loop of `M`.
- `M.IsColoop e` means that `e` is a loop of `M✶`.
- `M.coloops` is the set of coloops of `M✶`.
- `M.isColoop_tfae` gives a number of properties that are equivalent to `IsColoop`.
- `M.Loopless` is a typeclass meaning `M` has no loops.
- `M.removeLoops` is the matroid obtained from `M` by restricting to its set of nonloop elements.

source
def Matroid.loops {α : Type u_1} (M : Matroid α) :
Set α

`Matroid.loops M` is the closure of the empty set.

Equations

- M.loops = M.closure ∅

Instances For

source
theorem Matroid.loops_subset_ground {α : Type u_1} (M : Matroid α) :
M.loops ⊆ M.E
source
def Matroid.IsLoop {α : Type u_1} (M : Matroid α) (e : α) :
Prop

A 'loop' is a member of the closure of the empty set

Equations

- M.IsLoop e = (e ∈ M.loops)

Instances For

source
theorem Matroid.isLoop_iff {α : Type u_1} {M : Matroid α} {e : α} :
M.IsLoop e ↔ e ∈ M.loops
source
theorem Matroid.closure_empty {α : Type u_1} (M : Matroid α) :
M.closure ∅ = M.loops
source
theorem Matroid.IsLoop.mem_ground {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) :
e ∈ M.E
source
theorem Matroid.isLoop_tfae {α : Type u_1} (M : Matroid α) (e : α) :
[M.IsLoop e, e ∈ M.closure ∅, M.IsCircuit {e}, M.Dep {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B].TFAE
source
@[simp]
theorem Matroid.singleton_dep {α : Type u_1} {M : Matroid α} {e : α} :
M.Dep {e} ↔ M.IsLoop e
source
theorem Matroid.IsLoop.dep {α : Type u_1} {M : Matroid α} {e : α} :
M.IsLoop e → M.Dep {e}

Alias of the reverse direction of `Matroid.singleton_dep`.

source
theorem Matroid.singleton_not_indep {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :
¬M.Indep {e} ↔ M.IsLoop e
source
@[simp]
theorem Matroid.singleton_isCircuit {α : Type u_1} {M : Matroid α} {e : α} :
M.IsCircuit {e} ↔ M.IsLoop e
source
theorem Matroid.IsLoop.isCircuit {α : Type u_1} {M : Matroid α} {e : α} :
M.IsLoop e → M.IsCircuit {e}

Alias of the reverse direction of `Matroid.singleton_isCircuit`.

source
theorem Matroid.isLoop_iff_forall_mem_compl_isBase {α : Type u_1} {M : Matroid α} {e : α} :
M.IsLoop e ↔ ∀ (B : Set α), M.IsBase B → e ∈ M.E \ B
source
theorem Matroid.isLoop_iff_forall_notMem_isBase {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :
M.IsLoop e ↔ ∀ (B : Set α), M.IsBase B → e ∉ B
source
@[deprecated Matroid.isLoop_iff_forall_notMem_isBase (since := "2025-05-23")]
theorem Matroid.isLoop_iff_forall_not_mem_isBase {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :
M.IsLoop e ↔ ∀ (B : Set α), M.IsBase B → e ∉ B

Alias of `Matroid.isLoop_iff_forall_notMem_isBase`.

source
theorem Matroid.IsLoop.mem_closure {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) (X : Set α) :
e ∈ M.closure X
source
theorem Matroid.IsLoop.mem_of_isFlat {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) {F : Set α} (hF : M.IsFlat F) :
e ∈ F
source
theorem Matroid.IsFlat.loops_subset {α : Type u_1} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) :
M.loops ⊆ F
source
theorem Matroid.IsLoop.dep_of_mem {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (he : M.IsLoop e) (h : e ∈ X) (hXE : X ⊆ M.E := by aesop_mat) :
M.Dep X
source
theorem Matroid.IsLoop.not_indep_of_mem {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (he : M.IsLoop e) (h : e ∈ X) :
¬M.Indep X
source
theorem Matroid.IsLoop.notMem_of_indep {α : Type u_1} {M : Matroid α} {e : α} {I : Set α} (he : M.IsLoop e) (hI : M.Indep I) :
e ∉ I
source
@[deprecated Matroid.IsLoop.notMem_of_indep (since := "2025-05-23")]
theorem Matroid.IsLoop.not_mem_of_indep {α : Type u_1} {M : Matroid α} {e : α} {I : Set α} (he : M.IsLoop e) (hI : M.Indep I) :
e ∉ I

Alias of `Matroid.IsLoop.notMem_of_indep`.

source
theorem Matroid.IsLoop.eq_of_isCircuit_mem {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (he : M.IsLoop e) (hC : M.IsCircuit C) (h : e ∈ C) :
C = {e}
source
theorem Matroid.Indep.disjoint_loops {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) :
Disjoint I M.loops
source
theorem Matroid.Indep.eq_empty_of_subset_loops {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (h : I ⊆ M.loops) :
I = ∅
source
@[simp]
theorem Matroid.isBasis_loops_iff {α : Type u_1} {M : Matroid α} {I : Set α} :
M.IsBasis I M.loops ↔ I = ∅
source
theorem Matroid.closure_eq_loops_of_subset {α : Type u_1} {M : Matroid α} {X : Set α} (h : X ⊆ M.loops) :
M.closure X = M.loops
source
theorem Matroid.isBasis_iff_empty_of_subset_loops {α : Type u_1} {M : Matroid α} {X I : Set α} (hX : X ⊆ M.loops) :
M.IsBasis I X ↔ I = ∅
source
theorem Matroid.IsLoop.closure {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) :
M.closure {e} = M.loops
source
theorem Matroid.isLoop_iff_closure_eq_loops_and_mem_ground {α : Type u_1} {M : Matroid α} {e : α} :
M.IsLoop e ↔ M.closure {e} = M.loops ∧ e ∈ M.E
source
theorem Matroid.isLoop_iff_closure_eq_loops {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :
M.IsLoop e ↔ M.closure {e} = M.loops
source
@[simp]
theorem Matroid.closure_loops {α : Type u_1} (M : Matroid α) :
M.closure M.loops = M.loops
source
@[simp]
theorem Matroid.closure_union_loops_eq {α : Type u_1} (M : Matroid α) (X : Set α) :
M.closure (X ∪ M.loops) = M.closure X
source
@[simp]
theorem Matroid.closure_loops_union_eq {α : Type u_1} (M : Matroid α) (X : Set α) :
M.closure (M.loops ∪ X) = M.closure X
source
@[simp]
theorem Matroid.closure_diff_loops_eq {α : Type u_1} (M : Matroid α) (X : Set α) :
M.closure (X \ M.loops) = M.closure X
source
theorem Matroid.restrict_loops_eq' {α : Type u_1} (M : Matroid α) (R : Set α) :
(M.restrict R).loops = M.loops ∩ R ∪ R \ M.E

A version of `restrict_loops_eq` without the hypothesis that `R ⊆ M.E`

source
theorem Matroid.restrict_loops_eq {α : Type u_1} {M : Matroid α} {R : Set α} (hR : R ⊆ M.E) :
(M.restrict R).loops = M.loops ∩ R
source
@[simp]
theorem Matroid.restrict_isLoop_iff {α : Type u_1} {M : Matroid α} {e : α} {R : Set α} :
(M.restrict R).IsLoop e ↔ e ∈ R ∧ (M.IsLoop e ∨ e ∉ M.E)
source
theorem Matroid.IsRestriction.isLoop_iff {α : Type u_1} {M N : Matroid α} {e : α} (hNM : N.IsRestriction M) :
N.IsLoop e ↔ e ∈ N.E ∧ M.IsLoop e
source
theorem Matroid.IsLoop.of_isRestriction {α : Type u_1} {M N : Matroid α} {e : α} (he : N.IsLoop e) (hNM : N.IsRestriction M) :
M.IsLoop e
source
theorem Matroid.IsLoop.isLoop_isRestriction {α : Type u_1} {M N : Matroid α} {e : α} (he : M.IsLoop e) (hNM : N.IsRestriction M) (heN : e ∈ N.E) :
N.IsLoop e
source
@[simp]
theorem Matroid.map_loops {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : α → β} {hf : Set.InjOn f M.E} :
(M.map f hf).loops = f '' M.loops
source
@[simp]
theorem Matroid.map_isLoop_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {e : α} {f : α → β} {hf : Set.InjOn f M.E} (he : e ∈ M.E := by aesop_mat) :
(M.map f hf).IsLoop (f e) ↔ M.IsLoop e
source
@[simp]
theorem Matroid.mapEmbedding_isLoop_iff {α : Type u_1} {β : Type u_2} {M : Matroid α} {e : α} {f : α ↪ β} :
(M.mapEmbedding f).IsLoop (f e) ↔ M.IsLoop e
source
@[simp]
theorem Matroid.comap_loops {α : Type u_1} {β : Type u_2} {M : Matroid β} {f : α → β} :
(M.comap f).loops = f ⁻¹' M.loops
source
@[simp]
theorem Matroid.comap_isLoop_iff {α : Type u_1} {β : Type u_2} {e : α} {M : Matroid β} {f : α → β} :
(M.comap f).IsLoop e ↔ M.IsLoop (f e)
source
@[simp]
theorem Matroid.loopyOn_isLoop_iff {α : Type u_1} {e : α} {E : Set α} :
(loopyOn E).IsLoop e ↔ e ∈ E
source
theorem Matroid.eq_loopyOn_iff_loops {α : Type u_1} {M : Matroid α} {E : Set α} :
M = loopyOn E ↔ M.loops = E ∧ M.E = E
source
theorem Matroid.restrict_subset_loops_eq {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.loops) :
M.restrict X = loopyOn X
source
@[simp]
theorem Matroid.freeOn_not_isLoop {α : Type u_1} (E : Set α) (e : α) :
¬(freeOn E).IsLoop e
source
@[simp]
theorem Matroid.uniqueBaseOn_isLoop_iff {α : Type u_1} {e : α} {I E : Set α} :
(uniqueBaseOn I E).IsLoop e ↔ e ∈ E \ I
source
theorem Matroid.eq_loopyOn_iff_loops_eq {α : Type u_1} {M : Matroid α} {E : Set α} :
M = loopyOn E ↔ M.loops = E ∧ M.E = E
source
structure Matroid.IsNonloop {α : Type u_1} (M : Matroid α) (e : α) :
Prop

`M.IsNonloop e` means that `e` is an element of `M.E` but not a loop of `M`.

- not_isLoop : ¬M.IsLoop e
- mem_ground : e ∈ M.E

Instances For

source
theorem Matroid.isNonloop_iff {α : Type u_1} (M : Matroid α) (e : α) :
M.IsNonloop e ↔ ¬M.IsLoop e ∧ e ∈ M.E
source
theorem Matroid.IsLoop.not_isNonloop {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) :
¬M.IsNonloop e
source
theorem Matroid.compl_loops_eq {α : Type u_1} (M : Matroid α) :
M.E \ M.loops = {e : α | M.IsNonloop e}
source
theorem Matroid.isNonloop_of_not_isLoop {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) (h : ¬M.IsLoop e) :
M.IsNonloop e
source
theorem Matroid.isLoop_of_not_isNonloop {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) (h : ¬M.IsNonloop e) :
M.IsLoop e
source
@[simp]
theorem Matroid.not_isLoop_iff {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :
¬M.IsLoop e ↔ M.IsNonloop e
source
@[simp]
theorem Matroid.not_isNonloop_iff {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :
¬M.IsNonloop e ↔ M.IsLoop e
source
theorem Matroid.isNonloop_iff_mem_compl_loops {α : Type u_1} {M : Matroid α} {e : α} :
M.IsNonloop e ↔ e ∈ M.E \ M.loops
source
theorem Matroid.setOf_isNonloop_eq {α : Type u_1} (M : Matroid α) :
{e : α | M.IsNonloop e} = M.E \ M.loops
source
theorem Matroid.not_isNonloop_iff_closure {α : Type u_1} {M : Matroid α} {e : α} :
¬M.IsNonloop e ↔ M.closure {e} = M.loops
source
theorem Matroid.isLoop_or_isNonloop {α : Type u_1} (M : Matroid α) (e : α) (he : e ∈ M.E := by aesop_mat) :
M.IsLoop e ∨ M.IsNonloop e
source
@[simp]
theorem Matroid.indep_singleton {α : Type u_1} {M : Matroid α} {e : α} :
M.Indep {e} ↔ M.IsNonloop e
source
theorem Matroid.IsNonloop.indep {α : Type u_1} {M : Matroid α} {e : α} :
M.IsNonloop e → M.Indep {e}

Alias of the reverse direction of `Matroid.indep_singleton`.

source
theorem Matroid.Indep.isNonloop {α : Type u_1} {M : Matroid α} {e : α} :
M.Indep {e} → M.IsNonloop e

Alias of the forward direction of `Matroid.indep_singleton`.

source
theorem Matroid.Indep.isNonloop_of_mem {α : Type u_1} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (h : e ∈ I) :
M.IsNonloop e
source
theorem Matroid.IsNonloop.exists_mem_isBase {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsNonloop e) :
∃ (B : Set α), M.IsBase B ∧ e ∈ B
source
theorem Matroid.IsCocircuit.isNonloop_of_mem {α : Type u_1} {M : Matroid α} {e : α} {K : Set α} (hK : M.IsCocircuit K) (he : e ∈ K) :
M.IsNonloop e
source
theorem Matroid.IsCircuit.isNonloop_of_mem {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (hC : M.IsCircuit C) (hC' : C.Nontrivial) (he : e ∈ C) :
M.IsNonloop e
source
theorem Matroid.IsCircuit.isNonloop_of_mem_of_one_lt_card {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (hC : M.IsCircuit C) (h : 1 < C.encard) (he : e ∈ C) :
M.IsNonloop e
source
theorem Matroid.isNonloop_of_notMem_closure {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (h : e ∉ M.closure X) (he : e ∈ M.E := by aesop_mat) :
M.IsNonloop e
source
@[deprecated Matroid.isNonloop_of_notMem_closure (since := "2025-05-23")]
theorem Matroid.isNonloop_of_not_mem_closure {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (h : e ∉ M.closure X) (he : e ∈ M.E := by aesop_mat) :
M.IsNonloop e

Alias of `Matroid.isNonloop_of_notMem_closure`.

source
theorem Matroid.isNonloop_iff_notMem_loops {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :
M.IsNonloop e ↔ e ∉ M.loops
source
@[deprecated Matroid.isNonloop_iff_notMem_loops (since := "2025-05-23")]
theorem Matroid.isNonloop_iff_not_mem_loops {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :
M.IsNonloop e ↔ e ∉ M.loops

Alias of `Matroid.isNonloop_iff_notMem_loops`.

source
theorem Matroid.IsNonloop.mem_closure_singleton {α : Type u_1} {M : Matroid α} {e f : α} (he : M.IsNonloop e) (hef : e ∈ M.closure {f}) :
f ∈ M.closure {e}
source
theorem Matroid.IsNonloop.mem_closure_comm {α : Type u_1} {M : Matroid α} {e f : α} (he : M.IsNonloop e) (hf : M.IsNonloop f) :
f ∈ M.closure {e} ↔ e ∈ M.closure {f}
source
theorem Matroid.IsNonloop.isNonloop_of_mem_closure {α : Type u_1} {M : Matroid α} {e f : α} (he : M.IsNonloop e) (hef : e ∈ M.closure {f}) :
M.IsNonloop f
source
theorem Matroid.IsNonloop.closure_eq_of_mem_closure {α : Type u_1} {M : Matroid α} {e f : α} (he : M.IsNonloop e) (hef : e ∈ M.closure {f}) :
M.closure {e} = M.closure {f}
source
theorem Matroid.IsNonloop.closure_eq_closure_iff_isCircuit_of_ne {α : Type u_1} {M : Matroid α} {e f : α} (he : M.IsNonloop e) (hef : e ≠ f) :
M.closure {e} = M.closure {f} ↔ M.IsCircuit {e, f}

Two distinct nonloops with the same closure form a circuit.

source
theorem Matroid.IsNonloop.closure_eq_closure_iff_eq_or_dep {α : Type u_1} {M : Matroid α} {e f : α} (he : M.IsNonloop e) (hf : M.IsNonloop f) :
M.closure {e} = M.closure {f} ↔ e = f ∨ ¬M.Indep {e, f}
source
theorem Matroid.exists_isNonloop {α : Type u_1} (M : Matroid α) [M.RankPos] :
∃ (e : α), M.IsNonloop e
source
theorem Matroid.IsNonloop.rankPos {α : Type u_1} {M : Matroid α} {e : α} (h : M.IsNonloop e) :
M.RankPos
source
@[simp]
theorem Matroid.restrict_isNonloop_iff {α : Type u_1} {M : Matroid α} {e : α} {R : Set α} :
(M.restrict R).IsNonloop e ↔ M.IsNonloop e ∧ e ∈ R
source
theorem Matroid.IsNonloop.of_restrict {α : Type u_1} {M : Matroid α} {e : α} {R : Set α} (h : (M.restrict R).IsNonloop e) :
M.IsNonloop e
source
theorem Matroid.IsNonloop.of_isRestriction {α : Type u_1} {M N : Matroid α} {e : α} (h : N.IsNonloop e) (hNM : N.IsRestriction M) :
M.IsNonloop e
source
theorem Matroid.isNonloop_iff_restrict_of_mem {α : Type u_1} {M : Matroid α} {e : α} {R : Set α} (he : e ∈ R) :
M.IsNonloop e ↔ (M.restrict R).IsNonloop e
source
@[simp]
theorem Matroid.comap_isNonloop_iff {α : Type u_1} {β : Type u_2} {e : α} {M : Matroid β} {f : α → β} :
(M.comap f).IsNonloop e ↔ M.IsNonloop (f e)
source
@[simp]
theorem Matroid.freeOn_isNonloop_iff {α : Type u_1} {e : α} {E : Set α} :
(freeOn E).IsNonloop e ↔ e ∈ E
source
@[simp]
theorem Matroid.uniqueBaseOn_isNonloop_iff {α : Type u_1} {e : α} {I E : Set α} :
(uniqueBaseOn I E).IsNonloop e ↔ e ∈ I ∩ E
source
theorem Matroid.IsNonloop.exists_mem_isCocircuit {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsNonloop e) :
∃ (K : Set α), M.IsCocircuit K ∧ e ∈ K
source
@[simp]
theorem Matroid.closure_inter_setOf_isNonloop_eq {α : Type u_1} (M : Matroid α) (X : Set α) :
M.closure (X ∩ {e : α | M.IsNonloop e}) = M.closure X
source
def Matroid.IsColoop {α : Type u_1} (M : Matroid α) (e : α) :
Prop

A coloop is a loop of the dual matroid. See `Matroid.isColoop_tfae` for a number of equivalent definitions.

Equations

- M.IsColoop e = M✶.IsLoop e

Instances For

source
def Matroid.coloops {α : Type u_1} (M : Matroid α) :
Set α

`M.coloops` is the set of coloops of `M`.

Equations

- M.coloops = M✶.loops

Instances For

source
theorem Matroid.IsColoop.mem_ground {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsColoop e) :
e ∈ M.E
source
theorem Matroid.coloops_subset_ground {α : Type u_1} (M : Matroid α) :
M.coloops ⊆ M.E
source
theorem Matroid.isColoop_iff_mem_coloops {α : Type u_1} {M : Matroid α} {e : α} :
M.IsColoop e ↔ e ∈ M.coloops
source
@[simp]
theorem Matroid.dual_loops {α : Type u_1} {M : Matroid α} :
M✶.loops = M.coloops
source
@[simp]
theorem Matroid.dual_coloops {α : Type u_1} {M : Matroid α} :
M✶.coloops = M.loops
source
theorem Matroid.IsColoop.dual_isLoop {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsColoop e) :
M✶.IsLoop e
source
theorem Matroid.IsColoop.isCocircuit {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsColoop e) :
M.IsCocircuit {e}
source
theorem Matroid.IsLoop.dual_isColoop {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) :
M✶.IsColoop e
source
@[simp]
theorem Matroid.dual_isColoop_iff_isLoop {α : Type u_1} {M : Matroid α} {e : α} :
M✶.IsColoop e ↔ M.IsLoop e
source
@[simp]
theorem Matroid.dual_isLoop_iff_isColoop {α : Type u_1} {M : Matroid α} {e : α} :
M✶.IsLoop e ↔ M.IsColoop e
source
theorem Matroid.singleton_isCocircuit {α : Type u_1} {M : Matroid α} {e : α} :
M.IsCocircuit {e} ↔ M.IsColoop e
source
theorem Matroid.isColoop_tfae {α : Type u_1} (M : Matroid α) (e : α) :
[M.IsColoop e, e ∈ M.coloops, M.IsCocircuit {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B, (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E, ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X, ¬M.Spanning (M.E \ {e})].TFAE
source
theorem Matroid.isColoop_iff_forall_mem_isBase {α : Type u_1} {M : Matroid α} {e : α} :
M.IsColoop e ↔ ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B
source
theorem Matroid.IsBase.mem_of_isColoop {α : Type u_1} {M : Matroid α} {e : α} {B : Set α} (hB : M.IsBase B) (he : M.IsColoop e) :
e ∈ B
source
theorem Matroid.IsColoop.mem_of_isBase {α : Type u_1} {M : Matroid α} {e : α} {B : Set α} (he : M.IsColoop e) (hB : M.IsBase B) :
e ∈ B
source
theorem Matroid.IsBase.coloops_subset {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.IsBase B) :
M.coloops ⊆ B
source
theorem Matroid.IsColoop.isNonloop {α : Type u_1} {M : Matroid α} {e : α} (h : M.IsColoop e) :
M.IsNonloop e
source
theorem Matroid.IsLoop.not_isColoop {α : Type u_1} {M : Matroid α} {e : α} (h : M.IsLoop e) :
¬M.IsColoop e
source
theorem Matroid.IsColoop.notMem_isCircuit {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (he : M.IsColoop e) (hC : M.IsCircuit C) :
e ∉ C
source
@[deprecated Matroid.IsColoop.notMem_isCircuit (since := "2025-05-23")]
theorem Matroid.IsColoop.not_mem_isCircuit {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (he : M.IsColoop e) (hC : M.IsCircuit C) :
e ∉ C

Alias of `Matroid.IsColoop.notMem_isCircuit`.

source
theorem Matroid.IsCircuit.disjoint_coloops {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuit C) :
Disjoint C M.coloops
source
theorem Matroid.isColoop_iff_forall_notMem_isCircuit {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :
M.IsColoop e ↔ ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C
source
@[deprecated Matroid.isColoop_iff_forall_notMem_isCircuit (since := "2025-05-23")]
theorem Matroid.isColoop_iff_forall_not_mem_isCircuit {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :
M.IsColoop e ↔ ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C

Alias of `Matroid.isColoop_iff_forall_notMem_isCircuit`.

source
theorem Matroid.isColoop_iff_forall_mem_compl_isCircuit {α : Type u_1} {M : Matroid α} {e : α} [M✶.RankPos] :
M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C
source
theorem Matroid.IsCircuit.not_isColoop_of_mem {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (hC : M.IsCircuit C) (heC : e ∈ C) :
¬M.IsColoop e
source
theorem Matroid.isColoop_iff_forall_mem_closure_iff_mem {α : Type u_1} {M : Matroid α} {e : α} :
M.IsColoop e ↔ ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X
source
theorem Matroid.isColoop_iff_forall_mem_closure_iff_mem' {α : Type u_1} {M : Matroid α} {e : α} :
M.IsColoop e ↔ (∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X) ∧ e ∈ M.E

A version of `Matroid.isColoop_iff_forall_mem_closure_iff_mem` where we only quantify over subsets of the ground set.

source
theorem Matroid.IsColoop.mem_closure_iff_mem {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (he : M.IsColoop e) :
e ∈ M.closure X ↔ e ∈ X
source
theorem Matroid.IsColoop.mem_of_mem_closure {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (he : M.IsColoop e) (heX : e ∈ M.closure X) :
e ∈ X
source
theorem Matroid.isColoop_iff_diff_not_spanning {α : Type u_1} {M : Matroid α} {e : α} :
M.IsColoop e ↔ ¬M.Spanning (M.E \ {e})
source
theorem Matroid.IsColoop.diff_not_spanning {α : Type u_1} {M : Matroid α} {e : α} :
M.IsColoop e → ¬M.Spanning (M.E \ {e})

Alias of the forward direction of `Matroid.isColoop_iff_diff_not_spanning`.

source
theorem Matroid.isColoop_iff_diff_closure {α : Type u_1} {M : Matroid α} {e : α} :
M.IsColoop e ↔ M.closure (M.E \ {e}) ≠ M.E
source
theorem Matroid.isColoop_iff_notMem_closure_compl {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :
M.IsColoop e ↔ e ∉ M.closure (M.E \ {e})
source
@[deprecated Matroid.isColoop_iff_notMem_closure_compl (since := "2025-05-23")]
theorem Matroid.isColoop_iff_not_mem_closure_compl {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) :
M.IsColoop e ↔ e ∉ M.closure (M.E \ {e})

Alias of `Matroid.isColoop_iff_notMem_closure_compl`.

source
theorem Matroid.IsBase.isColoop_iff_forall_notMem_fundCircuit {α : Type u_1} {M : Matroid α} {e : α} {B : Set α} (hB : M.IsBase B) (he : e ∈ B) :
M.IsColoop e ↔ ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B
source
@[deprecated Matroid.IsBase.isColoop_iff_forall_notMem_fundCircuit (since := "2025-05-23")]
theorem Matroid.IsBase.isColoop_iff_forall_not_mem_fundCircuit {α : Type u_1} {M : Matroid α} {e : α} {B : Set α} (hB : M.IsBase B) (he : e ∈ B) :
M.IsColoop e ↔ ∀ x ∈ M.E \ B, e ∉ M.fundCircuit x B

Alias of `Matroid.IsBase.isColoop_iff_forall_notMem_fundCircuit`.

source
theorem Matroid.IsBasis'.inter_coloops_subset {α : Type u_1} {M : Matroid α} {X I : Set α} (hIX : M.IsBasis' I X) :
X ∩ M.coloops ⊆ I
source
theorem Matroid.IsBasis.inter_coloops_subset {α : Type u_1} {M : Matroid α} {X I : Set α} (hIX : M.IsBasis I X) :
X ∩ M.coloops ⊆ I
source
theorem Matroid.exists_mem_isCircuit_of_not_isColoop {α : Type u_1} {M : Matroid α} {e : α} (heE : e ∈ M.E) (he : ¬M.IsColoop e) :
∃ (C : Set α), M.IsCircuit C ∧ e ∈ C
source
@[simp]
theorem Matroid.closure_inter_coloops_eq {α : Type u_1} (M : Matroid α) (X : Set α) :
M.closure X ∩ M.coloops = X ∩ M.coloops
source
theorem Matroid.closure_inter_eq_of_subset_coloops {α : Type u_1} {M : Matroid α} {K : Set α} (X : Set α) (hK : K ⊆ M.coloops) :
M.closure X ∩ K = X ∩ K
source
theorem Matroid.closure_union_eq_of_subset_coloops {α : Type u_1} {M : Matroid α} {K : Set α} (X : Set α) (hK : K ⊆ M.coloops) :
M.closure (X ∪ K) = M.closure X ∪ K
source
theorem Matroid.closure_insert_isColoop_eq {α : Type u_1} {M : Matroid α} {e : α} (X : Set α) (he : M.IsColoop e) :
M.closure (insert e X) = insert e (M.closure X)
source
theorem Matroid.closure_eq_of_subset_coloops {α : Type u_1} {M : Matroid α} {K : Set α} (hK : K ⊆ M.coloops) :
M.closure K = K ∪ M.loops
source
theorem Matroid.closure_diff_eq_of_subset_coloops {α : Type u_1} {M : Matroid α} {K : Set α} (X : Set α) (hK : K ⊆ M.coloops) :
M.closure (X \ K) = M.closure X \ K
source
theorem Matroid.closure_disjoint_of_disjoint_of_subset_coloops {α : Type u_1} {M : Matroid α} {X K : Set α} (hXK : Disjoint X K) (hK : K ⊆ M.coloops) :
Disjoint (M.closure X) K
source
theorem Matroid.closure_disjoint_coloops_of_disjoint_coloops {α : Type u_1} {M : Matroid α} {X : Set α} (hX : Disjoint X M.coloops) :
Disjoint (M.closure X) M.coloops
source
theorem Matroid.closure_union_coloops_eq {α : Type u_1} (M : Matroid α) (X : Set α) :
M.closure (X ∪ M.coloops) = M.closure X ∪ M.coloops
source
theorem Matroid.IsColoop.notMem_closure_of_notMem {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (he : M.IsColoop e) (hX : e ∉ X) :
e ∉ M.closure X
source
@[deprecated Matroid.IsColoop.notMem_closure_of_notMem (since := "2025-05-23")]
theorem Matroid.IsColoop.not_mem_closure_of_not_mem {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (he : M.IsColoop e) (hX : e ∉ X) :
e ∉ M.closure X

Alias of `Matroid.IsColoop.notMem_closure_of_notMem`.

source
theorem Matroid.IsColoop.insert_indep_of_indep {α : Type u_1} {M : Matroid α} {e : α} {I : Set α} (he : M.IsColoop e) (hI : M.Indep I) :
M.Indep (insert e I)
source
theorem Matroid.union_indep_iff_indep_of_subset_coloops {α : Type u_1} {M : Matroid α} {I K : Set α} (hK : K ⊆ M.coloops) :
M.Indep (I ∪ K) ↔ M.Indep I
source
theorem Matroid.diff_indep_iff_indep_of_subset_coloops {α : Type u_1} {M : Matroid α} {I K : Set α} (hK : K ⊆ M.coloops) :
M.Indep (I \ K) ↔ M.Indep I
source
@[simp]
theorem Matroid.union_coloops_indep_iff {α : Type u_1} {M : Matroid α} {I : Set α} :
M.Indep (I ∪ M.coloops) ↔ M.Indep I
source
@[simp]
theorem Matroid.diff_coloops_indep_iff {α : Type u_1} {M : Matroid α} {I : Set α} :
M.Indep (I \ M.coloops) ↔ M.Indep I
source
theorem Matroid.coloops_indep {α : Type u_1} (M : Matroid α) :
M.Indep M.coloops
source
theorem Matroid.restrict_isColoop_iff {α : Type u_1} {M : Matroid α} {e : α} {R : Set α} (hRE : R ⊆ M.E) :
(M.restrict R).IsColoop e ↔ e ∉ M.closure (R \ {e}) ∧ e ∈ R
source
theorem Matroid.ext_indep_disjoint_loops_coloops {α : Type u_1} {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (hl : M₁.loops = M₂.loops) (hc : M₁.coloops = M₂.coloops) (h : ∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)) :
M₁ = M₂

If two matroids agree on loops and coloops, and have the same independent sets after loops/coloops are removed, they are equal.

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

A Matroid is `Loopless` if it has no loop

- loops_eq_empty : M.loops = ∅

Instances

source
theorem Matroid.loopless_iff {α : Type u_1} (M : Matroid α) :
M.Loopless ↔ M.loops = ∅
source
@[simp]
theorem Matroid.loops_eq_empty {α : Type u_1} (M : Matroid α) [M.Loopless] :
M.loops = ∅
source
theorem Matroid.isNonloop_of_loopless {α : Type u_1} {M : Matroid α} {e : α} [M.Loopless] (he : e ∈ M.E := by aesop_mat) :
M.IsNonloop e
source
theorem Matroid.subsingleton_indep {α : Type u_1} {M : Matroid α} {I : Set α} [M.Loopless] (hI : I.Subsingleton) (hIE : I ⊆ M.E := by aesop_mat) :
M.Indep I
source
theorem Matroid.not_isLoop {α : Type u_1} (M : Matroid α) [M.Loopless] (e : α) :
¬M.IsLoop e
source
theorem Matroid.loopless_iff_forall_isNonloop {α : Type u_1} {M : Matroid α} :
M.Loopless ↔ ∀ e ∈ M.E, M.IsNonloop e
source
theorem Matroid.loopless_iff_forall_not_isLoop {α : Type u_1} {M : Matroid α} :
M.Loopless ↔ ∀ e ∈ M.E, ¬M.IsLoop e
source
theorem Matroid.loopless_iff_forall_isCircuit {α : Type u_1} {M : Matroid α} :
M.Loopless ↔ ∀ (C : Set α), M.IsCircuit C → C.Nontrivial
source
theorem Matroid.Loopless.ground_eq {α : Type u_1} (M : Matroid α) [M.Loopless] :
M.E = {e : α | M.IsNonloop e}
source
theorem Matroid.IsRestriction.loopless {α : Type u_1} {M N : Matroid α} [M.Loopless] (hR : N.IsRestriction M) :
N.Loopless
source
instance Matroid.instRankPosOfNonemptyOfLoopless {α : Type u_1} {M : Matroid α} [M.Nonempty] [M.Loopless] :
M.RankPos
source
@[simp]
theorem Matroid.loopyOn_isLoopless_iff {α : Type u_1} {E : Set α} :
(loopyOn E).Loopless ↔ E = ∅
source
def Matroid.removeLoops {α : Type u_1} (M : Matroid α) :
Matroid α

The loopless matroid obtained from `M` by deleting all its loops.

Equations

- M.removeLoops = M.restrict {e : α | M.IsNonloop e}

Instances For

source
theorem Matroid.removeLoops_eq_restrict {α : Type u_1} (M : Matroid α) :
M.removeLoops = M.restrict {e : α | M.IsNonloop e}
source
theorem Matroid.removeLoops_ground_eq {α : Type u_1} (M : Matroid α) :
M.removeLoops.E = {e : α | M.IsNonloop e}
source
instance Matroid.removeLoops_loopless {α : Type u_1} (M : Matroid α) :
M.removeLoops.Loopless
source
@[simp]
theorem Matroid.removeLoops_eq_self {α : Type u_1} (M : Matroid α) [M.Loopless] :
M.removeLoops = M
source
theorem Matroid.removeLoops_eq_self_iff {α : Type u_1} {M : Matroid α} :
M.removeLoops = M ↔ M.Loopless
source
theorem Matroid.removeLoops_isRestriction {α : Type u_1} (M : Matroid α) :
M.removeLoops.IsRestriction M
source
theorem Matroid.eq_restrict_removeLoops {α : Type u_1} (M : Matroid α) :
M.removeLoops.restrict M.E = M
source
@[simp]
theorem Matroid.removeLoops_indep_eq {α : Type u_1} {M : Matroid α} :
M.removeLoops.Indep = M.Indep
source
@[simp]
theorem Matroid.removeLoops_isBasis'_eq {α : Type u_1} {M : Matroid α} :
M.removeLoops.IsBasis' = M.IsBasis'
source
@[simp]
theorem Matroid.removeLoops_isBase_eq {α : Type u_1} {M : Matroid α} :
M.removeLoops.IsBase = M.IsBase
source
@[simp]
theorem Matroid.removeLoops_isNonloop_eq {α : Type u_1} {M : Matroid α} :
M.removeLoops.IsNonloop = M.IsNonloop
source
theorem Matroid.IsNonloop.removeLoops_isNonloop {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsNonloop e) :
M.removeLoops.IsNonloop e
source
theorem Matroid.removeLoops_idem {α : Type u_1} (M : Matroid α) :
M.removeLoops.removeLoops = M.removeLoops
source
theorem Matroid.removeLoops_restrict_eq_restrict {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ {e : α | M.IsNonloop e}) :
M.removeLoops.restrict X = M.restrict X
source
@[simp]
theorem Matroid.restrict_univ_removeLoops_eq {α : Type u_1} {M : Matroid α} :
(M.restrict Set.univ).removeLoops = M.removeLoops
source
theorem Matroid.IsRestriction.isRestriction_removeLoops {α : Type u_1} {M N : Matroid α} (hNM : N.IsRestriction M) [N.Loopless] :
N.IsRestriction M.removeLoops
source
theorem Matroid.removeLoops_mono_isRestriction {α : Type u_1} {M N : Matroid α} (hNM : N.IsRestriction M) :
N.removeLoops.IsRestriction M.removeLoops