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.

Stacks Tag 02MD

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

The order of vanishing of 1 is 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.

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 ⊤.

Stacks Tag 02MD

Equations

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

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.

noncomputable def Ring.ordFrac (R : Type u_1) [CommRing R] [Nontrivial R] [IsNoetherianRing R] [KrullDimLE 1 R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] : 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.

Stacks Tag 02MD

Equations

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

theorem Ring.ordFrac_eq_ord (R : Type u_1) [CommRing R] [Nontrivial R] [IsNoetherianRing R] [KrullDimLE 1 R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] (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] [Nontrivial R] [IsNoetherianRing R] [KrullDimLE 1 R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] (a b : ↥(nonZeroDivisors R)) : (ordFrac R) (IsLocalization.mk' K (↑a) b) = (ordMonoidWithZeroHom R) ↑a / (ordMonoidWithZeroHom R) ↑b