English
Between two subsets s ⊆ t, under independence of s over R and algebraicity of A over adjoin_R t, there exists a subset u with s ⊆ u ⊆ t that forms a transcendence basis for A over R.
Русский
Между двумя подмножествами s ⊆ t, если s алгебраически независим над R и A алгебраично над adjoin_R t, существует подмножество u с s ⊆ u ⊆ t, образующее трансцендентный базис A над R.
LaTeX
$$$ s \\subseteq t \\Rightarrow ( AlgebraicIndepOn R id s ) \\rightarrow [ ht : Algebra.IsAlgebraic (adjoin R t) A ] \\rightarrow \\exists u, s \\subseteq u \\land u \\subseteq t \\land IsTranscendenceBasis R ((\\uparrow) : u \\to A) $$$
Lean4
/-- If `s ⊆ t` are subsets in an `R`-algebra `A` such that `s` is algebraically independent over
`R`, and `A` is algebraic over the `R`-algebra generated by `t`, then there is a transcendence
basis of `A` over `R` between `s` and `t`, provided that `A` is a domain.
This may fail if only `R` is assumed to be a domain but `A` is not, because of failure of
transitivity of algebraicity: there may exist `a : A` such that `S := R[a]` is algebraic over
`R` and `A` is algebraic over `S`, but `A` nonetheless contains a transcendental element over `R`.
The only `R`-algebraically independent subset of `{a}` is `∅`, which is not a transcendence basis.
See the docstring of `IsAlgebraic.restrictScalars_of_isIntegral` for an example. -/
theorem exists_isTranscendenceBasis_between [NoZeroDivisors A] (s t : Set A) (hst : s ⊆ t)
(hs : AlgebraicIndepOn R id s) [ht : Algebra.IsAlgebraic (adjoin R t) A] :
∃ u, s ⊆ u ∧ u ⊆ t ∧ IsTranscendenceBasis R ((↑) : u → A) :=
by
have := ht.nontrivial
have := Subtype.val_injective (p := (· ∈ adjoin R t)).nontrivial
have := (isDomain_iff_noZeroDivisors_and_nontrivial A).mpr ⟨inferInstance, inferInstance⟩
have := (faithfulSMul_iff_algebraMap_injective R A).mpr hs.algebraMap_injective
rw [← matroid_spanning_iff] at ht
rw [← matroid_indep_iff] at hs
have ⟨B, base, hsB, hBt⟩ := hs.exists_isBase_subset_spanning ht hst
exact ⟨B, hsB, hBt, base⟩
