English
For [IsDomain A], a subset s is a flat in the matroid of A over R if and only if there exists a Subalgebra S of A with S = adjoin_R s and every element algebraic over S lies in s.
Русский
Для области A над R подмножество s является плоским элементом матроида тогда и только тогда, когда существует подсоглобра A- над R, удовлетворяющая S = adjoin_R s и для каждого элемента a, алгебраичное над S ⇒ a ∈ s.
LaTeX
$$$ [IsDomain\\; A] \\; \\Rightarrow\\; (\\mathrm{matroid} \\; R\\, A).IsFlat(s) \\iff \\exists S: \\text{Subalgebra}_R A, S = s \\wedge \\forall a: A, IsAlgebraic S\\ a \\rightarrow a \\in s $$$
Lean4
theorem matroid_isFlat_iff [IsDomain A] {s : Set A} :
(matroid R A).IsFlat s ↔ ∃ S : Subalgebra R A, S = s ∧ ∀ a : A, IsAlgebraic S a → a ∈ s :=
by
rw [Matroid.isFlat_iff_closure_eq, matroid_closure_eq]
set S := algebraicClosure (adjoin R s) A
refine ⟨fun eq ↦ ⟨S.restrictScalars R, eq, fun a (h : IsAlgebraic S _) ↦ ?_⟩, ?_⟩
· rw [← eq]; exact h.restrictScalars (adjoin R s)
rintro ⟨s, rfl, hs⟩
refine Set.ext fun a ↦ ⟨(hs _ <| adjoin_eq s ▸ ·), fun h ↦ ?_⟩
exact isAlgebraic_algebraMap (A := A) (by exact (⟨a, subset_adjoin h⟩ : adjoin R s))
