Theorems · Theorem · algebraic geometry

AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyOfFinitePresentation f] (x : ↥X),
  (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x)).FormallySmooth →
    ∃ U,
      ∃ (_ : AlgebraicGeometry.IsAffineOpen U),
        ∃ V,
          ∃ (_ : AlgebraicGeometry.IsAffineOpen V) (hVU : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
            x ∈ V ∧ (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V hVU)).Smooth

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Smooth

Cited by

2 results in Mathlib

Foundations

Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AlgebraicGeometry.LocallyOfFinitePresentation