English
Given a nilpotent kernel for f: B → C and two algebra homomorphisms g1,g2: A →_R B, if f ∘ g1 = f ∘ g2 then g1 = g2.
Русский
При нильпотентном ядре отображения f: B → C и двух алгебра-гомоморфизмах g1,g2: A →_R B, если f ∘ g1 = f ∘ g2, тогда g1 = g2.
LaTeX
$$$[FormallyUnramified R A] \\rightarrow (f: B \\to C),\\ \\ ker f \\text{ is nilpotent} \\Rightarrow \\forall g_1,g_2: A \\to_R B,\\; f\\circ g_1 = f\\circ g_2 \\Rightarrow g_1 = g_2.$$$
Lean4
theorem lift_unique_of_ringHom [FormallyUnramified R A] {C : Type*} [Ring C] (f : B →+* C)
(hf : IsNilpotent <| RingHom.ker f) (g₁ g₂ : A →ₐ[R] B) (h : f.comp ↑g₁ = f.comp (g₂ : A →+* B)) : g₁ = g₂ :=
FormallyUnramified.lift_unique _ hf _ _
(by
ext x
have := RingHom.congr_fun h x
simpa only [Ideal.Quotient.eq, Function.comp_apply, AlgHom.coe_comp, Ideal.Quotient.mkₐ_eq_mk, RingHom.mem_ker,
map_sub, sub_eq_zero])
