Documentation

Mathlib.Data.Matroid.IndepAxioms

Matroid Independence and Basis axioms #

Matroids in mathlib are defined axiomatically in terms of bases, but can be described just as naturally via their collections of independent sets, and in fact such a description, being more 'verbose', can often be useful. As well as this, the definition of a Matroid uses an unwieldy 'maximality' axiom that can be dropped in cases where there is some finiteness assumption.

This file provides several ways to do define a matroid in terms of its independence or base predicates, using axiom sets that are appropriate in different settings, and often much simpler than the general definition. It also contains simp lemmas and typeclasses as appropriate.

All the independence axiom sets need nontriviality (the empty set is independent), monotonicity (subsets of independent sets are independent), and some form of 'augmentation' axiom, which allows one to enlarge a non-maximal independent set. This augmentation axiom is still required when there are finiteness assumptions, but is simpler. It just states that if I is a finite independent set and J is a larger finite independent set, then there exists e ∈ J \ I for which insert e I is independent. This is the axiom that appears in most of the definitions.

Implementation Details #

To facilitate building a matroid from its independent sets, we define a structure IndepMatroid which has a ground set E, an independence predicate Indep, and some axioms as its fields. This structure is another encoding of the data in a Matroid; the function IndepMatroid.matroid constructs a Matroid from an IndepMatroid.

This is convenient because if one wants to define M : Matroid α from a known independence predicate Ind, it is easier to define an M' : IndepMatroid α so that M'.Indep = Ind and then set M = M'.matroid than it is to directly define M with the base axioms. The simp lemma IndepMatroid.matroid_indep_iff is important here; it shows that M.Indep = Ind, so the Matroid constructed is the right one, and the intermediate IndepMatroid can be made essentially invisible by the simplifier when working with M.

Because of this setup, we don't define any API for IndepMatroid, as it would be a redundant copy of the existing API for Matroid.Indep. (In particular, one could define a natural equivalence e : IndepMatroid α ≃ Matroid α with e.toFun = IndepMatroid.matroid, but this would be pointless, as there is no need for the inverse of e).

Main definitions #

structure IndepMatroid (α : Type u_2) :
Type u_2

A matroid as defined by the independence axioms. This is the same thing as a Matroid, and so does not need its own API; it exists to make it easier to construct a matroid from its independent sets. The constructed IndepMatroid can then be converted into a matroid with IndepMatroid.matroid.

  • E : Set α

    The ground set

  • Indep : Set αProp

    The independence predicate

  • indep_empty : self.Indep
  • indep_subset : ∀ ⦃I J : Set α⦄, self.Indep JI Jself.Indep I
  • indep_aug : ∀ ⦃I B : Set α⦄, self.Indep I¬Maximal self.Indep IMaximal self.Indep BxB \ I, self.Indep (insert x I)
  • indep_maximal : Xself.E, Matroid.ExistsMaximalSubsetProperty self.Indep X
  • subset_ground : ∀ (I : Set α), self.Indep II self.E
