Order of vanishing in Noetherian rings. #
In this file we define various properties of the order of vanishing in Noetherian rings, including some API for computing the order of vanishing in discrete valuation rings.
Order of vanishing function as a monoid homomorphism
Equations
- Ring.ordMonoidHom = { toFun := fun (x : ↥(nonZeroDivisors R)) => Multiplicative.ofAdd (Ring.ord R ↑x).toNat, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Analogue of ord_ne_top for ordMonoidWithZeroHom.
Helper lemma to pass between the orders on ℕ∞ and ℤᵐ⁰ (which notably have different behaviour at
∞). Note that here we're using the fact that the order of any non zero divisor is finite, hence
the assumptions on the ring.
In a discrete valuation ring, ord R x is the same as addVal R x. We prefer the second spelling
here for most purposes.
For x y : R where R is a discrete valuation ring, we have that
min (ord R x) (ord R y) ≤ ord R (x + y). It should be noted that the order
we're using here is the order on ℕ∞, where ⊤ is greater than everything else.
This is relevant since when we're working with ordFrac we work with ℤᵐ⁰, where the
order instance has the 0 element less than everything else.
For any nonzero x : R, ordFrac R (algebraMap R K x) ≥ 1. Note here that this last
expression is in ℤᵐ⁰, so the syntax may be slightly different than expected. Namely,
the 1 here is WithZero.exp 0, and so would usually be written as 0 in the additive
context. Further, the order here is different to similar lemmas involving Ring.ord, since
here the order is on ℤᵐ⁰ has the ∞ element less than everything else, whereas in Ring.ord
we work with the order on ℕ∞ where the ∞ element is interpreted as a ⊤ element.
For x y : R, if x + y ≠ 0 then min (ordFrac R x) (ordFrac R y) ≤ ordFrac R (x + y). The
condition that x + y ≠ 0 is used to guarantee that all the elements we're taking ordFrac of
are nonzero, meaning none of them will be 0 in ℤᵐ⁰. This allows us to use ord_add (which
uses the ordering on ℕ∞), since these orders correspond on non ⊤ elements.