English
Let Q be a family of generators of S over T and P a family of generators of R over S. Then the induced algebra homomorphism (Q.ofComp P).toAlgHom is surjective; i.e., every element of the target algebra is the image of some element from the source.
Русский
Пусть Q задаёт множество порождающих для S над T, и P задаёт множество порождающих для R над S. Тогда получаемый отображение (Q.ofComp P).toAlgHom является сюръективным; то есть любый элемент целевой алгебры имеет прообраз в исходной.
LaTeX
$$$\\forall y,\\ \\exists x:\\text{Domain},\\ (Q\\circ P)^{\\!\\mathrm{toAlgHom}}(x)=y$$$
Lean4
theorem toAlgHom_ofComp_surjective (Q : Generators S T ι') (P : Generators R S ι) :
Function.Surjective (Q.ofComp P).toAlgHom := by
intro p
induction p using MvPolynomial.induction_on with
| C a =>
use MvPolynomial.rename Sum.inr (P.σ a)
simp only [Hom.toAlgHom, ofComp, Generators.comp, MvPolynomial.aeval_rename, Sum.elim_comp_inr]
simp_rw [Function.comp_def, ← MvPolynomial.algebraMap_eq, ← IsScalarTower.toAlgHom_apply R, ←
MvPolynomial.comp_aeval]
simp
| add p q hp hq =>
obtain ⟨p, rfl⟩ := hp
obtain ⟨q, rfl⟩ := hq
use p + q
simp
| mul_X p i hp =>
obtain ⟨(p : MvPolynomial (ι' ⊕ ι) R), rfl⟩ := hp
use p * MvPolynomial.X (R := R) (Sum.inl i)
simp [Algebra.Generators.ofComp, Algebra.Generators.Hom.toAlgHom]
