doc-next-gen

Mathlib.Algebra.Group.Irreducible.Defs

Module docstring

{"# Irreducible elements in a monoid

This file defines irreducible elements of a monoid (Irreducible), as non-units that can't be written as the product of two non-units. This generalises irreducible elements of a ring. We also define the additive variant (AddIrreducible).

In decomposition monoids (e.g., ℕ, ℤ), this predicate is equivalent to Prime (see irreducible_iff_prime), however this is not true in general. "}

AddIrreducible structure
[AddMonoid M] (p : M)
Full source 
/-- `AddIrreducible p` states that `p` is not an additive unit and cannot be written as a sum of
additive non-units. -/
structure AddIrreducible [AddMonoid M] (p : M) : Prop where
  /-- An irreducible element is not an additive unit. -/
  not_isAddUnit : ¬IsAddUnit p
  /-- If an irreducible element can be written as a sum, then one term is an additive unit. -/
  isAddUnit_or_isAddUnit ⦃a b⦄ : p = a + b → IsAddUnitIsAddUnit a ∨ IsAddUnit b
Additively irreducible element
Informal description
An element \( p \) of an additive monoid \( M \) is called *additively irreducible* if it is not an additive unit and cannot be expressed as the sum of two non-unit elements. In other words, for any \( a, b \in M \), if \( p = a + b \), then at least one of \( a \) or \( b \) must be an additive unit.
Irreducible structure
(p : M)
Full source 
/-- `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. -/
@[to_additive]
structure Irreducible (p : M) : Prop where
  /-- An irreducible element is not a unit. -/
  not_isUnit : ¬IsUnit p
  /-- If an irreducible element factors, then one factor is a unit. -/
  isUnit_or_isUnit ⦃a b⦄ : p = a * b → IsUnitIsUnit a ∨ IsUnit b
Irreducible element in a monoid
Informal description
An element \( p \) of a monoid \( M \) is called *irreducible* if it is not a unit and any factorization \( p = a \cdot b \) implies that either \( a \) or \( b \) is a unit.
irreducible_iff theorem
: Irreducible p ↔ ¬IsUnit p ∧ ∀ ⦃a b⦄, p = a * b → IsUnit a ∨ IsUnit b
Full source 
@[to_additive] lemma irreducible_iff :
    IrreducibleIrreducible p ↔ ¬IsUnit p ∧ ∀ ⦃a b⦄, p = a * b → IsUnit a ∨ IsUnit b where
  mp hp := ⟨hp.not_isUnit, hp.isUnit_or_isUnit⟩
  mpr hp := ⟨hp.1, hp.2⟩
Characterization of Irreducible Elements in a Monoid
Informal description
An element $p$ of a monoid $M$ is irreducible if and only if $p$ is not a unit and for any $a, b \in M$ such that $p = a \cdot b$, either $a$ or $b$ is a unit.
Irreducible.ne_one theorem
(hp : Irreducible p) : p ≠ 1
Full source 
@[to_additive]
lemma Irreducible.ne_one (hp : Irreducible p) : p ≠ 1 := by rintro rfl; exact not_irreducible_one hp
Irreducible elements are not the identity
Informal description
If an element $p$ in a monoid $M$ is irreducible, then $p$ is not equal to the multiplicative identity $1$.
of_irreducible_mul theorem
: Irreducible (x * y) → IsUnit x ∨ IsUnit y
Full source 
@[to_additive]
lemma of_irreducible_mul : Irreducible (x * y) → IsUnitIsUnit x ∨ IsUnit y | ⟨_, h⟩ => h rfl
Irreducibility of Product Implies One Factor is a Unit
Informal description
If the product $x \cdot y$ is irreducible in a monoid $M$, then either $x$ or $y$ must be a unit.
irreducible_or_factor theorem
(hp : ¬IsUnit p) : Irreducible p ∨ ∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ p = a * b
Full source 
@[to_additive]
lemma irreducible_or_factor (hp : ¬IsUnit p) :
    IrreducibleIrreducible p ∨ ∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ p = a * b := by
  simpa [irreducible_iff, hp, and_rotate] using em (∀ a b, p = a * b → IsUnitIsUnit a ∨ IsUnit b)
Decomposition of Non-Units into Irreducibles or Non-Unit Factors
Informal description
For any element $p$ in a monoid $M$ that is not a unit, either $p$ is irreducible or there exist non-unit elements $a$ and $b$ such that $p = a \cdot b$.