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 #

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

M.dualIndepMatroid.Indep I = (I ⊆ M.E ∧ ∃ (B : Set α), M.Base B ∧ Disjoint I B)

@[simp]

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

M.dualIndepMatroid.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.

Instances For

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

M✶ = M.dualIndepMatroid.matroid

Instances For

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 "✶")

Instances For

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 → (I ∩ B).Nonempty) ∧ I ⊆ M.E

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

M✶.Finite

Equations

⋯ = ⋯

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

M✶.Nonempty

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

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

¬M.Base M.E

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

B ⊂ M.E

theorem Matroid.Indep.ssubset_ground {α : Type u_1} {M : Matroid α} {I : Set α} [h : M✶.RkPos] (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

M.Coindep I = M✶.Indep I

Instances For

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.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✝) :

M.Coindep X ↔ ∃ (B : Set α), M.Base B ∧ B ⊆ M.E \ X

theorem Matroid.coindep_iff_subset_compl_base {α : Type u_1} {M : Matroid α} {X : Set α} :

M.Coindep X ↔ ∃ (B : Set α), M.Base 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_base_subset_compl {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.Coindep 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 : M.Coindep X) :

∃ (B : Set α), M.Base B ∧ X ⊆ M.E \ B