Documentation

Mathlib.AlgebraicGeometry.OrderOfVanishing.Basic

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, and develop its basic API.

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
      @[simp]
      theorem AlgebraicGeometry.Scheme.ord_one {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] :
      ord 1 = 0
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.ord_inv {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (z : ↥X) (f : ↑X.functionField) :
      ord f⁻¹ z = -ord f z
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.ord_div {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (z : ↥X) {f g : ↑X.functionField} (hf : f ≠ 0) (hg : g ≠ 0) :
      ord (f / g) z = ord f z - ord g z
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.ord_pow {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (z : ↥X) (f : ↑X.functionField) (n : ℕ) :
      ord (f ^ n) z = ↑n * ord f z
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.ord_zpow {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (z : ↥X) (f : ↑X.functionField) (n : ℤ) :
      ord (f ^ n) z = n * ord f z
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.ord_prod {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] {ι : Type u_1} (z : ↥X) (T : Finset ι) (F : ι → ↑X.functionField) (hF : ∀ i ∈ T, F i ≠ 0) :
      ord (∏ i ∈ T, F i) z = ∑ i ∈ T, ord (F i) z
      source
      @[simp]
      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
      @[simp]
      theorem AlgebraicGeometry.Scheme.ord_neg {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (f : ↑X.functionField) (z : ↥X) :
      ord (-f) z = ord f z
      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_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
      source
      theorem AlgebraicGeometry.Scheme.algebraMap_functionField_ne_zero {X : Scheme} [IsIntegral X] {x : ↥X} {a : ↑(X.presheaf.stalk x)} (ha : a ≠ 0) :
      (algebraMap ↑(X.presheaf.stalk x) ↑X.functionField) a ≠ 0
      source
      theorem AlgebraicGeometry.Scheme.ord_algebraMap_nonneg {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] {x : ↥X} {a : ↑(X.presheaf.stalk x)} (ha : a ≠ 0) :
      0 ≤ ord ((algebraMap ↑(X.presheaf.stalk x) ↑X.functionField) a) x
      source
      theorem AlgebraicGeometry.Scheme.ord_algebraMap_eq_zero_of_isUnit {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] {x : ↥X} {a : ↑(X.presheaf.stalk x)} (ha : IsUnit a) :
      ord ((algebraMap ↑(X.presheaf.stalk x) ↑X.functionField) a) x = 0
      source
      theorem AlgebraicGeometry.Scheme.ord_algebraMap_section_nonneg {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] {U : X.Opens} [Nonempty ↥↑U] (w : ↥U) {r : ↑(X.presheaf.obj (Opposite.op U))} (hr : r ≠ 0) :
      0 ≤ ord ((algebraMap ↑(X.presheaf.obj (Opposite.op U)) ↑X.functionField) r) ↑w
      source
      theorem AlgebraicGeometry.Scheme.ord_eq_zero_of_mem_basicOpen {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] {U : X.Opens} [Nonempty ↥↑U] (w : ↥U) {r : ↑(X.presheaf.obj (Opposite.op U))} (hmem : ↑w ∈ X.basicOpen r) :
      ord ((algebraMap ↑(X.presheaf.obj (Opposite.op U)) ↑X.functionField) r) ↑w = 0