Standard smooth of free Kaehler differentials

In this file we show a presentation independent characterization of being standard smooth: An R-algebra S of finite presentation is standard smooth if and only if H¹(S/R) = 0 and Ω[S⁄R] is free on {d sᵢ}ᵢ for some sᵢ : S.

From this we deduce relations of standard smooth with other local properties.

Main results

• IsStandardSmooth.iff_exists_basis_kaehlerDifferential: An R-algebra S of finite presentation is standard smooth if and only if H¹(S/R) = 0 and Ω[S⁄R] is free on {d sᵢ}ᵢ for some sᵢ : S.
• Etale.iff_isStandardSmoothOfRelativeDimension_zero: An R-algebra S is étale if and only if it is standard smooth of relative dimension zero.

Notes

For an example of an algebra with H¹(S/R) = 0 and Ω[S⁄R] finite and free, but S not standard smooth over R, consider R = ℝ and S = R[x,y]/(x² + y² - 1) the coordinate ring of the circle. One can show that then Ω[S⁄R] is S-free on ω = xdy - ydx, but there are no f g : S such that ω = g df.

TODOs

• Deduce from this that smooth is equivalent to locally standard smooth (TODO @chrisflav).

theorem Algebra.IsStandardSmooth.of_basis_kaehlerDifferential {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [FinitePresentation R S] [Subsingleton (H1Cotangent R S)] {I : Type u_3} (b : Module.Basis I S Ω[S⁄R]) (hb : Set.range ⇑b ⊆ Set.range ⇑(KaehlerDifferential.D R S)) : IsStandardSmooth R S

If H¹(S/R) = 0 and Ω[S⁄R] is free on {d sᵢ}ᵢ for some sᵢ : S, then S is R-standard smooth.

theorem Algebra.IsStandardSmooth.iff_exists_basis_kaehlerDifferential {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [FinitePresentation R S] : IsStandardSmooth R S ↔ Subsingleton (H1Cotangent R S) ∧ ∃ (I : Type) (b : Module.Basis I S Ω[S⁄R]), Set.range ⇑b ⊆ Set.range ⇑(KaehlerDifferential.D R S)

An R-algebra S of finite presentation is standard smooth if and only if H¹(S/R) = 0 and Ω[S⁄R] is free on {d sᵢ}ᵢ for some sᵢ : S.

theorem Algebra.Etale.iff_isStandardSmoothOfRelativeDimension_zero {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] : Etale R S ↔ IsStandardSmoothOfRelativeDimension 0 R S

S is an étale R-algebra if and only if it is standard smooth of relative dimension 0.