Documentation

Mathlib.Data.Matroid.Dual

Matroid Duality #

For a matroid M on ground set E, the collection of complements of the bases of M is the collection of bases of another matroid on E called the 'dual' of M. The map from M to its dual is an involution, interacts nicely with minors, and preserves many important matroid properties such as representability and connectivity.

This file defines the dual matroid M✶ of M, and gives associated API. The definition is in terms of its independent sets, using IndepMatroid.matroid.

We also define 'Co-independence' (independence in the dual) of a set as a predicate M.Coindep X. This is an abbreviation for M✶.Indep X, but has its own name for the sake of dot notation.

Main Definitions #

Given M : Matroid α, the IndepMatroid α whose independent sets are the subsets of M.E that are disjoint from some base of M

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Matroid.dualIndepMatroid_Indep {α : Type u_1} (M : Matroid α) (I : Set α) :
M.dualIndepMatroid.Indep I = (I M.E ∃ (B : Set α), M.IsBase B Disjoint I B)
@[simp]
theorem Matroid.dualIndepMatroid_E {α : Type u_1} (M : Matroid α) :
def Matroid.dual {α : Type u_1} (M : Matroid α) :

The dual of a matroid; the bases are the complements (w.r.t M.E) of the bases of M.

Equations

The symbol, which denotes matroid duality. (This is distinct from the usual * symbol for multiplication, due to precedence issues.)

Equations
theorem Matroid.dual_indep_iff_exists' {α : Type u_1} {M : Matroid α} {I : Set α} :
M.Indep I I M.E ∃ (B : Set α), M.IsBase B Disjoint I B
@[simp]
theorem Matroid.dual_ground {α : Type u_1} {M : Matroid α} :
M.E = M.E
theorem Matroid.dual_indep_iff_exists {α : Type u_1} {M : Matroid α} {I : Set α} (hI : I M.E := by aesop_mat) :
M.Indep I ∃ (B : Set α), M.IsBase B Disjoint I B
theorem Matroid.dual_dep_iff_forall {α : Type u_1} {M : Matroid α} {I : Set α} :
M.Dep I (∀ (B : Set α), M.IsBase B(I B).Nonempty) I M.E
instance Matroid.dual_finite {α : Type u_1} {M : Matroid α} [M.Finite] :
instance Matroid.dual_nonempty {α : Type u_1} {M : Matroid α} [M.Nonempty] :
@[simp]
theorem Matroid.dual_isBase_iff {α : Type u_1} {M : Matroid α} {B : Set α} (hB : B M.E := by aesop_mat) :
M.IsBase B M.IsBase (M.E \ B)
theorem Matroid.dual_isBase_iff' {α : Type u_1} {M : Matroid α} {B : Set α} :
M.IsBase B M.IsBase (M.E \ B) B M.E
theorem Matroid.setOf_dual_isBase_eq {α : Type u_1} {M : Matroid α} :
{B : Set α | M.IsBase B} = (fun (X : Set α) => M.E \ X) '' {B : Set α | M.IsBase B}
@[simp]
theorem Matroid.dual_dual {α : Type u_1} (M : Matroid α) :
@[simp]
theorem Matroid.dual_inj {α : Type u_1} {M₁ M₂ : Matroid α} :
M₁ = M₂ M₁ = M₂
theorem Matroid.eq_dual_comm {α : Type u_1} {M₁ M₂ : Matroid α} :
M₁ = M₂ M₂ = M₁
theorem Matroid.eq_dual_iff_dual_eq {α : Type u_1} {M₁ M₂ : Matroid α} :
M₁ = M₂ M₁ = M₂
theorem Matroid.IsBase.compl_isBase_of_dual {α : Type u_1} {M : Matroid α} {B : Set α} (h : M.IsBase B) :
M.IsBase (M.E \ B)
theorem Matroid.IsBase.compl_isBase_dual {α : Type u_1} {M : Matroid α} {B : Set α} (h : M.IsBase B) :
M.IsBase (M.E \ B)
theorem Matroid.IsBase.compl_inter_isBasis_of_inter_isBasis {α : Type u_1} {M : Matroid α} {B X : Set α} (hB : M.IsBase B) (hBX : M.IsBasis (B X) X) :
M.IsBasis (M.E \ B (M.E \ X)) (M.E \ X)
theorem Matroid.IsBase.inter_isBasis_iff_compl_inter_isBasis_dual {α : Type u_1} {M : Matroid α} {B X : Set α} (hB : M.IsBase B) (hX : X M.E := by aesop_mat) :
M.IsBasis (B X) X M.IsBasis (M.E \ B (M.E \ X)) (M.E \ X)
theorem Matroid.base_iff_dual_isBase_compl {α : Type u_1} {M : Matroid α} {B : Set α} (hB : B M.E := by aesop_mat) :
M.IsBase B M.IsBase (M.E \ B)
theorem Matroid.ground_not_isBase {α : Type u_1} (M : Matroid α) [h : M.RankPos] :
theorem Matroid.IsBase.ssubset_ground {α : Type u_1} {M : Matroid α} {B : Set α} [h : M.RankPos] (hB : M.IsBase B) :
B M.E
theorem Matroid.Indep.ssubset_ground {α : Type u_1} {M : Matroid α} {I : Set α} [h : M.RankPos] (hI : M.Indep I) :
I M.E
@[reducible, inline]
abbrev Matroid.Coindep {α : Type u_1} (M : Matroid α) (I : Set α) :

A coindependent set of M is an independent set of the dual of M✶. we give it a separate definition to enable dot notation. Which spelling is better depends on context.

Equations
theorem Matroid.coindep_def {α : Type u_1} {M : Matroid α} {X : Set α} :
theorem Matroid.Coindep.indep {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Coindep X) :
@[simp]
theorem Matroid.dual_coindep_iff {α : Type u_1} {M : Matroid α} {X : Set α} :
theorem Matroid.Indep.coindep {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) :
theorem Matroid.coindep_iff_exists' {α : Type u_1} {M : Matroid α} {X : Set α} :
M.Coindep X (∃ (B : Set α), M.IsBase B B M.E \ X) X M.E
theorem Matroid.coindep_iff_exists {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X M.E := by aesop_mat) :
M.Coindep X ∃ (B : Set α), M.IsBase B B M.E \ X
theorem Matroid.coindep_iff_subset_compl_isBase {α : Type u_1} {M : Matroid α} {X : Set α} :
M.Coindep X ∃ (B : Set α), M.IsBase B X M.E \ B
theorem Matroid.Coindep.subset_ground {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Coindep X) :
X M.E
theorem Matroid.Coindep.exists_isBase_subset_compl {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.Coindep X) :
∃ (B : Set α), M.IsBase B B M.E \ X
theorem Matroid.Coindep.exists_subset_compl_isBase {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.Coindep X) :
∃ (B : Set α), M.IsBase B X M.E \ B