Radical of an element of a unique factorization normalization monoid

This file defines a radical of an element a of a unique factorization normalization monoid, which is defined as a product of normalized prime factors of a without duplication. This is different from the radical of an ideal.

Main declarations

• radical: The radical of an element a in a unique factorization monoid is the product of its prime factors.
• radical_eq_of_associated: If a and b are associates, i.e. a * u = b for some unit u, then radical a = radical b.
• radical_unit_mul: Multiplying unit does not change the radical.
• radical_dvd_self: radical a divides a.
• radical_pow: radical (a ^ n) = radical a for any n ≥ 1
• radical_of_prime: Radical of a prime element is equal to its normalization
• radical_pow_of_prime: Radical of a power of prime element is equal to its normalization

For unique factorization domains

• radical_mul: Radical is multiplicative for coprime elements.

For Euclidean domains

• EuclideanDomain.divRadical: For an element a in an Euclidean domain, a / radical a.
• EuclideanDomain.divRadical_mul: divRadical of a product is the product of divRadicals.
• IsCoprime.divRadical: divRadical of coprime elements are coprime.

TODO

• Make a comparison with Ideal.radical. Especially, for principal ideal, Ideal.radical (Ideal.span {a}) = Ideal.span {radical a}.
• Prove radical (radical a) = radical a.
• Prove a comparison between primeFactors and Nat.primeFactors.

def UniqueFactorizationMonoid.primeFactors {M : Type u_1} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] (a : M) : Finset M

The finite set of prime factors of an element in a unique factorization monoid.

Equations

• UniqueFactorizationMonoid.primeFactors a = (UniqueFactorizationMonoid.normalizedFactors a).toFinset

theorem Associated.primeFactors_eq {M : Type u_1} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} (h : Associated a b) : UniqueFactorizationMonoid.primeFactors a = UniqueFactorizationMonoid.primeFactors b

def UniqueFactorizationMonoid.radical {M : Type u_1} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] (a : M) : M

Radical of an element a in a unique factorization monoid is the product of the prime factors of a.

Equations

• UniqueFactorizationMonoid.radical a = (UniqueFactorizationMonoid.primeFactors a).prod id

@[simp]

theorem UniqueFactorizationMonoid.radical_zero_eq {M : Type u_1} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] : radical 0 = 1

@[simp]

theorem UniqueFactorizationMonoid.radical_one_eq {M : Type u_1} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] : radical 1 = 1

theorem UniqueFactorizationMonoid.radical_eq_of_associated {M : Type u_1} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a b : M} (h : Associated a b) : radical a = radical b

theorem UniqueFactorizationMonoid.radical_of_isUnit {M : Type u_1} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} (h : IsUnit a) : radical a = 1

theorem UniqueFactorizationMonoid.radical_mul_of_isUnit_left {M : Type u_1} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a u : M} (h : IsUnit u) : radical (u * a) = radical a

theorem UniqueFactorizationMonoid.radical_mul_of_isUnit_right {M : Type u_1} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a u : M} (h : IsUnit u) : radical (a * u) = radical a

theorem UniqueFactorizationMonoid.primeFactors_pow {M : Type u_1} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] (a : M) {n : ℕ} (hn : 0 < n) : primeFactors (a ^ n) = primeFactors a

theorem UniqueFactorizationMonoid.radical_pow {M : Type u_1} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] (a : M) {n : ℕ} (hn : 0 < n) : radical (a ^ n) = radical a

theorem UniqueFactorizationMonoid.radical_dvd_self {M : Type u_1} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] (a : M) : radical a ∣ a

theorem UniqueFactorizationMonoid.radical_of_prime {M : Type u_1} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} (ha : Prime a) : radical a = normalize a

theorem UniqueFactorizationMonoid.radical_pow_of_prime {M : Type u_1} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} (ha : Prime a) {n : ℕ} (hn : 0 < n) : radical (a ^ n) = normalize a

theorem UniqueFactorizationMonoid.radical_ne_zero {M : Type u_1} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] (a : M) [Nontrivial M] : radical a ≠ 0

theorem UniqueFactorizationDomain.disjoint_normalizedFactors {R : Type u_1} [CommRing R] [IsDomain R] [NormalizationMonoid R] [UniqueFactorizationMonoid R] {a b : R} (hc : IsCoprime a b) : Disjoint (UniqueFactorizationMonoid.normalizedFactors a) (UniqueFactorizationMonoid.normalizedFactors b)

