# mathlib3documentation

order.irreducible

# Irreducible and prime elements in an order #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• sup_irred a: Sup-irreducibility, a isn't minimal and a = b ⊔ c → a = b ∨ a = c
• inf_irred a: Inf-irreducibility, a isn't maximal and a = b ⊓ c → a = b ∨ a = c
• sup_prime a: Sup-primality, a isn't minimal and a ≤ b ⊔ c → a ≤ b ∨ a ≤ c
• inf_irred a: Inf-primality, a isn't maximal and a ≥ b ⊓ c → a ≥ b ∨ a ≥ c
• exists_sup_irred_decomposition/exists_inf_irred_decomposition: Decomposition into irreducibles in a well-founded semilattice.

### Irreducible and prime elements #

def sup_irred {α : Type u_2} (a : α) :
Prop

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

Equations
def sup_prime {α : Type u_2} (a : α) :
Prop

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

Equations
theorem sup_irred.not_is_min {α : Type u_2} {a : α} (ha : sup_irred a) :
theorem sup_prime.not_is_min {α : Type u_2} {a : α} (ha : sup_prime a) :
theorem is_min.not_sup_irred {α : Type u_2} {a : α} (ha : is_min a) :
theorem is_min.not_sup_prime {α : Type u_2} {a : α} (ha : is_min a) :
@[simp]
theorem not_sup_irred {α : Type u_2} {a : α} :
(b c : α), b c = a b < a c < a
@[simp]
theorem not_sup_prime {α : Type u_2} {a : α} :
(b c : α), a b c ¬a b ¬a c
@[protected]
theorem sup_prime.sup_irred {α : Type u_2} {a : α} :
theorem sup_prime.le_sup {α : Type u_2} {a b c : α} (ha : sup_prime a) :
a b c a b a c
@[simp]
theorem not_sup_irred_bot {α : Type u_2} [order_bot α] :
@[simp]
theorem not_sup_prime_bot {α : Type u_2} [order_bot α] :
theorem sup_irred.ne_bot {α : Type u_2} {a : α} [order_bot α] (ha : sup_irred a) :
theorem sup_prime.ne_bot {α : Type u_2} {a : α} [order_bot α] (ha : sup_prime a) :
theorem sup_irred.finset_sup_eq {ι : Type u_1} {α : Type u_2} {a : α} [order_bot α] {s : finset ι} {f : ι α} (ha : sup_irred a) (h : s.sup f = a) :
(i : ι) (H : i s), f i = a
theorem sup_prime.le_finset_sup {ι : Type u_1} {α : Type u_2} {a : α} [order_bot α] {s : finset ι} {f : ι α} (ha : sup_prime a) :
a s.sup f (i : ι) (H : i s), a f i
theorem exists_sup_irred_decomposition {α : Type u_2} [order_bot α] (a : α) :
(s : finset α), s.sup 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 inf_irred {α : Type u_2} (a : α) :
Prop

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

Equations
def inf_prime {α : Type u_2} (a : α) :
Prop

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

Equations
@[simp]
theorem is_max.not_inf_irred {α : Type u_2} {a : α} (ha : is_max a) :
@[simp]
theorem is_max.not_inf_prime {α : Type u_2} {a : α} (ha : is_max a) :
@[simp]
theorem not_inf_irred {α : Type u_2} {a : α} :
(b c : α), b c = a a < b a < c
@[simp]
theorem not_inf_prime {α : Type u_2} {a : α} :
(b c : α), b c a ¬b a ¬c a
@[protected]
theorem inf_prime.inf_irred {α : Type u_2} {a : α} :
theorem inf_prime.inf_le {α : Type u_2} {a b c : α} (ha : inf_prime a) :
b c a b a c a
@[simp]
theorem not_inf_irred_top {α : Type u_2} [order_top α] :
@[simp]
theorem not_inf_prime_top {α : Type u_2} [order_top α] :
theorem inf_irred.ne_top {α : Type u_2} {a : α} [order_top α] (ha : inf_irred a) :
theorem inf_prime.ne_top {α : Type u_2} {a : α} [order_top α] (ha : inf_prime a) :
theorem inf_irred.finset_inf_eq {ι : Type u_1} {α : Type u_2} {a : α} [order_top α] {s : finset ι} {f : ι α} :
s.inf f = a ( (i : ι) (H : i s), f i = a)
theorem inf_prime.finset_inf_le {ι : Type u_1} {α : Type u_2} {a : α} [order_top α] {s : finset ι} {f : ι α} (ha : inf_prime a) :
s.inf f a (i : ι) (H : i s), f i a
theorem exists_inf_irred_decomposition {α : Type u_2} [order_top α] (a : α) :
(s : finset α), s.inf 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 inf_irred_to_dual {α : Type u_2} {a : α} :
@[simp]
theorem inf_prime_to_dual {α : Type u_2} {a : α} :
@[simp]
theorem sup_irred_of_dual {α : Type u_2} {a : αᵒᵈ} :
@[simp]
theorem sup_prime_of_dual {α : Type u_2} {a : αᵒᵈ} :
theorem sup_irred.dual {α : Type u_2} {a : α} :

Alias of the reverse direction of inf_irred_to_dual.

theorem sup_prime.dual {α : Type u_2} {a : α} :

Alias of the reverse direction of inf_prime_to_dual.

theorem inf_irred.of_dual {α : Type u_2} {a : αᵒᵈ} :

Alias of the reverse direction of sup_irred_of_dual.

theorem inf_prime.of_dual {α : Type u_2} {a : αᵒᵈ} :

Alias of the reverse direction of sup_prime_of_dual.

@[simp]
theorem sup_irred_to_dual {α : Type u_2} {a : α} :
@[simp]
theorem sup_prime_to_dual {α : Type u_2} {a : α} :
@[simp]
theorem inf_irred_of_dual {α : Type u_2} {a : αᵒᵈ} :
@[simp]
theorem inf_prime_of_dual {α : Type u_2} {a : αᵒᵈ} :
theorem inf_irred.dual {α : Type u_2} {a : α} :

Alias of the reverse direction of sup_irred_to_dual.

theorem inf_prime.dual {α : Type u_2} {a : α} :

Alias of the reverse direction of sup_prime_to_dual.

theorem sup_irred.of_dual {α : Type u_2} {a : αᵒᵈ} :

Alias of the reverse direction of inf_irred_of_dual.

theorem sup_prime.of_dual {α : Type u_2} {a : αᵒᵈ} :

Alias of the reverse direction of inf_prime_of_dual.

@[simp]
theorem sup_prime_iff_sup_irred {α : Type u_2} {a : α} :
@[simp]
theorem inf_prime_iff_inf_irred {α : Type u_2} {a : α} :
@[protected]
theorem sup_irred.sup_prime {α : Type u_2} {a : α} :

Alias of the reverse direction of sup_prime_iff_sup_irred.

@[protected]
theorem inf_irred.inf_prime {α : Type u_2} {a : α} :

Alias of the reverse direction of inf_prime_iff_inf_irred.

@[simp]
theorem sup_prime_iff_not_is_min {α : Type u_2} [linear_order α] {a : α} :
@[simp]
theorem inf_prime_iff_not_is_max {α : Type u_2} [linear_order α] {a : α} :
@[simp]
theorem sup_irred_iff_not_is_min {α : Type u_2} [linear_order α] {a : α} :
@[simp]
theorem inf_irred_iff_not_is_max {α : Type u_2} [linear_order α] {a : α} :