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.
• IsSmoothAt.exists_notMem_isStandardSmooth: If S is R-smooth at a prime p, it is standard smooth on a standard open containing p.

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.

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.

theorem Algebra.IsSmoothAt.exists_notMem_isStandardSmooth (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [FinitePresentation R S] (p : Ideal S) [p.IsPrime] [IsSmoothAt R p] : ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)

If S is R-smooth at a prime p, then S is R-standard-smooth in a neighbourhood of p: there exists a basic open p ∈ D(f) of Spec S such that S[1/f] is standard smooth.

theorem Algebra.Smooth.exists_span_eq_top_isStandardSmooth (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [Smooth R S] : ∃ (s : Set S), Ideal.span s = ⊤ ∧ ∀ x ∈ s, IsStandardSmooth R (Localization.Away x)

If S is R-smooth, there exists a cover by basic opens D(sᵢ) such that S[1/sᵢ] is R-standard-smooth.