Retracts of formally smooth algebras

An R-algebra A is a retract of an R-algebra C if there are R-algebra homomorphisms α : A →ₐ[R] C and β : C →ₐ[R] A with β ∘ α = id. If C is formally smooth over R, then so is A: an infinitesimal lifting problem for A becomes one for C after composing with β, and a solution for C gives one for A after composing with α.

Geometrically, a retract of a formally smooth scheme over a base is formally smooth over it. This is the local input to the stability of smooth morphisms of schemes under retracts.

Main results

• Algebra.FormallySmooth.of_retract: a retract of a formally smooth algebra is formally smooth.
• RingHom.FormallySmooth.of_retract: the same statement for ring homomorphisms.

References

• The Stacks Project, Tag 00TL, for the infinitesimal lifting characterisation of formal smoothness.

theorem Algebra.FormallySmooth.of_retract {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommRing R] [CommRing A] [CommRing C] [Algebra R A] [Algebra R C] [FormallySmooth R C] (α : A →ₐ[R] C) (β : C →ₐ[R] A) (h : β.comp α = AlgHom.id R A) : FormallySmooth R A

A retract of a formally smooth algebra is formally smooth. If A is a retract of a formally smooth R-algebra C, through α : A →ₐ[R] C and β : C →ₐ[R] A with β ∘ α = id, then A is formally smooth over R.

theorem RingHom.FormallySmooth.of_retract {R : Type u_1} {A : Type u_2} {C : Type u_3} [CommRing R] [CommRing A] [CommRing C] {φ : R →+* A} (α : A →+* C) (β : C →+* A) (h : β.comp α = id A) (hφ : (α.comp φ).FormallySmooth) : φ.FormallySmooth

A retract of a formally smooth ring homomorphism is formally smooth. Let φ : R →+* A, and let α : A →+* C and β : C →+* A satisfy β ∘ α = id. If α ∘ φ is formally smooth, then so is φ.