English
Let x be algebraically independent over R, and suppose range x lies inside the range of the S-algebra map A. If y is algebraically independent over S, then Sum.elim y x is algebraically independent over R.
Русский
Пусть x: I → A алгебраически независим над R, и диапазон x вложен в образ алгебраического отображения S → A. Если y: J → A алгебраически независим над S, то Sum.elim y x алгебраически независимо над R.
LaTeX
$$$\\mathrm{AlgebraicIndependent}_R x \\quad\\text{and}\\quad (\\operatorname{range} x \\subseteq \\operatorname{range}(\\mathrm{algebraMap}\\,S\\,A)) \\quad\\to\\quad \\mathrm{AlgebraicIndependent}_S y \\to \\mathrm{AlgebraicIndependent}_R(\\mathrm{Sum\\_elim}\\; y\\; x)$$$
Lean4
theorem sumElim_of_tower {ι'} {y : ι' → A} (hxS : range x ⊆ range (algebraMap S A)) (hy : AlgebraicIndependent S y) :
AlgebraicIndependent R (Sum.elim y x) :=
by
let e := AlgEquiv.ofInjective (IsScalarTower.toAlgHom R S A) hy.algebraMap_injective
set Rx := adjoin R (range x)
let _ : Algebra Rx S := (e.symm.toAlgHom.comp <| Subalgebra.inclusion <| adjoin_le hxS).toAlgebra
have : IsScalarTower Rx S A := .of_algebraMap_eq fun x ↦ show _ = (e (e.symm _)).1 by simp
refine hx.sumElim (hy.restrictScalars (e.symm.injective.comp ?_))
simpa only [AlgHom.coe_toRingHom] using Subalgebra.inclusion_injective _
