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} {p : } (h₁ : p 0) :
theorem DivisorChain.exists_chain_of_prime_pow {M : Type u_1} {p : } {n : } (hn : n 0) (hp : ) :
∃ (c : Fin (n + 1)), c 1 = p ∀ {r : }, 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} {n : } {i : Fin (n + 1)} (i_pos : i 0) {c : Fin (n + 1)} (h₁ : ) :
¬IsUnit (c i)
theorem DivisorChain.first_of_chain_isUnit {M : Type u_1} {q : } {n : } {c : Fin (n + 1)} (h₁ : ) (h₂ : ∀ {r : }, r q ∃ (i : Fin (n + 1)), r = c i) :
IsUnit (c 0)
theorem DivisorChain.second_of_chain_is_irreducible {M : Type u_1} {q : } {n : } (hn : n 0) {c : Fin (n + 1)} (h₁ : ) (h₂ : ∀ {r : }, r q ∃ (i : Fin (n + 1)), r = c i) (hq : q 0) :

The second element of a chain is irreducible.

theorem DivisorChain.eq_second_of_chain_of_prime_dvd {M : Type u_1} {p : } {q : } {r : } {n : } (hn : n 0) {c : Fin (n + 1)} (h₁ : ) (h₂ : ∀ {r : }, r q ∃ (i : Fin (n + 1)), r = c i) (hp : ) (hr : r q) (hp' : p r) :
p = c 1
theorem DivisorChain.card_subset_divisors_le_length_of_chain {M : Type u_1} {q : } {n : } {c : Fin (n + 1)} (h₂ : ∀ {r : }, r q ∃ (i : Fin (n + 1)), r = c i) {m : Finset ()} (hm : rm, r q) :
m.card n + 1
theorem DivisorChain.element_of_chain_eq_pow_second_of_chain {M : Type u_1} {q : } {r : } {n : } (hn : n 0) {c : Fin (n + 1)} (h₁ : ) (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 DivisorChain.eq_pow_second_of_chain_of_has_chain {M : Type u_1} {q : } {n : } (hn : n 0) {c : Fin (n + 1)} (h₁ : ) (h₂ : ∀ {r : }, 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} {q : } {n : } (hn : n 0) {c : Fin (n + 1)} (h₁ : ) (h₂ : ∀ {r : }, r q ∃ (i : Fin (n + 1)), r = c i) (hq : q 0) :
theorem factor_orderIso_map_one_eq_bot {M : Type u_1} {N : Type u_2} {m : } {n : } (d : { l : // l m } ≃o { l : // l n }) :
(d 1, ) = 1
theorem coe_factor_orderIso_map_eq_one_iff {M : Type u_1} {N : Type u_2} {m : } {u : } {n : } (hu' : u m) (d : () ≃o ()) :
(d u, hu') = 1 u = 1
theorem pow_image_of_prime_by_factor_orderIso_dvd {M : Type u_1} {N : Type u_2} {m : } {p : } {n : } (hn : n 0) (hp : ) (d : () ≃o ()) {s : } (hs' : p ^ s m) :
(d p, ) ^ s n
theorem map_prime_of_factor_orderIso {M : Type u_1} {N : Type u_2} {m : } {p : } {n : } (hn : n 0) (hp : ) (d : () ≃o ()) :
Prime (d p, )
theorem mem_normalizedFactors_factor_orderIso_of_mem_normalizedFactors {M : Type u_1} {N : Type u_2} {m : } {p : } {n : } (hn : n 0) (hp : ) (d : () ≃o ()) :
(d p, )
theorem multiplicity_prime_le_multiplicity_image_by_factor_orderIso {M : Type u_1} {N : Type u_2} [DecidableRel fun (x x_1 : M) => x x_1] [DecidableRel fun (x x_1 : N) => x x_1] {m : } {p : } {n : } (hp : ) (d : () ≃o ()) :
multiplicity ((d p, )) n
theorem multiplicity_prime_eq_multiplicity_image_by_factor_orderIso {M : Type u_1} {N : Type u_2} [DecidableRel fun (x x_1 : M) => x x_1] [DecidableRel fun (x x_1 : N) => x x_1] {m : } {p : } {n : } (hn : n 0) (hp : ) (d : () ≃o ()) :
= multiplicity ((d p, )) n
@[simp]
theorem mkFactorOrderIsoOfFactorDvdEquiv_apply_coe {M : Type u_1} {N : Type u_2} [] [] {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 : ()) :
() = Associates.mk (d associatesEquivOfUniqueUnits l, )
@[simp]
theorem mkFactorOrderIsoOfFactorDvdEquiv_symm_apply_coe {M : Type u_1} {N : Type u_2} [] [] {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 : ()) :
() = Associates.mk (d.symm associatesEquivOfUniqueUnits l, )
def mkFactorOrderIsoOfFactorDvdEquiv {M : Type u_1} {N : Type u_2} [] [] {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') :
() ≃o ()

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.
Instances For
theorem mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors {M : Type u_1} {N : Type u_2} [] [] {m : M} {p : M} {n : N} (hm : m 0) (hn : n 0) (hp : ) {d : { l : M // l m } { l : N // l n }} (hd : ∀ (l l' : { l : M // l m }), (d l) (d l') l l') :
(d p, )
theorem multiplicity_factor_dvd_iso_eq_multiplicity_of_mem_normalizedFactors {M : Type u_1} {N : Type u_2} [] [] [DecidableRel fun (x x_1 : M) => x x_1] [DecidableRel fun (x x_1 : N) => x x_1] {m : M} {p : M} {n : N} (hm : m 0) (hn : n 0) (hp : ) {d : { l : M // l m } { l : N // l n }} (hd : ∀ (l l' : { l : M // l m }), (d l) (d l') l l') :
multiplicity ((d p, )) n =