English
Repeated formulation: a transcendence basis x exists implies isomorphism with algebraicity conditions.
Русский
Повторная формулировка: базис трансцендентности x эквивалентен алгебраическим условиям над R.
LaTeX
$$$ \text{IsEmpty ι} \iff \text{Algebra.IsAlgebraic } R A$$$
Lean4
theorem matroid_isBasis_iff [IsDomain A] {s t : Set A} :
(matroid R A).IsBasis s t ↔ AlgebraicIndepOn R id s ∧ s ⊆ t ∧ ∀ a ∈ t, IsAlgebraic (adjoin R s) a :=
by
rw [Matroid.IsBasis, maximal_iff_forall_insert fun s t h hst ↦ ⟨h.1.subset hst, hst.trans h.2⟩]
simp_rw [matroid_indep_iff, ← and_assoc, matroid_e, subset_univ, and_true]
exact
and_congr_right fun h ↦
⟨fun max a ha ↦
of_not_not fun tr ↦
max _ (fun ha ↦ tr (isAlgebraic_algebraMap (⟨a, subset_adjoin ha⟩ : adjoin R s)))
⟨.insert h.1 (by rwa [image_id]), insert_subset ha h.2⟩,
fun alg a ha h ↦
((AlgebraicIndepOn.insert_iff ha).mp h.1).2 <| by rw [image_id]; exact alg _ <| h.2 <| mem_insert ..⟩
