English
If x is algebraically independent over R and y is algebraically independent over S, then the combined family obtained by Sum.elim y (algebraMap S A ∘ x) is algebraically independent over R.
Русский
Если x алгебраически независим над R, а y алгебраически независим над S, то объединение Sum.elim y (algebraMap S A ∘ x) алгебраически независимо над R.
LaTeX
$$$\\mathrm{AlgebraicIndependent}_R x \\to \\mathrm{AlgebraicIndependent}_S y \\to \\mathrm{AlgebraicIndependent}_R(\\mathrm{Sum\\_elim}\\; y\\; (\\mathrm{algebraMap}\\,S\\,A \\circ x))$$$
Lean4
theorem sumElim_comp {ι'} {x : ι → S} {y : ι' → A} (hx : AlgebraicIndependent R x) (hy : AlgebraicIndependent S y) :
AlgebraicIndependent R (Sum.elim y (algebraMap S A ∘ x)) :=
(hx.map' (f := IsScalarTower.toAlgHom R S A) hy.algebraMap_injective).sumElim_of_tower (range_comp_subset_range ..) hy
