English
For an IsDomain algebra A over R, the matroid closure of a subset s coincides with the algebraic closure of the R-adjoin of s inside A.
Русский
Если A — область над R, то замыкание матроида множества s совпадает с алгебраическим замыканием подалгебры adjoin_R s в A.
LaTeX
$$$ ( \\mathrm{matroid} \\; R\\, A ).closure(s) = \\mathrm{algebraicClosure}(\\operatorname{adjoin}_R s)\\, A $$$
Lean4
theorem matroid_closure_eq [IsDomain A] {s : Set A} : (matroid R A).closure s = algebraicClosure (adjoin R s) A :=
by
have ⟨B, hB⟩ := (matroid R A).exists_isBasis s
simp_rw [← hB.closure_eq_closure, hB.1.1.1.closure_eq_setOf_isBasis_insert, Set.ext_iff, mem_setOf,
matroid_isBasis_iff, ← matroid_indep_iff, hB.1.1.1, subset_insert, true_and, SetLike.mem_coe, mem_algebraicClosure,
← isAlgebraic_adjoin_iff_of_matroid_isBasis hB, forall_mem_insert]
exact fun _ ↦ and_iff_left fun x hx ↦ isAlgebraic_algebraMap (⟨x, subset_adjoin hx⟩ : adjoin R B)
