Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.Smooth f ↔
    ∀ (x : ↥X),
      ∃ U,
        ∃ (_ : AlgebraicGeometry.IsAffineOpen U),
          ∃ V,
            ∃ (_ : AlgebraicGeometry.IsAffineOpen V) (_ : x ∈ V) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).IsStandardSmooth

A morphism of schemes is smooth if and only if for each x : X there exists an affine open neighborhood V of x and an affine open neighborhood U of f.base x with V ≤ f ⁻¹ᵁ U such that the induced map Γ(Y, U) ⟶ Γ(X, V) is standard smooth.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Smooth

Cited by

2 results in Mathlib

Foundations

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