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

• M.Dual, written M✶, is the matroid on M.E which a set B ⊆ M.E is a base if and only if M.E \ B is a base for M.

• M.Coindep X means M✶.Indep X, or equivalently that X is contained in M.E \ B for some base B of M.

def Matroid.dualIndepMatroid {α : Type u_1} (M : Matroid α) : IndepMatroid α

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

@[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 α) : M.dualIndepMatroid.E = M.E

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

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

def Matroid.«term_✶» : Lean.TrailingParserDescr

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

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] : M✶.Finite

instance Matroid.dual_nonempty {α : Type u_1} {M : Matroid α} [M.Nonempty] : 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 α) : M✶✶ = M

theorem Matroid.dual_involutive {α : Type u_1} : Function.Involutive dual

theorem Matroid.dual_injective {α : Type u_1} : Function.Injective dual

@[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] : ¬M.IsBase M.E

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

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.

theorem Matroid.coindep_def {α : Type u_1} {M : Matroid α} {X : Set α} : M.Coindep X ↔ M✶.Indep X

theorem Matroid.Coindep.indep {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Coindep X) : M✶.Indep X

@[simp]

theorem Matroid.dual_coindep_iff {α : Type u_1} {M : Matroid α} {X : Set α} : M✶.Coindep X ↔ M.Indep X

theorem Matroid.Indep.coindep {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : M✶.Coindep 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