English
For a base change setup with maps S → S′, the compatibility condition holds: f.toAlgHom respects the algebraMap and aligns with the source’s aeval under algebraMap.
Русский
В условиях базового изменения совместимость сохраняется: f.toAlgHom согласуется с algebraMap и с aeval источника через алгебраическое отображение.
LaTeX
$$$\\text{algebraMap}_{S S'} \\circ \\mathrm{aeval}_{P.val} = \\mathrm{aeval}_{P'.val} \\circ f.toAlgHom$$$
Lean4
/-- Giving a hom between two families of generators is equivalent to
giving an algebra homomorphism between the polynomial rings. -/
@[simps]
noncomputable def equivAlgHom :
Hom P P' ≃ { f : P.Ring →ₐ[R] P'.Ring // ∀ x, aeval P'.val (f x) = algebraMap S S' (aeval P.val x) }
where
toFun f := ⟨f.toAlgHom, f.algebraMap_toAlgHom⟩
invFun f := ⟨fun i ↦ f.1 (.X i), fun i ↦ by simp [f.2]⟩
left_inv f := by ext; simp
right_inv f := by ext; simp
