Documentation

Mathlib.Data.Matroid.Loop

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

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.IsNonloop e means that e ∈ M.E, but e is not a loop of M.

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

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

M.loops ⊆ M.E

def Matroid.IsLoop {α : Type u_1} (M : Matroid α) (e : α) :

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

Equations

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

Instances For

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.

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

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

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

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

@[simp]

theorem Matroid.closure_loops {α : Type u_1} (M : Matroid α) :

M.closure M.loops = M.loops

@[simp]

theorem Matroid.closure_union_loops_eq {α : Type u_1} (M : Matroid α) (X : Set α) :

M.closure (X ∪ M.loops) = M.closure X

@[simp]

theorem Matroid.closure_loops_union_eq {α : Type u_1} (M : Matroid α) (X : Set α) :

M.closure (M.loops ∪ X) = M.closure X

@[simp]

theorem Matroid.closure_diff_loops_eq {α : Type u_1} (M : Matroid α) (X : Set α) :

M.closure (X \ M.loops) = M.closure X

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

theorem Matroid.IsLoop.isLoop_isRestriction {α : Type u_1} {M N : Matroid α} {e : α} (he : M.IsLoop e) (hNM : N.IsRestriction M) (heN : e ∈ N.E) :

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

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

@[simp]

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

structure Matroid.IsNonloop {α : Type u_1} (M : Matroid α) (e : α) :

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

theorem Matroid.isNonloop_iff {α : Type u_1} (M : Matroid α) (e : α) :

M.IsNonloop e ↔ ¬M.IsLoop e ∧ e ∈ M.E

theorem Matroid.IsLoop.not_isNonloop {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) :

¬M.IsNonloop e

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

theorem Matroid.isLoop_of_not_isNonloop {α : Type u_1} {M : Matroid α} {e : α} (he : e ∈ M.E := by aesop_mat) (h : ¬M.IsNonloop e) :

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

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

theorem Matroid.isNonloop_iff_mem_compl_loops {α : Type u_1} {M : Matroid α} {e : α} :

M.IsNonloop e ↔ e ∈ M.E \ M.loops

theorem Matroid.setOf_isNonloop_eq {α : Type u_1} (M : Matroid α) :

{e : α | M.IsNonloop e} = M.E \ M.loops

theorem Matroid.not_isNonloop_iff_closure {α : Type u_1} {M : Matroid α} {e : α} :

¬M.IsNonloop e ↔ M.closure {e} = M.loops

theorem Matroid.isLoop_or_isNonloop {α : Type u_1} (M : Matroid α) (e : α) (he : e ∈ M.E := by aesop_mat) :

M.IsLoop e ∨ M.IsNonloop e

@[simp]

theorem Matroid.indep_singleton {α : Type u_1} {M : Matroid α} {e : α} :

M.Indep {e} ↔ M.IsNonloop e

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.

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.

theorem Matroid.Indep.isNonloop_of_mem {α : Type u_1} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (h : e ∈ I) :

theorem Matroid.IsNonloop.exists_mem_isBase {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsNonloop e) :

∃ (B : Set α), M.IsBase B ∧ e ∈ B

theorem Matroid.IsCocircuit.isNonloop_of_mem {α : Type u_1} {M : Matroid α} {e : α} {K : Set α} (hK : M.IsCocircuit K) (he : e ∈ K) :

theorem Matroid.IsCircuit.isNonloop_of_mem {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (hC : M.IsCircuit C) (hC' : C.Nontrivial) (he : e ∈ C) :

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

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

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

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}

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}

theorem Matroid.IsNonloop.isNonloop_of_mem_closure {α : Type u_1} {M : Matroid α} {e f : α} (he : M.IsNonloop e) (hef : e ∈ M.closure {f}) :

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}

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.

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}

theorem Matroid.exists_isNonloop {α : Type u_1} (M : Matroid α) [M.RankPos] :

∃ (e : α), M.IsNonloop e

theorem Matroid.IsNonloop.rankPos {α : Type u_1} {M : Matroid α} {e : α} (h : M.IsNonloop e) :

@[simp]

theorem Matroid.restrict_isNonloop_iff {α : Type u_1} {M : Matroid α} {e : α} {R : Set α} :

(M.restrict R).IsNonloop e ↔ M.IsNonloop e ∧ e ∈ R

theorem Matroid.IsNonloop.of_restrict {α : Type u_1} {M : Matroid α} {e : α} {R : Set α} (h : (M.restrict R).IsNonloop e) :

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

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

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

@[simp]

theorem Matroid.freeOn_isNonloop_iff {α : Type u_1} {e : α} {E : Set α} :

(freeOn E).IsNonloop e ↔ e ∈ E

@[simp]

theorem Matroid.uniqueBaseOn_isNonloop_iff {α : Type u_1} {e : α} {I E : Set α} :

(uniqueBaseOn I E).IsNonloop e ↔ e ∈ I ∩ E

theorem Matroid.IsNonloop.exists_mem_isCocircuit {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsNonloop e) :

∃ (K : Set α), M.IsCocircuit K ∧ e ∈ K

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