Parameter algebra in a regular local ring

Divisibility facts about a regular system of parameters z of a regular local ring R [Kol07, Definition 24]: a parameter is a nonzero prime element; distinct parameters do not divide each other; powers of distinct parameters dividing f divide f jointly; a divisor of z_c^N not divisible by z_c is a unit. Then the membership half of the order along a subvariety [Kol07, Definition 47] for a principal prime (le_pow_of_le_ordAlong_span_singleton: m ≤ ord_{(p)} I ⟹ I ⊆ (p)^m), its (p) = P form, the joint divisibility by pairwise non-dividing prime powers, and ordElem_parameter (a parameter has order one). These are the ring-level facts behind the splitting of an ideal into its monomial and non-monomial parts along the boundary (Hironaka.Resolution.Algebraic.MarkedOrderReduction.Split, Step 3 of the proof of Kol07, Theorem 107) and behind the components of a boundary (Hironaka.Resolution.Algebraic.Snc.ComponentStalks, Hironaka.Resolution.Algebraic.Snc.DictionaryRegular, Hironaka.Resolution.Algebraic.Kol07.UnionIdealInvertible). The names live in the namespace Hironaka.BMO of the order-reduction modules that use them.

A. Parameters of a regular local ring

theorem AlgebraicGeometry.ne_zero_of_parameters {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.maximalIdeal R = Ideal.span (Set.range z)) (hn : ↑n = ringKrullDim R) (c : Fin n) : z c ≠ 0

A member of a regular system of parameters is nonzero (it lies outside 𝔪²).

theorem AlgebraicGeometry.prime_of_parameters {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.maximalIdeal R = Ideal.span (Set.range z)) (hn : ↑n = ringKrullDim R) (c : Fin n) : Prime (z c)

A member of a regular system of parameters is a prime element (isPrime_span_singleton_of_parameters).

theorem AlgebraicGeometry.not_dvd_of_ne {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.maximalIdeal R = Ideal.span (Set.range z)) (hn : ↑n = ringKrullDim R) {c d : Fin n} (h : c ≠ d) : ¬z c ∣ z d

Distinct parameters do not divide each other (notMem_span_image_of_notMem of Hironaka.Scheme.Snc.ParameterSubset).

theorem AlgebraicGeometry.not_dvd_prod_pow {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.maximalIdeal R = Ideal.span (Set.range z)) (hn : ↑n = ringKrullDim R) {s : Finset (Fin n)} {d : Fin n} (hd : d ∉ s) (a : Fin n → ℕ) : ¬z d ∣ ∏ c ∈ s, z c ^ a c

A parameter outside s does not divide a monomial in the parameters of s.

theorem AlgebraicGeometry.prod_pow_dvd_of_forall_dvd {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.maximalIdeal R = Ideal.span (Set.range z)) (hn : ↑n = ringKrullDim R) (s : Finset (Fin n)) (a : Fin n → ℕ) {f : R} (h : ∀ c ∈ s, z c ^ a c ∣ f) : ∏ c ∈ s, z c ^ a c ∣ f

Powers of distinct parameters dividing f divide f jointly: the intersection of the ideals (z_c^{a_c}) is the ideal of their product.

theorem AlgebraicGeometry.isUnit_of_dvd_pow_of_not_dvd {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.maximalIdeal R = Ideal.span (Set.range z)) (hn : ↑n = ringKrullDim R) {c : Fin n} {g : R} (hg : ¬z c ∣ g) {N : ℕ} (h : g ∣ z c ^ N) : IsUnit g

A divisor of a power of the parameter z_c not divisible by z_c is a unit.

E. Local algebra: membership from the order along a principal prime

theorem AlgebraicGeometry.le_pow_of_le_ordAlong_span_singleton {R : Type u} [CommRing R] [IsDomain R] {p : R} (hp : Prime p) (I : Ideal R) (m : ℕ) [hP : (Ideal.span {p}).IsPrime] (h : ↑m ≤ IsLocalRing.ordAlong (Ideal.span {p}) I) : I ≤ Ideal.span {p} ^ m

The membership half of the order along a subvariety [Kol07, Definition 47] for a principal prime: for a prime element p, m ≤ ord_{(p)} I (the order of I in the localization at (p)) gives I ⊆ (p)^m — an element f ∈ I has t s f ∈ (p^m) with t, s ∉ (p), and p^m ∣ f since p is prime.

theorem AlgebraicGeometry.le_pow_of_le_ordAlong_of_eq_span {R : Type u} [CommRing R] [IsDomain R] {P : Ideal R} [P.IsPrime] {p : R} (hp : Prime p) (hPp : P = Ideal.span {p}) (I : Ideal R) (m : ℕ) (h : ↑m ≤ IsLocalRing.ordAlong P I) : I ≤ P ^ m

le_pow_of_le_ordAlong_span_singleton for a prime ideal given as (p).

theorem AlgebraicGeometry.prod_dvd_of_forall_dvd_of_pairwise {R : Type u} [CommRing R] [IsDomain R] {ι : Type u_1} (S : Finset ι) (q : ι → R) (hq : ∀ d ∈ S, IsUnit (q d) ∨ ∃ (p : R), Prime p ∧ (∃ (a : ℕ), q d = p ^ a) ∧ ∀ i ∈ S, i ≠ d → ¬p ∣ q i) {f : R} (h : ∀ i ∈ S, q i ∣ f) : ∏ i ∈ S, q i ∣ f

Powers of pairwise non-dividing primes (or units) dividing f divide f jointly.

theorem AlgebraicGeometry.ordElem_parameter {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : Ideal.span (Set.range z) = IsLocalRing.maximalIdeal R ∧ ↑n = ringKrullDim R) (c : Fin n) : IsLocalRing.ordElem (z c) = 1

A member of a regular system of parameters has order one.