# Documentation

Mathlib.Order.Irreducible

# Irreducible and prime elements in an order #

This file defines irreducible and prime elements in an order and shows that in a well-founded lattice every element decomposes as a supremum of irreducible elements.

An element is sup-irreducible (resp. inf-irreducible) if it isn't ⊥ and can't be written as the supremum of any strictly smaller elements. An element is sup-prime (resp. inf-prime) if it isn't ⊥ and is greater than the supremum of any two elements less than it.

Primality implies irreducibility in general. The converse only holds in distributive lattices. Both hold for all (non-minimal) elements in a linear order.

## Main declarations #

• SupIrred a: Sup-irreducibility, a isn't minimal and a = b ⊔ c → a = b ∨ a = c
• InfIrred a: Inf-irreducibility, a isn't maximal and a = b ⊓ c → a = b ∨ a = c
• SupPrime a: Sup-primality, a isn't minimal and a ≤ b ⊔ c → a ≤ b ∨ a ≤ c
• InfIrred a: Inf-primality, a isn't maximal and a ≥ b ⊓ c → a ≥ b ∨ a ≥ c
• exists_supIrred_decomposition/exists_infIrred_decomposition: Decomposition into irreducibles in a well-founded semilattice.

### Irreducible and prime elements #

def SupIrred {α : Type u_2} [] (a : α) :

A sup-irreducible element is a non-bottom element which isn't the supremum of anything smaller.

Instances For
def SupPrime {α : Type u_2} [] (a : α) :

A sup-prime element is a non-bottom element which isn't less than the supremum of anything smaller.

Instances For
theorem SupIrred.not_isMin {α : Type u_2} [] {a : α} (ha : ) :
theorem SupPrime.not_isMin {α : Type u_2} [] {a : α} (ha : ) :
theorem IsMin.not_supIrred {α : Type u_2} [] {a : α} (ha : ) :
theorem IsMin.not_supPrime {α : Type u_2} [] {a : α} (ha : ) :
@[simp]
theorem not_supIrred {α : Type u_2} [] {a : α} :
b c, b c = a b < a c < a
@[simp]
theorem not_supPrime {α : Type u_2} [] {a : α} :
b c, a b c ¬a b ¬a c
theorem SupPrime.supIrred {α : Type u_2} [] {a : α} :
theorem SupPrime.le_sup {α : Type u_2} [] {a : α} {b : α} {c : α} (ha : ) :
a b c a b a c
@[simp]
theorem not_supIrred_bot {α : Type u_2} [] [] :
@[simp]
theorem not_supPrime_bot {α : Type u_2} [] [] :
theorem SupIrred.ne_bot {α : Type u_2} [] {a : α} [] (ha : ) :
theorem SupPrime.ne_bot {α : Type u_2} [] {a : α} [] (ha : ) :
theorem SupIrred.finset_sup_eq {ι : Type u_1} {α : Type u_2} [] {a : α} [] {s : } {f : ια} (ha : ) (h : = a) :
i, i s f i = a
theorem SupPrime.le_finset_sup {ι : Type u_1} {α : Type u_2} [] {a : α} [] {s : } {f : ια} (ha : ) :
a i, i s a f i
theorem exists_supIrred_decomposition {α : Type u_2} [] [] [] (a : α) :
s, Finset.sup s id = a ∀ ⦃b : α⦄, b s

In a well-founded lattice, any element is the supremum of finitely many sup-irreducible elements. This is the order-theoretic analogue of prime factorisation.

def InfIrred {α : Type u_2} [] (a : α) :

An inf-irreducible element is a non-top element which isn't the infimum of anything bigger.

Instances For
def InfPrime {α : Type u_2} [] (a : α) :

An inf-prime element is a non-top element which isn't bigger than the infimum of anything bigger.

