Some constructions of matroids

This file defines some very elementary examples of matroids, namely those with at most one base.

Main definitions

• emptyOn α is the matroid on α with empty ground set.

For E : Set α, ...

• loopyOn E is the matroid on E whose elements are all loops, or equivalently in which ∅ is the only base.
• freeOn E is the 'free matroid' whose ground set E is the only base.
• For I ⊆ E, uniqueBaseOn I E is the matroid with ground set E in which I is the only base.

Implementation details

To avoid the tedious process of certifying the matroid axioms for each of these easy examples, we bootstrap the definitions starting with emptyOn α (which simp can prove is a matroid) and then construct the other examples using duality and restriction.

def Matroid.emptyOn (α : Type u_2) : Matroid α

The Matroid α with empty ground set.

@[simp]

theorem Matroid.emptyOn_ground {α : Type u_1} : (emptyOn α).E = ∅

@[simp]

theorem Matroid.emptyOn_isBase_iff {α : Type u_1} {B : Set α} : (emptyOn α).IsBase B ↔ B = ∅

@[simp]

theorem Matroid.emptyOn_indep_iff {α : Type u_1} {I : Set α} : (emptyOn α).Indep I ↔ I = ∅

theorem Matroid.ground_eq_empty_iff {α : Type u_1} {M : Matroid α} : M.E = ∅ ↔ M = emptyOn α

@[simp]

theorem Matroid.emptyOn_dual_eq {α : Type u_1} : (emptyOn α)✶ = emptyOn α

@[simp]

theorem Matroid.restrict_empty {α : Type u_1} (M : Matroid α) : M.restrict ∅ = emptyOn α

theorem Matroid.eq_emptyOn_or_nonempty {α : Type u_1} (M : Matroid α) : M = emptyOn α ∨ M.Nonempty

theorem Matroid.eq_emptyOn {α : Type u_1} [IsEmpty α] (M : Matroid α) : M = emptyOn α

instance Matroid.finite_emptyOn (α : Type u_2) : (emptyOn α).Finite

def Matroid.loopyOn {α : Type u_1} (E : Set α) : Matroid α

The Matroid α with ground set E whose only base is ∅. The elements are all 'loops' - see Matroid.IsLoop and Matroid.loopyOn_isLoop_iff.

@[simp]

theorem Matroid.loopyOn_ground {α : Type u_1} (E : Set α) : (loopyOn E).E = E

@[simp]

theorem Matroid.loopyOn_empty (α : Type u_2) : loopyOn ∅ = emptyOn α

@[simp]

theorem Matroid.loopyOn_indep_iff {α : Type u_1} {E I : Set α} : (loopyOn E).Indep I ↔ I = ∅

theorem Matroid.eq_loopyOn_iff {α : Type u_1} {M : Matroid α} {E : Set α} : M = loopyOn E ↔ M.E = E ∧ ∀ X ⊆ M.E, M.Indep X → X = ∅

@[simp]

theorem Matroid.loopyOn_isBase_iff {α : Type u_1} {E B : Set α} : (loopyOn E).IsBase B ↔ B = ∅

@[simp]

theorem Matroid.loopyOn_isBasis_iff {α : Type u_1} {E I X : Set α} : (loopyOn E).IsBasis I X ↔ I = ∅ ∧ X ⊆ E

instance Matroid.loopyOn_rankFinite {α : Type u_1} {E : Set α} : (loopyOn E).RankFinite

theorem Matroid.Finite.loopyOn_finite {α : Type u_1} {E : Set α} (hE : E.Finite) : (loopyOn E).Finite

@[simp]

theorem Matroid.loopyOn_restrict {α : Type u_1} (E R : Set α) : (loopyOn E).restrict R = loopyOn R

theorem Matroid.empty_isBase_iff {α : Type u_1} {M : Matroid α} : M.IsBase ∅ ↔ M = loopyOn M.E

theorem Matroid.eq_loopyOn_or_rankPos {α : Type u_1} (M : Matroid α) : M = loopyOn M.E ∨ M.RankPos

theorem Matroid.not_rankPos_iff {α : Type u_1} {M : Matroid α} : ¬M.RankPos ↔ M = loopyOn M.E

def Matroid.freeOn {α : Type u_1} (E : Set α) : Matroid α

The Matroid α with ground set E whose only base is E.

@[simp]

theorem Matroid.freeOn_ground {α : Type u_1} {E : Set α} : (freeOn E).E = E

@[simp]

theorem Matroid.freeOn_dual_eq {α : Type u_1} {E : Set α} : (freeOn E)✶ = loopyOn E

@[simp]

theorem Matroid.loopyOn_dual_eq {α : Type u_1} {E : Set α} : (loopyOn E)✶ = freeOn E

@[simp]

theorem Matroid.freeOn_empty (α : Type u_2) : freeOn ∅ = emptyOn α

@[simp]

