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 #

@[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

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

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

      Equations
      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