Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.ordHom

{X : AlgebraicGeometry.Scheme} →
  [inst : AlgebraicGeometry.IsIntegral X] →
    [AlgebraicGeometry.IsLocallyNoetherian X] →
      (z : ↥X) → Order.coheight z = 1 → ↑X.functionField →*₀ WithZero (Multiplicative ℤ)

Order of vanishing on a locally Noetherian integral scheme as a monoid with zero hom to ℤᵐ⁰.

Defined in

Mathlib.AlgebraicGeometry.OrderOfVanishing

Cited by

10 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsIntegralAlgebraicGeometry.IsLocallyNoetherian