Coprime elements have disjoint prime factors (as multisets).

theorem UniqueFactorizationDomain.disjoint_primeFactors {R : Type u_1} [CommRing R] [IsDomain R] [NormalizationMonoid R] [UniqueFactorizationMonoid R] {a b : R} (hc : IsCoprime a b) : Disjoint (UniqueFactorizationMonoid.primeFactors a) (UniqueFactorizationMonoid.primeFactors b)

Coprime elements have disjoint prime factors (as finsets).

theorem UniqueFactorizationDomain.mul_primeFactors_disjUnion {R : Type u_1} [CommRing R] [IsDomain R] [NormalizationMonoid R] [UniqueFactorizationMonoid R] {a b : R} (ha : a ≠ 0) (hb : b ≠ 0) (hc : IsCoprime a b) : UniqueFactorizationMonoid.primeFactors (a * b) = (UniqueFactorizationMonoid.primeFactors a).disjUnion (UniqueFactorizationMonoid.primeFactors b) ⋯

@[simp]

theorem UniqueFactorizationDomain.radical_neg_one {R : Type u_1} [CommRing R] [IsDomain R] [NormalizationMonoid R] [UniqueFactorizationMonoid R] : UniqueFactorizationMonoid.radical (-1) = 1

theorem UniqueFactorizationDomain.radical_mul {R : Type u_1} [CommRing R] [IsDomain R] [NormalizationMonoid R] [UniqueFactorizationMonoid R] {a b : R} (hc : IsCoprime a b) : UniqueFactorizationMonoid.radical (a * b) = UniqueFactorizationMonoid.radical a * UniqueFactorizationMonoid.radical b

Radical is multiplicative for coprime elements.

theorem UniqueFactorizationDomain.radical_neg {R : Type u_1} [CommRing R] [IsDomain R] [NormalizationMonoid R] [UniqueFactorizationMonoid R] {a : R} : UniqueFactorizationMonoid.radical (-a) = UniqueFactorizationMonoid.radical a

def EuclideanDomain.divRadical {E : Type u_1} [EuclideanDomain E] [NormalizationMonoid E] [UniqueFactorizationMonoid E] (a : E) : E

Division of an element by its radical in an Euclidean domain.

Equations

• EuclideanDomain.divRadical a = a / UniqueFactorizationMonoid.radical a

theorem EuclideanDomain.radical_mul_divRadical {E : Type u_1} [EuclideanDomain E] [NormalizationMonoid E] [UniqueFactorizationMonoid E] (a : E) : UniqueFactorizationMonoid.radical a * divRadical a = a

theorem EuclideanDomain.divRadical_mul_radical {E : Type u_1} [EuclideanDomain E] [NormalizationMonoid E] [UniqueFactorizationMonoid E] (a : E) : divRadical a * UniqueFactorizationMonoid.radical a = a

theorem EuclideanDomain.divRadical_ne_zero {E : Type u_1} [EuclideanDomain E] [NormalizationMonoid E] [UniqueFactorizationMonoid E] {a : E} (ha : a ≠ 0) : divRadical a ≠ 0

theorem EuclideanDomain.divRadical_isUnit {E : Type u_1} [EuclideanDomain E] [NormalizationMonoid E] [UniqueFactorizationMonoid E] {u : E} (hu : IsUnit u) : IsUnit (divRadical u)

theorem EuclideanDomain.eq_divRadical {E : Type u_1} [EuclideanDomain E] [NormalizationMonoid E] [UniqueFactorizationMonoid E] {a x : E} (h : UniqueFactorizationMonoid.radical a * x = a) : x = divRadical a

theorem EuclideanDomain.divRadical_mul {E : Type u_1} [EuclideanDomain E] [NormalizationMonoid E] [UniqueFactorizationMonoid E] {a b : E} (hab : IsCoprime a b) : divRadical (a * b) = divRadical a * divRadical b

theorem EuclideanDomain.divRadical_dvd_self {E : Type u_1} [EuclideanDomain E] [NormalizationMonoid E] [UniqueFactorizationMonoid E] (a : E) : divRadical a ∣ a

theorem IsCoprime.divRadical {E : Type u_1} [EuclideanDomain E] [NormalizationMonoid E] [UniqueFactorizationMonoid E] {a b : E} (h : IsCoprime a b) : IsCoprime (EuclideanDomain.divRadical a) (EuclideanDomain.divRadical b)