English
Two extensions are equal if they agree on the base ring under the nilpotent kernel condition.
Русский
Две расширения равны, если они совпадают на базе при условии нильпотентного ядра.
LaTeX
$$ext [FormallyUnramified R A] (hI : IsNilpotent I) {g1 g2 : A →ₐ[R] B} (H : ∀ x, I-things) : g1 = g2$$
Lean4
theorem iff_comp_injective :
FormallyUnramified R A ↔
∀ ⦃B : Type u⦄ [CommRing B],
∀ [Algebra R B] (I : Ideal B) (_ : I ^ 2 = ⊥),
Function.Injective ((Ideal.Quotient.mkₐ R I).comp : (A →ₐ[R] B) → A →ₐ[R] B ⧸ I) :=
by
constructor
· intros; exact comp_injective _ ‹_›
· intro H
constructor
by_contra! h
obtain ⟨f₁, f₂, e⟩ := (KaehlerDifferential.endEquiv R A).injective.nontrivial
apply e
ext1
refine H (RingHom.ker (TensorProduct.lmul' R (S := A)).kerSquareLift.toRingHom) ?_ ?_
· rw [AlgHom.ker_kerSquareLift]
exact Ideal.cotangentIdeal_square _
· ext x
apply RingHom.kerLift_injective (TensorProduct.lmul' R (S := A)).kerSquareLift.toRingHom
simpa using DFunLike.congr_fun (f₁.2.trans f₂.2.symm) x
