Smooth algebras are flat

Let A be a smooth R-algebra. In this file we show that then A is R-flat. The proof proceeds in two steps:

1. If R is Noetherian, let R[X₁, ..., Xₙ] →ₐ[R] A be surjective with kernel I. By formal smoothness we construct a section A →ₐ[R] AdicCompletion I R[X₁, ..., Xₙ] of the canonical map AdicCompletion I R[X₁, ..., Xₙ] →ₐ[R] R[X₁, ..., Xₙ] ⧸ I ≃ₐ[R] A. Since R is Noetherian, AdicCompletion I R is R-flat so A is a retract of a flat R-module and hence flat.
2. In the general case, we choose a model of A over a finitely generated ℤ-subalgebra of R and apply 1.

References

• Conde-Lago, A short proof of smooth implies flat

theorem Algebra.FormallySmooth.flat_of_algHom_of_isNoetherianRing {R : Type u_1} {A : Type u_2} {S : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [CommRing S] [Algebra R S] (f : S →ₐ[R] A) (hf : Function.Surjective ⇑f) [Module.Flat R S] [IsNoetherianRing S] [FormallySmooth R A] : Module.Flat R A

theorem Algebra.Smooth.flat_of_isNoetherianRing (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] [IsNoetherianRing R] [Smooth R A] : Module.Flat R A

If A is R-smooth and R is Noetherian, then A is R-flat.

instance Algebra.Smooth.flat (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] [Smooth R A] : Module.Flat R A

Any smooth algebra is flat.

theorem RingHom.Smooth.flat {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.Smooth) : f.Flat