English
Finitary matroids have a cardinality-valued rank function (invariant cardinal rank).
Русский
У конечноподобных матроидов имеется ранговая функция с кардиналами (инвариантная кардинальная ранг).
LaTeX
$$[Finitary M] ⇒ InvariantCardinalRank M$$
Lean4
/-- `Finitary` matroids have a cardinality-valued rank function. -/
instance invariantCardinalRank_of_finitary [Finitary M] : InvariantCardinalRank M :=
by
suffices aux : ∀ ⦃B B'⦄ ⦃N : Matroid α⦄, Finitary N → N.IsBase B → N.IsBase B' → #(B \ B' : Set α) ≤ #(B' \ B : Set α)
from
⟨fun I J X hI hJ ↦
(aux (restrict_finitary X) hI.isBase_restrict hJ.isBase_restrict).antisymm
(aux (restrict_finitary X) hJ.isBase_restrict hI.isBase_restrict)⟩
intro B B' N hfin hB hB'
by_cases h : (B' \ B).Finite
· rw [← cast_ncard h, ← cast_ncard, hB.ncard_diff_comm hB']
exact (hB'.diff_finite_comm hB).mp h
rw [← Set.Infinite, ← infinite_coe_iff] at h
have (a : α) (ha : a ∈ B' \ B) : ∃ S : Set α, Finite S ∧ S ⊆ B ∧ ¬N.Indep (insert a S) :=
by
have := (hB.insert_dep ⟨hB'.subset_ground ha.1, ha.2⟩).1
contrapose! this
exact
Finitary.indep_of_forall_finite _ fun J hJ fin ↦
(this (J \ { a }) fin.diff.to_subtype <| diff_singleton_subset_iff.mpr hJ).subset
(subset_insert_diff_singleton ..)
choose S S_fin hSB dep using this
let U := ⋃ a : ↥(B' \ B), S a a.2
suffices B \ B' ⊆ U
by
refine
(mk_le_mk_of_subset this).trans <| (mk_iUnion_le ..).trans <| (mul_le_max_of_aleph0_le_left (by simp)).trans ?_
simp only [sup_le_iff, le_refl, true_and]
exact ciSup_le' fun e ↦ (lt_aleph0_of_finite _).le.trans <| by simp
rw [← diff_inter_self_eq_diff, diff_subset_iff, inter_comm]
have hUB : (B ∩ B') ∪ U ⊆ B := union_subset inter_subset_left (iUnion_subset fun e ↦ (hSB e.1 e.2))
by_contra hBU
have ⟨a, ha, ind⟩ := hB.exists_insert_of_ssubset ⟨hUB, hBU⟩ hB'
have : a ∈ B' \ B := ⟨ha.1, fun haB ↦ ha.2 (.inl ⟨haB, ha.1⟩)⟩
refine dep a this (ind.subset <| insert_subset_insert <| .trans ?_ subset_union_right)
exact subset_iUnion_of_subset ⟨a, this⟩ subset_rfl
