English
If A is NoZeroDivisors and FaithfulSMul over R, and adjoin_R s is algebraic over A, then there exists t ⊆ s such that t forms a transcendence basis over R for A when viewed as a subset of A.
Русский
Пусть A — без нулевых делителей, и действует верно отображение смещения; тогда существует t ⊆ s такое, что t образует трансцендентный базис над R для A.
LaTeX
$$$ [NoZeroDivisors\\; A] [FaithfulSMul\\; R\\; A] (s : Set A) [Algebra.IsAlgebraic (adjoin R s) A] : \\exists t, t \\subseteq s \\land IsTranscendenceBasis R ((\\uparrow) : t \\to A) $$$
Lean4
theorem exists_isTranscendenceBasis_subset [NoZeroDivisors A] [FaithfulSMul R A] (s : Set A)
[Algebra.IsAlgebraic (adjoin R s) A] : ∃ t, t ⊆ s ∧ IsTranscendenceBasis R ((↑) : t → A) :=
by
have ⟨t, _, ht⟩ :=
exists_isTranscendenceBasis_between ∅ s (empty_subset _)
((algebraicIndependent_empty_iff ..).mpr <| FaithfulSMul.algebraMap_injective R A)
exact ⟨t, ht⟩
