English
Let R be a commutative ring and A, B, C R-algebras. Suppose f: B → C is an algebra homomorphism whose kernel is nilpotent, and g1, g2: A → B are R-algebra homomorphisms such that f ∘ g1 = f ∘ g2. Then g1 = g2.
Русский
Пусть R — коммутативное кольцо, A, B, C — R-алгебры. Пусть f: B → C — алгебра-гомоморфизм с нилпотентным ядром, и g1, g2: A → B — R-алгебра-гомоморфизмы такие, что f ∘ g1 = f ∘ g2. Тогда g1 = g2.
LaTeX
$$$\forall R\, A\, B\, C\, (f : B \to_R C)\, (hf : \operatorname{IsNilpotent}(\ker(f)))\, (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' [FormallyUnramified R A] {C : Type*} [Ring C] [Algebra R C] (f : B →ₐ[R] C)
(hf : IsNilpotent <| RingHom.ker (f : B →+* C)) (g₁ g₂ : A →ₐ[R] B) (h : f.comp g₁ = f.comp g₂) : g₁ = g₂ :=
FormallyUnramified.ext' _ hf g₁ g₂ (AlgHom.congr_fun h)
