Unique factorization lemmas

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.

theorem normalizedFactors_map_mulEquiv_eq {α : Type u_1} [CommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] (σ : α ≃* α) {p : α} (hp0 : p ≠ 0) (hassoc : Associated (σ p) p) : Multiset.map (fun (q : α) => normalize (σ q)) (UniqueFactorizationMonoid.normalizedFactors p) = UniqueFactorizationMonoid.normalizedFactors p

If σ is a multiplicative automorphism of a normalization UFD and σ p is associated to p, then normalize ∘ σ permutes the multiset of normalized factors of p.

theorem pow_dvd_iff_le_factorization {R : Type u_1} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] [NormalizationMonoid R] [DecidableEq R] {p x : R} (hp : Prime p) (hpn : normalize p = p) (hx : x ≠ 0) {k : ℕ} : p ^ k ∣ x ↔ k ≤ (factorization x) p

p ^ k ∣ x iff k is at most the multiplicity of a normalized prime p in x ≠ 0.

theorem one_le_factorization_iff_dvd {R : Type u_1} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] [NormalizationMonoid R] [DecidableEq R] {p x : R} (hp : Prime p) (hpn : normalize p = p) (hx : x ≠ 0) : 1 ≤ (factorization x) p ↔ p ∣ x

A normalized prime p divides x ≠ 0 iff its multiplicity in x is positive.

theorem factorization_eq_zero_iff_not_dvd {R : Type u_1} [CommMonoidWithZero R] [UniqueFactorizationMonoid R] [NormalizationMonoid R] [DecidableEq R] {p x : R} (hp : Prime p) (hpn : normalize p = p) (hx : x ≠ 0) : (factorization x) p = 0 ↔ ¬p ∣ x

The multiplicity of a normalized prime p in x ≠ 0 vanishes iff p ∤ x.

theorem factorization_eq_of_dvd_sub {S : Type u_1} [CommRing S] [UniqueFactorizationMonoid S] [NormalizationMonoid S] [DecidableEq S] {p : S} (hp : Prime p) (hpn : normalize p = p) {x y : S} (hx : x ≠ 0) (hy : y ≠ 0) {E : ℕ} (hyE : (factorization y) p = E) (hcong : p ^ (E + 1) ∣ x - y) : (factorization x) p = E

The multiplicity at p is determined by the residue mod p ^ (E+1): if v_p y = E and p ^ (E+1) ∣ x - y, then v_p x = E.

theorem factorization_periodic_shape {S : Type u_1} [CommRing S] [UniqueFactorizationMonoid S] [NormalizationMonoid S] [DecidableEq S] {p : S} (hp : Prime p) (hpn : normalize p = p) (x : ℕ → S) (m E : ℕ) (hm : 2 ≤ m) (hne : ∀ n ≥ 1, x n ≠ 0) (hE : (factorization (x m)) p = E) (hmin : ∀ k < m, ¬(1 ≤ k ∧ p ∣ x k)) (hpm1 : ¬p ∣ x (m + 1)) (hper : ∀ n ≥ 2, p ^ (E + 1) ∣ x (n + m) - x n) (n : ℕ) : n ≥ 1 → (factorization (x n)) p = if m ∣ n then E else 0

If a sequence x in a UFD is nonzero on [1,∞), first p-divisible at index m ≥ 2 with p ∤ x (m+1), and periodic modulo p ^ (E+1) with period m from index 2 on (where E = v_p (x m)), then v_p (x n) = E when m ∣ n and 0 otherwise.