Matroid 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. This file defines loops, and provides API for interacting with them.

Main Declarations

• For M : Matroid α, M.loops is the set M.closure ∅.
• For M : Matroid α and e : α, M.IsLoop e means that e is a loop of M, defined as the statement e ∈ M.loops.

@[reducible, inline]

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

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

Equations

• M.loops = M.closure ∅

theorem Matroid.loops_subset_ground {α : Type u_1} (M : Matroid α) : M.loops ⊆ M.E

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)

theorem Matroid.isLoop_iff {α : Type u_1} {M : Matroid α} {e : α} : M.IsLoop e ↔ e ∈ M.loops

theorem Matroid.closure_empty {α : Type u_1} (M : Matroid α) : M.closure ∅ = M.loops

theorem Matroid.IsLoop.mem_ground {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) : e ∈ M.E

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

@[simp]

theorem Matroid.singleton_dep {α : Type u_1} {M : Matroid α} {e : α} : M.Dep {e} ↔ M.IsLoop e

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.

@[simp]

theorem Matroid.singleton_not_indep {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) : ¬M.Indep {e} ↔ M.IsLoop e

@[simp]

theorem Matroid.singleton_isCircuit {α : Type u_1} {M : Matroid α} {e : α} : M.IsCircuit {e} ↔ M.IsLoop e

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.

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

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

theorem Matroid.IsLoop.mem_closure {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) (X : Set α) : e ∈ M.closure X

theorem Matroid.IsLoop.mem_of_isFlat {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) {F : Set α} (hF : M.IsFlat F) : e ∈ F

theorem Matroid.IsFlat.loops_subset {α : Type u_1} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) : M.loops ⊆ F

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

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

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

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}

theorem Matroid.Indep.disjoint_loops {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : Disjoint I M.loops

theorem Matroid.Indep.eq_empty_of_subset_loops {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) (h : I ⊆ M.loops) : I = ∅

@[simp]

theorem Matroid.isBasis_loops_iff {α : Type u_1} {M : Matroid α} {I : Set α} : M.IsBasis I M.loops ↔ I = ∅

theorem Matroid.closure_eq_loops_of_subset {α : Type u_1} {M : Matroid α} {X : Set α} (h : X ⊆ M.loops) : M.closure X = M.loops

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 = ∅

theorem Matroid.IsLoop.closure {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) : M.closure {e} = M.loops

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

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

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

theorem Matroid.restrict_loops_eq {α : Type u_1} {M : Matroid α} {R : Set α} (hR : R ⊆ M.E) : (M.restrict R).loops = M.loops ∩ R

@[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)

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

theorem Matroid.IsLoop.of_isRestriction {α : Type u_1} {M N : Matroid α} {e : α} (he : N.IsLoop e) (hNM : N.IsRestriction M) : M.IsLoop e

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

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

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

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

theorem Matroid.comap_loops {α : Type u_1} {β : Type u_2} {M : Matroid β} {f : α → β} : (M.comap f).loops = f ⁻¹' M.loops

@[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)

@[simp]

theorem Matroid.loopyOn_isLoop_iff {α : Type u_1} {e : α} {E : Set α} : (loopyOn E).IsLoop e ↔ e ∈ E

@[simp]

theorem Matroid.freeOn_not_isLoop {α : Type u_1} (E : Set α) (e : α) : ¬(freeOn E).IsLoop e

@[simp]

theorem Matroid.uniqueBaseOn_isLoop_iff {α : Type u_1} {e : α} {I E : Set α} : (uniqueBaseOn I E).IsLoop e ↔ e ∈ E \ I