Documentation

Mathlib.RingTheory.ChainOfDivisors

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 #

Todo #

theorem DivisorChain.exists_chain_of_prime_pow {M : Type u_1} [CancelCommMonoidWithZero M] {p : Associates M} {n : } (hn : n 0) (hp : Prime p) :
c, c 1 = p StrictMono c ∀ {r : Associates M}, r p ^ n i, r = c i
theorem DivisorChain.element_of_chain_not_isUnit_of_index_ne_zero {M : Type u_1} [CancelCommMonoidWithZero 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} [CancelCommMonoidWithZero M] {q : Associates M} {n : } {c : Fin (n + 1)Associates M} (h₁ : StrictMono c) (h₂ : ∀ {r : Associates M}, r q i, r = c i) :
IsUnit (c 0)
theorem DivisorChain.second_of_chain_is_irreducible {M : Type u_1} [CancelCommMonoidWithZero M] {q : Associates M} {n : } (hn : n 0) {c : Fin (n + 1)Associates M} (h₁ : StrictMono c) (h₂ : ∀ {r : Associates M}, r q i, 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} [CancelCommMonoidWithZero M] {p : Associates M} {q : Associates M} {r : Associates M} {n : } (hn : n 0) {c : Fin (n + 1)Associates M} (h₁ : StrictMono c) (h₂ : ∀ {r : Associates M}, r q i, 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} [CancelCommMonoidWithZero M] {q : Associates M} {n : } {c : Fin (n + 1)Associates M} (h₂ : ∀ {r : Associates M}, r q i, r = c i) {m : Finset (Associates M)} (hm : ∀ (r : Associates M), r mr q) :
theorem DivisorChain.element_of_chain_eq_pow_second_of_chain {M : Type u_1} [CancelCommMonoidWithZero M] [UniqueFactorizationMonoid M] {q : Associates M} {r : Associates M} {n : } (hn : n 0) {c : Fin (n + 1)Associates M} (h₁ : StrictMono c) (h₂ : ∀ {r : Associates M}, r q i, r = c i) (hr : r q) (hq : q 0) :
i, r = c 1 ^ i
theorem DivisorChain.eq_pow_second_of_chain_of_has_chain {M : Type u_1} [CancelCommMonoidWithZero 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, r = c i) (hq : q 0) :
q = c 1 ^ n
theorem DivisorChain.isPrimePow_of_has_chain {M : Type u_1} [CancelCommMonoidWithZero 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, r = c i) (hq : q 0) :
theorem factor_orderIso_map_one_eq_bot {M : Type u_1} [CancelCommMonoidWithZero M] {N : Type u_2} [CancelCommMonoidWithZero N] {m : Associates M} {n : Associates N} (d : { l // l m } ≃o { l // l n }) :
↑(d { val := 1, property := (_ : 1 m) }) = 1
theorem coe_factor_orderIso_map_eq_one_iff {M : Type u_1} [CancelCommMonoidWithZero M] {N : Type u_2} [CancelCommMonoidWithZero N] {m : Associates M} {u : Associates M} {n : Associates N} (hu' : u m) (d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)) :
↑(d { val := u, property := hu' }) = 1 u = 1
theorem pow_image_of_prime_by_factor_orderIso_dvd {M : Type u_1} [CancelCommMonoidWithZero M] {N : Type u_2} [CancelCommMonoidWithZero N] [UniqueFactorizationMonoid N] [UniqueFactorizationMonoid M] [DecidableEq (Associates M)] {m : Associates 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 { val := p, property := (_ : p m) }) ^ s n
theorem map_prime_of_factor_orderIso {M : Type u_1} [CancelCommMonoidWithZero M] {N : Type u_2} [CancelCommMonoidWithZero N] [UniqueFactorizationMonoid N] [UniqueFactorizationMonoid M] [DecidableEq (Associates M)] {m : Associates 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 { val := p, property := (_ : p m) })
theorem multiplicity_prime_eq_multiplicity_image_by_factor_orderIso {M : Type u_1} [CancelCommMonoidWithZero M] {N : Type u_2} [CancelCommMonoidWithZero N] [UniqueFactorizationMonoid N] [UniqueFactorizationMonoid M] [DecidableRel fun x x_1 => x x_1] [DecidableRel fun x x_1 => x x_1] [DecidableEq (Associates M)] {m : Associates M} {p : Associates M} {n : Associates N} (hn : n 0) (hp : p UniqueFactorizationMonoid.normalizedFactors m) (d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)) :
multiplicity p m = multiplicity (↑(d { val := p, property := (_ : p m) })) n
@[simp]
theorem mkFactorOrderIsoOfFactorDvdEquiv_apply_coe {M : Type u_1} [CancelCommMonoidWithZero M] {N : Type u_2} [CancelCommMonoidWithZero 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))) :
↑(↑(mkFactorOrderIsoOfFactorDvdEquiv hd) l) = Associates.mk ↑(d { val := associatesEquivOfUniqueUnits l, property := (_ : associatesEquivOfUniqueUnits l m) })
@[simp]
theorem mkFactorOrderIsoOfFactorDvdEquiv_symm_apply_coe {M : Type u_1} [CancelCommMonoidWithZero M] {N : Type u_2} [CancelCommMonoidWithZero 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))) :
↑(↑(RelIso.symm (mkFactorOrderIsoOfFactorDvdEquiv hd)) l) = Associates.mk ↑(d.symm { val := associatesEquivOfUniqueUnits l, property := (_ : associatesEquivOfUniqueUnits l n) })
def mkFactorOrderIsoOfFactorDvdEquiv {M : Type u_1} [CancelCommMonoidWithZero M] {N : Type u_2} [CancelCommMonoidWithZero 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') :

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 .

Instances For
    theorem mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors {M : Type u_1} [CancelCommMonoidWithZero M] {N : Type u_2} [CancelCommMonoidWithZero N] [Unique Mˣ] [Unique Nˣ] [UniqueFactorizationMonoid M] [UniqueFactorizationMonoid N] [DecidableEq M] [DecidableEq N] {m : M} {p : M} {n : N} (hm : m 0) (hn : n 0) (hp : p UniqueFactorizationMonoid.normalizedFactors m) {d : { l // l m } { l // l n }} (hd : ∀ (l l' : { l // l m }), ↑(d l) ↑(d l') l l') :
    ↑(d { val := p, property := (_ : p m) }) UniqueFactorizationMonoid.normalizedFactors n
    theorem multiplicity_factor_dvd_iso_eq_multiplicity_of_mem_normalizedFactors {M : Type u_1} [CancelCommMonoidWithZero M] {N : Type u_2} [CancelCommMonoidWithZero N] [Unique Mˣ] [Unique Nˣ] [UniqueFactorizationMonoid M] [UniqueFactorizationMonoid N] [DecidableEq M] [DecidableRel fun x x_1 => x x_1] [DecidableRel fun x x_1 => x x_1] {m : M} {p : M} {n : N} (hm : m 0) (hn : n 0) (hp : p UniqueFactorizationMonoid.normalizedFactors m) {d : { l // l m } { l // l n }} (hd : ∀ (l l' : { l // l m }), ↑(d l) ↑(d l') l l') :
    multiplicity (↑(d { val := p, property := (_ : p m) })) n = multiplicity p m