English
If I is a basis for X in M, then contracting X equals contracting I and deleting X \ I from the result: M / X = (M / I) \ (X \ I).
Русский
Если I является базисом для X в M, то сокращение по X равняется сокращению по I и последующему удалению X \ I: M / X = (M / I) \ (X \ I).
LaTeX
$$$ M / X = (M / I) \ (X \ I) \quad\text{when } MIsBasisI for X$$$
Lean4
/-- Contracting a set is the same as contracting a basis for the set, and deleting the rest. -/
theorem contract_eq_contract_delete (hI : M.IsBasis I X) : M ／ X = M ／ I ＼ (X \ I) :=
by
nth_rw 1 [← diff_union_of_subset hI.subset, ← dual_inj, dual_contract_delete, dual_contract, union_comm, ←
delete_delete, ext_iff_indep]
refine ⟨rfl, fun J hJ ↦ ?_⟩
have hss : X \ I ⊆ (M✶ ＼ I).coloops := fun e he ↦
by
rw [← dual_contract, dual_coloops, ← IsLoop, ← singleton_dep, hI.indep.contract_dep_iff, singleton_union,
and_iff_right (by simpa using he.2), hI.indep.insert_dep_iff, hI.closure_eq_closure]
exact diff_subset_diff_left (M.subset_closure X) he
rw [((coloops_indep _).subset hss).contract_indep_iff, delete_indep_iff, union_indep_iff_indep_of_subset_coloops hss,
and_comm]
