Theorems · Inductive type · algebraic geometry

AlgebraicGeometry.SmoothOfRelativeDimension

ℕ → {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop

A morphism of schemes f : X ⟶ Y is smooth of relative dimension n 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 of relative dimension n.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Smooth

Cited by

8 results in Mathlib

Foundations

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