English
In formality unramified setting, a lifting of homomorphisms is injective when certain square-zero conditions hold.
Русский
В формально неразменном контексте лифтинг гомоморфизмов инъективен при соблюдении условий квадратного нуля.
LaTeX
$$comp_injective [FormallyUnramified R A] (hI : I^2 = 0) : Function.Injective ((Ideal.Quotient.mkₐ R I).comp : (A →ₐ[R] B) → A →ₐ[R] B ⧸ I)$$
Lean4
theorem comp_injective [FormallyUnramified R A] (hI : I ^ 2 = ⊥) :
Function.Injective ((Ideal.Quotient.mkₐ R I).comp : (A →ₐ[R] B) → A →ₐ[R] B ⧸ I) :=
by
intro f₁ f₂ e
letI := f₁.toRingHom.toAlgebra
haveI := IsScalarTower.of_algebraMap_eq' f₁.comp_algebraMap.symm
have :=
((KaehlerDifferential.linearMapEquivDerivation R A).toEquiv.trans
(derivationToSquareZeroEquivLift I hI)).surjective.subsingleton
exact Subtype.ext_iff.mp (@Subsingleton.elim _ this ⟨f₁, rfl⟩ ⟨f₂, e.symm⟩)
