English
If g divides f in R[X], there is a canonical R-algebra hom algHomOfDvd f g hgf : AdjoinRoot f →ₐ[R] AdjoinRoot g.
Русский
Если g делит f в R[X], существует канонический R-алгеброморф algHomOfDvd f g hgf: AdjoinRoot f → AdjoinRoot g.
LaTeX
$$$\\text{algHomOfDvd}_{R}(f,g,hgf): AdjoinRoot f \\to_{R} AdjoinRoot g$$$
Lean4
@[simp]
theorem liftHom_eq_algHom (f : R[X]) (ϕ : AdjoinRoot f →ₐ[R] S) :
liftHom f (ϕ (root f)) (aeval_algHom_eq_zero f ϕ) = ϕ :=
by
suffices AlgHom.equalizer ϕ (liftHom f (ϕ (root f)) (aeval_algHom_eq_zero f ϕ)) = ⊤ by
exact (AlgHom.ext fun x => (SetLike.ext_iff.mp this x).mpr Algebra.mem_top).symm
rw [eq_top_iff, ← adjoinRoot_eq_top, Algebra.adjoin_le_iff, Set.singleton_subset_iff]
exact (@lift_root _ _ _ _ _ _ _ (aeval_algHom_eq_zero f ϕ)).symm
