mathlib3 documentation

ring_theory.chain_of_divisors

Chains of divisors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 associates.is_atom_iff {M : Type u_1} [cancel_comm_monoid_with_zero M] {p : associates M} (h₁ : p ≠ 0) :

is_atom p ↔ irreducible p

theorem divisor_chain.exists_chain_of_prime_pow {M : Type u_1} [cancel_comm_monoid_with_zero M] {p : associates M} {n : ℕ} (hn : n ≠ 0) (hp : prime p) :

∃ (c : fin (n + 1) → associates M), c 1 = p ∧ strict_mono c ∧ ∀ {r : associates M}, 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} [cancel_comm_monoid_with_zero M] {n : ℕ} {i : fin (n + 1)} (i_pos : i ≠ 0) {c : fin (n + 1) → associates M} (h₁ : strict_mono c) :

¬is_unit (c i)

theorem divisor_chain.first_of_chain_is_unit {M : Type u_1} [cancel_comm_monoid_with_zero M] {q : associates M} {n : ℕ} {c : fin (n + 1) → associates M} (h₁ : strict_mono c) (h₂ : ∀ {r : associates M}, r ≤ q ↔ ∃ (i : fin (n + 1)), r = c i) :

theorem divisor_chain.second_of_chain_is_irreducible {M : Type u_1} [cancel_comm_monoid_with_zero M] {q : associates M} {n : ℕ} (hn : n ≠ 0) {c : fin (n + 1) → associates M} (h₁ : strict_mono 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 divisor_chain.eq_second_of_chain_of_prime_dvd {M : Type u_1} [cancel_comm_monoid_with_zero M] {p q r : associates M} {n : ℕ} (hn : n ≠ 0) {c : fin (n + 1) → associates M} (h₁ : strict_mono 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 divisor_chain.card_subset_divisors_le_length_of_chain {M : Type u_1} [cancel_comm_monoid_with_zero 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 : associates M), r ∈ m → r ≤ q) :

m.card ≤ n + 1

theorem divisor_chain.element_of_chain_eq_pow_second_of_chain {M : Type u_1} [cancel_comm_monoid_with_zero M] [unique_factorization_monoid M] {q r : associates M} {n : ℕ} (hn : n ≠ 0) {c : fin (n + 1) → associates M} (h₁ : strict_mono 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 divisor_chain.eq_pow_second_of_chain_of_has_chain {M : Type u_1} [cancel_comm_monoid_with_zero M] [unique_factorization_monoid M] {q : associates M} {n : ℕ} (hn : n ≠ 0) {c : fin (n + 1) → associates M} (h₁ : strict_mono c) (h₂ : ∀ {r : associates M}, 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} [cancel_comm_monoid_with_zero M] [unique_factorization_monoid M] {q : associates M} {n : ℕ} (hn : n ≠ 0) {c : fin (n + 1) → associates M} (h₁ : strict_mono c) (h₂ : ∀ {r : associates M}, r ≤ q ↔ ∃ (i : fin (n + 1)), r = c i) (hq : q ≠ 0) :

theorem factor_order_iso_map_one_eq_bot {M : Type u_1} [cancel_comm_monoid_with_zero M] {N : Type u_2} [cancel_comm_monoid_with_zero N] {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} [cancel_comm_monoid_with_zero M] {N : Type u_2} [cancel_comm_monoid_with_zero 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_order_iso_dvd {M : Type u_1} [cancel_comm_monoid_with_zero M] {N : Type u_2} [cancel_comm_monoid_with_zero N] [unique_factorization_monoid N] [unique_factorization_monoid M] [decidable_eq (associates M)] {m p : associates M} {n : associates N} (hn : n ≠ 0) (hp : p ∈ unique_factorization_monoid.normalized_factors m) (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} [cancel_comm_monoid_with_zero M] {N : Type u_2} [cancel_comm_monoid_with_zero N] [unique_factorization_monoid N] [unique_factorization_monoid M] [decidable_eq (associates M)] {m p : associates M} {n : associates N} (hn : n ≠ 0) (hp : p ∈ unique_factorization_monoid.normalized_factors m) (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} [cancel_comm_monoid_with_zero M] {N : Type u_2} [cancel_comm_monoid_with_zero N] [unique_factorization_monoid N] [unique_factorization_monoid M] [decidable_eq (associates M)] [decidable_eq (associates N)] {m p : associates M} {n : associates N} (hn : n ≠ 0) (hp : p ∈ unique_factorization_monoid.normalized_factors m) (d : ↥(set.Iic m) ≃o ↥(set.Iic n)) :

↑(⇑d ⟨p, _⟩) ∈ unique_factorization_monoid.normalized_factors n

theorem multiplicity_prime_le_multiplicity_image_by_factor_order_iso {M : Type u_1} [cancel_comm_monoid_with_zero M] {N : Type u_2} [cancel_comm_monoid_with_zero N] [unique_factorization_monoid N] [unique_factorization_monoid M] [decidable_rel has_dvd.dvd] [decidable_rel has_dvd.dvd] [decidable_eq (associates M)] {m p : associates M} {n : associates N} (hp : p ∈ unique_factorization_monoid.normalized_factors m) (d : ↥(set.Iic m) ≃o ↥(set.Iic n)) :

multiplicity p m ≤ multiplicity ↑(⇑d ⟨p, _⟩) n

theorem multiplicity_prime_eq_multiplicity_image_by_factor_order_iso {M : Type u_1} [cancel_comm_monoid_with_zero M] {N : Type u_2} [cancel_comm_monoid_with_zero N] [unique_factorization_monoid N] [unique_factorization_monoid M] [decidable_rel has_dvd.dvd] [decidable_rel has_dvd.dvd] [decidable_eq (associates M)] {m p : associates M} {n : associates N} (hn : n ≠ 0) (hp : p ∈ unique_factorization_monoid.normalized_factors m) (d : ↥(set.Iic m) ≃o ↥(set.Iic n)) :

multiplicity p m = multiplicity ↑(⇑d ⟨p, _⟩) n

def mk_factor_order_iso_of_factor_dvd_equiv {M : Type u_1} [cancel_comm_monoid_with_zero M] {N : Type u_2} [cancel_comm_monoid_with_zero N] [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') :

↥(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

mk_factor_order_iso_of_factor_dvd_equiv hd = {to_equiv := {to_fun := λ (l : ↥(set.Iic (associates.mk m))), ⟨associates.mk ↑(⇑d ⟨⇑associates_equiv_of_unique_units ↑l, _⟩), _⟩, inv_fun := λ (l : ↥(set.Iic (associates.mk n))), ⟨associates.mk ↑(⇑(d.symm) ⟨⇑associates_equiv_of_unique_units ↑l, _⟩), _⟩, left_inv := _, right_inv := _}, map_rel_iff' := _}

@[simp]

theorem mk_factor_order_iso_of_factor_dvd_equiv_apply_coe {M : Type u_1} [cancel_comm_monoid_with_zero M] {N : Type u_2} [cancel_comm_monoid_with_zero N] [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))) :

↑(⇑(mk_factor_order_iso_of_factor_dvd_equiv hd) l) = associates.mk ↑(⇑d ⟨⇑associates_equiv_of_unique_units ↑l, _⟩)

@[simp]

theorem mk_factor_order_iso_of_factor_dvd_equiv_symm_apply_coe {M : Type u_1} [cancel_comm_monoid_with_zero M] {N : Type u_2} [cancel_comm_monoid_with_zero N] [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))) :

↑(⇑(rel_iso.symm (mk_factor_order_iso_of_factor_dvd_equiv hd)) l) = associates.mk ↑(⇑(d.symm) ⟨⇑associates_equiv_of_unique_units ↑l, _⟩)

theorem mem_normalized_factors_factor_dvd_iso_of_mem_normalized_factors {M : Type u_1} [cancel_comm_monoid_with_zero M] {N : Type u_2} [cancel_comm_monoid_with_zero N] [unique Mˣ] [unique Nˣ] [unique_factorization_monoid M] [unique_factorization_monoid N] [decidable_eq M] [decidable_eq N] {m p : M} {n : N} (hm : m ≠ 0) (hn : n ≠ 0) (hp : p ∈ unique_factorization_monoid.normalized_factors m) {d : {l // l ∣ m} ≃ {l // l ∣ n}} (hd : ∀ (l l' : {l // l ∣ m}), ↑(⇑d l) ∣ ↑(⇑d l') ↔ ↑l ∣ ↑l') :

↑(⇑d ⟨p, _⟩) ∈ unique_factorization_monoid.normalized_factors n

theorem multiplicity_factor_dvd_iso_eq_multiplicity_of_mem_normalized_factor {M : Type u_1} [cancel_comm_monoid_with_zero M] {N : Type u_2} [cancel_comm_monoid_with_zero N] [unique Mˣ] [unique Nˣ] [unique_factorization_monoid M] [unique_factorization_monoid N] [decidable_eq M] [decidable_rel has_dvd.dvd] [decidable_rel has_dvd.dvd] {m p : M} {n : N} (hm : m ≠ 0) (hn : n ≠ 0) (hp : p ∈ unique_factorization_monoid.normalized_factors m) {d : {l // l ∣ m} ≃ {l // l ∣ n}} (hd : ∀ (l l' : {l // l ∣ m}), ↑(⇑d l) ∣ ↑(⇑d l') ↔ ↑l ∣ ↑l') :

multiplicity ↑(⇑d ⟨p, _⟩) n = multiplicity p m