English
Given a finite set s of monic polynomials, there is an algebra homomorphism from the polynomial ring in Vars to the splitting field of the product of s, sending indeterminates to chosen roots when each monic is in s.
Русский
Для конечного множества s монических многочленов существует алгебраическое однородное отображение из полиномиального кольца в разложение произведения элементов s, отправляющее индeterminанты в выбранные корни, когда каждый монический принадлежит s.
LaTeX
$$$toSplittingField\\; s : MvPolynomial(Vars(k),k) \\to\\ SplittingField(\\prod f \\in s, f.1)$$$
Lean4
/-- Given a finite set of monic polynomials, construct an algebra homomorphism
to the splitting field of the product of the polynomials
sending indeterminates $X_{f_i}$ to the distinct roots of `f`. -/
def toSplittingField (s : Finset (Monics k)) : MvPolynomial (Vars k) k →ₐ[k] SplittingField (∏ f ∈ s, f.1) :=
MvPolynomial.aeval fun fi ↦ if hf : fi.1 ∈ s then (finEquivRoots (Monics.splits_finsetProd hf) fi.2).1.1 else 37
