The tuning parameter

[Kol07, Aside 99.10] remarks that (m − 1) · lcm(2, …, m) ≤ m! for m ≥ 6, that (99.6) can be checked by hand for t ≥ m! when m = 1, …, 5, and hence that W_{m!}(I) is D-balanced, "the traditional choice of the coefficient ideal". This module proves the first remark and fixes the parameter s(m) of the tuning ideal W_{s(m)}(I) used throughout the library.

• (m − 1) L_m ≤ m! for m ≥ 6 (sub_one_mul_Lcm_le_factorial), with L_m = lcm(2, …, m). The proof is the library's own: L_{n+1} = lcm(L_n, n + 1) (Lcm_succ), so d · L_{n+1} ≤ L_n (n + 1) for every common divisor d of L_n and n + 1 (mul_Lcm_succ_le); if n + 2 is composite, its least prime factor is such a common divisor of L_{n+1} and n + 2, and if n + 2 is an odd prime, then n + 1 is even and 2 is a common divisor of L_n and n + 1. The invariant m L_m ≤ m! for m ≥ 6 follows by a two-step induction from the cases m = 6, 7 (mul_Lcm_le_factorial).
• For m ∈ {1, 2} and m ≥ 6, m! = r L_m with r ≥ m − 1 (exists_factorial_eq_mul_Lcm), so [Kol07, Proposition 99 (6)–(8)] apply with s = m!: W_{m!}(I) is D-balanced (isDBalanced_W_factorial).
• The tuning parameter of the library is tuningParam m = max (m − 1) 1 · L_m, the smallest multiple r L_m with r ≥ m − 1 and r ≥ 1; it is admissible for Kol07, Proposition 99 (6)–(8) for every m ≥ 1 without any hand check. W_{s(m)}(I) is D-balanced (isDBalanced_W_tuningParam), MC-invariant (isMCInvariant_W_tuningParam) and of order s(m) when ord I = m (ord_W_tuningParam). The factorial m! is not used as the parameter anywhere in the library.

Used for the tuned triple of the order-reduction theorems (Hironaka/Resolution/Algebraic/OrderReduction/Tuned.lean, Hironaka/Resolution/Algebraic/Tuning/Parameter.lean, Hironaka/Resolution/Algebraic/Stage/Amalgam.lean) and on manifolds (Hironaka/Manifold/IdealSheaf/Tuning.lean).

Number theory of L_m

theorem IsLocalRing.Lcm_dvd_Lcm_succ (n : ℕ) : Lcm n ∣ Lcm (n + 1)

theorem IsLocalRing.succ_dvd_Lcm_succ (n : ℕ) (hn : 1 ≤ n) : n + 1 ∣ Lcm (n + 1)

theorem IsLocalRing.Lcm_dvd_factorial (m : ℕ) : Lcm m ∣ m.factorial

theorem IsLocalRing.Lcm_succ (n : ℕ) (hn : 1 ≤ n) : Lcm (n + 1) = (Lcm n).lcm (n + 1)

L_{n+1} = lcm(L_n, n + 1).

theorem IsLocalRing.mul_Lcm_succ_le {n d : ℕ} (hn : 1 ≤ n) (hd : d ∣ Lcm n) (hd' : d ∣ n + 1) : d * Lcm (n + 1) ≤ Lcm n * (n + 1)

A common divisor d of L_n and n + 1 gives d · L_{n+1} ≤ L_n (n + 1).

theorem IsLocalRing.Lcm_succ_le (n : ℕ) (hn : 1 ≤ n) : Lcm (n + 1) ≤ Lcm n * (n + 1)

theorem IsLocalRing.mul_Lcm_le_factorial_step {n : ℕ} (hn : 6 ≤ n) (h1 : n * Lcm n ≤ n.factorial) (h2 : (n + 1) * Lcm (n + 1) ≤ (n + 1).factorial) : (n + 2) * Lcm (n + 2) ≤ (n + 2).factorial

The induction step for m L_m ≤ m!: from the cases n and n + 1 to n + 2 (n ≥ 6), by the least prime factor of n + 2 when it is composite and by 2 ∣ n + 1 when it is an odd prime.

theorem IsLocalRing.mul_Lcm_le_factorial {m : ℕ} (hm : 6 ≤ m) : m * Lcm m ≤ m.factorial

m L_m ≤ m! for m ≥ 6.

theorem IsLocalRing.sub_one_mul_Lcm_le_factorial {m : ℕ} (hm : 6 ≤ m) : (m - 1) * Lcm m ≤ m.factorial

[Kol07, Aside 99.10]: (m − 1) · lcm(2, …, m) ≤ m! for m ≥ 6, which Kollár says "is easy to see".

theorem IsLocalRing.exists_factorial_eq_mul_Lcm {m : ℕ} (hm : m = 1 ∨ m = 2 ∨ 6 ≤ m) : ∃ (r : ℕ), m.factorial = r * Lcm m ∧ m - 1 ≤ r

For m ∈ {1, 2} and m ≥ 6, m! = r L_m with r ≥ m − 1, so Kol07, Proposition 99 (6)–(8) apply with s = m!.

The tuning parameter

def IsLocalRing.tuningParam (m : ℕ) : ℕ

The tuning parameter s(m) = max (m − 1) 1 · L_m of the library: the smallest multiple r L_m of L_m with r ≥ m − 1 and r ≥ 1, for which [Kol07, Proposition 99 (6)–(8)] apply.

Equations

• IsLocalRing.tuningParam m = max (m - 1) 1 * IsLocalRing.Lcm m

theorem IsLocalRing.one_le_tuningParam (m : ℕ) : 1 ≤ tuningParam m

theorem IsLocalRing.RegularCoords.isDBalanced_W_factorial {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : m = 1 ∨ m = 2 ∨ 6 ≤ m) {I : Ideal R} (hI : ord I ≤ ↑m) : c.IsDBalanced (c.W m m.factorial I) m.factorial

[Kol07, Aside 99.10] ("Thus we conclude that W_{m!}(I) is D-balanced") for m ∈ {1, 2} and m ≥ 6: W_{m!}(I) is D-balanced with respect to m!.

theorem IsLocalRing.RegularCoords.isDBalanced_W_tuningParam {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) {I : Ideal R} (hI : ord I ≤ ↑m) : c.IsDBalanced (c.W m (tuningParam m) I) (tuningParam m)

W_{s(m)}(I) is D-balanced with respect to s(m) ([Kol07, (99.8)]).

theorem IsLocalRing.RegularCoords.isMCInvariant_W_tuningParam {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) {I : Ideal R} (hI : ord I ≤ ↑m) : c.IsMCInvariant (c.W m (tuningParam m) I) (tuningParam m)

W_{s(m)}(I) is MC-invariant with respect to s(m) ([Kol07, (99.5)]).

theorem IsLocalRing.RegularCoords.ord_W_tuningParam {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {m : ℕ} (hm : 1 ≤ m) {I : Ideal R} (hI : ord I = ↑m) : ord (c.W m (tuningParam m) I) = ↑(tuningParam m)

ord W_{s(m)}(I) = s(m) when ord I = m ≥ 1 (ord_W).