Smooth morphisms and their fibers

Main results

• Smooth.of_smooth_fiberToSpecResidueField: A flat morphism, locally of finite presentation and smooth fibers is smooth.

theorem AlgebraicGeometry.Smooth.of_smooth_fiberToSpecResidueField {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f] (h : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) : Smooth f

If f : X ⟶ Y is locally of finite presentation, flat and has smooth fibers, then f is smooth.