Order of vanishing

This file defines the order of vanishing of an element of a ring as the length of the quotient of the ring by the ideal generated by that element. We also define the extension of this notion to the field of fractions

noncomputable def Ring.ord (R : Type u_1) [Ring R] (x : R) : ℕ∞

Order of vanishing function for elements of a ring.

Equations

• Ring.ord R x = Module.length R (R ⧸ Ideal.span {x})

@[simp]

theorem Ring.ord_one (R : Type u_1) [Ring R] : ord R 1 = 0

def Ideal.mulQuot {R : Type u_1} [CommRing R] (a : R) (I : Ideal R) : R ⧸ I →ₗ[R] R ⧸ a • I

The map R ⧸ I →ₗ[R] R ⧸ (a • I) defined by multiplication by a

Equations

• Ideal.mulQuot a I = Submodule.mapQ I (a • I) ((LinearMap.mul R R) a) ⋯

theorem Ideal.mulQuot_injective {R : Type u_1} [CommRing R] {a : R} (I : Ideal R) (ha : a ∈ nonZeroDivisors R) : Function.Injective ⇑(mulQuot a I)

The map R ⧸ I →ₗ[R] R ⧸ (a • I) defined by multiplication by a is injective if a is a nonzero divisor.

def Ideal.quotOfMul {R : Type u_1} [CommRing R] (a : R) (I : Ideal R) : R ⧸ a • I →ₗ[R] R ⧸ span {a}

The quotient map (R ⧸ a • I) →ₗ[R] (R ⧸ Ideal.span {a}).

Equations

• Ideal.quotOfMul a I = Submodule.factor ⋯

theorem Ideal.quotOfMul_surjective {R : Type u_1} [CommRing R] {a : R} (I : Ideal R) : Function.Surjective ⇑(quotOfMul a I)

The quotient map (R ⧸ a • I) →ₗ[R] (R ⧸ Ideal.span {a}) is surjective.

theorem Ideal.exact_mulQuot_quotOfMul {R : Type u_1} [CommRing R] {a : R} (I : Ideal R) : Function.Exact ⇑(mulQuot a I) ⇑(quotOfMul a I)

The sequence R ⧸ I →ₗ[R] R ⧸ (a • I) →ₗ[R] R ⧸ (Ideal.span {a}) given by multiplication by a then quotienting by the ideal generated by a is exact.

theorem Ring.ord_mul (R : Type u_1) [CommRing R] {a b : R} (hb : b ∈ nonZeroDivisors R) : ord R (a * b) = ord R a + ord R b

The order of vanishing of a * b is the order of vanishing of a plus the order of vanishing of b.

theorem Ring.ord_mul' (R : Type u_1) [CommRing R] {a b : R} (ha : a ∈ nonZeroDivisors R) : ord R (a * b) = ord R a + ord R b

Variation of ord_mul where the user has to show the first input is a non zero divisor rather than the second.

theorem Ring.ord_zero (R : Type u_1) [CommRing R] : ord R 0 = Module.length R R

The order of zero is Module.length R R. Use this when it is necessary to unfold the definition of ord to avoid annoyances of working with R ⧸ Ideal.span {0} instead of R.

@[simp]

theorem Ring.ord_pow {R : Type u_1} [CommRing R] {x : R} (hx : x ∈ nonZeroDivisors R) (n : ℕ) : ord R (x ^ n) = n • ord R x

For x : R a non zero divisor, ord R (x ^ n) = n • ord R x.

@[simp]

theorem Ring.ord_mul_of_isUnit_left {R : Type u_1} [CommRing R] {a : R} (h : IsUnit a) (x : R) : ord R (a * x) = ord R x

@[simp]

theorem Ring.ord_mul_of_isUnit_right {R : Type u_1} [CommRing R] {a : R} (h : IsUnit a) (x : R) : ord R (x * a) = ord R x

theorem Ring.ord_eq_of_associated {R : Type u_1} [CommRing R] {x y : R} (h : Associated x y) : ord R x = ord R y

@[simp]

theorem Ring.ord_neg {R : Type u_1} [CommRing R] (x : R) : ord R (-x) = ord R x

@[simp]

theorem Ring.ord_smul_of_isUnit {R : Type u_1} [CommRing R] {S : Type u_3} [CommRing S] [Algebra S R] {a : S} (h : IsUnit a) (x : R) : ord R (a • x) = ord R x

In an S algebra R, the order of vanishing of x : R is equal to the order of vanishing of a • x for a a unit in S.

theorem Ring.ord_le_ord_mul {R : Type u_1} [CommRing R] (a x : R) : ord R x ≤ ord R (a * x)

theorem Ring.ord_le_ord_of_dvd {R : Type u_1} [CommRing R] {a x : R} (h : a ∣ x) : ord R a ≤ ord R x

theorem Ring.ord_le_smul {R : Type u_1} [CommRing R] {S : Type u_3} [CommRing S] [Algebra S R] (a : S) (x : R) : ord R x ≤ ord R (a • x)

