Order of vanishing at a point whose local ring is a discrete valuation ring

This file collects the results about AlgebraicGeometry.Scheme.ord, the order of vanishing of an element of the function field of a locally Noetherian integral scheme, that need the local ring at the point in question to be a discrete valuation ring. The results that do not are in Mathlib/AlgebraicGeometry/OrderOfVanishing/Basic.lean.

theorem AlgebraicGeometry.Scheme.coheight_eq_one_of_isDiscreteValuationRing {X : Scheme} [IsIntegral X] {x : ↥X} [IsDiscreteValuationRing ↑(X.presheaf.stalk x)] : Order.coheight x = 1

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

theorem AlgebraicGeometry.Scheme.ord_algebraMap_irreducible {X : Scheme} [IsIntegral X] {x : ↥X} [IsDiscreteValuationRing ↑(X.presheaf.stalk x)] [IsLocallyNoetherian X] {ϖ : ↑(X.presheaf.stalk x)} (hϖ : Irreducible ϖ) : ord ((algebraMap ↑(X.presheaf.stalk x) ↑X.functionField) ϖ) x = 1

theorem AlgebraicGeometry.Scheme.ord_zpow_algebraMap_irreducible {X : Scheme} [IsIntegral X] {x : ↥X} [IsDiscreteValuationRing ↑(X.presheaf.stalk x)] [IsLocallyNoetherian X] {ϖ : ↑(X.presheaf.stalk x)} (hϖ : Irreducible ϖ) (n : ℤ) : ord ((algebraMap ↑(X.presheaf.stalk x) ↑X.functionField) ϖ ^ n) x = n

theorem AlgebraicGeometry.Scheme.mem_maximalIdeal_iff_one_le_ord {X : Scheme} [IsIntegral X] {x : ↥X} [IsDiscreteValuationRing ↑(X.presheaf.stalk x)] [IsLocallyNoetherian X] {a : ↑(X.presheaf.stalk x)} (ha : a ≠ 0) : a ∈ IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x) ↔ 1 ≤ ord ((algebraMap ↑(X.presheaf.stalk x) ↑X.functionField) a) x

theorem AlgebraicGeometry.Scheme.exists_algebraMap_eq_iff_ord_nonneg {X : Scheme} [IsIntegral X] {x : ↥X} [IsDiscreteValuationRing ↑(X.presheaf.stalk x)] [IsLocallyNoetherian X] (f : ↑X.functionField) : (∃ (a : ↑(X.presheaf.stalk x)), (algebraMap ↑(X.presheaf.stalk x) ↑X.functionField) a = f) ↔ 0 ≤ ord f x

theorem AlgebraicGeometry.Scheme.ord_algebraMap_eq_of_eq_unit_mul_pow {X : Scheme} [IsIntegral X] {x : ↥X} [IsDiscreteValuationRing ↑(X.presheaf.stalk x)] [IsLocallyNoetherian X] (a : ↑(X.presheaf.stalk x)) (u : (↑(X.presheaf.stalk x))ˣ) {ϖ : ↑(X.presheaf.stalk x)} (hϖ : Irreducible ϖ) (n : ℕ) (ha : a = ↑u * ϖ ^ n) : ord ((algebraMap ↑(X.presheaf.stalk x) ↑X.functionField) a) x = ↑n

If an element of the local ring at a codimension-one point factors as a unit times the n-th power of a uniformizer, then the rational function it determines has order of vanishing n. This is the scheme-level form of IsDiscreteValuationRing.addVal_def.

theorem AlgebraicGeometry.Scheme.one_le_ord_iff_notMem_basicOpen {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] {U : X.Opens} [Nonempty ↥↑U] (w : ↥U) [IsDiscreteValuationRing ↑(X.presheaf.stalk ↑w)] {r : ↑(X.presheaf.obj (Opposite.op U))} (hr : r ≠ 0) : 1 ≤ ord ((algebraMap ↑(X.presheaf.obj (Opposite.op U)) ↑X.functionField) r) ↑w ↔ ↑w ∉ X.basicOpen r