The order of an ideal in a local ring

Kollár defines, for a smooth variety X, a nonzero ideal sheaf I and a point x with ideal sheaf 𝔪ₓ, the order of I at x as ord_x I := max {r : 𝔪ₓ^r 𝒪_{x,X} ⊇ I 𝒪_{x,X}}; for a principal ideal (f) it is the multiplicity of the hypersurface f = 0 [Kol07, Definition 47]. The order IsLocalRing.ord I of an ideal of a local ring is the supremum in ℕ∞ of the r with I ≤ 𝔪^r, so that the zero ideal has order ⊤ (Kollár assumes I ≠ 0; Krull's intersection theorem, recalled in [Kol07, Definition 55], is what makes the two readings agree). This file defines the order of an element and proves the elementary calculus:

• ordElem f, the order of the principal ideal (f);
• le_ord_iff: r ≤ ord I ↔ I ≤ 𝔪^r, the characterization everything else reduces to;
• ord_eq_top_iff, ordElem_eq_top_iff: Krull's intersection theorem, ord I = ⊤ iff I = 0 for a Noetherian local ring;
• ord_eq_iInf, ord_span, exists_ord_span_eq_ordElem: the order of an ideal is the infimum of the orders of its elements, or of any generating set, attained by a generator when the set is finite and nonempty;
• ord_top, ord_eq_zero_iff, one_le_ordElem_iff, ordElem_eq_one_iff.

In K⟦X⟧ with finitely many variables the order of an element is Mathlib's MvPowerSeries.order (MvPowerSeries.ordElem_eq_order, in Hironaka/Algebra/Local/PowerSeries.lean).

The calculus of the order

The local forms of the elementary properties (1)–(4) of the cosupport of a marked ideal listed in [Kol07, Definition 59]:

• ord_anti (property (1)): I ≤ J → ord J ≤ ord I.
• le_ord_mul (property (2)): ord I + ord J ≤ ord (I * J).
• ord_sup (property (4)): ord (I ⊔ J) = min (ord I) (ord J).
• le_ord_pow (property (3), one inclusion): c * ord I ≤ ord (I ^ c).
• ord_pow_of_ordElem_mul (property (3), the converse) and ord_span_singleton_mul_of_ordElem_mul: both need multiplicativity of the order on elements, ord (f g) = ord f + ord g (used silently by Kollár in property (3) and in [Kol07, Theorem 54.2]), which holds in every regular local ring and, for rings containing ℚ, is ordElem_mul_of_algebraRat of Hironaka/Algebra/Local/CohenIso.lean, through R̂ ≅ K⟦x⟧; here they take it as an explicit hypothesis.
• ord_le_ord_map (the proof of [Wlo05, Lemma 2.10.3]: "the order of an ideal does not drop but may rise after restriction"): for a local homomorphism φ, ord I ≤ ord (I.map φ); the quotient R/(x₁) is the case φ = Ideal.Quotient.mk.
• ordAlong (Kollár's ord_Z I := ord_η I at the generic point, [Kol07, Definition 47]): the order of I in the localization at a prime.

The scheme-level statements of Definition 47 (upper semicontinuity, ord_Z, max-ord) are proved for the order of an ideal sheaf, Scheme.IdealSheafData.ord.

noncomputable def IsLocalRing.ordElem {R : Type u_1} [CommRing R] [IsLocalRing R] (f : R) : ℕ∞

The order of an element: ord f = ord (f), the multiplicity of the hypersurface f = 0 [Kol07, Definition 47].

Equations

• IsLocalRing.ordElem f = IsLocalRing.ord (Ideal.span {f})

theorem IsLocalRing.le_ord_of_le {R : Type u_1} [CommRing R] [IsLocalRing R] {I : Ideal R} {r : ℕ} (h : I ≤ maximalIdeal R ^ r) : ↑r ≤ ord I

theorem IsLocalRing.le_ord_iff {R : Type u_1} [CommRing R] [IsLocalRing R] {I : Ideal R} {r : ℕ} : ↑r ≤ ord I ↔ I ≤ maximalIdeal R ^ r

r ≤ ord I iff I ≤ 𝔪^r; uses that the powers of 𝔪 decrease.

theorem IsLocalRing.mem_maximalIdeal_pow_iff_le_ordElem {R : Type u_1} [CommRing R] [IsLocalRing R] {f : R} {r : ℕ} : f ∈ maximalIdeal R ^ r ↔ ↑r ≤ ordElem f

theorem IsLocalRing.ord_anti {R : Type u_1} [CommRing R] [IsLocalRing R] {I J : Ideal R} (h : I ≤ J) : ord J ≤ ord I

The order is antitone: I ≤ J → ord J ≤ ord I (property (1) of the cosupport in [Kol07, Definition 59]).

@[simp]

theorem IsLocalRing.ord_top {R : Type u_1} [CommRing R] [IsLocalRing R] : ord ⊤ = 0

The unit ideal has order 0.

theorem IsLocalRing.ord_eq_zero_iff {R : Type u_1} [CommRing R] [IsLocalRing R] {I : Ideal R} : ord I = 0 ↔ I = ⊤

ord I = 0 iff I is the unit ideal (in a local ring a proper ideal lies in 𝔪).

theorem IsLocalRing.one_le_ordElem_iff {R : Type u_1} [CommRing R] [IsLocalRing R] {f : R} : 1 ≤ ordElem f ↔ f ∈ maximalIdeal R

1 ≤ ord f iff f ∈ 𝔪.

theorem IsLocalRing.ordElem_eq_one_iff {R : Type u_1} [CommRing R] [IsLocalRing R] {f : R} : ordElem f = 1 ↔ f ∈ maximalIdeal R ∧ f ∉ maximalIdeal R ^ 2

ord f = 1 iff f ∈ 𝔪 ∖ 𝔪².

theorem IsLocalRing.ord_eq_iInf {R : Type u_1} [CommRing R] [IsLocalRing R] (I : Ideal R) : ord I = ⨅ f ∈ I, ordElem f

The order of an ideal is the infimum of the orders of its elements.

theorem IsLocalRing.ord_span {R : Type u_1} [CommRing R] [IsLocalRing R] (S : Set R) : ord (Ideal.span S) = ⨅ f ∈ S, ordElem f

The order of ⟨S⟩ is the infimum of the orders of the generators.

theorem IsLocalRing.exists_ord_span_eq_ordElem {R : Type u_1} [CommRing R] [IsLocalRing R] {S : Set R} (hS : S.Finite) (hne : S.Nonempty) : ∃ f ∈ S, ord (Ideal.span S) = ordElem f

For a finite nonempty generating set the infimum is attained by a generator.

theorem IsLocalRing.ord_eq_top_iff {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] {I : Ideal R} : ord I = ⊤ ↔ I = ⊥

In a Noetherian local ring the only ideal of infinite order is the zero ideal (Krull's intersection theorem, recalled in [Kol07, Definition 55]).

theorem IsLocalRing.ordElem_eq_top_iff {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] {f : R} : ordElem f = ⊤ ↔ f = 0

The only element of infinite order is 0.

theorem IsLocalRing.le_ord_mul {R : Type u_2} [CommRing R] [IsLocalRing R] (I J : Ideal R) : ord I + ord J ≤ ord (I * J)

Superadditivity, ord I + ord J ≤ ord (I J), from 𝔪^a 𝔪^b = 𝔪^(a+b) (property (2) of the cosupport in [Kol07, Definition 59]).

theorem IsLocalRing.ord_sup {R : Type u_2} [CommRing R] [IsLocalRing R] (I J : Ideal R) : ord (I ⊔ J) = min (ord I) (ord J)

ord (I + J) = min (ord I) (ord J) (property (4) of the cosupport in [Kol07, Definition 59]).

theorem IsLocalRing.le_ord_pow {R : Type u_2} [CommRing R] [IsLocalRing R] (I : Ideal R) (c : ℕ) : ↑c * ord I ≤ ord (I ^ c)

c · ord I ≤ ord (I ^ c) (one inclusion of property (3) of the cosupport in [Kol07, Definition 59]).

theorem IsLocalRing.ord_le_ord_map {R : Type u_2} [CommRing R] [IsLocalRing R] {S : Type u_3} [CommRing S] [IsLocalRing S] (φ : R →+* S) [IsLocalHom φ] (I : Ideal R) : ord I ≤ ord (Ideal.map φ I)

The order does not drop under a local homomorphism, ord I ≤ ord (I.map φ) (the proof of [Wlo05, Lemma 2.10.3]; the inclusion (58.2) of [Kol07, 58] is its sheaf form); restriction to R/(x₁) is the case φ = Ideal.Quotient.mk.

theorem IsLocalRing.ordElem_one {R : Type u_2} [CommRing R] [IsLocalRing R] : ordElem 1 = 0

theorem IsLocalRing.ordElem_pow_of_ordElem_mul {R : Type u_2} [CommRing R] [IsLocalRing R] (hmul : ∀ (f g : R), ordElem (f * g) = ordElem f + ordElem g) (f : R) (n : ℕ) : ordElem (f ^ n) = ↑n * ordElem f

Multiplicativity of the order on elements implies ord (f ^ n) = n · ord f.

theorem IsLocalRing.ord_bot {R : Type u_2} [CommRing R] [IsLocalRing R] : ord ⊥ = ⊤

theorem IsLocalRing.ord_pow_of_ordElem_mul {R : Type u_2} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (hmul : ∀ (f g : R), ordElem (f * g) = ordElem f + ordElem g) (I : Ideal R) {c : ℕ} (hc : 1 ≤ c) : ord (I ^ c) = ↑c * ord I

Given multiplicativity of the order on elements, ord (I ^ c) = c · ord I for c ≥ 1 (the equality behind property (3) of the cosupport in [Kol07, Definition 59]). Pick a generator f of I with ord f = ord I; then f ^ c ∈ I ^ c has order c · ord I.

theorem IsLocalRing.ord_span_singleton_mul_of_ordElem_mul {R : Type u_2} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (hmul : ∀ (f g : R), ordElem (f * g) = ordElem f + ordElem g) (f : R) (I : Ideal R) : ord (Ideal.span {f} * I) = ordElem f + ord I

Given multiplicativity of the order on elements, ord (f I) = ord f + ord I.

noncomputable def IsLocalRing.ordAlong {R : Type u_2} [CommRing R] (P : Ideal R) [P.IsPrime] (I : Ideal R) : ℕ∞

The order of I along the prime P, computed in the local ring R_P: Kollár's ord_Z I := ord_η I at the generic point η of Z [Kol07, Definition 47].

Equations

• IsLocalRing.ordAlong P I = IsLocalRing.ord (Ideal.map (algebraMap R (Localization.AtPrime P)) I)