Instances For
    theorem IndepMatroid.indep_empty {α : Type u_2} (self : IndepMatroid α) :
    self.Indep
    theorem IndepMatroid.indep_subset {α : Type u_2} (self : IndepMatroid α) ⦃I : Set α ⦃J : Set α :
    self.Indep JI Jself.Indep I
    theorem IndepMatroid.indep_aug {α : Type u_2} (self : IndepMatroid α) ⦃I : Set α ⦃B : Set α :
    self.Indep I¬Maximal self.Indep IMaximal self.Indep BxB \ I, self.Indep (insert x I)
    theorem IndepMatroid.indep_maximal {α : Type u_2} (self : IndepMatroid α) (X : Set α) :
    X self.EMatroid.ExistsMaximalSubsetProperty self.Indep X
    theorem IndepMatroid.subset_ground {α : Type u_2} (self : IndepMatroid α) (I : Set α) :
    self.Indep II self.E
    @[simp]
    theorem IndepMatroid.matroid_E {α : Type u_1} (M : IndepMatroid α) :
    M.matroid.E = M.E
    @[simp]
    theorem IndepMatroid.matroid_Indep {α : Type u_1} (M : IndepMatroid α) :
    ∀ (a : Set α), M.matroid.Indep a = M.Indep a
    @[simp]
    theorem IndepMatroid.matroid_Base {α : Type u_1} (M : IndepMatroid α) (x : Set α) :
    M.matroid.Base x = Maximal M.Indep x
    def IndepMatroid.matroid {α : Type u_1} (M : IndepMatroid α) :

    An M : IndepMatroid α gives a Matroid α whose bases are the maximal M-independent sets.

    Equations
    • M.matroid = { E := M.E, Base := Maximal M.Indep, Indep := M.Indep, indep_iff' := , exists_base := , base_exchange := , maximality := , subset_ground := }
    Instances For
      @[simp]
      theorem IndepMatroid.matroid_indep_iff {α : Type u_1} {M : IndepMatroid α} {I : Set α} :
      M.matroid.Indep I M.Indep I
      @[simp]
      theorem IndepMatroid.ofFinitary_E {α : Type u_1} (E : Set α) (Indep : Set αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Set α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep II.FiniteIndep JJ.FiniteI.ncard < J.ncardeJ, eI Indep (insert e I)) (indep_compact : ∀ (I : Set α), (∀ JI, J.FiniteIndep J)Indep I) (subset_ground : ∀ (I : Set α), Indep II E) :
      (IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).E = E
      def IndepMatroid.ofFinitary {α : Type u_1} (E : Set α) (Indep : Set αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Set α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep II.FiniteIndep JJ.FiniteI.ncard < J.ncardeJ, eI Indep (insert e I)) (indep_compact : ∀ (I : Set α), (∀ JI, J.FiniteIndep J)Indep I) (subset_ground : ∀ (I : Set α), Indep II E) :

      An independence predicate satisfying the finite matroid axioms determines a matroid, provided independence is determined by its behaviour on finite sets. This fundamentally needs choice, since it can be used to prove that every vector space has a basis.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem IndepMatroid.ofFinitary_indep {α : Type u_1} (E : Set α) (Indep : Set αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Set α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep II.FiniteIndep JJ.FiniteI.ncard < J.ncardeJ, eI Indep (insert e I)) (indep_compact : ∀ (I : Set α), (∀ JI, J.FiniteIndep J)Indep I) (subset_ground : ∀ (I : Set α), Indep II E) :
        (IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).Indep = Indep
        instance IndepMatroid.ofFinitary_finitary {α : Type u_1} (E : Set α) (Indep : Set αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Set α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep II.FiniteIndep JJ.FiniteI.ncard < J.ncardeJ, eI Indep (insert e I)) (indep_compact : ∀ (I : Set α), (∀ JI, J.FiniteIndep J)Indep I) (subset_ground : ∀ (I : Set α), Indep II E) :
        (IndepMatroid.ofFinitary E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).matroid.Finitary
        Equations
        • =
        theorem Matroid.existsMaximalSubsetProperty_of_bdd {α : Type u_1} {P : Set αProp} (hP : ∃ (n : ), ∀ (Y : Set α), P YY.encard n) (X : Set α) :

        If there is an absolute upper bound on the size of a set satisfying P, then the maximal subset property always holds.

        @[simp]
        theorem IndepMatroid.ofBdd_E {α : Type u_1} (E : Set α) (Indep : Set αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Set α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I B : Set α⦄, Indep I¬Maximal Indep IMaximal Indep BxB \ I, Indep (insert x I)) (subset_ground : ∀ (I : Set α), Indep II E) (indep_bdd : ∃ (n : ), ∀ (I : Set α), Indep II.encard n) :
        (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground indep_bdd).E = E
        def IndepMatroid.ofBdd {α : Type u_1} (E : Set α) (Indep : Set αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Set α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I B : Set α⦄, Indep I¬Maximal Indep IMaximal Indep BxB \ I, Indep (insert x I)) (subset_ground : ∀ (I : Set α), Indep II E) (indep_bdd : ∃ (n : ), ∀ (I : Set α), Indep II.encard n) :

        If there is an absolute upper bound on the size of an independent set, then the maximality axiom isn't needed to define a matroid by independent sets.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem IndepMatroid.ofBdd_indep {α : Type u_1} (E : Set α) (Indep : Set αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Set α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I B : Set α⦄, Indep I¬Maximal Indep IMaximal Indep BxB \ I, Indep (insert x I)) (subset_ground : ∀ (I : Set α), Indep II E) (h_bdd : ∃ (n : ), ∀ (I : Set α), Indep II.encard n) :
          (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd).Indep = Indep
          instance IndepMatroid.instFiniteRkMatroidOfBdd {α : Type u_1} (E : Set α) (Indep : Set αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Set α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I B : Set α⦄, Indep I¬Maximal Indep IMaximal Indep BxB \ I, Indep (insert x I)) (subset_ground : ∀ (I : Set α), Indep II E) (h_bdd : ∃ (n : ), ∀ (I : Set α), Indep II.encard n) :
          (IndepMatroid.ofBdd E Indep indep_empty indep_subset indep_aug subset_ground h_bdd).matroid.FiniteRk

          IndepMatroid.ofBdd constructs a FiniteRk matroid.

          Equations
          • =
          def IndepMatroid.ofBddAugment {α : Type u_1} (E : Set α) (Indep : Set αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Set α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep IIndep JI.encard < J.encardeJ, eI Indep (insert e I)) (indep_bdd : ∃ (n : ), ∀ (I : Set α), Indep II.encard n) (subset_ground : ∀ (I : Set α), Indep II E) :

          If there is an absolute upper bound on the size of an independent set, then matroids can be defined using an 'augmentation' axiom similar to the standard definition of finite matroids for independent sets.

          Equations
          Instances For
            @[simp]
            theorem IndepMatroid.ofBddAugment_E {α : Type u_1} (E : Set α) (Indep : Set αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Set α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep IIndep JI.encard < J.encardeJ, eI Indep (insert e I)) (indep_bdd : ∃ (n : ), ∀ (I : Set α), Indep II.encard n) (subset_ground : ∀ (I : Set α), Indep II E) :
            (IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd subset_ground).E = E
            @[simp]
            theorem IndepMatroid.ofBddAugment_indep {α : Type u_1} (E : Set α) (Indep : Set αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Set α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep IIndep JI.encard < J.encardeJ, eI Indep (insert e I)) (indep_bdd : ∃ (n : ), ∀ (I : Set α), Indep II.encard n) (subset_ground : ∀ (I : Set α), Indep II E) :
            (IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd subset_ground).Indep = Indep
            instance IndepMatroid.ofBddAugment_finiteRk {α : Type u_1} (E : Set α) (Indep : Set αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Set α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep IIndep JI.encard < J.encardeJ, eI Indep (insert e I)) (indep_bdd : ∃ (n : ), ∀ (I : Set α), Indep II.encard n) (subset_ground : ∀ (I : Set α), Indep II E) :
            (IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd subset_ground).matroid.FiniteRk
            Equations
            • =
            def IndepMatroid.ofFinite {α : Type u_1} {E : Set α} (hE : E.Finite) (Indep : Set αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Set α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep IIndep JI.ncard < J.ncardeJ, eI Indep (insert e I)) (subset_ground : ∀ ⦃I : Set α⦄, Indep II E) :

            If E is finite, then any collection of subsets of E satisfying the usual independence axioms determines a matroid

            Equations
            Instances For
              @[simp]
              theorem IndepMatroid.ofFinite_E {α : Type u_1} {E : Set α} (hE : E.Finite) (Indep : Set αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Set α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep IIndep JI.ncard < J.ncardeJ, eI Indep (insert e I)) (subset_ground : ∀ ⦃I : Set α⦄, Indep II E) :
              (IndepMatroid.ofFinite hE Indep indep_empty indep_subset indep_aug subset_ground).E = E
              @[simp]
              theorem IndepMatroid.ofFinite_indep {α : Type u_1} {E : Set α} (hE : E.Finite) (Indep : Set αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Set α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep IIndep JI.ncard < J.ncardeJ, eI Indep (insert e I)) (subset_ground : ∀ ⦃I : Set α⦄, Indep II E) :
              (IndepMatroid.ofFinite hE Indep indep_empty indep_subset indep_aug subset_ground).Indep = Indep
              instance IndepMatroid.ofFinite_finite {α : Type u_1} {E : Set α} (hE : E.Finite) (Indep : Set αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Set α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I J : Set α⦄, Indep IIndep JI.ncard < J.ncardeJ, eI Indep (insert e I)) (subset_ground : ∀ ⦃I : Set α⦄, Indep II E) :
              (IndepMatroid.ofFinite hE Indep indep_empty indep_subset indep_aug subset_ground).matroid.Finite
              Equations
              • =
              def IndepMatroid.ofFinset {α : Type u_1} [DecidableEq α] (E : Set α) (Indep : Finset αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Finset α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I J : Finset α⦄, Indep IIndep JI.card < J.cardeJ, eI Indep (insert e I)) (subset_ground : ∀ ⦃I : Finset α⦄, Indep II E) :

              An independence predicate on Finset α that obeys the finite matroid axioms determines a finitary matroid on α.

              Equations
              Instances For
                @[simp]
                theorem IndepMatroid.ofFinset_E {α : Type u_1} [DecidableEq α] (E : Set α) (Indep : Finset αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Finset α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I J : Finset α⦄, Indep IIndep JI.card < J.cardeJ, eI Indep (insert e I)) (subset_ground : ∀ ⦃I : Finset α⦄, Indep II E) :
                (IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).E = E
                @[simp]
                theorem IndepMatroid.ofFinset_indep {α : Type u_1} [DecidableEq α] (E : Set α) (Indep : Finset αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Finset α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I J : Finset α⦄, Indep IIndep JI.card < J.cardeJ, eI Indep (insert e I)) (subset_ground : ∀ ⦃I : Finset α⦄, Indep II E) {I : Finset α} :
                (IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).Indep I Indep I
                theorem IndepMatroid.ofFinset_indep' {α : Type u_1} [DecidableEq α] (E : Set α) (Indep : Finset αProp) (indep_empty : Indep ) (indep_subset : ∀ ⦃I J : Finset α⦄, Indep JI JIndep I) (indep_aug : ∀ ⦃I J : Finset α⦄, Indep IIndep JI.card < J.cardeJ, eI Indep (insert e I)) (subset_ground : ∀ ⦃I : Finset α⦄, Indep II E) {I : Set α} :
                (IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).Indep I ∀ (J : Finset α), J IIndep J

                This can't be @[simp], because it would cause the more useful Matroid.ofIndepFinset_apply not to be in simp normal form.

                @[simp]
                theorem Matroid.ofExistsMatroid_E {α : Type u_1} (E : Set α) (Indep : Set αProp) (hM : ∃ (M : Matroid α), E = M.E ∀ (I : Set α), M.Indep I Indep I) :
                (Matroid.ofExistsMatroid E Indep hM).E = E
                def Matroid.ofExistsMatroid {α : Type u_1} (E : Set α) (Indep : Set αProp) (hM : ∃ (M : Matroid α), E = M.E ∀ (I : Set α), M.Indep I Indep I) :

                Construct an Matroid from an independence predicate that agrees with that of some matroid M. This is computable even if M is only known existentially, or when M exists for different reasons in different cases. This can also be used to change the independence predicate to a more useful definitional form.

                Equations
                • Matroid.ofExistsMatroid E Indep hM = (let_fun hex := ; { E := E, Indep := Indep, indep_empty := , indep_subset := , indep_aug := , indep_maximal := , subset_ground := }).matroid
                Instances For
                  @[simp]
                  theorem Matroid.ofBase_E {α : Type u_1} (E : Set α) (Base : Set αProp) (exists_base : ∃ (B : Set α), Base B) (base_exchange : Matroid.ExchangeProperty Base) (maximality : XE, Matroid.ExistsMaximalSubsetProperty (fun (x : Set α) => ∃ (B : Set α), Base B x B) X) (subset_ground : ∀ (B : Set α), Base BB E) :
                  (Matroid.ofBase E Base exists_base base_exchange maximality subset_ground).E = E
                  def Matroid.ofBase {α : Type u_1} (E : Set α) (Base : Set αProp) (exists_base : ∃ (B : Set α), Base B) (base_exchange : Matroid.ExchangeProperty Base) (maximality : XE, Matroid.ExistsMaximalSubsetProperty (fun (x : Set α) => ∃ (B : Set α), Base B x B) X) (subset_ground : ∀ (B : Set α), Base BB E) :

                  A matroid defined purely in terms of its bases.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem Matroid.ofExistsFiniteBase_E {α : Type u_1} (E : Set α) (Base : Set αProp) (exists_finite_base : ∃ (B : Set α), Base B B.Finite) (base_exchange : Matroid.ExchangeProperty Base) (subset_ground : ∀ (B : Set α), Base BB E) :
                    (Matroid.ofExistsFiniteBase E Base exists_finite_base base_exchange subset_ground).E = E
                    def Matroid.ofExistsFiniteBase {α : Type u_1} (E : Set α) (Base : Set αProp) (exists_finite_base : ∃ (B : Set α), Base B B.Finite) (base_exchange : Matroid.ExchangeProperty Base) (subset_ground : ∀ (B : Set α), Base BB E) :

                    A collection of bases with the exchange property and at least one finite member is a matroid

                    Equations
                    Instances For
                      @[simp]
                      theorem Matroid.ofExistsFiniteBase_base {α : Type u_1} (E : Set α) (Base : Set αProp) (exists_finite_base : ∃ (B : Set α), Base B B.Finite) (base_exchange : Matroid.ExchangeProperty Base) (subset_ground : ∀ (B : Set α), Base BB E) :
                      (Matroid.ofExistsFiniteBase E Base exists_finite_base base_exchange subset_ground).Base = Base
                      instance Matroid.ofExistsFiniteBase_finiteRk {α : Type u_1} (E : Set α) (Base : Set αProp) (exists_finite_base : ∃ (B : Set α), Base B B.Finite) (base_exchange : Matroid.ExchangeProperty Base) (subset_ground : ∀ (B : Set α), Base BB E) :
                      (Matroid.ofExistsFiniteBase E Base exists_finite_base base_exchange subset_ground).FiniteRk
                      Equations
                      • =
                      def Matroid.ofBaseOfFinite {α : Type u_1} {E : Set α} (hE : E.Finite) (Base : Set αProp) (exists_base : ∃ (B : Set α), Base B) (base_exchange : Matroid.ExchangeProperty Base) (subset_ground : ∀ (B : Set α), Base BB E) :

                      If E is finite, then any nonempty collection of its subsets with the exchange property is the collection of bases of a matroid on E.

                      Equations
                      Instances For
                        @[simp]
                        theorem Matroid.ofBaseOfFinite_E {α : Type u_1} {E : Set α} (hE : E.Finite) (Base : Set αProp) (exists_base : ∃ (B : Set α), Base B) (base_exchange : Matroid.ExchangeProperty Base) (subset_ground : ∀ (B : Set α), Base BB E) :
                        (Matroid.ofBaseOfFinite hE Base exists_base base_exchange subset_ground).E = E
                        @[simp]
                        theorem Matroid.ofBaseOfFinite_base {α : Type u_1} {E : Set α} (hE : E.Finite) (Base : Set αProp) (exists_base : ∃ (B : Set α), Base B) (base_exchange : Matroid.ExchangeProperty Base) (subset_ground : ∀ (B : Set α), Base BB E) :
                        (Matroid.ofBaseOfFinite hE Base exists_base base_exchange subset_ground).Base = Base
                        instance Matroid.ofBaseOfFinite_finite {α : Type u_1} {E : Set α} (hE : E.Finite) (Base : Set αProp) (exists_base : ∃ (B : Set α), Base B) (base_exchange : Matroid.ExchangeProperty Base) (subset_ground : ∀ (B : Set α), Base BB E) :
                        (Matroid.ofBaseOfFinite hE Base exists_base base_exchange subset_ground).Finite
                        Equations
                        • =