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 in which a set B is a base if and only if B ⊆ M.E and 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.

@[simp]

theorem Matroid.dualIndepMatroid_Indep {α : Type u_1} (M : Matroid α) (I : Set α) : (Matroid.dualIndepMatroid M).Indep I = (I ⊆ M.E ∧ ∃ (B : Set α), M.Base B ∧ Disjoint I B)

@[simp]

theorem Matroid.dualIndepMatroid_E {α : Type u_1} (M : Matroid α) : (Matroid.dualIndepMatroid M).E = M.E

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• M﹡ = IndepMatroid.matroid (Matroid.dualIndepMatroid 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. )

Equations

• Matroid.«term_﹡» = Lean.ParserDescr.trailingNode `Matroid.term_﹡ 1024 1024 (Lean.ParserDescr.symbol "﹡")

theorem Matroid.dual_indep_iff_exists' {α : Type u_1} {M : Matroid α} {I : Set α} : M﹡.Indep I ↔ I ⊆ M.E ∧ ∃ (B : Set α), M.Base B ∧ Disjoint I B

@[simp]

theorem Matroid.dual_ground {α : Type u_1} {M : Matroid α} : M﹡.E = M.E

@[simp]

theorem Matroid.dual_indep_iff_exists {α : Type u_1} {M : Matroid α} {I : Set α} (hI : autoParam (I ⊆ M.E) _auto✝) : M﹡.Indep I ↔ ∃ (B : Set α), M.Base B ∧ Disjoint I B

theorem Matroid.dual_dep_iff_forall {α : Type u_1} {M : Matroid α} {I : Set α} : M﹡.Dep I ↔ (∀ (B : Set α), M.Base B → Set.Nonempty (I ∩ B)) ∧ I ⊆ M.E

instance Matroid.dual_finite {α : Type u_1} {M : Matroid α} [Matroid.Finite M] : Matroid.Finite M﹡

Equations

• ⋯ = ⋯

instance Matroid.dual_nonempty {α : Type u_1} {M : Matroid α} [Matroid.Nonempty M] : Matroid.Nonempty M﹡

Equations

• ⋯ = ⋯

@[simp]

theorem Matroid.dual_base_iff {α : Type u_1} {M : Matroid α} {B : Set α} (hB : autoParam (B ⊆ M.E) _auto✝) : M﹡.Base B ↔ M.Base (M.E \ B)

theorem Matroid.dual_base_iff' {α : Type u_1} {M : Matroid α} {B : Set α} : M﹡.Base B ↔ M.Base (M.E \ B) ∧ B ⊆ M.E

theorem Matroid.setOf_dual_base_eq {α : Type u_1} {M : Matroid α} : {B : Set α | M﹡.Base B} = (fun (X : Set α) => M.E \ X) '' {B : Set α | M.Base B}

@[simp]

theorem Matroid.dual_dual {α : Type u_1} (M : Matroid α) : M﹡﹡ = M

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

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

@[simp]

theorem Matroid.dual_inj {α : Type u_1} {M₁ : Matroid α} {M₂ : Matroid α} : M₁﹡ = M₂﹡ ↔ M₁ = M₂

theorem Matroid.eq_dual_comm {α : Type u_1} {M₁ : Matroid α} {M₂ : Matroid α} : M₁ = M₂﹡ ↔ M₂ = M₁﹡

theorem Matroid.eq_dual_iff_dual_eq {α : Type u_1} {M₁ : Matroid α} {M₂ : Matroid α} : M₁ = M₂﹡ ↔ M₁﹡ = M₂

theorem Matroid.Base.compl_base_of_dual {α : Type u_1} {M : Matroid α} {B : Set α} (h : M﹡.Base B) : M.Base (M.E \ B)

theorem Matroid.Base.compl_base_dual {α : Type u_1} {M : Matroid α} {B : Set α} (h : M.Base B) : M﹡.Base (M.E \ B)

theorem Matroid.Base.compl_inter_basis_of_inter_basis {α : Type u_1} {M : Matroid α} {B : Set α} {X : Set α} (hB : M.Base B) (hBX : M.Basis (B ∩ X) X) : M﹡.Basis (M.E \ B ∩ (M.E \ X)) (M.E \ X)

theorem Matroid.Base.inter_basis_iff_compl_inter_basis_dual {α : Type u_1} {M : Matroid α} {B : Set α} {X : Set α} (hB : M.Base B) (hX : autoParam (X ⊆ M.E) _auto✝) : M.Basis (B ∩ X) X ↔ M﹡.Basis (M.E \ B ∩ (M.E \ X)) (M.E \ X)

theorem Matroid.base_iff_dual_base_compl {α : Type u_1} {M : Matroid α} {B : Set α} (hB : autoParam (B ⊆ M.E) _auto✝) : M.Base B ↔ M﹡.Base (M.E \ B)

theorem Matroid.ground_not_base {α : Type u_1} (M : Matroid α) [h : Matroid.RkPos M﹡] : ¬M.Base M.E

theorem Matroid.Base.ssubset_ground {α : Type u_1} {M : Matroid α} {B : Set α} [h : Matroid.RkPos M﹡] (hB : M.Base B) : B ⊂ M.E

theorem Matroid.Indep.ssubset_ground {α : Type u_1} {M : Matroid α} {I : Set α} [h : Matroid.RkPos M﹡] (hI : M.Indep I) : I ⊂ M.E

@[inline, reducible]

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.

Equations

• Matroid.Coindep M I = M﹡.Indep I

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

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

@[simp]

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

theorem Matroid.Indep.coindep {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : Matroid.Coindep M﹡ I

theorem Matroid.coindep_iff_exists' {α : Type u_1} {M : Matroid α} {X : Set α} : Matroid.Coindep M X ↔ (∃ (B : Set α), M.Base B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E

theorem Matroid.coindep_iff_exists {α : Type u_1} {M : Matroid α} {X : Set α} (hX : autoParam (X ⊆ M.E) _auto✝) : Matroid.Coindep M X ↔ ∃ (B : Set α), M.Base B ∧ B ⊆ M.E \ X

theorem Matroid.coindep_iff_subset_compl_base {α : Type u_1} {M : Matroid α} {X : Set α} : Matroid.Coindep M X ↔ ∃ (B : Set α), M.Base B ∧ X ⊆ M.E \ B

theorem Matroid.Coindep.subset_ground {α : Type u_1} {M : Matroid α} {X : Set α} (hX : Matroid.Coindep M X) : X ⊆ M.E

theorem Matroid.Coindep.exists_base_subset_compl {α : Type u_1} {M : Matroid α} {X : Set α} (h : Matroid.Coindep M X) : ∃ (B : Set α), M.Base B ∧ B ⊆ M.E \ X

theorem Matroid.Coindep.exists_subset_compl_base {α : Type u_1} {M : Matroid α} {X : Set α} (h : Matroid.Coindep M X) : ∃ (B : Set α), M.Base B ∧ X ⊆ M.E \ B