theorem Matroid.freeOn_isBase_iff {α : Type u_1} {E B : Set α} : (freeOn E).IsBase B ↔ B = E

@[simp]

theorem Matroid.freeOn_indep_iff {α : Type u_1} {E I : Set α} : (freeOn E).Indep I ↔ I ⊆ E

theorem Matroid.freeOn_indep {α : Type u_1} {E I : Set α} (hIE : I ⊆ E) : (freeOn E).Indep I

@[simp]

theorem Matroid.freeOn_isBasis_iff {α : Type u_1} {E I X : Set α} : (freeOn E).IsBasis I X ↔ I = X ∧ X ⊆ E

@[simp]

theorem Matroid.freeOn_isBasis'_iff {α : Type u_1} {E I X : Set α} : (freeOn E).IsBasis' I X ↔ I = X ∩ E

theorem Matroid.eq_freeOn_iff {α : Type u_1} {M : Matroid α} {E : Set α} : M = freeOn E ↔ M.E = E ∧ M.Indep E

theorem Matroid.ground_indep_iff_eq_freeOn {α : Type u_1} {M : Matroid α} : M.Indep M.E ↔ M = freeOn M.E

theorem Matroid.freeOn_restrict {α : Type u_1} {E R : Set α} (h : R ⊆ E) : (freeOn E).restrict R = freeOn R

theorem Matroid.restrict_eq_freeOn_iff {α : Type u_1} {M : Matroid α} {I : Set α} : M.restrict I = freeOn I ↔ M.Indep I

theorem Matroid.Indep.restrict_eq_freeOn {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : M.restrict I = freeOn I

instance Matroid.freeOn_finitary {α : Type u_1} {E : Set α} : (freeOn E).Finitary

theorem Matroid.freeOn_rankPos {α : Type u_1} {E : Set α} (hE : E.Nonempty) : (freeOn E).RankPos

def Matroid.uniqueBaseOn {α : Type u_1} (I E : Set α) : Matroid α

The matroid on E whose unique base is the subset I of E. Intended for use when I ⊆ E; if this is not the case, then the base is I ∩ E.

@[simp]

theorem Matroid.uniqueBaseOn_ground {α : Type u_1} {E I : Set α} : (uniqueBaseOn I E).E = E

theorem Matroid.uniqueBaseOn_isBase_iff {α : Type u_1} {E B I : Set α} (hIE : I ⊆ E) : (uniqueBaseOn I E).IsBase B ↔ B = I

theorem Matroid.uniqueBaseOn_inter_ground_eq {α : Type u_1} (I E : Set α) : uniqueBaseOn (I ∩ E) E = uniqueBaseOn I E

@[simp]

theorem Matroid.uniqueBaseOn_indep_iff' {α : Type u_1} {E I J : Set α} : (uniqueBaseOn I E).Indep J ↔ J ⊆ I ∩ E

theorem Matroid.uniqueBaseOn_indep_iff {α : Type u_1} {E I J : Set α} (hIE : I ⊆ E) : (uniqueBaseOn I E).Indep J ↔ J ⊆ I

theorem Matroid.uniqueBaseOn_isBasis_iff {α : Type u_1} {E I X J : Set α} (hX : X ⊆ E) : (uniqueBaseOn I E).IsBasis J X ↔ J = X ∩ I

theorem Matroid.uniqueBaseOn_inter_isBasis {α : Type u_1} {E I X : Set α} (hX : X ⊆ E) : (uniqueBaseOn I E).IsBasis (X ∩ I) X

@[simp]

theorem Matroid.uniqueBaseOn_dual_eq {α : Type u_1} (I E : Set α) : (uniqueBaseOn I E)✶ = uniqueBaseOn (E \ I) E

@[simp]

theorem Matroid.uniqueBaseOn_self {α : Type u_1} (I : Set α) : uniqueBaseOn I I = freeOn I

@[simp]

theorem Matroid.uniqueBaseOn_empty {α : Type u_1} (I : Set α) : uniqueBaseOn ∅ I = loopyOn I

theorem Matroid.uniqueBaseOn_restrict' {α : Type u_1} (I E R : Set α) : (uniqueBaseOn I E).restrict R = uniqueBaseOn (I ∩ R ∩ E) R

theorem Matroid.uniqueBaseOn_restrict {α : Type u_1} {E I : Set α} (h : I ⊆ E) (R : Set α) : (uniqueBaseOn I E).restrict R = uniqueBaseOn (I ∩ R) R

theorem Matroid.uniqueBaseOn_rankFinite {α : Type u_1} {E I : Set α} (hI : I.Finite) : (uniqueBaseOn I E).RankFinite

instance Matroid.uniqueBaseOn_finitary {α : Type u_1} {E I : Set α} : (uniqueBaseOn I E).Finitary

theorem Matroid.uniqueBaseOn_rankPos {α : Type u_1} {E I : Set α} (hIE : I ⊆ E) (hI : I.Nonempty) : (uniqueBaseOn I E).RankPos