Matroid Closure

A Flat of a matroid M is a combinatorial analogue of a subspace of a vector space, and is defined to be a subset F of the ground set of M such that for each basis I for M, every set having I as a basis is contained in F.

The closure of a set X in a matroid M is the intersection of all flats of M containing X. This is a combinatorial analogue of the linear span of a set of vectors.

For M : Matroid α, this file defines a predicate M.Flat : Set α → Prop and a function M.closure : Set α → Set α corresponding to these notions, and develops API for the latter. API for Matroid.Flat will appear in another file; we include the definition here since it is used in the definition of Matroid.closure.

Main definitions

• For M : Matroid α and F : Set α, M.Flat F means that F is a flat of M.
• For M : Matroid α and X : Set α, M.closure X is the closure of X in M.
• For M : Matroid α and X : ↑(Iic M.E) (i.e. a bundled subset of M.E), M.subtypeClosure X is the closure of X, viewed as a term in ↑(Iic M.E). This is a ClosureOperator on ↑(Iic M.E).

Implementation details

If X : Set α satisfies X ⊆ M.E, then it is clear how M.closure X should be defined. But M.closure X also needs to be defined for all X : Set α, so a convention is needed for how it handles sets containing junk elements outside M.E. All such choices come with tradeoffs. Provided that M.closure X has already been defined for X ⊆ M.E, the two best candidates for extending it to all X seem to be:

(1) The function for which M.closure X = M.closure (X ∩ M.E) for all X : Set α

(2) The function for which M.closure X = M.closure (X ∩ M.E) ∪ X for all X : Set α

For both options, the function closure is monotone and idempotent with no assumptions on X.

Choice (1) has the advantage that M.closure X ⊆ M.E holds for all X without the assumption that X ⊆ M.E, which is very nice for aesop_mat. It is also fairly convenient to rewrite M.closure X to M.closure (X ∩ M.E) when one needs to work with a subset of the ground set. Its disadvantage is that the statement X ⊆ M.closure X is only true provided that X ⊆ M.E.