In an S algebra R, the order of vanishing of x : R is less than or equal to the order of vanishing of a • x for any a : S. One should note that the order here is the order on ℕ∞ where ∞ is a top element.

@[simp]

theorem Ring.ord_of_isUnit {R : Type u_1} [CommRing R] {x : R} (hx : IsUnit x) : ord R x = 0

The order of vanishing of a unit is 0.

theorem Ring.ord_of_irreducible {R : Type u_1} [CommRing R] [IsPrincipalIdealRing R] {ϖ : R} (hϖ : Irreducible ϖ) : ord R ϖ = 1

In a principal ideal ring, the order of vanishing of an irreducible element is 1.

noncomputable def Ring.ordMonoidWithZeroHom (R : Type u_1) [CommRing R] [Nontrivial R] : R →*₀ WithZero (Multiplicative ℤ)

Zero-preserving monoid homomorphism from a nontrivial commutative ring R to ℤᵐ⁰.

Note that we cannot just use fun x ↦ ord R x without further assumptions on R. This is because if R is finite length, then ord R 0 will be some non-top value, meaning in this case 0 will not be mapped to ⊤.

Equations

• One or more equations did not get rendered due to their size.

theorem Ring.ordMonoidWithZeroHom_eq_zero_iff (R : Type u_1) [CommRing R] [Nontrivial R] (y : ↥(nonZeroDivisors R)) : (ordMonoidWithZeroHom R) ↑y = 0 ↔ ord R ↑y = ⊤

theorem Ring.ordMonoidWithZeroHom_eq_ord {R : Type u_1} [CommRing R] [Nontrivial R] {x : R} (h : x ∈ nonZeroDivisors R) : (ordMonoidWithZeroHom R) x = ENat.recTopCoe 0 (fun (x : ℕ) => ↑(Multiplicative.ofAdd ↑x)) (ord R x)

If x is a non zero divisor, ordMonoidWithZeroHom is equal to the canonical embedding of Ring.ord R x into WithZero (Multiplicative ℤ).

theorem Ring.ordMonoidWithZeroHom_eq_coe (R : Type u_1) [CommRing R] [Nontrivial R] {x : R} (hx : x ∈ nonZeroDivisors R) {n : ℕ} (hn : ord R x = ↑n) : (ordMonoidWithZeroHom R) x = ↑(Multiplicative.ofAdd ↑n)

@[simp]

theorem Ring.ordMonoidWithZeroHom_eq_zero {R : Type u_1} [CommRing R] [Nontrivial R] {x : R} (h : x ∉ nonZeroDivisors R) : (ordMonoidWithZeroHom R) x = 0

If x is not a non zero divisor, ordMonoidWithZeroHom is equal to 0.

theorem isFiniteLength_quotient_span_singleton (R : Type u_1) [CommRing R] [IsNoetherianRing R] [Ring.KrullDimLE 1 R] {x : R} (hx : x ∈ nonZeroDivisors R) : IsFiniteLength R (R ⧸ Ideal.span {x})

The quotient of a Noetherian ring of krull dimension less than or equal to 1 by a principal ideal is of finite length.

theorem Ring.ord_ne_top {R : Type u_1} [CommRing R] [IsNoetherianRing R] [KrullDimLE 1 R] {a : R} (ha : a ∈ nonZeroDivisors R) : ord R a ≠ ⊤

theorem Ring.ord_lt_top {R : Type u_1} [CommRing R] [IsNoetherianRing R] [KrullDimLE 1 R] {a : R} (ha : a ∈ nonZeroDivisors R) : ord R a < ⊤

theorem Ring.ordMonoidWithZeroHom_isUnit (R : Type u_1) [CommRing R] [IsNoetherianRing R] [KrullDimLE 1 R] [Nontrivial R] (y : ↥(nonZeroDivisors R)) : IsUnit ((ordMonoidWithZeroHom R) ↑y)

noncomputable def Ring.ordFrac (R : Type u_1) [CommRing R] [IsNoetherianRing R] [KrullDimLE 1 R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] [Nontrivial R] : K →*₀ WithZero (Multiplicative ℤ)

Order of vanishing function for elements of the fraction field defined as the extension of CommRing.ordMonoidWithZeroHom to the field of fractions.

Equations

• Ring.ordFrac R = (IsLocalization.toLocalizationMap (nonZeroDivisors R) K).lift₀ (Ring.ordMonoidWithZeroHom R) ⋯

theorem Ring.ordFrac_eq_ord (R : Type u_1) [CommRing R] [IsNoetherianRing R] [KrullDimLE 1 R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] [Nontrivial R] {x : R} (hx : x ≠ 0) : (ordFrac R) ((algebraMap R K) x) = (ordMonoidWithZeroHom R) x

theorem Ring.ordFrac_eq_div (R : Type u_1) [CommRing R] [IsNoetherianRing R] [KrullDimLE 1 R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] [Nontrivial R] (a b : ↥(nonZeroDivisors R)) : (ordFrac R) (IsLocalization.mk' K (↑a) b) = (ordMonoidWithZeroHom R) ↑a / (ordMonoidWithZeroHom R) ↑b