Integrality of Möbius factors of strong divisibility sequences

For a strong divisibility sequence c in a UFD R (nowhere zero on n ≥ 1), the Möbius factor ∏_{d ∣ n} c_d ^ μ(n/d), a priori an element of the fraction field, lies in the image of R. moebiusFactorR c n is its unique R-preimage, characterised by algebraMap_moebiusFactorR: its image in any fraction field is the Möbius formula.

Auxiliary material for the formalization of M. Stoll, Galois groups over ℚ of some iterated polynomials, Arch. Math. 59 (1992), 239-244; upstreaming candidates for Mathlib.

noncomputable def moebiusFactorK {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] (c : ℕ → R) (n : ℕ) : K

The Möbius factor of c in the fraction field.

Equations

• moebiusFactorK c n = ∏ x ∈ n.divisorsAntidiagonal, (algebraMap R K) (c x.2) ^ ArithmeticFunction.moebius x.1

noncomputable def numProd {R : Type u_1} [CommRing R] (c : ℕ → R) (n : ℕ) : R

numerator product (μ = 1 part) and denominator product (μ = -1 part), in R.

Equations

• numProd c n = ∏ x ∈ n.divisorsAntidiagonal with ArithmeticFunction.moebius x.1 = 1, c x.2

noncomputable def denProd {R : Type u_1} [CommRing R] (c : ℕ → R) (n : ℕ) : R

The product of sequence values whose Möbius coefficient is negative.

Equations

• denProd c n = ∏ x ∈ n.divisorsAntidiagonal with ArithmeticFunction.moebius x.1 = -1, c x.2

theorem moebiusFactorK_eq_div {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {c : ℕ → R} (hc : ∀ d ≥ 1, c d ≠ 0) (n : ℕ) : moebiusFactorK c n = (algebraMap R K) (numProd c n) / (algebraMap R K) (denProd c n)

theorem moebiusFactorK_ne_zero {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {c : ℕ → R} (hc : ∀ d ≥ 1, c d ≠ 0) (n : ℕ) : moebiusFactorK c n ≠ 0

A Möbius factor of a nowhere-zero sequence is nonzero in the fraction field.

@[simp]

theorem moebiusFactorK_one {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] (c : ℕ → R) : moebiusFactorK c 1 = (algebraMap R K) (c 1)

theorem prod_moebiusFactorK {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {c : ℕ → R} (hc : ∀ d ≥ 1, c d ≠ 0) (n : ℕ) (hn : 1 ≤ n) : (algebraMap R K) (c n) = ∏ d ∈ n.divisors, moebiusFactorK c d

Möbius inversion in the fraction field: c n = ∏_{d ∣ n} moebiusFactorK c d.

theorem isInteger_div_iff_dvd {R : Type u_1} [CommRing R] [IsDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (a b : R) (hb : b ≠ 0) : IsLocalization.IsInteger R ((algebraMap R K) a / (algebraMap R K) b) ↔ b ∣ a

algebraMap a / algebraMap b is integral iff b ∣ a (for b ≠ 0).

noncomputable def moebiusFactorR {R : Type u_1} [CommRing R] [IsDomain R] (c : ℕ → R) (n : ℕ) : R

The R-valued Möbius factor: the (unique, by injectivity) preimage of the fraction-field factor. Junk value if the factor is not integral.

Equations

• moebiusFactorR c n = Function.invFun (⇑(algebraMap R (FractionRing R))) (moebiusFactorK c n)

@[simp]

theorem moebiusFactorR_one {R : Type u_1} [CommRing R] [IsDomain R] (c : ℕ → R) : moebiusFactorR c 1 = c 1

theorem factorization_prod {R : Type u_1} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] [NormalizedGCDMonoid R] [DecidableEq R] {ι : Type u_3} {s : Finset ι} {f : ι → R} (hf : ∀ i ∈ s, f i ≠ 0) (p : R) : (factorization (∏ i ∈ s, f i)) p = ∑ i ∈ s, (factorization (f i)) p

theorem factorization_numProd_sub_denProd {R : Type u_1} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] [NormalizedGCDMonoid R] [DecidableEq R] {c : ℕ → R} (hc : ∀ d ≥ 1, c d ≠ 0) (n : ℕ) (p : R) : ↑((factorization (numProd c n)) p) - ↑((factorization (denProd c n)) p) = ∑ x ∈ n.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 * ↑((factorization (c x.2)) p)

The valuation gap v_p(numProd) - v_p(denProd) is the Möbius transform of v_p ∘ c.

theorem factorization_gcd_min {R : Type u_1} [CommRing R] [UniqueFactorizationMonoid R] [NormalizedGCDMonoid R] [DecidableEq R] (a b : R) (ha : a ≠ 0) (hb : b ≠ 0) (p : R) : (factorization (gcd a b)) p = min ((factorization a) p) ((factorization b) p)

The p-multiplicity of a gcd is the minimum of the multiplicities.

theorem factorization_c_gcd_min {R : Type u_1} [CommRing R] [UniqueFactorizationMonoid R] [NormalizedGCDMonoid R] [DecidableEq R] {c : ℕ → R} (hc : ∀ d ≥ 1, c d ≠ 0) (hsd : ∀ (m n : ℕ), Associated (gcd (c m) (c n)) (c (m.gcd n))) (p : R) (x : ℕ) : x ≥ 1 → ∀ y ≥ 1, (factorization (c (x.gcd y))) p = min ((factorization (c x)) p) ((factorization (c y)) p)

v_p ∘ c is a gcd-min function when c is a strong divisibility sequence.

theorem denProd_dvd_numProd {R : Type u_1} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] [NormalizedGCDMonoid R] {c : ℕ → R} (hc : ∀ d ≥ 1, c d ≠ 0) (hsd : ∀ (m n : ℕ), Associated (gcd (c m) (c n)) (c (m.gcd n))) (n : ℕ) (hn : 1 ≤ n) : denProd c n ∣ numProd c n

theorem moebiusFactorK_isInteger {R : Type u_1} [CommRing R] [IsDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [UniqueFactorizationMonoid R] [NormalizedGCDMonoid R] {c : ℕ → R} (hc : ∀ d ≥ 1, c d ≠ 0) (hsd : ∀ (m n : ℕ), Associated (gcd (c m) (c n)) (c (m.gcd n))) (n : ℕ) (hn : 1 ≤ n) : IsLocalization.IsInteger R (moebiusFactorK c n)

Integrality (approach a). For a nowhere-zero strong divisibility sequence c in a UFD R, the fraction-field Möbius factor moebiusFactorK c n lies in the image of R.

theorem algebraMap_moebiusFactorR {R : Type u_1} [CommRing R] [IsDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [UniqueFactorizationMonoid R] [NormalizedGCDMonoid R] {c : ℕ → R} (hc : ∀ d ≥ 1, c d ≠ 0) (hsd : ∀ (m n : ℕ), Associated (gcd (c m) (c n)) (c (m.gcd n))) (n : ℕ) (hn : 1 ≤ n) : (algebraMap R K) (moebiusFactorR c n) = moebiusFactorK c n

API lemma. In any fraction field K of R, the image of moebiusFactorR c n is the Möbius formula (for a nowhere-zero strong divisibility sequence).

theorem prod_moebiusFactorR {R : Type u_1} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] [NormalizedGCDMonoid R] {c : ℕ → R} (hc : ∀ d ≥ 1, c d ≠ 0) (hsd : ∀ (m n : ℕ), Associated (gcd (c m) (c n)) (c (m.gcd n))) (n : ℕ) (hn : 1 ≤ n) : c n = ∏ d ∈ n.divisors, moebiusFactorR c d

Möbius inversion in R: c n = ∏_{d ∣ n} moebiusFactorR c d for a nowhere-zero strong divisibility sequence.

theorem moebiusFactorR_mul_denProd {R : Type u_1} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] [NormalizedGCDMonoid R] {c : ℕ → R} (hc : ∀ d ≥ 1, c d ≠ 0) (hsd : ∀ (m n : ℕ), Associated (gcd (c m) (c n)) (c (m.gcd n))) (n : ℕ) (hn : 1 ≤ n) : moebiusFactorR c n * denProd c n = numProd c n

The defining identity of the R-valued factor: β_n · denProd = numProd.

theorem moebiusFactorR_ne_zero {R : Type u_1} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] [NormalizedGCDMonoid R] {c : ℕ → R} (hc : ∀ d ≥ 1, c d ≠ 0) (hsd : ∀ (m n : ℕ), Associated (gcd (c m) (c n)) (c (m.gcd n))) (n : ℕ) (hn : 1 ≤ n) : moebiusFactorR c n ≠ 0

