Lean4
/-- An independence predicate satisfying the finite matroid axioms determines a matroid,
provided independence is determined by its behaviour on finite sets. -/
@[simps! E]
protected def ofFinitaryCardAugment (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅)
(indep_subset : ∀ ⦃I J⦄, Indep J → I ⊆ J → Indep I)
(indep_aug :
∀ ⦃I J⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
(indep_compact : ∀ I, (∀ J, J ⊆ I → J.Finite → Indep J) → Indep I) (subset_ground : ∀ I, Indep I → I ⊆ E) :
IndepMatroid α :=
IndepMatroid.ofFinitary (E := E) (Indep := Indep) (indep_empty := indep_empty) (indep_subset := indep_subset)
(indep_compact := indep_compact) (indep_aug :=
by
have htofin : ∀ I e, Indep I → ¬Indep (insert e I) → ∃ I₀, I₀ ⊆ I ∧ I₀.Finite ∧ ¬Indep (insert e I₀) :=
by
by_contra h; push_neg at h
obtain ⟨I, e, -, hIe, h⟩ := h
refine hIe <| indep_compact _ fun J hJss hJfin ↦ ?_
exact indep_subset (h (J \ { e }) (by rwa [diff_subset_iff]) hJfin.diff) (by simp)
intro I B hI hImax hBmax
obtain ⟨e, heI, hins⟩ := exists_insert_of_not_maximal indep_subset hI hImax
by_cases heB : e ∈ B
· exact ⟨e, ⟨heB, heI⟩, hins⟩
by_contra hcon; push_neg at hcon
have heBdep :=
hBmax.not_prop_of_ssuperset
(ssubset_insert heB)
-- There is a finite subset `B₀` of `B` so that `B₀ + e` is dependent
obtain ⟨B₀, hB₀B, hB₀fin, hB₀e⟩ := htofin B e hBmax.1 heBdep
have hB₀ := indep_subset hBmax.1 hB₀B
have hexI₀ : ∃ I₀, I₀ ⊆ I ∧ I₀.Finite ∧ ∀ x, x ∈ B₀ \ I₀ → ¬Indep (insert x I₀) :=
by
have hch : ∀ (b : ↑(B₀ \ I)), ∃ Ib, Ib ⊆ I ∧ Ib.Finite ∧ ¬Indep (insert (b : α) Ib) := by rintro ⟨b, hb⟩;
exact htofin I b hI (hcon b ⟨hB₀B hb.1, hb.2⟩)
choose! f hf using hch
have : Finite ↑(B₀ \ I) := hB₀fin.diff.to_subtype
refine
⟨iUnion f ∪ (B₀ ∩ I), union_subset (iUnion_subset (fun i ↦ (hf i).1)) inter_subset_right,
(finite_iUnion fun i ↦ (hf i).2.1).union (hB₀fin.subset inter_subset_left), fun x ⟨hxB₀, hxn⟩ hi ↦ ?_⟩
have hxI : x ∉ I := fun hxI ↦ hxn <| Or.inr ⟨hxB₀, hxI⟩
refine (hf ⟨x, ⟨hxB₀, hxI⟩⟩).2.2 (indep_subset hi <| insert_subset_insert ?_)
apply subset_union_of_subset_left
apply subset_iUnion
obtain ⟨I₀, hI₀I, hI₀fin, hI₀⟩ := hexI₀
set E₀ := insert e (I₀ ∪ B₀)
have hE₀fin : E₀.Finite := (hI₀fin.union hB₀fin).insert e
obtain ⟨J, ⟨hB₀J, hJ, hJss⟩, hJmax⟩ :=
Finite.exists_maximalFor (f := id) (s := {J | B₀ ⊆ J ∧ Indep J ∧ J ⊆ E₀}) (hE₀fin.finite_subsets.subset (by simp))
⟨B₀, Subset.rfl, hB₀, subset_union_right.trans (subset_insert _ _)⟩
have heI₀ : e ∉ I₀ := notMem_subset hI₀I heI
have heI₀i : Indep (insert e I₀) := indep_subset hins (insert_subset_insert hI₀I)
have heJ : e ∉ J := fun heJ ↦ hB₀e (indep_subset hJ <| insert_subset heJ hB₀J)
have hJfin := hE₀fin.subset hJss
have hcard : (insert e I₀).ncard ≤ J.ncard :=
by
refine not_lt.1 fun hlt ↦ ?_
obtain ⟨f, hfI, hfJ, hfi⟩ := indep_aug hJ hJfin heI₀i (hI₀fin.insert e) hlt
have hfE₀ : f ∈ E₀ := mem_of_mem_of_subset hfI (insert_subset_insert subset_union_left)
exact
hfJ <|
insert_eq_self.1 <|
le_imp_eq_iff_le_imp_ge'.2 (hJmax ⟨hB₀J.trans <| subset_insert _ _, hfi, insert_subset hfE₀ hJss⟩)
(subset_insert _ _)
-- But this means `|I₀| < |J|`, and extending `I₀` into `J` gives a contradiction
rw [ncard_insert_of_notMem heI₀ hI₀fin, ← Nat.lt_iff_add_one_le] at hcard
obtain ⟨f, hfJ, hfI₀, hfi⟩ := indep_aug (indep_subset hI hI₀I) hI₀fin hJ hJfin hcard
exact hI₀ f ⟨Or.elim (hJss hfJ) (fun hfe ↦ (heJ <| hfe ▸ hfJ).elim) (by aesop), hfI₀⟩ hfi) (subset_ground :=
subset_ground)
