English
Given a ring hom i: R →+* S and a ∈ S with f.eval₂ i a = 0, there is a canonical lift AdjoinRoot f →+* S sending the root to a and agreeing with i on R; on mk f g it matches g.eval₂ i a.
Русский
Для кольцевого гомоморфизма i: R →+* S и элемента a ∈ S с f.eval₂ i a = 0 существует канонический подъём AdjoinRoot f →+* S, отправляющий корень в a и совпадающий на R; на mk f g выполняется g.eval₂ i a.
LaTeX
$$$\\exists$ lift: AdjoinRoot f →+* S, с свойством: \\forall g : R[X],\\\\ lift(i,a,h)(mk f g) = g.eval₂ i a$$$
Lean4
/-- Lift a ring homomorphism `i : R →+* S` to `AdjoinRoot f →+* S`. -/
def lift (i : R →+* S) (x : S) (h : f.eval₂ i x = 0) : AdjoinRoot f →+* S :=
by
apply Ideal.Quotient.lift _ (eval₂RingHom i x)
intro g H
rcases mem_span_singleton.1 H with ⟨y, hy⟩
rw [hy, RingHom.map_mul, coe_eval₂RingHom, h, zero_mul]
