Associated, prime, and irreducible elements. #
In this file we define the predicate Prime p
saying that an element of a commutative monoid with zero is prime.
Namely, Prime p means that p isn't zero, it isn't a unit,
and p ∣ a * b → p ∣ a ∨ p ∣ b for all a, b;
In decomposition monoids (e.g., ℕ, ℤ), this predicate is equivalent to Irreducible,
however this is not true in general.
We also define an equivalence relation Associated
saying that two elements of a monoid differ by a multiplication by a unit.
Then we show that the quotient type Associates is a monoid
and prove basic properties of this quotient.
theorem
comap_prime
{M : Type u_1}
{N : Type u_2}
[CommMonoidWithZero M]
[CommMonoidWithZero N]
{F : Type u_3}
{G : Type u_4}
[FunLike F M N]
[MonoidWithZeroHomClass F M N]
[FunLike G N M]
[MulHomClass G N M]
(f : F)
(g : G)
{p : M}
(hinv : ∀ (a : M), g (f a) = a)
(hp : Prime (f p))
:
Prime p
theorem
MulEquiv.prime_iff
{M : Type u_1}
{N : Type u_2}
[CommMonoidWithZero M]
[CommMonoidWithZero N]
{p : M}
{E : Type u_5}
[EquivLike E M N]
[MulEquivClass E M N]
(e : E)
:
theorem
Prime.left_dvd_or_dvd_right_of_dvd_mul
{M : Type u_1}
[CommMonoidWithZero M]
[IsCancelMulZero M]
{p : M}
(hp : Prime p)
{a b : M}
:
a ∣ p * b → p ∣ a ∨ a ∣ b
theorem
Prime.pow_dvd_of_dvd_mul_left
{M : Type u_1}
[CommMonoidWithZero M]
[IsCancelMulZero M]
{p a b : M}
(hp : Prime p)
(n : ℕ)
(h : ¬p ∣ a)
(h' : p ^ n ∣ a * b)
:
p ^ n ∣ b
theorem
Prime.pow_dvd_of_dvd_mul_right
{M : Type u_1}
[CommMonoidWithZero M]
[IsCancelMulZero M]
{p a b : M}
(hp : Prime p)
(n : ℕ)
(h : ¬p ∣ b)
(h' : p ^ n ∣ a * b)
:
p ^ n ∣ a
theorem
Prime.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd
{M : Type u_1}
[CommMonoidWithZero M]
[IsCancelMulZero M]
{p a b : M}
{n : ℕ}
(hp : Prime p)
(hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n)
(hb : ¬p ^ 2 ∣ b)
:
p ∣ a
theorem
prime_pow_succ_dvd_mul
{M : Type u_1}
[CommMonoidWithZero M]
[IsCancelMulZero M]
{p x y : M}
(h : Prime p)
{i : ℕ}
(hxy : p ^ (i + 1) ∣ x * y)
:
p ^ (i + 1) ∣ x ∨ p ∣ y
theorem
succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul
{M : Type u_1}
[CommMonoidWithZero M]
[IsCancelMulZero M]
{p : M}
(hp : Prime p)
{a b : M}
{k l : ℕ}
:
p ^ k ∣ a → p ^ l ∣ b → p ^ (k + l + 1) ∣ a * b → p ^ (k + 1) ∣ a ∨ p ^ (l + 1) ∣ b
theorem
Prime.not_isSquare
{M : Type u_1}
[CommMonoidWithZero M]
[IsCancelMulZero M]
{p : M}
(hp : Prime p)
:
¬IsSquare p
theorem
IsSquare.not_prime
{M : Type u_1}
[CommMonoidWithZero M]
[IsCancelMulZero M]
{a : M}
(ha : IsSquare a)
:
¬Prime a
theorem
not_prime_pow
{M : Type u_1}
[CommMonoidWithZero M]
[IsCancelMulZero M]
{a : M}
{n : ℕ}
(hn : n ≠ 1)
:
¬Prime (a ^ n)
theorem
DvdNotUnit.isUnit_of_irreducible_right
{M : Type u_1}
[CommMonoidWithZero M]
{p q : M}
(h : DvdNotUnit p q)
(hq : Irreducible q)
:
IsUnit p
theorem
not_irreducible_of_not_unit_dvdNotUnit
{M : Type u_1}
[CommMonoidWithZero M]
{p q : M}
(hp : ¬IsUnit p)
(h : DvdNotUnit p q)
:
¬Irreducible q
theorem
DvdNotUnit.not_unit
{M : Type u_1}
[CommMonoidWithZero M]
{p q : M}
(hp : DvdNotUnit p q)
:
¬IsUnit q
theorem
DvdNotUnit.ne
{M : Type u_1}
[CommMonoidWithZero M]
[IsCancelMulZero M]
{p q : M}
(h : DvdNotUnit p q)
:
p ≠ q
theorem
pow_injective_of_not_isUnit
{M : Type u_1}
[CommMonoidWithZero M]
[IsCancelMulZero M]
{q : M}
(hq : ¬IsUnit q)
(hq' : q ≠ 0)
:
Function.Injective fun (n : ℕ) => q ^ n
theorem
pow_inj_of_not_isUnit
{M : Type u_1}
[CommMonoidWithZero M]
[IsCancelMulZero M]
{q : M}
(hq : ¬IsUnit q)
(hq' : q ≠ 0)
{m n : ℕ}
:
q ^ m = q ^ n ↔ m = n
theorem
IsRelPrime.of_map
{M : Type u_3}
{N : Type u_4}
{F : Type u_5}
[Monoid M]
[Monoid N]
[FunLike F M N]
[MulHomClass F M N]
(f : F)
[IsLocalHom f]
{a b : M}
(hab : IsRelPrime (f a) (f b))
:
IsRelPrime a b