Choice (2) has the reverse property: we would have X ⊆ M.closure X for all X, but the condition M.closure X ⊆ M.E requires X ⊆ M.E to hold. It has a couple of other advantages too: is is actually the closure function of a matroid on α with ground set univ (specifically, the direct sum of M and a free matroid on M.Eᶜ), and because of this, it is an example of a ClosureOperator on α, which in turn gives access to nice existing API for both ClosureOperator and GaloisInsertion. This also relates to flats; F ⊆ M.E ∧ ClosureOperator.IsClosed F is equivalent to M.Flat F. (All of this fails for choice (1), since X ⊆ M.closure X is required for a ClosureOperator, but isn't true for non-subsets of M.E)

The API that choice (2) would offer is very beguiling, but after extensive experimentation in an external repo, it seems that (1) is far less rough around the edges in practice, so we go with (1). It may be helpful at some point to define a primed version Matroid.closure' : ClosureOperator (Set α) corresponding to choice (2). Failing that, the ClosureOperator/GaloisInsertion API is still available on the subtype ↑(Iic M.E) via Matroid.SubtypeClosure, albeit less elegantly.

theorem Matroid.flat_iff {α : Type u_2} (M : Matroid α) (F : Set α) : M.Flat F ↔ (∀ ⦃I X : Set α⦄, M.Basis I F → M.Basis I X → X ⊆ F) ∧ F ⊆ M.E

structure Matroid.Flat {α : Type u_2} (M : Matroid α) (F : Set α) : Prop

A flat is a maximal set having a given basis

• subset_of_basis_of_basis : ∀ ⦃I X : Set α⦄, M.Basis I F → M.Basis I X → X ⊆ F
• subset_ground : F ⊆ M.E

theorem Matroid.Flat.subset_of_basis_of_basis {α : Type u_2} {M : Matroid α} {F : Set α} (self : M.Flat F) ⦃I : Set α⦄ ⦃X : Set α⦄ : M.Basis I F → M.Basis I X → X ⊆ F

theorem Matroid.Flat.subset_ground {α : Type u_2} {M : Matroid α} {F : Set α} (self : M.Flat F) : F ⊆ M.E

@[simp]

theorem Matroid.ground_flat {α : Type u_2} (M : Matroid α) : M.Flat M.E

theorem Matroid.Flat.iInter {α : Type u_2} {M : Matroid α} {ι : Type u_3} [Nonempty ι] {Fs : ι → Set α} (hFs : ∀ (i : ι), M.Flat (Fs i)) : M.Flat (⋂ (i : ι), Fs i)

def Matroid.subtypeClosure {α : Type u_2} (M : Matroid α) : ClosureOperator ↑(Set.Iic M.E)

The property of being a flat gives rise to a ClosureOperator on the subsets of M.E, in which the IsClosed sets correspond to Flats. (We can't define such an operator on all of Set α, since this would incorrectly force univ to always be a flat.)

Equations

• M.subtypeClosure = ClosureOperator.ofCompletePred (fun (F : ↑(Set.Iic M.E)) => M.Flat ↑F) ⋯

theorem Matroid.flat_iff_isClosed {α : Type u_2} {M : Matroid α} {F : Set α} : M.Flat F ↔ ∃ (h : F ⊆ M.E), M.subtypeClosure.IsClosed ⟨F, h⟩

theorem Matroid.isClosed_iff_flat {α : Type u_2} {M : Matroid α} {F : ↑(Set.Iic M.E)} : M.subtypeClosure.IsClosed F ↔ M.Flat ↑F

def Matroid.closure {α : Type u_2} (M : Matroid α) (X : Set α) : Set α

The closure of X ⊆ M.E is the intersection of all the flats of M containing X. A set X that doesn't satisfy X ⊆ M.E has the junk value M.closure X := M.closure (X ∩ M.E).

Equations

• M.closure X = ⋂₀ {F : Set α | M.Flat F ∧ X ∩ M.E ⊆ F}

theorem Matroid.closure_def {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure X = ⋂₀ {F : Set α | M.Flat F ∧ X ∩ M.E ⊆ F}

theorem Matroid.closure_def' {α : Type u_2} (M : Matroid α) (X : Set α) (hX : autoParam (X ⊆ M.E) _auto✝) : M.closure X = ⋂₀ {F : Set α | M.Flat F ∧ X ⊆ F}

theorem Matroid.closure_eq_subtypeClosure {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure X = ↑(M.subtypeClosure ⟨X ∩ M.E, ⋯⟩)

theorem Matroid.closure_subset_ground {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure X ⊆ M.E

@[simp]

theorem Matroid.ground_subset_closure_iff {α : Type u_2} {M : Matroid α} {X : Set α} : M.E ⊆ M.closure X ↔ M.closure X = M.E

@[simp]

theorem Matroid.closure_inter_ground {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure (X ∩ M.E) = M.closure X

theorem Matroid.inter_ground_subset_closure {α : Type u_2} (M : Matroid α) (X : Set α) : X ∩ M.E ⊆ M.closure X

theorem Matroid.mem_closure_iff_forall_mem_flat {α : Type u_2} {M : Matroid α} {e : α} (X : Set α) (hX : autoParam (X ⊆ M.E) _auto✝) : e ∈ M.closure X ↔ ∀ (F : Set α), M.Flat F → X ⊆ F → e ∈ F

theorem Matroid.subset_closure_iff_forall_subset_flat {α : Type u_2} {M : Matroid α} {Y : Set α} (X : Set α) (hX : autoParam (X ⊆ M.E) _auto✝) : Y ⊆ M.closure X ↔ ∀ (F : Set α), M.Flat F → X ⊆ F → Y ⊆ F

theorem Matroid.subset_closure {α : Type u_2} (M : Matroid α) (X : Set α) (hX : autoParam (X ⊆ M.E) _auto✝) : X ⊆ M.closure X

theorem Matroid.Flat.closure {α : Type u_2} {M : Matroid α} {F : Set α} (hF : M.Flat F) : M.closure F = F

@[simp]

theorem Matroid.closure_ground {α : Type u_2} (M : Matroid α) : M.closure M.E = M.E

@[simp]

theorem Matroid.closure_univ {α : Type u_2} (M : Matroid α) : M.closure Set.univ = M.E

theorem Matroid.closure_subset_closure {α : Type u_2} {X : Set α} {Y : Set α} (M : Matroid α) (h : X ⊆ Y) : M.closure X ⊆ M.closure Y

theorem Matroid.closure_mono {α : Type u_2} (M : Matroid α) : Monotone M.closure

@[simp]

theorem Matroid.closure_closure {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure (M.closure X) = M.closure X

theorem Matroid.closure_subset_closure_of_subset_closure {α : Type u_2} {M : Matroid α} {X : Set α} {Y : Set α} (hXY : X ⊆ M.closure Y) : M.closure X ⊆ M.closure Y

theorem Matroid.closure_subset_closure_iff_subset_closure {α : Type u_2} {M : Matroid α} {X : Set α} {Y : Set α} (hX : autoParam (X ⊆ M.E) _auto✝) : M.closure X ⊆ M.closure Y ↔ X ⊆ M.closure Y

theorem Matroid.subset_closure_of_subset {α : Type u_2} {X : Set α} {Y : Set α} (M : Matroid α) (hXY : X ⊆ Y) (hY : autoParam (Y ⊆ M.E) _auto✝) : X ⊆ M.closure Y

theorem Matroid.subset_closure_of_subset' {α : Type u_2} {X : Set α} {Y : Set α} (M : Matroid α) (hXY : X ⊆ Y) (hX : autoParam (X ⊆ M.E) _auto✝) : X ⊆ M.closure Y

theorem Matroid.exists_of_closure_ssubset {α : Type u_2} {M : Matroid α} {X : Set α} {Y : Set α} (hXY : M.closure X ⊂ M.closure Y) : ∃ e ∈ Y, e ∉ M.closure X

theorem Matroid.mem_closure_of_mem {α : Type u_2} {X : Set α} {e : α} (M : Matroid α) (h : e ∈ X) (hX : autoParam (X ⊆ M.E) _auto✝) : e ∈ M.closure X

theorem Matroid.mem_closure_of_mem' {α : Type u_2} {X : Set α} {e : α} (M : Matroid α) (heX : e ∈ X) (h : autoParam (e ∈ M.E) _auto✝) : e ∈ M.closure X

theorem Matroid.not_mem_of_mem_diff_closure {α : Type u_2} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ M.E \ M.closure X) : e ∉ X

theorem Matroid.mem_ground_of_mem_closure {α : Type u_2} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ M.closure X) : e ∈ M.E

theorem Matroid.closure_iUnion_closure_eq_closure_iUnion {ι : Type u_1} {α : Type u_2} (M : Matroid α) (Xs : ι → Set α) : M.closure (⋃ (i : ι), M.closure (Xs i)) = M.closure (⋃ (i : ι), Xs i)

theorem Matroid.closure_iUnion_congr {ι : Type u_1} {α : Type u_2} {M : Matroid α} (Xs : ι → Set α) (Ys : ι → Set α) (h : ∀ (i : ι), M.closure (Xs i) = M.closure (Ys i)) : M.closure (⋃ (i : ι), Xs i) = M.closure (⋃ (i : ι), Ys i)

theorem Matroid.closure_biUnion_closure_eq_closure_sUnion {α : Type u_2} (M : Matroid α) (Xs : Set (Set α)) : M.closure (⋃ X ∈ Xs, M.closure X) = M.closure (⋃₀ Xs)

theorem Matroid.closure_biUnion_closure_eq_closure_biUnion {ι : Type u_1} {α : Type u_2} (M : Matroid α) (Xs : ι → Set α) (A : Set ι) : M.closure (⋃ i ∈ A, M.closure (Xs i)) = M.closure (⋃ i ∈ A, Xs i)

theorem Matroid.closure_biUnion_congr {ι : Type u_1} {α : Type u_2} (M : Matroid α) (Xs : ι → Set α) (Ys : ι → Set α) (A : Set ι) (h : ∀ i ∈ A, M.closure (Xs i) = M.closure (Ys i)) : M.closure (⋃ i ∈ A, Xs i) = M.closure (⋃ i ∈ A, Ys i)

theorem Matroid.closure_closure_union_closure_eq_closure_union {α : Type u_2} (M : Matroid α) (X : Set α) (Y : Set α) : M.closure (M.closure X ∪ M.closure Y) = M.closure (X ∪ Y)

@[simp]

theorem Matroid.closure_union_closure_right_eq {α : Type u_2} (M : Matroid α) (X : Set α) (Y : Set α) : M.closure (X ∪ M.closure Y) = M.closure (X ∪ Y)

@[simp]

theorem Matroid.closure_union_closure_left_eq {α : Type u_2} (M : Matroid α) (X : Set α) (Y : Set α) : M.closure (M.closure X ∪ Y) = M.closure (X ∪ Y)

@[simp]

theorem Matroid.closure_insert_closure_eq_closure_insert {α : Type u_2} (M : Matroid α) (e : α) (X : Set α) : M.closure (insert e (M.closure X)) = M.closure (insert e X)

@[simp]

theorem Matroid.closure_union_closure_empty_eq {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure X ∪ M.closure ∅ = M.closure X

@[simp]

theorem Matroid.closure_empty_union_closure_eq {α : Type u_2} (M : Matroid α) (X : Set α) : M.closure ∅ ∪ M.closure X = M.closure X

theorem Matroid.closure_insert_eq_of_mem_closure {α : Type u_2} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ M.closure X) : M.closure (insert e X) = M.closure X

theorem Matroid.mem_closure_self {α : Type u_2} (M : Matroid α) (e : α) (he : autoParam (e ∈ M.E) _auto✝) : e ∈ M.closure {e}

theorem Matroid.Indep.closure_eq_setOf_basis_insert {α : Type u_2} {M : Matroid α} {I : Set α} (hI : M.Indep I) : M.closure I = {x : α | M.Basis I (insert x I)}

theorem Matroid.Indep.insert_basis_iff_mem_closure {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) : M.Basis I (insert e I) ↔ e ∈ M.closure I

theorem Matroid.Indep.basis_closure {α : Type u_2} {M : Matroid α} {I : Set α} (hI : M.Indep I) : M.Basis I (M.closure I)

theorem Matroid.Basis.closure_eq_closure {α : Type u_2} {M : Matroid α} {X : Set α} {I : Set α} (h : M.Basis I X) : M.closure I = M.closure X

theorem Matroid.Basis.closure_eq_right {α : Type u_2} {M : Matroid α} {X : Set α} {I : Set α} (h : M.Basis I (M.closure X)) : M.closure I = M.closure X

theorem Matroid.Basis'.closure_eq_closure {α : Type u_2} {M : Matroid α} {X : Set α} {I : Set α} (h : M.Basis' I X) : M.closure I = M.closure X

theorem Matroid.Basis.subset_closure {α : Type u_2} {M : Matroid α} {X : Set α} {I : Set α} (h : M.Basis I X) : X ⊆ M.closure I

theorem Matroid.Basis'.basis_closure_right {α : Type u_2} {M : Matroid α} {X : Set α} {I : Set α} (h : M.Basis' I X) : M.Basis I (M.closure X)

theorem Matroid.Basis.basis_closure_right {α : Type u_2} {M : Matroid α} {X : Set α} {I : Set α} (h : M.Basis I X) : M.Basis I (M.closure X)

theorem Matroid.Indep.mem_closure_iff {α : Type u_2} {M : Matroid α} {I : Set α} {x : α} (hI : M.Indep I) : x ∈ M.closure I ↔ M.Dep (insert x I) ∨ x ∈ I

theorem Matroid.Indep.mem_closure_iff' {α : Type u_2} {M : Matroid α} {I : Set α} {x : α} (hI : M.Indep I) : x ∈ M.closure I ↔ x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)

theorem Matroid.Indep.insert_dep_iff {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) : M.Dep (insert e I) ↔ e ∈ M.closure I \ I

theorem Matroid.Indep.mem_closure_iff_of_not_mem {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (heI : e ∉ I) : e ∈ M.closure I ↔ M.Dep (insert e I)

theorem Matroid.Indep.not_mem_closure_iff {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (he : autoParam (e ∈ M.E) _auto✝) : e ∉ M.closure I ↔ M.Indep (insert e I) ∧ e ∉ I

theorem Matroid.Indep.not_mem_closure_iff_of_not_mem {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (heI : e ∉ I) (he : autoParam (e ∈ M.E) _auto✝) : e ∉ M.closure I ↔ M.Indep (insert e I)

theorem Matroid.Indep.insert_indep_iff_of_not_mem {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) (heI : e ∉ I) : M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I

theorem Matroid.Indep.insert_indep_iff {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} (hI : M.Indep I) : M.Indep (insert e I) ↔ e ∈ M.E \ M.closure I ∨ e ∈ I

theorem Matroid.insert_indep_iff {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} : M.Indep (insert e I) ↔ M.Indep I ∧ (e ∉ I → e ∈ M.E \ M.closure I)

theorem Matroid.Indep.insert_diff_indep_iff {α : Type u_2} {M : Matroid α} {e : α} {I : Set α} {f : α} (hI : M.Indep (I \ {e})) (heI : e ∈ I) : M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I

This can be used for rewriting if the LHS is inside a binder and whether f = e is unknown.

theorem Matroid.Indep.basis_of_subset_of_subset_closure {α : Type u_2} {M : Matroid α} {X : Set α} {I : Set α} (hI : M.Indep I) (hIX : I ⊆ X) (hXI : X ⊆ M.closure I) : M.Basis I X

theorem Matroid.basis_iff_indep_subset_closure {α : Type u_2} {M : Matroid α} {X : Set α} {I : Set α} : M.Basis I X ↔ M.Indep I ∧ I ⊆ X ∧ X ⊆ M.closure I

theorem Matroid.Indep.base_of_ground_subset_closure {α : Type u_2} {M : Matroid α} {I : Set α} (hI : M.Indep I) (h : M.E ⊆ M.closure I) : M.Base I

theorem Matroid.Base.closure_eq {α : Type u_2} {M : Matroid α} {B : Set α} (hB : M.Base B) : M.closure B = M.E

theorem Matroid.Base.closure_of_superset {α : Type u_2} {M : Matroid α} {X : Set α} {B : Set α} (hB : M.Base B) (hBX : B ⊆ X) : M.closure X = M.E

theorem Matroid.base_iff_indep_closure_eq {α : Type u_2} {M : Matroid α} {B : Set α} : M.Base B ↔ M.Indep B ∧ M.closure B = M.E

theorem Matroid.Indep.base_iff_ground_subset_closure {α : Type u_2} {M : Matroid α} {I : Set α} (hI : M.Indep I) : M.Base I ↔ M.E ⊆ M.closure I

theorem Matroid.Indep.closure_inter_eq_self_of_subset {α : Type u_2} {M : Matroid α} {I : Set α} {J : Set α} (hI : M.Indep I) (hJI : J ⊆ I) : M.closure J ∩ I = J

theorem Matroid.Indep.closure_sInter_eq_biInter_closure_of_forall_subset {α : Type u_2} {M : Matroid α} {I : Set α} {Js : Set (Set α)} (hI : M.Indep I) (hne : Js.Nonempty) (hIs : ∀ J ∈ Js, J ⊆ I) : M.closure (⋂₀ Js) = ⋂ J ∈ Js, M.closure J

For a nonempty collection of subsets of a given independent set, the closure of the intersection is the intersection of the closure.

theorem Matroid.closure_iInter_eq_iInter_closure_of_iUnion_indep {α : Type u_2} {M : Matroid α} {ι : Sort u_3} [hι : Nonempty ι] (Is : ι → Set α) (h : M.Indep (⋃ (i : ι), Is i)) : M.closure (⋂ (i : ι), Is i) = ⋂ (i : ι), M.closure (Is i)

theorem Matroid.closure_sInter_eq_biInter_closure_of_sUnion_indep {α : Type u_2} {M : Matroid α} (Is : Set (Set α)) (hIs : Is.Nonempty) (h : M.Indep (⋃₀ Is)) : M.closure (⋂₀ Is) = ⋂ I ∈ Is, M.closure I

theorem Matroid.closure_biInter_eq_biInter_closure_of_biUnion_indep {α : Type u_2} {M : Matroid α} {ι : Type u_4} {A : Set ι} (hA : A.Nonempty) {I : ι → Set α} (h : M.Indep (⋃ i ∈ A, I i)) : M.closure (⋂ i ∈ A, I i) = ⋂ i ∈ A, M.closure (I i)

theorem Matroid.Indep.closure_iInter_eq_biInter_closure_of_forall_subset {α : Type u_2} {M : Matroid α} {ι : Sort u_3} {I : Set α} [hι : Nonempty ι] {Js : ι → Set α} (hI : M.Indep I) (hJs : ∀ (i : ι), Js i ⊆ I) : M.closure (⋂ (i : ι), Js i) = ⋂ (i : ι), M.closure (Js i)

theorem Matroid.Indep.closure_inter_eq_inter_closure {α : Type u_2} {M : Matroid α} {I : Set α} {J : Set α} (h : M.Indep (I ∪ J)) : M.closure (I ∩ J) = M.closure I ∩ M.closure J

theorem Matroid.basis_iff_basis_closure_of_subset {α : Type u_2} {M : Matroid α} {X : Set α} {I : Set α} (hIX : I ⊆ X) (hX : autoParam (X ⊆ M.E) _auto✝) : M.Basis I X ↔ M.Basis I (M.closure X)

theorem Matroid.basis_iff_basis_closure_of_subset' {α : Type u_2} {M : Matroid α} {X : Set α} {I : Set α} (hIX : I ⊆ X) : M.Basis I X ↔ M.Basis I (M.closure X) ∧ X ⊆ M.E

theorem Matroid.basis'_iff_basis_closure {α : Type u_2} {M : Matroid α} {X : Set α} {I : Set α} : M.Basis' I X ↔ M.Basis I (M.closure X) ∧ I ⊆ X

theorem Matroid.exists_basis_inter_ground_basis_closure {α : Type u_2} (M : Matroid α) (X : Set α) : ∃ (I : Set α), M.Basis I (X ∩ M.E) ∧ M.Basis I (M.closure X)

theorem Matroid.Basis.basis_of_closure_eq_closure {α : Type u_2} {M : Matroid α} {X : Set α} {Y : Set α} {I : Set α} (hI : M.Basis I X) (hY : I ⊆ Y) (h : M.closure X = M.closure Y) (hYE : autoParam (Y ⊆ M.E) _auto✝) : M.Basis I Y

theorem Matroid.basis_union_iff_indep_closure {α : Type u_2} {M : Matroid α} {X : Set α} {I : Set α} : M.Basis I (I ∪ X) ↔ M.Indep I ∧ X ⊆ M.closure I

theorem Matroid.basis_iff_indep_closure {α : Type u_2} {M : Matroid α} {X : Set α} {I : Set α} : M.Basis I X ↔ M.Indep I ∧ X ⊆ M.closure I ∧ I ⊆ X

theorem Matroid.Basis.eq_of_closure_subset {α : Type u_2} {M : Matroid α} {X : Set α} {I : Set α} {J : Set α} (hI : M.Basis I X) (hJI : J ⊆ I) (hJ : X ⊆ M.closure J) : J = I

@[simp]

theorem Matroid.empty_basis_iff {α : Type u_2} {M : Matroid α} {X : Set α} : M.Basis ∅ X ↔ X ⊆ M.closure ∅