theorem factorization_moebiusFactorR {R : Type u_1} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] [NormalizedGCDMonoid R] [DecidableEq R] {c : ℕ → R} (hc : ∀ d ≥ 1, c d ≠ 0) (hsd : ∀ (m n : ℕ), Associated (gcd (c m) (c n)) (c (m.gcd n))) (n : ℕ) (hn : 1 ≤ n) (p : R) : ↑((factorization (moebiusFactorR c n)) p) = ∑ x ∈ n.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 * ↑((factorization (c x.2)) p)

v_p(β_n) is the Möbius transform of v_p ∘ c.

theorem factorization_moebiusFactorR_shape {R : Type u_1} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] [NormalizedGCDMonoid R] [DecidableEq R] {c : ℕ → R} (hc : ∀ d ≥ 1, c d ≠ 0) (hsd : ∀ (m n : ℕ), Associated (gcd (c m) (c n)) (c (m.gcd n))) (p : R) {m E : ℕ} (hm : 1 ≤ m) (hshape : ∀ k ≥ 1, (factorization (c k)) p = if m ∣ k then E else 0) (n : ℕ) (hn : 1 ≤ n) : (factorization (moebiusFactorR c n)) p = if n = m then E else 0

If v_p ∘ c has the constant-valuation shape (value E exactly on the multiples of m), then v_p(β_n) is supported at the single index n = m.

theorem moebiusFactorR_isRelPrime {R : Type u_1} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] [NormalizedGCDMonoid R] [DecidableEq R] {c : ℕ → R} (hc : ∀ d ≥ 1, c d ≠ 0) (hsd : ∀ (m n : ℕ), Associated (gcd (c m) (c n)) (c (m.gcd n))) (hshape : ∀ (p : R), Prime p → normalize p = p → ∃ m ≥ 1, ∃ (E : ℕ), ∀ k ≥ 1, (factorization (c k)) p = if m ∣ k then E else 0) (m n : ℕ) (hm : 1 ≤ m) (hn : 1 ≤ n) (hmn : m ≠ n) : IsRelPrime (moebiusFactorR c m) (moebiusFactorR c n)

Pairwise relative primality of the Möbius factors of a strong divisibility sequence with the constant-valuation property: distinct factors share no prime.