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.
An element p
of a commutative monoid with zero (e.g., a ring) is called prime,
if it's not zero, not a unit, and p ∣ a * b → p ∣ a ∨ p ∣ b
for all a
, b
.
Instances For
Irreducible p
states that p
is non-unit and only factors into units.
We explicitly avoid stating that p
is non-zero, this would require a semiring. Assuming only a
monoid allows us to reuse irreducible for associated elements.
p
is not a unitif
p
factors then one factor is a unit
Instances For
p
is not a unit
if p
factors then one factor is a unit
If p
and q
are irreducible, then p ∣ q
implies q ∣ p
.
Two elements of a Monoid
are Associated
if one of them is another one
multiplied by a unit on the right.
Equations
- Associated x y = ∃ (u : αˣ), x * ↑u = y
Instances For
The setoid of the relation x ~ᵤ y
iff there is a unit u
such that x * u = y
Equations
- Associated.setoid α = { r := Associated, iseqv := ⋯ }
Instances For
Equations
- instDecidableRelAssociatedOfDvd x✝ x = decidable_of_iff (x✝ ∣ x ∧ x ∣ x✝) ⋯
See also Irreducible.coprime_iff_not_dvd
.
The quotient of a monoid by the Associated
relation. Two elements x
and y
are associated iff there is a unit u
such that x * u = y
. There is a natural
monoid structure on Associates α
.
Equations
- Associates α = Quotient (Associated.setoid α)
Instances For
The canonical quotient map from a monoid α
into the Associates
of α
Equations
- Associates.mk a = ⟦a⟧
Instances For
Equations
- Associates.instInhabited = { default := ⟦1⟧ }
Equations
- Associates.instOne = { one := ⟦1⟧ }
Equations
- Associates.instBot = { bot := 1 }
Equations
- Associates.instUniqueOfSubsingleton = { default := 1, uniq := ⋯ }
Equations
- Associates.instMul = { mul := Quotient.map₂ (fun (x x_1 : α) => x * x_1) ⋯ }
Equations
- Associates.instCommMonoid = CommMonoid.mk ⋯
Equations
- Associates.instPreorder = Preorder.mk ⋯ ⋯ ⋯
Associates.mk
as a MonoidHom
.
Equations
- Associates.mkMonoidHom = { toFun := Associates.mk, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Equations
- Associates.uniqueUnits = { default := 1, uniq := ⋯ }
Equations
- Associates.instOrderBot = OrderBot.mk ⋯
Alias of Associates.mk_le_mk_iff_dvd
.
Alias of Associates.isPrimal_mk
.
Equations
- ⋯ = ⋯
Equations
- Associates.instZero = { zero := ⟦0⟧ }
Equations
- Associates.instTopOfZero = { top := 0 }
Equations
- ⋯ = ⋯
Equations
- Associates.instCommMonoidWithZero = CommMonoidWithZero.mk ⋯ ⋯
Equations
- Associates.instOrderTop = OrderTop.mk ⋯
Equations
- Associates.instBoundedOrder = BoundedOrder.mk
Equations
- a.instDecidableRelDvd b = Quotient.recOnSubsingleton₂ a b fun (x x_1 : α) => decidable_of_iff' (x ∣ x_1) ⋯
Equations
- Associates.instPartialOrder = PartialOrder.mk ⋯
Equations
- Associates.instCancelCommMonoidWithZero = let __src := inferInstance; CancelCommMonoidWithZero.mk
Equations
- ⋯ = ⋯