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