Flat and smooth fibers imply smooth

Main results

• Algebra.FormallySmooth.of_formallySmooth_residueField_tensor: Let (R, m, k) be a local ring, S be a local R-algebra that is flat, essentially of finite presentation, and k ⊗[R] S is k-formally smooth. Then S is R-formally smooth.
• Algebra.mem_smoothLocus_of_formallySmooth_fiber: Let S be a flat and finitely presented R-algebra, and q be a prime of S lying over p. If κ(p) ⊗[R] S is κ(p)-smooth, then S is smooth at q.
• Algebra.Smooth.of_formallySmooth_fiber: Flat and finitely presented and smooth fibers imply smooth.
• Algebra.Etale.of_formallyUnramified_of_flat: Flat and finitely presented and (formally) unramified implies etale.

Note

For the converse that smooth imples flat, see Mathlib/RingTheory/Smooth/Flat.lean.

theorem Algebra.FormallySmooth.of_formallySmooth_residueField_tensor {R : Type u_1} {S : Type u_2} {P : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S] [CommRing P] [Algebra R P] [Algebra P S] [IsScalarTower R P S] [IsLocalRing R] [IsLocalRing S] [IsLocalHom (algebraMap R S)] [FormallySmooth (IsLocalRing.ResidueField R) (TensorProduct R (IsLocalRing.ResidueField R) S)] (M : Submonoid P) [IsLocalization M S] [FinitePresentation R P] : FormallySmooth R S

Let (R, m, k) be a local ring, S be a local R-algebra that is flat, essentially of finite presentation, and k ⊗[R] S is k-formally smooth. Then S is R-formally smooth.

Since we don't have an "essentially of finite presentation" type class yet, we explicitly require a P that is of finite presentation over R and that S is a localization of it.

theorem Algebra.IsSmoothAt.of_formallySmooth_fiber {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S] [FinitePresentation R S] (p : Ideal R) (q : Ideal S) [p.IsPrime] [q.IsPrime] [q.LiesOver p] [FormallySmooth p.ResidueField (p.Fiber S)] : IsSmoothAt R q

Stacks Tag 00TF (We require the whole fiber to be smooth instead)

theorem Algebra.Smooth.of_formallySmooth_fiber {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S] [FinitePresentation R S] (H : ∀ (I : Ideal R) [inst : I.IsPrime], FormallySmooth I.ResidueField (I.Fiber S)) : Smooth R S

theorem Algebra.Etale.of_formallyUnramified_of_flat {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] [Algebra R S] [FinitePresentation R S] [Module.Flat R S] [FormallyUnramified R S] : Etale R S

Stacks Tag 08WD ((3) => (1))

theorem Algebra.IsEtaleAt.of_isUnramifiedAt_of_flat {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S] [FinitePresentation R S] (q : Ideal S) [q.IsPrime] [IsUnramifiedAt R q] : IsEtaleAt R q