English
From a surjective algebra hom f : MvPolynomial I R →ₐ[R] S and a surjectivity witness, construct a Generators R S I that encodes S as an algebra over R generated by I.
Русский
По сюрьективному алгебровому отображению f: MvPolynomial I R →ₐ[R] S и доказательству сюръективности конструируем Generators R S I, кодирующий S как алгебра над R, порожденную I.
LaTeX
$$ofAlgHom {I : Type*} (f : MvPolynomial I R →ₐ[R] S) (h : Function.Surjective f) : Algebra.Generators R S I$$
Lean4
/-- Construct `Generators` from an assignment `I → S` such that `R[X] → S` is surjective. -/
@[simps val]
noncomputable def ofSurjective (val : ι → S) (h : Function.Surjective (aeval (R := R) val)) : Generators R S ι
where
val := val
σ' x := (h x).choose
aeval_val_σ' x := (h x).choose_spec
