Order of vanishing in a scheme

In this file we define the order of vanishing of an element of the function field of a locally Noetherian integral scheme at a point of codimension 1.

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

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

Equations

• AlgebraicGeometry.Scheme.ordHom z hz = Ring.ordFrac ↑(X.presheaf.stalk z)

theorem AlgebraicGeometry.Scheme.ordHom_of_isUnit {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] {U : X.Opens} [Nonempty ↥↑U] {f : ↑(X.presheaf.obj (Opposite.op U))} (hf : IsUnit f) {x : ↥X} (hx : Order.coheight x = 1) (hx' : x ∈ U) : (ordHom x hx) ((CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U)) f) = 1

noncomputable def AlgebraicGeometry.Scheme.ord {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (f : ↑X.functionField) (z : ↥X) : ℤ

The order of vanishing of an element of the function field of a locally Noetherian integral scheme at a point. This has a junk value of 0 if f = 0 or if coheight z ≠ 1.

Equations

• AlgebraicGeometry.Scheme.ord f z = if hz : Order.coheight z = 1 then Multiplicative.toAdd (WithZero.unzeroD 1 ((AlgebraicGeometry.Scheme.ordHom z hz) f)) else 0

theorem AlgebraicGeometry.Scheme.ord_eq_ordHom_of_coheight_eq_one {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] {z : ↥X} (hz : Order.coheight z = 1) (f : ↑X.functionField) : ord f z = Multiplicative.toAdd (WithZero.unzeroD 1 ((ordHom z hz) f))

@[simp]

theorem AlgebraicGeometry.Scheme.ord_eq_zero_of_coheight_neq_one {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] {z : ↥X} (hz : Order.coheight z ≠ 1) (f : ↑X.functionField) : ord f z = 0

@[simp]

theorem AlgebraicGeometry.Scheme.ord_zero {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] : ord 0 = 0

theorem AlgebraicGeometry.Scheme.ord_eq_unzero_ordHom {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] {x : ↥X} (hx : Order.coheight x = 1) {f : ↑X.functionField} (hf : f ≠ 0) : ord f x = Multiplicative.toAdd (WithZero.unzero ⋯)

theorem AlgebraicGeometry.Scheme.ord_eq_iff {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] {z : ↥X} (hz : Order.coheight z = 1) {f : ↑X.functionField} (hf : f ≠ 0) {n : ℤ} : ord f z = n ↔ (ordHom z hz) f = ↑(Multiplicative.ofAdd n)

@[simp]

theorem AlgebraicGeometry.Scheme.ord_mul {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] {x : ↥X} {f g : ↑X.functionField} (hf : f ≠ 0) (hg : g ≠ 0) : ord (f * g) x = ord f x + ord g x

theorem AlgebraicGeometry.Scheme.ord_of_isUnit {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] {U : X.Opens} [Nonempty ↥↑U] {f : ↑(X.presheaf.obj (Opposite.op U))} (hf : IsUnit f) {x : ↥X} (hx' : x ∈ U) : ord ((CategoryTheory.ConcreteCategory.hom (X.germToFunctionField U)) f) x = 0

theorem AlgebraicGeometry.Scheme.ord_le_ord_iff {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] {x y : ↥X} (hx : Order.coheight x = 1) (hy : Order.coheight y = 1) {f g : ↑X.functionField} (hf : f ≠ 0) (hg : g ≠ 0) : ord f x ≤ ord g y ↔ (ordHom x hx) f ≤ (ordHom y hy) g

theorem AlgebraicGeometry.Scheme.le_ord_iff {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] {x : ↥X} (hx : Order.coheight x = 1) {f : ↑X.functionField} (hf : f ≠ 0) {n : ℤ} : n ≤ ord f x ↔ ↑(Multiplicative.ofAdd n) ≤ (ordHom x hx) f

theorem AlgebraicGeometry.Scheme.ord_add {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] {x : ↥X} [IsDiscreteValuationRing ↑(X.presheaf.stalk x)] {f g : ↑X.functionField} (hfg : f + g ≠ 0) : min (ord f x) (ord g x) ≤ ord (f + g) x

theorem AlgebraicGeometry.Scheme.ord_le_smul {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] {x : ↥X} {U : X.Opens} [Nonempty ↥↑U] (hxU : x ∈ U) {a : ↑(X.presheaf.obj (Opposite.op U))} (ha : a ≠ 0) (f : ↑X.functionField) : ord f x ≤ ord (a • f) x