English
If f is surjective, then the base change of f along a polynomial variable map is surjective.
Русский
Если f сюръективен, то базовое изменение f вдоль отображения по переменной многочлена сюръективно.
LaTeX
$$$\\text{Surjective}(f) \\Rightarrow \\text{Surjective}(\\text{TensorProduct.map}(\\mathrm{id}, f))$$$
Lean4
instance baseChange [hfa : FiniteType R A] : Algebra.FiniteType B (B ⊗[R] A) :=
by
rw [iff_quotient_mvPolynomial''] at *
obtain ⟨n, f, hf⟩ := hfa
let g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := Algebra.TensorProduct.map (AlgHom.id B B) f
have : Function.Surjective g := baseChangeAux_surj B hf
use n, AlgHom.comp g (MvPolynomial.algebraTensorAlgEquiv R B).symm.toAlgHom
simpa