Multiplicative maps on unique factorization domains

Main results

• UniqueFactorizationMonoid.induction_on_coprime: if P holds for 0, units and powers of primes, and P x ∧ P y for coprime x, y implies P (x * y), then P holds on all a : α.
• UniqueFactorizationMonoid.multiplicative_of_coprime: if f maps p ^ i to (f p) ^ i for primes p, and f is multiplicative on coprime elements, then f is multiplicative everywhere.

theorem UniqueFactorizationMonoid.prime_pow_coprime_prod_of_coprime_insert {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] [DecidableEq α] {s : Finset α} (i : α → ℕ) (p : α) (hps : p ∉ s) (is_prime : ∀ q ∈ insert p s, Prime q) (is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q') : IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')

theorem UniqueFactorizationMonoid.induction_on_prime_power {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {P : α → Prop} (s : Finset α) (i : α → ℕ) (is_prime : ∀ p ∈ s, Prime p) (is_coprime : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q) (h1 : ∀ {x : α}, IsUnit x → P x) (hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)) (hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)) : P (∏ p ∈ s, p ^ i p)

If P holds for units and powers of primes, and P x ∧ P y for coprime x, y implies P (x * y), then P holds on a product of powers of distinct primes.

theorem UniqueFactorizationMonoid.induction_on_coprime {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {P : α → Prop} (a : α) (h0 : P 0) (h1 : ∀ {x : α}, IsUnit x → P x) (hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)) (hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)) : P a

If P holds for 0, units and powers of primes, and P x ∧ P y for coprime x, y implies P (x * y), then P holds on all a : α.

theorem UniqueFactorizationMonoid.multiplicative_prime_power {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {β : Type u_3} [CommMonoidWithZero β] {f : α → β} (s : Finset α) (i j : α → ℕ) (is_prime : ∀ p ∈ s, Prime p) (is_coprime : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q) (h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y) (hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i) (hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y) : f (∏ p ∈ s, p ^ (i p + j p)) = f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p)

If f maps p ^ i to (f p) ^ i for primes p, and f is multiplicative on coprime elements, then f is multiplicative on all products of primes.

theorem UniqueFactorizationMonoid.multiplicative_of_coprime {α : Type u_1} [CommMonoidWithZero α] [UniqueFactorizationMonoid α] {β : Type u_3} [CommMonoidWithZero β] (f : α → β) (a b : α) (h0 : f 0 = 0) (h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y) (hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i) (hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y) : f (a * b) = f a * f b

If f maps p ^ i to (f p) ^ i for primes p, and f is multiplicative on coprime elements, then f is multiplicative everywhere.