English
The evaluation of pb.gen under minpolyGen annihilates, i.e., aeval pb.gen (minpolyGen pb) = 0.
Русский
Пусть aeval pb.gen (minpolyGen pb) = 0.
LaTeX
$$$\operatorname{aeval}_{pb.gen}\big(\text{minpolyGen}(pb)\big) = 0$$$
Lean4
/-- `pb.lift y hy` is the algebra map sending `pb.gen` to `y`,
where `hy` states the higher powers of `y` are the same as the higher powers of `pb.gen`.
See `PowerBasis.liftEquiv` for a bundled equiv sending `⟨y, hy⟩` to the algebra map.
-/
noncomputable def lift (pb : PowerBasis A S) (y : S') (hy : aeval y (minpoly A pb.gen) = 0) : S →ₐ[A] S' :=
{
pb.basis.constr A fun i =>
y ^ (i :
ℕ) with
map_one' := by convert pb.constr_pow_algebraMap hy 1 using 2 <;> rw [RingHom.map_one]
map_zero' := by convert pb.constr_pow_algebraMap hy 0 using 2 <;> rw [RingHom.map_zero]
map_mul' := pb.constr_pow_mul hy
commutes' := pb.constr_pow_algebraMap hy }
