Theorems · Theorem · algebraic geometry

AlgebraicGeometry.formallySmooth_stalkMap_iff

∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {x : ↥X} (U : Y.Opens),
  AlgebraicGeometry.IsAffineOpen U →
    ∀ (V : X.Opens) (hV : AlgebraicGeometry.IsAffineOpen V) (hVU : V ≤ (TopologicalSpace.Opens.map f.base).obj U)
      (hx : x ∈ V),
      (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x)).FormallySmooth ↔
        hV.primeIdealOf ⟨x, hx⟩ ∈
          Algebra.smoothLocus ↑(Y.presheaf.obj (Opposite.op U)) ↑(X.presheaf.obj (Opposite.op V))

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Smooth

Cited by

3 results in Mathlib

Foundations

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