Instances For
@[simp]
theorem IsMax.not_infIrred {α : Type u_2} [] {a : α} (ha : ) :
@[simp]
theorem IsMax.not_infPrime {α : Type u_2} [] {a : α} (ha : ) :
@[simp]
theorem not_infIrred {α : Type u_2} [] {a : α} :
b c, b c = a a < b a < c
@[simp]
theorem not_infPrime {α : Type u_2} [] {a : α} :
b c, b c a ¬b a ¬c a
theorem InfPrime.infIrred {α : Type u_2} [] {a : α} :
theorem InfPrime.inf_le {α : Type u_2} [] {a : α} {b : α} {c : α} (ha : ) :
b c a b a c a
theorem not_infIrred_top {α : Type u_2} [] [] :
theorem not_infPrime_top {α : Type u_2} [] [] :
theorem InfIrred.ne_top {α : Type u_2} [] {a : α} [] (ha : ) :
theorem InfPrime.ne_top {α : Type u_2} [] {a : α} [] (ha : ) :
theorem InfIrred.finset_inf_eq {ι : Type u_1} {α : Type u_2} [] {a : α} [] {s : } {f : ια} :
= ai, i s f i = a
theorem InfPrime.finset_inf_le {ι : Type u_1} {α : Type u_2} [] {a : α} [] {s : } {f : ια} (ha : ) :
a i, i s f i a
theorem exists_infIrred_decomposition {α : Type u_2} [] [] [] (a : α) :
s, Finset.inf s id = a ∀ ⦃b : α⦄, b s

In a cowell-founded lattice, any element is the infimum of finitely many inf-irreducible elements. This is the order-theoretic analogue of prime factorisation.

@[simp]
theorem infIrred_toDual {α : Type u_2} [] {a : α} :
InfIrred (OrderDual.toDual a)
@[simp]
theorem infPrime_toDual {α : Type u_2} [] {a : α} :
InfPrime (OrderDual.toDual a)
@[simp]
theorem supIrred_ofDual {α : Type u_2} [] {a : αᵒᵈ} :
SupIrred (OrderDual.ofDual a)
@[simp]
theorem supPrime_ofDual {α : Type u_2} [] {a : αᵒᵈ} :
SupPrime (OrderDual.ofDual a)
theorem SupIrred.dual {α : Type u_2} [] {a : α} :
InfIrred (OrderDual.toDual a)

Alias of the reverse direction of infIrred_toDual.

theorem SupPrime.dual {α : Type u_2} [] {a : α} :
InfPrime (OrderDual.toDual a)

Alias of the reverse direction of infPrime_toDual.

theorem InfIrred.ofDual {α : Type u_2} [] {a : αᵒᵈ} :
SupIrred (OrderDual.ofDual a)

Alias of the reverse direction of supIrred_ofDual.

theorem InfPrime.ofDual {α : Type u_2} [] {a : αᵒᵈ} :
SupPrime (OrderDual.ofDual a)

Alias of the reverse direction of supPrime_ofDual.

@[simp]
theorem supIrred_toDual {α : Type u_2} [] {a : α} :
SupIrred (OrderDual.toDual a)
@[simp]
theorem supPrime_toDual {α : Type u_2} [] {a : α} :
SupPrime (OrderDual.toDual a)
@[simp]
theorem infIrred_ofDual {α : Type u_2} [] {a : αᵒᵈ} :
InfIrred (OrderDual.ofDual a)
@[simp]
theorem infPrime_ofDual {α : Type u_2} [] {a : αᵒᵈ} :
InfPrime (OrderDual.ofDual a)
theorem InfIrred.dual {α : Type u_2} [] {a : α} :
SupIrred (OrderDual.toDual a)

Alias of the reverse direction of supIrred_toDual.

theorem InfPrime.dual {α : Type u_2} [] {a : α} :
SupPrime (OrderDual.toDual a)

Alias of the reverse direction of supPrime_toDual.

theorem SupIrred.ofDual {α : Type u_2} [] {a : αᵒᵈ} :
InfIrred (OrderDual.ofDual a)

Alias of the reverse direction of infIrred_ofDual.

theorem SupPrime.ofDual {α : Type u_2} [] {a : αᵒᵈ} :
InfPrime (OrderDual.ofDual a)

Alias of the reverse direction of infPrime_ofDual.

@[simp]
theorem supPrime_iff_supIrred {α : Type u_2} [] {a : α} :
@[simp]
theorem infPrime_iff_infIrred {α : Type u_2} [] {a : α} :
theorem SupIrred.supPrime {α : Type u_2} [] {a : α} :

Alias of the reverse direction of supPrime_iff_supIrred.

theorem InfIrred.infPrime {α : Type u_2} [] {a : α} :

Alias of the reverse direction of infPrime_iff_infIrred.

theorem supPrime_iff_not_isMin {α : Type u_2} [] {a : α} :
theorem infPrime_iff_not_isMax {α : Type u_2} [] {a : α} :
@[simp]
theorem supIrred_iff_not_isMin {α : Type u_2} [] {a : α} :
@[simp]
theorem infIrred_iff_not_isMax {α : Type u_2} [] {a : α} :