English
Let f: P →ₐ[R] S be surjective with square-zero kernel. If there is a section g: S →ₐ[R] P with f ∘ g = id, then A is formally smooth over R.
Русский
Пусть f: P →ₐ[R] S сюръективно с ядром, нулевым до квадрата. Если существует секция g: S →ₐ[R] P с f ∘ g = id, тогда A формально гладко над R.
LaTeX
$$$\text{FormallySmooth}(R, P) \Rightarrow \text{FormallySmooth}(R, A)$ при условии существования g с $f.\ker^2$-квадратом и $f.kerSquareLift \circ g = \mathrm{id}$$$
Lean4
theorem of_split [FormallySmooth R P] (g : A →ₐ[R] P ⧸ (RingHom.ker f.toRingHom) ^ 2)
(hg : f.kerSquareLift.comp g = AlgHom.id R A) : FormallySmooth R A :=
by
constructor
intro C _ _ I hI i
let l : P ⧸ (RingHom.ker f.toRingHom) ^ 2 →ₐ[R] C :=
by
refine Ideal.Quotient.liftₐ _ (FormallySmooth.lift I ⟨2, hI⟩ (i.comp f)) ?_
have : RingHom.ker f ≤ I.comap (FormallySmooth.lift I ⟨2, hI⟩ (i.comp f)) :=
by
rintro x (hx : f x = 0)
have : _ = i (f x) := (FormallySmooth.mk_lift I ⟨2, hI⟩ (i.comp f) x :)
rwa [hx, map_zero, ← Ideal.Quotient.mk_eq_mk, Submodule.Quotient.mk_eq_zero] at this
intro x hx
have := (Ideal.pow_right_mono this 2).trans (Ideal.le_comap_pow _ 2) hx
rwa [hI] at this
have : i.comp f.kerSquareLift = (Ideal.Quotient.mkₐ R _).comp l :=
by
apply AlgHom.coe_ringHom_injective
apply Ideal.Quotient.ringHom_ext
ext x
exact (FormallySmooth.mk_lift I ⟨2, hI⟩ (i.comp f) x).symm
exact ⟨l.comp g, by rw [← AlgHom.comp_assoc, ← this, AlgHom.comp_assoc, hg, AlgHom.comp_id]⟩
