Cardinal-valued rank

In a finitary matroid, all bases have the same cardinality. In fact, something stronger holds: if each of I and J is a basis 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 (provably) 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/Data/Matroid/Basic.lean). Lemmas like Matroid.Base.cardinalMk_diff_comm become true for all matroids only if they are weakened by replacing Cardinal.mk with the cruder ℕ∞-valued Set.encard. The ℕ∞-valued rank and rank functions Matroid.eRank and Matroid.eRk, which have a more unconditionally strong API, are developed in Mathlib/Data/Matroid/Rank/ENat.lean.

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 InvariantCardinalRank 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.

noncomputable def Matroid.cRank {α : Type u} (M : Matroid α) : Cardinal.{u}

The rank (supremum of the cardinalities of bases) of a matroid M as a Cardinal. See Matroid.eRank for a better-behaved ℕ∞-valued version.

Equations

• M.cRank = ⨆ (B : { B : Set α // M.IsBase B }), Cardinal.mk ↑↑B

noncomputable def Matroid.cRk {α : Type u} (M : Matroid α) (X : Set α) : Cardinal.{u}

The rank (supremum of the cardinalities of bases) of a set X in a matroid M, as a Cardinal. See Matroid.eRk for a better-behaved ℕ∞-valued version.

Equations

• M.cRk X = (M.restrict X).cRank

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

theorem Matroid.Indep.cardinalMk_le_cRank {α : Type u} {M : Matroid α} {I : Set α} (ind : M.Indep I) : Cardinal.mk ↑I ≤ M.cRank

theorem Matroid.cRank_eq_iSup_cardinalMk_indep {α : Type u} {M : Matroid α} : M.cRank = ⨆ (I : { I : Set α // M.Indep I }), Cardinal.mk ↑↑I

theorem Matroid.IsBasis'.cardinalMk_le_cRk {α : Type u} {M : Matroid α} {I X : Set α} (hIX : M.IsBasis' I X) : Cardinal.mk ↑I ≤ M.cRk X

theorem Matroid.IsBasis.cardinalMk_le_cRk {α : Type u} {M : Matroid α} {I X : Set α} (hIX : M.IsBasis I X) : Cardinal.mk ↑I ≤ M.cRk X

theorem Matroid.cRank_le_iff {α : Type u} {M : Matroid α} {κ : Cardinal.{u}} : M.cRank ≤ κ ↔ ∀ ⦃B : Set α⦄, M.IsBase B → Cardinal.mk ↑B ≤ κ

theorem Matroid.cRk_le_iff {α : Type u} {M : Matroid α} {X : Set α} {κ : Cardinal.{u}} : M.cRk X ≤ κ ↔ ∀ ⦃I : Set α⦄, M.IsBasis' I X → Cardinal.mk ↑I ≤ κ

theorem Matroid.Indep.cardinalMk_le_cRk_of_subset {α : Type u} {M : Matroid α} {I X : Set α} (hI : M.Indep I) (hIX : I ⊆ X) : Cardinal.mk ↑I ≤ M.cRk X

theorem Matroid.cRk_le_cardinalMk {α : Type u} (M : Matroid α) (X : Set α) : M.cRk X ≤ Cardinal.mk ↑X

@[simp]

theorem Matroid.cRk_ground {α : Type u} (M : Matroid α) : M.cRk M.E = M.cRank

@[simp]

theorem Matroid.cRank_restrict {α : Type u} (M : Matroid α) (X : Set α) : (M.restrict X).cRank = M.cRk X

theorem Matroid.cRk_mono {α : Type u} (M : Matroid α) : Monotone M.cRk

theorem Matroid.cRk_le_of_subset {α : Type u} {X Y : Set α} (M : Matroid α) (hXY : X ⊆ Y) : M.cRk X ≤ M.cRk Y

@[simp]

theorem Matroid.cRk_inter_ground {α : Type u} (M : Matroid α) (X : Set α) : M.cRk (X ∩ M.E) = M.cRk X

theorem Matroid.cRk_restrict_subset {α : Type u} {X Y : Set α} (M : Matroid α) (hYX : Y ⊆ X) : (M.restrict X).cRk Y = M.cRk Y

theorem Matroid.cRk_restrict {α : Type u} (M : Matroid α) (X Y : Set α) : (M.restrict X).cRk Y = M.cRk (X ∩ Y)

theorem Matroid.Indep.cRk_eq_cardinalMk {α : Type u} {M : Matroid α} {I : Set α} (hI : M.Indep I) : Cardinal.mk ↑I = M.cRk I

@[simp]

theorem Matroid.cRk_map_image_lift {α : Type u} {β : Type v} {f : α → β} (M : Matroid α) (hf : Set.InjOn f M.E) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : Cardinal.lift.{u, v} ((M.map f hf).cRk (f '' X)) = Cardinal.lift.{v, u} (M.cRk X)

@[simp]

theorem Matroid.cRk_map_image {α β : Type u} {f : α → β} (M : Matroid α) (hf : Set.InjOn f M.E) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : (M.map f hf).cRk (f '' X) = M.cRk X

theorem Matroid.cRk_map_eq {α β : Type u} {f : α → β} {X : Set β} (M : Matroid α) (hf : Set.InjOn f M.E) : (M.map f hf).cRk X = M.cRk (f ⁻¹' X)

@[simp]

theorem Matroid.cRk_comap_lift {α : Type u} {β : Type v} (M : Matroid β) (f : α → β) (X : Set α) : Cardinal.lift.{v, u} ((M.comap f).cRk X) = Cardinal.lift.{u, v} (M.cRk (f '' X))

@[simp]

theorem Matroid.cRk_comap {α β : Type u} (M : Matroid β) (f : α → β) (X : Set α) : (M.comap f).cRk X = M.cRk (f '' X)

class Matroid.InvariantCardinalRank {α : Type u} (M : Matroid α) : Prop

A class stating that cardinality-valued rank is well-defined (i.e. all bases are equicardinal) for a matroid M and its minors. Notably, this holds for Finitary matroids; see Matroid.invariantCardinalRank_of_finitary.

• forall_card_isBasis_diff ⦃I J X : Set α⦄ : M.IsBasis I X → M.IsBasis J X → Cardinal.mk ↑(I \ J) = Cardinal.mk ↑(J \ I)

theorem Matroid.invariantCardinalRank_iff {α : Type u} (M : Matroid α) : M.InvariantCardinalRank ↔ ∀ ⦃I J X : Set α⦄, M.IsBasis I X → M.IsBasis J X → Cardinal.mk ↑(I \ J) = Cardinal.mk ↑(J \ I)

theorem Matroid.IsBasis.cardinalMk_diff_comm {α : Type u} {M : Matroid α} {I J X : Set α} [M.InvariantCardinalRank] (hIX : M.IsBasis I X) (hJX : M.IsBasis J X) : Cardinal.mk ↑(I \ J) = Cardinal.mk ↑(J \ I)

theorem Matroid.IsBasis'.cardinalMk_diff_comm {α : Type u} {M : Matroid α} {I J X : Set α} [M.InvariantCardinalRank] (hIX : M.IsBasis' I X) (hJX : M.IsBasis' J X) : Cardinal.mk ↑(I \ J) = Cardinal.mk ↑(J \ I)

theorem Matroid.IsBase.cardinalMk_diff_comm {α : Type u} {M : Matroid α} {B B' : Set α} [M.InvariantCardinalRank] (hB : M.IsBase B) (hB' : M.IsBase B') : Cardinal.mk ↑(B \ B') = Cardinal.mk ↑(B' \ B)

theorem Matroid.IsBasis.cardinalMk_eq {α : Type u} {M : Matroid α} {I J X : Set α} [M.InvariantCardinalRank] (hIX : M.IsBasis I X) (hJX : M.IsBasis J X) : Cardinal.mk ↑I = Cardinal.mk ↑J

theorem Matroid.IsBasis'.cardinalMk_eq {α : Type u} {M : Matroid α} {I J X : Set α} [M.InvariantCardinalRank] (hIX : M.IsBasis' I X) (hJX : M.IsBasis' J X) : Cardinal.mk ↑I = Cardinal.mk ↑J

theorem Matroid.IsBase.cardinalMk_eq {α : Type u} {M : Matroid α} {B B' : Set α} [M.InvariantCardinalRank] (hB : M.IsBase B) (hB' : M.IsBase B') : Cardinal.mk ↑B = Cardinal.mk ↑B'

theorem Matroid.Indep.cardinalMk_le_isBase {α : Type u} {M : Matroid α} {I B : Set α} [M.InvariantCardinalRank] (hI : M.Indep I) (hB : M.IsBase B) : Cardinal.mk ↑I ≤ Cardinal.mk ↑B

theorem Matroid.Indep.cardinalMk_le_isBasis' {α : Type u} {M : Matroid α} {I J X : Set α} [M.InvariantCardinalRank] (hI : M.Indep I) (hJ : M.IsBasis' J X) (hIX : I ⊆ X) : Cardinal.mk ↑I ≤ Cardinal.mk ↑J

theorem Matroid.Indep.cardinalMk_le_isBasis {α : Type u} {M : Matroid α} {I J X : Set α} [M.InvariantCardinalRank] (hI : M.Indep I) (hJ : M.IsBasis J X) (hIX : I ⊆ X) : Cardinal.mk ↑I ≤ Cardinal.mk ↑J

theorem Matroid.IsBase.cardinalMk_eq_cRank {α : Type u} {M : Matroid α} {B : Set α} [M.InvariantCardinalRank] (hB : M.IsBase B) : Cardinal.mk ↑B = M.cRank

instance Matroid.invariantCardinalRank_restrict {α : Type u} {M : Matroid α} {X : Set α} [M.InvariantCardinalRank] : (M.restrict X).InvariantCardinalRank

Restrictions of matroids with cardinal rank functions have cardinal rank functions.

theorem Matroid.IsBasis'.cardinalMk_eq_cRk {α : Type u} {M : Matroid α} {I X : Set α} [M.InvariantCardinalRank] (hIX : M.IsBasis' I X) : Cardinal.mk ↑I = M.cRk X

theorem Matroid.IsBasis.cardinalMk_eq_cRk {α : Type u} {M : Matroid α} {I X : Set α} [M.InvariantCardinalRank] (hIX : M.IsBasis I X) : Cardinal.mk ↑I = M.cRk X

@[simp]

theorem Matroid.cRk_closure {α : Type u} (M : Matroid α) [M.InvariantCardinalRank] (X : Set α) : M.cRk (M.closure X) = M.cRk X

theorem Matroid.cRk_closure_congr {α : Type u} {M : Matroid α} {X Y : Set α} [M.InvariantCardinalRank] (hXY : M.closure X = M.closure Y) : M.cRk X = M.cRk Y

theorem Matroid.Spanning.cRank_le_cardinalMk {α : Type u} {M : Matroid α} {X : Set α} [M.InvariantCardinalRank] (h : M.Spanning X) : M.cRank ≤ Cardinal.mk ↑X

@[simp]

theorem Matroid.cRk_union_closure_right_eq {α : Type u} (M : Matroid α) [M.InvariantCardinalRank] (X Y : Set α) : M.cRk (X ∪ M.closure Y) = M.cRk (X ∪ Y)

@[simp]

theorem Matroid.cRk_union_closure_left_eq {α : Type u} (M : Matroid α) [M.InvariantCardinalRank] (X Y : Set α) : M.cRk (M.closure X ∪ Y) = M.cRk (X ∪ Y)

@[simp]

theorem Matroid.cRk_insert_closure_eq {α : Type u} (M : Matroid α) [M.InvariantCardinalRank] (e : α) (X : Set α) : M.cRk (insert e (M.closure X)) = M.cRk (insert e X)

theorem Matroid.cRk_union_closure_eq {α : Type u} (M : Matroid α) [M.InvariantCardinalRank] (X Y : Set α) : M.cRk (M.closure X ∪ M.closure Y) = M.cRk (X ∪ Y)

theorem Matroid.cRk_inter_add_cRk_union_le {α : Type u} (M : Matroid α) [M.InvariantCardinalRank] (X Y : Set α) : M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y

The Cardinal rank function is submodular.

instance Matroid.invariantCardinalRank_of_finitary {α : Type u} {M : Matroid α} [M.Finitary] : M.InvariantCardinalRank

Finitary matroids have a cardinality-valued rank function.

instance Matroid.invariantCardinalRank_map {α : Type u} {β : Type v} {f : α → β} (M : Matroid α) [M.InvariantCardinalRank] (hf : Set.InjOn f M.E) : (M.map f hf).InvariantCardinalRank

instance Matroid.invariantCardinalRank_comap {α : Type u} {β : Type v} (M : Matroid β) [M.InvariantCardinalRank] (f : α → β) : (M.comap f).InvariantCardinalRank

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

theorem Matroid.rankInfinite_iff_aleph0_le_cRank {α : Type u} {M : Matroid α} : M.RankInfinite ↔ Cardinal.aleph0 ≤ M.cRank

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

theorem Matroid.Indep.isBase_of_cRank_le {α : Type u} {M : Matroid α} {I : Set α} [M.RankFinite] (ind : M.Indep I) (le : M.cRank ≤ Cardinal.mk ↑I) : M.IsBase I

theorem Matroid.Spanning.isBase_of_le_cRank {α : Type u} {M : Matroid α} {X : Set α} [M.RankFinite] (h : M.Spanning X) (le : Cardinal.mk ↑X ≤ M.cRank) : M.IsBase X

theorem Matroid.Indep.isBase_of_cRank_le_of_finite {α : Type u} {M : Matroid α} {I : Set α} (ind : M.Indep I) (le : M.cRank ≤ Cardinal.mk ↑I) (fin : I.Finite) : M.IsBase I

theorem Matroid.Spanning.isBase_of_le_cRank_of_finite {α : Type u} {M : Matroid α} {X : Set α} (h : M.Spanning X) (le : Cardinal.mk ↑X ≤ M.cRank) (fin : X.Finite) : M.IsBase X

@[simp]

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

@[simp]

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