Chains of divisors

The results in this file show that in the monoid Associates M of a UniqueFactorizationMonoid M, an element a is an n-th prime power iff its set of divisors is a strictly increasing chain of length n + 1, meaning that we can find a strictly increasing bijection between Fin (n + 1) and the set of factors of a.

Main results

• DivisorChain.exists_chain_of_prime_pow : existence of a chain for prime powers.
• DivisorChain.is_prime_pow_of_has_chain : elements that have a chain are prime powers.
• multiplicity_prime_eq_multiplicity_image_by_factor_orderIso : if there is a monotone bijection d between the set of factors of a : Associates M and the set of factors of b : Associates N then for any prime p ∣ a, multiplicity p a = multiplicity (d p) b.
• multiplicity_eq_multiplicity_factor_dvd_iso_of_mem_normalizedFactors : if there is a bijection between the set of factors of a : M and b : N then for any prime p ∣ a, multiplicity p a = multiplicity (d p) b

TODO

• Create a structure for chains of divisors.
• Simplify proof of mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors using mem_normalizedFactors_factor_order_iso_of_mem_normalizedFactors or vice versa.

theorem Associates.isAtom_iff {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {p : Associates M} (h₁ : p ≠ 0) : IsAtom p ↔ Irreducible p

theorem DivisorChain.exists_chain_of_prime_pow {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {p : Associates M} {n : ℕ} (hn : n ≠ 0) (hp : Prime p) : ∃ (c : Fin (n + 1) → Associates M), c 1 = p ∧ StrictMono c ∧ ∀ {r : Associates M}, r ≤ p ^ n ↔ ∃ (i : Fin (n + 1)), r = c i

theorem DivisorChain.element_of_chain_not_isUnit_of_index_ne_zero {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {n : ℕ} {i : Fin (n + 1)} (i_pos : i ≠ 0) {c : Fin (n + 1) → Associates M} (h₁ : StrictMono c) : ¬IsUnit (c i)

theorem DivisorChain.first_of_chain_isUnit {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {q : Associates M} {n : ℕ} {c : Fin (n + 1) → Associates M} (h₁ : StrictMono c) (h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i) : IsUnit (c 0)

theorem DivisorChain.second_of_chain_is_irreducible {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {q : Associates M} {n : ℕ} (hn : n ≠ 0) {c : Fin (n + 1) → Associates M} (h₁ : StrictMono c) (h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i) (hq : q ≠ 0) : Irreducible (c 1)

The second element of a chain is irreducible.

theorem DivisorChain.eq_second_of_chain_of_prime_dvd {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {p q r : Associates M} {n : ℕ} (hn : n ≠ 0) {c : Fin (n + 1) → Associates M} (h₁ : StrictMono c) (h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i) (hp : Prime p) (hr : r ∣ q) (hp' : p ∣ r) : p = c 1

theorem DivisorChain.card_subset_divisors_le_length_of_chain {M : Type u_1} [CommMonoidWithZero M] {q : Associates M} {n : ℕ} {c : Fin (n + 1) → Associates M} (h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i) {m : Finset (Associates M)} (hm : ∀ r ∈ m, r ≤ q) : m.card ≤ n + 1

theorem DivisorChain.element_of_chain_eq_pow_second_of_chain {M : Type u_1} [CommMonoidWithZero M] [UniqueFactorizationMonoid M] {q r : Associates M} {n : ℕ} (hn : n ≠ 0) {c : Fin (n + 1) → Associates M} (h₁ : StrictMono c) (h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i) (hr : r ∣ q) (hq : q ≠ 0) : ∃ (i : Fin (n + 1)), r = c 1 ^ ↑i

theorem DivisorChain.eq_pow_second_of_chain_of_has_chain {M : Type u_1} [CommMonoidWithZero M] [UniqueFactorizationMonoid M] {q : Associates M} {n : ℕ} (hn : n ≠ 0) {c : Fin (n + 1) → Associates M} (h₁ : StrictMono c) (h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i) (hq : q ≠ 0) : q = c 1 ^ n

theorem DivisorChain.isPrimePow_of_has_chain {M : Type u_1} [CommMonoidWithZero M] [UniqueFactorizationMonoid M] {q : Associates M} {n : ℕ} (hn : n ≠ 0) {c : Fin (n + 1) → Associates M} (h₁ : StrictMono c) (h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ (i : Fin (n + 1)), r = c i) (hq : q ≠ 0) : IsPrimePow q

theorem factor_orderIso_map_one_eq_bot {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [CommMonoidWithZero N] [IsCancelMulZero N] {m : Associates M} {n : Associates N} (d : { l : Associates M // l ≤ m } ≃o { l : Associates N // l ≤ n }) : ↑(d ⟨1, ⋯⟩) = 1

theorem coe_factor_orderIso_map_eq_one_iff {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [CommMonoidWithZero N] [IsCancelMulZero N] {m u : Associates M} {n : Associates N} (hu' : u ≤ m) (d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)) : ↑(d ⟨u, hu'⟩) = 1 ↔ u = 1

theorem pow_image_of_prime_by_factor_orderIso_dvd {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [CommMonoidWithZero N] [UniqueFactorizationMonoid N] [UniqueFactorizationMonoid M] {m p : Associates M} {n : Associates N} (hn : n ≠ 0) (hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m) (d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)) {s : ℕ} (hs' : p ^ s ≤ m) : ↑(d ⟨p, ⋯⟩) ^ s ≤ n

theorem map_prime_of_factor_orderIso {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [CommMonoidWithZero N] [UniqueFactorizationMonoid N] [UniqueFactorizationMonoid M] {m p : Associates M} {n : Associates N} (hn : n ≠ 0) (hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m) (d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)) : Prime ↑(d ⟨p, ⋯⟩)

theorem mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [CommMonoidWithZero N] [UniqueFactorizationMonoid N] [UniqueFactorizationMonoid M] {m p : Associates M} {n : Associates N} (hn : n ≠ 0) (hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m) (d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)) : ↑(d ⟨p, ⋯⟩) ∈ UniqueFactorizationMonoid.normalizedFactors n

theorem emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [CommMonoidWithZero N] [UniqueFactorizationMonoid N] [UniqueFactorizationMonoid M] {m p : Associates M} {n : Associates N} (hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m) (d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)) : emultiplicity p m ≤ emultiplicity (↑(d ⟨p, ⋯⟩)) n

theorem emultiplicity_prime_eq_emultiplicity_image_by_factor_orderIso {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [CommMonoidWithZero N] [UniqueFactorizationMonoid N] [UniqueFactorizationMonoid M] {m p : Associates M} {n : Associates N} (hn : n ≠ 0) (hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m) (d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)) : emultiplicity p m = emultiplicity (↑(d ⟨p, ⋯⟩)) n

def mkFactorOrderIsoOfFactorDvdEquiv {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [CommMonoidWithZero N] [Subsingleton Mˣ] [Subsingleton Nˣ] [IsCancelMulZero N] {m : M} {n : N} {d : { l : M // l ∣ m } ≃ { l : N // l ∣ n }} (hd : ∀ (l l' : { l : M // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l') : ↑(Set.Iic (Associates.mk m)) ≃o ↑(Set.Iic (Associates.mk n))

The order isomorphism between the factors of mk m and the factors of mk n induced by a bijection between the factors of m and the factors of n that preserves ∣.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem mkFactorOrderIsoOfFactorDvdEquiv_apply_coe {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [CommMonoidWithZero N] [Subsingleton Mˣ] [Subsingleton Nˣ] [IsCancelMulZero N] {m : M} {n : N} {d : { l : M // l ∣ m } ≃ { l : N // l ∣ n }} (hd : ∀ (l l' : { l : M // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l') (l : ↑(Set.Iic (Associates.mk m))) : ↑((mkFactorOrderIsoOfFactorDvdEquiv hd) l) = Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩)

@[simp]

theorem mkFactorOrderIsoOfFactorDvdEquiv_symm_apply_coe {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [CommMonoidWithZero N] [Subsingleton Mˣ] [Subsingleton Nˣ] [IsCancelMulZero N] {m : M} {n : N} {d : { l : M // l ∣ m } ≃ { l : N // l ∣ n }} (hd : ∀ (l l' : { l : M // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l') (l : ↑(Set.Iic (Associates.mk n))) : ↑((RelIso.symm (mkFactorOrderIsoOfFactorDvdEquiv hd)) l) = Associates.mk ↑(d.symm ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩)

theorem mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [CommMonoidWithZero N] [Subsingleton Mˣ] [Subsingleton Nˣ] [UniqueFactorizationMonoid M] [UniqueFactorizationMonoid N] {m p : M} {n : N} (hm : m ≠ 0) (hn : n ≠ 0) (hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m) {d : { l : M // l ∣ m } ≃ { l : N // l ∣ n }} (hd : ∀ (l l' : { l : M // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l') : ↑(d ⟨p, ⋯⟩) ∈ UniqueFactorizationMonoid.normalizedFactors n

theorem emultiplicity_factor_dvd_iso_eq_emultiplicity_of_mem_normalizedFactors {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [CommMonoidWithZero N] [Subsingleton Mˣ] [Subsingleton Nˣ] [UniqueFactorizationMonoid M] [UniqueFactorizationMonoid N] {m p : M} {n : N} (hm : m ≠ 0) (hn : n ≠ 0) (hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m) {d : { l : M // l ∣ m } ≃ { l : N // l ∣ n }} (hd : ∀ (l l' : { l : M // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l') : emultiplicity (↑(d ⟨p, ⋯⟩)) n = emultiplicity p m