English
Another formulation of ext_indep_disjoint_loops_coloops: if two matroids have equal ground, loops and coloops and agree on independence for all I ⊆ E, then they are equal.
Русский
Ещё одно формулирование ext_indep_disjoint_loops_coloops: если два матроидa имеют равное множество E, одинаковые петли и колоопы и сходятся по независимости для всех I ⊆ E, то они равны.
LaTeX
$$$$ \forall M_1, M_2, \; M_1.E = M_2.E \land M_1.loops = M_2.loops \land M_1.coloops = M_2.coloops \land \forall I \subseteq M_1.E, M_1.Indep(I) \iff M_2.Indep(I) \Rightarrow M_1 = M_2. $$$$
Lean4
/-- If two matroids agree on loops and coloops, and have the same independent sets after
loops/coloops are removed, they are equal. -/
theorem ext_indep_disjoint_loops_coloops {M₁ M₂ : Matroid α} (hE : M₁.E = M₂.E) (hl : M₁.loops = M₂.loops)
(hc : M₁.coloops = M₂.coloops)
(h : ∀ I, I ⊆ M₁.E → Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)) : M₁ = M₂ :=
by
refine ext_indep hE fun I hI ↦ ?_
rw [← diff_coloops_indep_iff, ← @diff_coloops_indep_iff _ M₂, ← hc]
obtain hdj | hndj := em (Disjoint I (M₁.loops))
· rw [h _ (diff_subset.trans hI)]
rw [disjoint_union_right]
exact ⟨disjoint_of_subset_left diff_subset hdj, disjoint_sdiff_left⟩
obtain ⟨e, heI, hel : M₁.IsLoop e⟩ := not_disjoint_iff_nonempty_inter.mp hndj
refine iff_of_false (hel.not_indep_of_mem ⟨heI, hel.not_isColoop⟩) ?_
rw [isLoop_iff, hl, ← isLoop_iff] at hel
rw [hc]
exact hel.not_indep_of_mem ⟨heI, hel.not_isColoop⟩
