English
Let f: P →ₐ[R] A be a surjection with square-zero kernel. Then A is formally smooth over R if and only if there exists a lifting g satisfying f.kerSquareLift ∘ g = id and one has a FormallySmooth structure on P.
Русский
Пусть f: P →ₐ[R] A сюръекция с ядром квадратно нулевого свойства. Тогда A формально гладко над R тогда и только тогда, когда существует подъем g с f.kerSquareLift ∘ g = id и имеется структура FormallySmooth на P.
LaTeX
$$$[\operatorname{FormallySmooth} R P] \Rightarrow \big( \operatorname{FormallySmooth} R A \iff \exists g, f.\kerSquareLift \circ g = \mathrm{id} \big)$$$
Lean4
/-- Let `P →ₐ[R] A` be a surjection with kernel `J`, and `P` a formally smooth `R`-algebra,
then `A` is formally smooth over `R` iff the surjection `P ⧸ J ^ 2 →ₐ[R] A` has a section.
Geometric intuition: we require that a first-order thickening of `Spec A` inside `Spec P` admits
a retraction. -/
theorem iff_split_surjection [FormallySmooth R P] : FormallySmooth R A ↔ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A :=
by
constructor
· intro
have surj : Function.Surjective f.kerSquareLift := fun x =>
⟨Submodule.Quotient.mk (hf x).choose, (hf x).choose_spec⟩
have sqz : RingHom.ker f.kerSquareLift.toRingHom ^ 2 = 0 := by
rw [AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square, Ideal.zero_eq_bot]
dsimp only [AlgHom.toRingHom_eq_coe, RingHom.ker_coe_toRingHom] at sqz
refine ⟨FormallySmooth.lift _ ⟨2, sqz⟩ (Ideal.quotientKerAlgEquivOfSurjective surj).symm.toAlgHom, ?_⟩
dsimp only [AlgHom.toRingHom_eq_coe, AlgEquiv.toAlgHom_eq_coe]
ext x
have :=
(Ideal.quotientKerAlgEquivOfSurjective surj).congr_arg
(FormallySmooth.mk_lift (R := R) _ ⟨2, sqz⟩ (Ideal.quotientKerAlgEquivOfSurjective surj).symm x)
dsimp only [AlgHom.toRingHom_eq_coe, AlgHom.coe_coe] at this
rw [AlgEquiv.apply_symm_apply] at this
conv_rhs => rw [← this, AlgHom.id_apply]
rfl
· rintro ⟨g, hg⟩; exact FormallySmooth.of_split f g hg
