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

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

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] : UniqueFactorizationMonoid.radical 0 = 1

@[simp]

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

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

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

theorem UniqueFactorizationMonoid.radical_unit_mul {M : Type u_1} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {u : Mˣ} {a : M} : UniqueFactorizationMonoid.radical (↑u * a) = UniqueFactorizationMonoid.radical a

theorem UniqueFactorizationMonoid.radical_mul_unit {M : Type u_1} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {u : Mˣ} {a : M} : UniqueFactorizationMonoid.radical (a * ↑u) = UniqueFactorizationMonoid.radical a

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

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

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

theorem UniqueFactorizationMonoid.radical_of_prime {M : Type u_1} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M] {a : M} (ha : Prime a) : UniqueFactorizationMonoid.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) : UniqueFactorizationMonoid.radical (a ^ n) = normalize a