Algebra.FormallySmooth.iff_split_surjection

theorem Algebra.FormallySmooth.iff_split_surjection : ∀ {R : Type u} [inst : CommRing R] {P A : Type u} [inst_1 : CommRing A] [inst_2 : Algebra R A] [inst_3 : CommRing P] [inst_4 : Algebra R P] (f : P →ₐ[R] A), Function.Surjective ⇑f → ∀ [inst_5 : Algebra.FormallySmooth R P], Algebra.FormallySmooth R A ↔ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A

This theorem states that, given a commutative ring `R` and two types `P` and `A`, which are also rings and `R`-algebras, if we have a surjective algebra homomorphism `f : P →ₐ[R] A`, then `A` is formally smooth over `R`, if and only if there exists another ring homomorphism `g` such that composing `f` with the lift of the square of its kernel and `g` results in the identity map on `A`. This condition is under the assumption that `P` is formally smooth over `R`. In geometrical terms, this theorem requires that a first-order thickening of the spectrum of `A` inside the spectrum of `P` admits a retraction.

More concisely: Given a commutative ring `R`, `R`-algebras `P` and `A`, and a surjective algebra homomorphism `f : P →ₐ[R] A`, if `P` is formally smooth over `R` then `A` is formally smooth over `R` if and only if there exists a ring homomorphism `g` such that `f ∘ (lift (ker f)²) ∘ g = id_A`.