English
If ker f is nilpotent, then two algebra homomorphisms into B are equal whenever their compositions with f agree.
Русский
Если ядро f нильпотентно, то два алгебра-гомоморфа в B совпадают, когда их композиции с f совпадают.
LaTeX
$$lift_unique_of_ringHom [FormallyUnramified R A] (I : Ideal B) (hI : IsNilpotent I) (g1 g2 : A →ₐ[R] B) (h : f ∘ g1 = f ∘ g2) : g1 = g2$$
Lean4
theorem lift_unique [FormallyUnramified R A] (I : Ideal B) (hI : IsNilpotent I) (g₁ g₂ : A →ₐ[R] B)
(h : (Ideal.Quotient.mkₐ R I).comp g₁ = (Ideal.Quotient.mkₐ R I).comp g₂) : g₁ = g₂ :=
by
revert g₁ g₂
change Function.Injective (Ideal.Quotient.mkₐ R I).comp
revert ‹Algebra R B›
apply Ideal.IsNilpotent.induction_on (S := B) I hI
· intro B _ I hI _; exact FormallyUnramified.comp_injective I hI
· intro B _ I J hIJ h₁ h₂ _ g₁ g₂ e
apply h₁
apply h₂
ext x
replace e := AlgHom.congr_fun e x
dsimp only [AlgHom.comp_apply, Ideal.Quotient.mkₐ_eq_mk] at e ⊢
rwa [Ideal.Quotient.eq, ← map_sub, Ideal.mem_quotient_iff_mem hIJ, ← Ideal.Quotient.eq]
