ℕ∞-valued rank

If the 'cardinality' of s : Set α is taken to mean the ℕ∞-valued term Set.encard s, then all bases of any M : Matroid α have the same cardinality, and for each X : Set α with X ⊆ M.E, all M-bases for X have the same cardinality. The 'rank' of a matroid is the cardinality of all its bases, and the 'rank' of a set X in a matroid M is the cardinality of each M-basis of X. This file defines these two concepts as a term Matroid.eRank M : ℕ∞ and a function Matroid.eRk M : Set α → ℕ∞ respectively.

The rank function Matroid.eRk satisfies three properties, often known as (R1), (R2), (R3):

• M.eRk X ≤ Set.encard X,
• M.eRk X ≤ M.eRk Y for all X ⊆ Y,
• M.eRk X + M.eRk Y ≥ M.eRk (X ∪ Y) + M.eRk (X ∩ Y) for all X, Y. In fact, if α is finite, then any function Set α → ℕ∞ satisfying these these properties is the rank function of a Matroid α; in other words, properties (R1) - (R3) give an alternative definition of finite matroids, and a finite matroid is determined by its rank function. Because of this, and the convenient quantitative language of these axioms, the rank function is often the preferred perspective on matroids in the literature. (The above doesn't work as well for infinite matroids, which is why mathlib defines matroids using bases/independence. )

Main Declarations

• Matroid.eRank M is the ℕ∞-valued cardinality of each base of M.
• Matroid.eRk M X is the ℕ∞-valued cardinality of each M-basis of X.
• Matroid.eRk_inter_add_eRk_union_le : the function M.eRk is submodular.

Notes

It is natural to ask if equicardinality of bases holds if 'cardinality' refers to a term in Cardinal instead of ℕ∞, but the answer is that it doesn't. The cardinal-valued rank functions Matroid.cRank and Matroid.cRk are defined in Data.Matroid.Rank.Cardinal, but have less desirable properties in general. See the module docstring of that file for a discussion.

Implementation Details

It would be equivalent to define Matroid.eRank (M : Matroid α) := (Matroid.cRank M).toENat and similar for Matroid.eRk, and some of the API for cRank/cRk would carry over in a way that shortens certain proofs in this file (though not substantially). Although this file transitively imports Cardinal via Set.encard, there are plans to refactor the latter to be independent of the former, which would carry over to the current version of this file.

noncomputable def Matroid.eRank {α : Type u_1} (M : Matroid α) : ℕ∞

The rank Matroid.eRank M of M is the ℕ∞-valued cardinality of each base of M. (See Matroid.cRank for a worse-behaved cardinal-valued version)

Equations

• M.eRank = ⨆ (B : { B : Set α // M.IsBase B }), (↑B).encard

noncomputable def Matroid.eRk {α : Type u_1} (M : Matroid α) (X : Set α) : ℕ∞

The rank Matroid.eRk M X of a set X is the ℕ∞-valued cardinality of each basis of X. (See Matroid.cRk for a worse-behaved cardinal-valued version)

Equations

• M.eRk X = (M.restrict X).eRank

theorem Matroid.eRank_def {α : Type u_1} (M : Matroid α) : M.eRank = M.eRk M.E

@[simp]

theorem Matroid.eRank_restrict {α : Type u_1} (M : Matroid α) (X : Set α) : (M.restrict X).eRank = M.eRk X

theorem Matroid.IsBase.encard_eq_eRank {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.IsBase B) : B.encard = M.eRank

theorem Matroid.IsBasis'.encard_eq_eRk {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis' I X) : I.encard = M.eRk X

theorem Matroid.IsBasis.encard_eq_eRk {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.IsBasis I X) : I.encard = M.eRk X

theorem Matroid.eq_eRk_iff {α : Type u_1} {M : Matroid α} {X : Set α} {n : ℕ∞} (hX : X ⊆ M.E := by aesop_mat) : M.eRk X = n ↔ ∃ (I : Set α), M.IsBasis I X ∧ I.encard = n

theorem Matroid.Indep.eRk_eq_encard {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : M.eRk I = I.encard

theorem Matroid.IsBasis'.eRk_eq_eRk {α : Type u_1} {M : Matroid α} {I X : Set α} (hIX : M.IsBasis' I X) : M.eRk I = M.eRk X

theorem Matroid.IsBasis.eRk_eq_eRk {α : Type u_1} {M : Matroid α} {I X : Set α} (hIX : M.IsBasis I X) : M.eRk I = M.eRk X

theorem Matroid.IsBasis'.eRk_eq_encard {α : Type u_1} {M : Matroid α} {I X : Set α} (hIX : M.IsBasis' I X) : M.eRk X = I.encard

theorem Matroid.IsBasis.eRk_eq_encard {α : Type u_1} {M : Matroid α} {I X : Set α} (hIX : M.IsBasis I X) : M.eRk X = I.encard

theorem Matroid.IsBase.eRk_eq_eRank {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.IsBase B) : M.eRk B = M.eRank

@[simp]

theorem Matroid.eRank_map {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : α → β) (hf : Set.InjOn f M.E) : (M.map f hf).eRank = M.eRank

@[simp]

theorem Matroid.eRank_loopyOn {α : Type u_1} (E : Set α) : (loopyOn E).eRank = 0

@[simp]

theorem Matroid.eRank_emptyOn (α : Type u_2) : (emptyOn α).eRank = 0

@[simp]

theorem Matroid.eRk_ground {α : Type u_1} (M : Matroid α) : M.eRk M.E = M.eRank

@[simp]

theorem Matroid.eRk_inter_ground {α : Type u_1} (M : Matroid α) (X : Set α) : M.eRk (X ∩ M.E) = M.eRk X

@[simp]

theorem Matroid.eRk_ground_inter {α : Type u_1} (M : Matroid α) (X : Set α) : M.eRk (M.E ∩ X) = M.eRk X

theorem Matroid.eRk_eq_eRank {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.E ⊆ X) : M.eRk X = M.eRank

@[simp]

theorem Matroid.eRk_union_ground {α : Type u_1} (M : Matroid α) (X : Set α) : M.eRk (X ∪ M.E) = M.eRank

@[simp]

theorem Matroid.eRk_ground_union {α : Type u_1} (M : Matroid α) (X : Set α) : M.eRk (M.E ∪ X) = M.eRank

theorem Matroid.eRk_insert_of_not_mem_ground {α : Type u_1} {M : Matroid α} {e : α} (X : Set α) (he : e ∉ M.E) : M.eRk (insert e X) = M.eRk X

theorem Matroid.eRk_compl_union_of_disjoint {α : Type u_1} {X Y : Set α} (M : Matroid α) (hXY : Disjoint X Y) : M.eRk (M.E \ X ∪ Y) = M.eRk (M.E \ X)

theorem Matroid.one_le_eRank {α : Type u_1} (M : Matroid α) [M.RankPos] : 1 ≤ M.eRank

theorem Matroid.rankFinite_iff_eRank_ne_top {α : Type u_1} (M : Matroid α) : M.RankFinite ↔ M.eRank ≠ ⊤

theorem Matroid.rankInfinite_iff_eRank_eq_top {α : Type u_1} (M : Matroid α) : M.RankInfinite ↔ M.eRank = ⊤

@[simp]

theorem Matroid.eRank_eq_top {α : Type u_1} {M : Matroid α} [M.RankInfinite] : M.eRank = ⊤

@[simp]

theorem Matroid.eRk_map_eq {α : Type u_1} {X : Set α} {β : Type u_2} {f : α → β} (M : Matroid α) (hf : Set.InjOn f M.E) (hX : X ⊆ M.E := by aesop_mat) : (M.map f hf).eRk (f '' X) = M.eRk X

@[simp]

theorem Matroid.eRk_comap_eq {α : Type u_1} {β : Type u_2} {f : α → β} (M : Matroid β) (X : Set α) : (M.comap f).eRk X = M.eRk (f '' X)

@[simp]

theorem Matroid.eRk_univ_eq {α : Type u_1} (M : Matroid α) : M.eRk Set.univ = M.eRank

@[simp]

theorem Matroid.eRk_empty {α : Type u_1} (M : Matroid α) : M.eRk ∅ = 0

@[simp]

theorem Matroid.eRk_closure_eq {α : Type u_1} (M : Matroid α) (X : Set α) : M.eRk (M.closure X) = M.eRk X

@[simp]

theorem Matroid.eRk_union_closure_right_eq {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRk (X ∪ M.closure Y) = M.eRk (X ∪ Y)

@[simp]

theorem Matroid.eRk_union_closure_left_eq {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRk (M.closure X ∪ Y) = M.eRk (X ∪ Y)

@[simp]

theorem Matroid.eRk_insert_closure_eq {α : Type u_1} (M : Matroid α) (e : α) (X : Set α) : M.eRk (insert e (M.closure X)) = M.eRk (insert e X)

@[simp]

theorem Matroid.restrict_eRk_eq' {α : Type u_1} (M : Matroid α) (R X : Set α) : (M.restrict R).eRk X = M.eRk (X ∩ R)

A version of Matroid.restrict_eRk_eq with no X ⊆ R hypothesis and thus a less simple RHS.

theorem Matroid.restrict_eRk_eq {α : Type u_1} {X : Set α} (M : Matroid α) {R : Set α} (h : X ⊆ R) : (M.restrict R).eRk X = M.eRk X

theorem Matroid.eRk_lt_top_of_finite {α : Type u_1} {X : Set α} (M : Matroid α) (hX : X.Finite) : M.eRk X < ⊤

theorem Matroid.IsBasis'.eRk_eq_eRk_union {α : Type u_1} {M : Matroid α} {I X : Set α} (hIX : M.IsBasis' I X) (Y : Set α) : M.eRk (I ∪ Y) = M.eRk (X ∪ Y)

theorem Matroid.IsBasis'.eRk_eq_eRk_insert {α : Type u_1} {M : Matroid α} {I X : Set α} (hIX : M.IsBasis' I X) (e : α) : M.eRk (insert e I) = M.eRk (insert e X)

theorem Matroid.IsBasis.eRk_eq_eRk_union {α : Type u_1} {M : Matroid α} {I X : Set α} (hIX : M.IsBasis I X) (Y : Set α) : M.eRk (I ∪ Y) = M.eRk (X ∪ Y)

theorem Matroid.IsBasis.eRk_eq_eRk_insert {α : Type u_1} {M : Matroid α} {I X : Set α} (hIX : M.IsBasis I X) (e : α) : M.eRk (insert e I) = M.eRk (insert e X)

theorem Matroid.eRk_le_encard {α : Type u_1} (M : Matroid α) (X : Set α) : M.eRk X ≤ X.encard

theorem Matroid.eRank_le_encard_ground {α : Type u_1} (M : Matroid α) : M.eRank ≤ M.E.encard

theorem Matroid.eRk_mono {α : Type u_1} (M : Matroid α) : Monotone M.eRk

theorem Matroid.eRk_le_eRank {α : Type u_1} (M : Matroid α) (X : Set α) : M.eRk X ≤ M.eRank

theorem Matroid.le_eRk_iff {α : Type u_1} {M : Matroid α} {X : Set α} {n : ℕ∞} : n ≤ M.eRk X ↔ ∃ I ⊆ X, M.Indep I ∧ I.encard = n

theorem Matroid.eRk_le_iff {α : Type u_1} {M : Matroid α} {X : Set α} {n : ℕ∞} : M.eRk X ≤ n ↔ ∀ ⦃I : Set α⦄, I ⊆ X → M.Indep I → I.encard ≤ n

theorem Matroid.Indep.encard_le_eRk_of_subset {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Indep I) (hIX : I ⊆ X) : I.encard ≤ M.eRk X

theorem Matroid.Indep.encard_le_eRank {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : I.encard ≤ M.eRank

theorem Matroid.eRk_inter_add_eRk_union_le {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y

The ℕ∞-valued rank function is submodular.

theorem Matroid.eRk_submod {α : Type u_1} (M : Matroid α) (X Y : Set α) : M.eRk (X ∩ Y) + M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y

Alias of Matroid.eRk_inter_add_eRk_union_le.

---

The ℕ∞-valued rank function is submodular.