Theorems · Theorem · algebraic geometry

AlgebraicGeometry.smoothOfRelativeDimension_iff

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

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Smooth

Cited by

0 results in Mathlib

Foundations

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