Cardinal-valued rank

In a finitary matroid, all bases have the same cardinality. In fact, something stronger holds: if I and J are both bases for a set X, then #(I \ J) = #(J \ I) and (consequently) #I = #J. This file introduces a typeclass InvariantCardinalRank that applies to any matroid such that this property holds for all I, J and X.

A matroid satisfying this condition has a well-defined cardinality-valued rank function, both for itself and all its minors.

Main Declarations

• Matroid.InvariantCardinalRank : a typeclass capturing the idea that a matroid and all its minors have a well-behaved cardinal-valued rank function.
• Matroid.cRank M is the supremum of the cardinalities of the bases of matroid M.
• Matroid.cRk M X is the supremum of the cardinalities of the bases of a set X in a matroid M.
• invariantCardinalRank_of_finitary is the instance showing that Finitary matroids are InvariantCardinalRank.
• cRk_inter_add_cRk_union_le states that cardinal rank is submodular.

Notes

It is not the case that all matroids are InvariantCardinalRank, since the equicardinality of bases in general matroids is independent of ZFC (see the module docstring of Mathlib.Combinatorics.Matroid.Basic). Lemmas like Matroid.IsBase.cardinalMk_diff_comm become true for all matroids only if they are weakened by replacing Cardinal.mk with the cruder ℕ∞-valued Set.encard; see, for example, Matroid.IsBase.encard_sdiff_comm.

Implementation Details

Since the functions cRank and cRk are defined as suprema, independently of the Matroid.InvariantCardinalRank typeclass, they are well-defined for all matroids. However, for matroids that do not satisfy InvariantCardinalRank, they are badly behaved. For instance, in general cRk is not submodular, and its value may differ on a set X and the closure of X. We state and prove theorems without the instance whenever possible, which sometime makes their proofs longer than they would be with the instance.

TODO

• Higgs' theorem : if the generalized continuum hypothesis holds, then every matroid is InvariantCardinalRank.

  Sketch : If the generalized continuum hypothesis is true, then there is a chain of size 2 ^ #B contained in each base B. Then IsBase.two_pow_cardinalMk_ge_of_isBase_isChain implies that 2 ^ #B ≤ 2 ^ #B' for each pair B, B' of bases. By GCH, this gives #B = #B'.

@[simp]

theorem Matroid.cRank_eq_zero {α : Type u} {M : Matroid α} : M.cRank = 0 ↔ ∃ (E : Set α), M = loopyOn E

theorem Matroid.cRank_eq_zero_iff {α : Type u} {M : Matroid α} : M.cRank = 0 ↔ M = loopyOn M.E

theorem Matroid.cRk_eq_zero_iff' {α : Type u} {M : Matroid α} {X : Set α} : M.cRk X = 0 ↔ X ∩ M.E ⊆ M.loops

A version of Matroid.cRk_eq_zero_iff applying to sets not contained in the ground set.

theorem Matroid.cRk_le_one_iff {α : Type u} {M : Matroid α} {X : Set α} [Nonempty α] (hX : X ⊆ M.E := by aesop_mat) : M.cRk X ≤ 1 ↔ ∃ (e : α), X ⊆ M.closure {e}

theorem Matroid.crk_lt_aleph0_iff {α : Type u} {M : Matroid α} {X : Set α} : M.cRk X < Cardinal.aleph0 ↔ M.IsRkFinite X

theorem Matroid.cRank_lt_aleph0_iff {α : Type u} {M : Matroid α} : M.cRank < Cardinal.aleph0 ↔ M.RankFinite

@[simp]

theorem Matroid.cRank_toENat {α : Type u} (M : Matroid α) : Cardinal.toENat M.cRank = M.eRank

@[simp]

theorem Matroid.cRk_toENat {α : Type u} (M : Matroid α) (X : Set α) : Cardinal.toENat (M.cRk X) = M.eRk X

@[simp]

theorem Matroid.cRank_toNat {α : Type u} (M : Matroid α) : Cardinal.toNat M.cRank = M.rank

@[simp]

theorem Matroid.cRk_toNat {α : Type u} (M : Matroid α) (X : Set α) : Cardinal.toNat (M.cRk X) = M.rk X

theorem Matroid.IsBase.nonempty_embedding_of_isBase_isChain {α : Type u} {M : Matroid α} {B B' : Set α} (hB : M.IsBase B) (hB' : M.IsBase B') (S : Set (Set α)) (hS : ∀ X ∈ S, X ⊆ B) (hS_chain : IsChain (fun (x1 x2 : Set α) => x1 ⊆ x2) S) : Nonempty (↑S ↪ Set ↑B')

theorem Matroid.Indep.nonempty_embedding_set_of_isBase {α : Type u} {M : Matroid α} {I B : Set α} (hI : M.Indep I) (hB : M.IsBase B) : Nonempty (↑I ↪ Set ↑B)

No independent set is larger than the power set of a base.

theorem Matroid.IsBase.two_pow_cardinalMk_ge_of_isBase_isChain {α : Type u} {M : Matroid α} {B B' : Set α} (hB : M.IsBase B) (hB' : M.IsBase B') (S : Set (Set α)) (hS : ∀ X ∈ S, X ⊆ B) (hS_chain : IsChain (fun (x1 x2 : Set α) => x1 ⊆ x2) S) : Cardinal.mk ↑S ≤ 2 ^ Cardinal.mk ↑B'

theorem Matroid.IsBase.two_pow_cardinalMk_ge_of_isBase {α : Type u} {M : Matroid α} {B B' : Set α} (hB : M.IsBase B) (hB' : M.IsBase B') : Cardinal.mk ↑B' ≤ 2 ^ Cardinal.mk ↑B

theorem Matroid.Indep.two_pow_cardinalMk_ge_of_isBase {α : Type u} {M : Matroid α} {I B : Set α} (hI : M.Indep I) (hB : M.IsBase B) : Cardinal.mk ↑I ≤ 2 ^ Cardinal.mk ↑B

theorem Matroid.IsBase.cRank_le_two_pow_cardinalMk {α : Type u} {M : Matroid α} {B : Set α} (hB : M.IsBase B) : M.cRank ≤ 2 ^ Cardinal.mk ↑B