Documentation

Mathlib.AlgebraicGeometry.OrderOfVanishing

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.

source
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
Instances For
    source
    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
    source
    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
    Instances For
      source
      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))
      source
      @[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
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.ord_zero {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] :
      ord 0 = 0
      source
      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 ⋯)
      source
      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)
      source
      @[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
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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