# mathlibdocumentation

ring_theory.chain_of_divisors

# Chains of divisors #

The results in this file show that in the monoid associates M of a unique_factorization_monoid 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 #

• divisor_chain.exists_chain_of_prime_pow : existence of a chain for prime powers.
• divisor_chain.is_prime_pow_of_has_chain : elements that have a chain are prime powers.
• multiplicity_prime_eq_multiplicity_image_by_factor_order_iso : 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_normalized_factor : 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_normalized_factors_factor_dvd_iso_of_mem_normalized_factors using mem_normalized_factors_factor_order_iso_of_mem_normalized_factors or vice versa.
theorem divisor_chain.exists_chain_of_prime_pow {M : Type u_1} {p : associates M} {n : } (hn : n 0) (hp : prime p) :
∃ (c : fin (n + 1), c 1 = p ∀ {r : , r p ^ n ∃ (i : fin (n + 1)), r = c i
theorem divisor_chain.element_of_chain_not_is_unit_of_index_ne_zero {M : Type u_1} {n : } {i : fin (n + 1)} (i_pos : i 0) {c : fin (n + 1)} (h₁ : strict_mono c) :
¬is_unit (c i)
theorem divisor_chain.first_of_chain_is_unit {M : Type u_1} {q : associates M} {n : } {c : fin (n + 1)} (h₁ : strict_mono c) (h₂ : ∀ {r : , r q ∃ (i : fin (n + 1)), r = c i) :
is_unit (c 0)
theorem divisor_chain.second_of_chain_is_irreducible {M : Type u_1} {q : associates M} {n : } (hn : n 0) {c : fin (n + 1)} (h₁ : strict_mono c) (h₂ : ∀ {r : , r q ∃ (i : fin (n + 1)), r = c i) (hq : q 0) :

The second element of a chain is irreducible.

theorem divisor_chain.eq_second_of_chain_of_prime_dvd {M : Type u_1} {p q r : associates M} {n : } (hn : n 0) {c : fin (n + 1)} (h₁ : strict_mono c) (h₂ : ∀ {r : , r q ∃ (i : fin (n + 1)), r = c i) (hp : prime p) (hr : r q) (hp' : p r) :
p = c 1
theorem divisor_chain.card_subset_divisors_le_length_of_chain {M : Type u_1} {q : associates M} {n : } {c : fin (n + 1)} (h₂ : ∀ {r : , r q ∃ (i : fin (n + 1)), r = c i) {m : finset (associates M)} (hm : ∀ (r : , r mr q) :
m.card n + 1
theorem divisor_chain.element_of_chain_eq_pow_second_of_chain {M : Type u_1} {q r : associates M} {n : } (hn : n 0) {c : fin (n + 1)} (h₁ : strict_mono c) (h₂ : ∀ {r : , r q ∃ (i : fin (n + 1)), r = c i) (hr : r q) (hq : q 0) :
∃ (i : fin (n + 1)), r = c 1 ^ i
theorem divisor_chain.eq_pow_second_of_chain_of_has_chain {M : Type u_1} {q : associates M} {n : } (hn : n 0) {c : fin (n + 1)} (h₁ : strict_mono c) (h₂ : ∀ {r : , r q ∃ (i : fin (n + 1)), r = c i) (hq : q 0) :
q = c 1 ^ n
theorem divisor_chain.is_prime_pow_of_has_chain {M : Type u_1} {q : associates M} {n : } (hn : n 0) {c : fin (n + 1)} (h₁ : strict_mono c) (h₂ : ∀ {r : , r q ∃ (i : fin (n + 1)), r = c i) (hq : q 0) :
theorem factor_order_iso_map_one_eq_bot {M : Type u_1} {N : Type u_2} {m : associates M} {n : associates N} (d : {l // l m} ≃o {l // l n}) :
(d 1, _⟩) = 1
theorem coe_factor_order_iso_map_eq_one_iff {M : Type u_1} {N : Type u_2} {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_order_iso_dvd {M : Type u_1} {N : Type u_2} [decidable_eq (associates M)] {m p : associates M} {n : associates N} (hn : n 0) (d : (set.Iic m) ≃o (set.Iic n)) {s : } (hs' : p ^ s m) :
(d p, _⟩) ^ s n
theorem map_prime_of_factor_order_iso {M : Type u_1} {N : Type u_2} [decidable_eq (associates M)] {m p : associates M} {n : associates N} (hn : n 0) (d : (set.Iic m) ≃o (set.Iic n)) :
prime (d p, _⟩)
theorem mem_normalized_factors_factor_order_iso_of_mem_normalized_factors {M : Type u_1} {N : Type u_2} [decidable_eq (associates M)] [decidable_eq (associates N)] {m p : associates M} {n : associates N} (hn : n 0) (d : (set.Iic m) ≃o (set.Iic n)) :
theorem multiplicity_prime_le_multiplicity_image_by_factor_order_iso {M : Type u_1} {N : Type u_2} [decidable_eq (associates M)] {m p : associates M} {n : associates N} (d : (set.Iic m) ≃o (set.Iic n)) :
m multiplicity (d p, _⟩) n
theorem multiplicity_prime_eq_multiplicity_image_by_factor_order_iso {M : Type u_1} {N : Type u_2} [decidable_eq (associates M)] {m p : associates M} {n : associates N} (hn : n 0) (d : (set.Iic m) ≃o (set.Iic n)) :
m = multiplicity (d p, _⟩) n
def mk_factor_order_iso_of_factor_dvd_equiv {M : Type u_1} {N : Type u_2} [unique Mˣ] [unique Nˣ] {m : M} {n : N} {d : {l // l m} {l // l n}} (hd : ∀ (l l' : {l // l m}), (d l) (d l') l l') :

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
@[simp]
theorem mk_factor_order_iso_of_factor_dvd_equiv_apply_coe {M : Type u_1} {N : Type u_2} [unique Mˣ] [unique Nˣ] {m : M} {n : N} {d : {l // l m} {l // l n}} (hd : ∀ (l l' : {l // l m}), (d l) (d l') l l') (l : (set.Iic (associates.mk m))) :
@[simp]
theorem mk_factor_order_iso_of_factor_dvd_equiv_symm_apply_coe {M : Type u_1} {N : Type u_2} [unique Mˣ] [unique Nˣ] {m : M} {n : N} {d : {l // l m} {l // l n}} (hd : ∀ (l l' : {l // l m}), (d l) (d l') l l') (l : (set.Iic (associates.mk n))) :
theorem mem_normalized_factors_factor_dvd_iso_of_mem_normalized_factors {M : Type u_1} {N : Type u_2} [unique Mˣ] [unique Nˣ] [decidable_eq M] [decidable_eq N] {m p : M} {n : N} (hm : m 0) (hn : n 0) {d : {l // l m} {l // l n}} (hd : ∀ (l l' : {l // l m}), (d l) (d l') l l') :
theorem multiplicity_factor_dvd_iso_eq_multiplicity_of_mem_normalized_factor {M : Type u_1} {N : Type u_2} [unique Mˣ] [unique Nˣ] [decidable_eq M] {m p : M} {n : N} (hm : m 0) (hn : n 0) {d : {l // l m} {l // l n}} (hd : ∀ (l l' : {l // l m}), (d l) (d l') l l') :
multiplicity (d p, _⟩) n = m