mathlib3 documentation

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} [semilattice_sup α] (a : α) :

Prop

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

Equations

sup_irred a = (¬is_min a ∧ ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a)

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

Prop

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

Equations

sup_prime a = (¬is_min a ∧ ∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c)

theorem sup_irred.not_is_min {α : Type u_2} [semilattice_sup α] {a : α} (ha : sup_irred a) :

theorem sup_prime.not_is_min {α : Type u_2} [semilattice_sup α] {a : α} (ha : sup_prime a) :

theorem is_min.not_sup_irred {α : Type u_2} [semilattice_sup α] {a : α} (ha : is_min a) :

theorem is_min.not_sup_prime {α : Type u_2} [semilattice_sup α] {a : α} (ha : is_min a) :

@[simp]

theorem not_sup_irred {α : Type u_2} [semilattice_sup α] {a : α} :

¬sup_irred a ↔ is_min a ∨ ∃ (b c : α), b ⊔ c = a ∧ b < a ∧ c < a

@[simp]

theorem not_sup_prime {α : Type u_2} [semilattice_sup α] {a : α} :

¬sup_prime a ↔ is_min a ∨ ∃ (b c : α), a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c

@[protected]

theorem sup_prime.sup_irred {α : Type u_2} [semilattice_sup α] {a : α} :

sup_prime a → sup_irred a

theorem sup_prime.le_sup {α : Type u_2} [semilattice_sup α] {a b c : α} (ha : sup_prime a) :

a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c

@[simp]

theorem not_sup_irred_bot {α : Type u_2} [semilattice_sup α] [order_bot α] :

¬sup_irred ⊥

@[simp]

theorem not_sup_prime_bot {α : Type u_2} [semilattice_sup α] [order_bot α] :

¬sup_prime ⊥

theorem sup_irred.ne_bot {α : Type u_2} [semilattice_sup α] {a : α} [order_bot α] (ha : sup_irred a) :

theorem sup_prime.ne_bot {α : Type u_2} [semilattice_sup α] {a : α} [order_bot α] (ha : sup_prime a) :

theorem sup_irred.finset_sup_eq {ι : Type u_1} {α : Type u_2} [semilattice_sup α] {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} [semilattice_sup α] {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} [semilattice_sup α] [order_bot α] [well_founded_lt α] (a : α) :

∃ (s : finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → sup_irred b

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} [semilattice_inf α] (a : α) :

Prop

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

Equations

inf_irred a = (¬is_max a ∧ ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a)

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

Prop

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

Equations

inf_prime a = (¬is_max a ∧ ∀ ⦃b c : α⦄, b ⊓ c ≤ a → b ≤ a ∨ c ≤ a)

@[simp]

theorem is_max.not_inf_irred {α : Type u_2} [semilattice_inf α] {a : α} (ha : is_max a) :

@[simp]

theorem is_max.not_inf_prime {α : Type u_2} [semilattice_inf α] {a : α} (ha : is_max a) :

@[simp]

theorem not_inf_irred {α : Type u_2} [semilattice_inf α] {a : α} :

¬inf_irred a ↔ is_max a ∨ ∃ (b c : α), b ⊓ c = a ∧ a < b ∧ a < c

@[simp]

theorem not_inf_prime {α : Type u_2} [semilattice_inf α] {a : α} :

¬inf_prime a ↔ is_max a ∨ ∃ (b c : α), b ⊓ c ≤ a ∧ ¬b ≤ a ∧ ¬c ≤ a

@[protected]

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

inf_prime a → inf_irred a

theorem inf_prime.inf_le {α : Type u_2} [semilattice_inf α] {a b c : α} (ha : inf_prime a) :

b ⊓ c ≤ a ↔ b ≤ a ∨ c ≤ a

@[simp]

theorem not_inf_irred_top {α : Type u_2} [semilattice_inf α] [order_top α] :

¬inf_irred ⊤

@[simp]

theorem not_inf_prime_top {α : Type u_2} [semilattice_inf α] [order_top α] :

¬inf_prime ⊤

theorem inf_irred.ne_top {α : Type u_2} [semilattice_inf α] {a : α} [order_top α] (ha : inf_irred a) :

theorem inf_prime.ne_top {α : Type u_2} [semilattice_inf α] {a : α} [order_top α] (ha : inf_prime a) :

theorem inf_irred.finset_inf_eq {ι : Type u_1} {α : Type u_2} [semilattice_inf α] {a : α} [order_top α] {s : finset ι} {f : ι → α} :

inf_irred a → s.inf f = a → (∃ (i : ι) (H : i ∈ s), f i = a)

theorem inf_prime.finset_inf_le {ι : Type u_1} {α : Type u_2} [semilattice_inf α] {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} [semilattice_inf α] [order_top α] [well_founded_gt α] (a : α) :

∃ (s : finset α), s.inf id = a ∧ ∀ ⦃b : α⦄, b ∈ s → inf_irred b

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} [semilattice_sup α] {a : α} :

inf_irred (⇑order_dual.to_dual a) ↔ sup_irred a

@[simp]

theorem inf_prime_to_dual {α : Type u_2} [semilattice_sup α] {a : α} :

inf_prime (⇑order_dual.to_dual a) ↔ sup_prime a

@[simp]

theorem sup_irred_of_dual {α : Type u_2} [semilattice_sup α] {a : αᵒᵈ} :

sup_irred (⇑order_dual.of_dual a) ↔ inf_irred a

@[simp]

theorem sup_prime_of_dual {α : Type u_2} [semilattice_sup α] {a : αᵒᵈ} :

sup_prime (⇑order_dual.of_dual a) ↔ inf_prime a

theorem sup_irred.dual {α : Type u_2} [semilattice_sup α] {a : α} :

sup_irred a → inf_irred (⇑order_dual.to_dual a)

Alias of the reverse direction of inf_irred_to_dual.

theorem sup_prime.dual {α : Type u_2} [semilattice_sup α] {a : α} :

sup_prime a → inf_prime (⇑order_dual.to_dual a)

Alias of the reverse direction of inf_prime_to_dual.

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

inf_irred a → sup_irred (⇑order_dual.of_dual a)

Alias of the reverse direction of sup_irred_of_dual.

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

inf_prime a → sup_prime (⇑order_dual.of_dual a)

Alias of the reverse direction of sup_prime_of_dual.

@[simp]

theorem sup_irred_to_dual {α : Type u_2} [semilattice_inf α] {a : α} :

sup_irred (⇑order_dual.to_dual a) ↔ inf_irred a

@[simp]

theorem sup_prime_to_dual {α : Type u_2} [semilattice_inf α] {a : α} :

sup_prime (⇑order_dual.to_dual a) ↔ inf_prime a

@[simp]

theorem inf_irred_of_dual {α : Type u_2} [semilattice_inf α] {a : αᵒᵈ} :

inf_irred (⇑order_dual.of_dual a) ↔ sup_irred a

@[simp]

theorem inf_prime_of_dual {α : Type u_2} [semilattice_inf α] {a : αᵒᵈ} :

inf_prime (⇑order_dual.of_dual a) ↔ sup_prime a

theorem inf_irred.dual {α : Type u_2} [semilattice_inf α] {a : α} :

inf_irred a → sup_irred (⇑order_dual.to_dual a)

Alias of the reverse direction of sup_irred_to_dual.

theorem inf_prime.dual {α : Type u_2} [semilattice_inf α] {a : α} :

inf_prime a → sup_prime (⇑order_dual.to_dual a)

Alias of the reverse direction of sup_prime_to_dual.

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

sup_irred a → inf_irred (⇑order_dual.of_dual a)

Alias of the reverse direction of inf_irred_of_dual.

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

sup_prime a → inf_prime (⇑order_dual.of_dual a)

Alias of the reverse direction of inf_prime_of_dual.

@[simp]

theorem sup_prime_iff_sup_irred {α : Type u_2} [distrib_lattice α] {a : α} :

sup_prime a ↔ sup_irred a

@[simp]

theorem inf_prime_iff_inf_irred {α : Type u_2} [distrib_lattice α] {a : α} :

inf_prime a ↔ inf_irred a

@[protected]

theorem sup_irred.sup_prime {α : Type u_2} [distrib_lattice α] {a : α} :

sup_irred a → sup_prime a

Alias of the reverse direction of sup_prime_iff_sup_irred.

@[protected]

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

inf_irred a → inf_prime 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 : α} :

sup_prime a ↔ ¬is_min a

@[simp]

theorem inf_prime_iff_not_is_max {α : Type u_2} [linear_order α] {a : α} :

inf_prime a ↔ ¬is_max a

@[simp]

theorem sup_irred_iff_not_is_min {α : Type u_2} [linear_order α] {a : α} :

sup_irred a ↔ ¬is_min a

@[simp]

theorem inf_irred_iff_not_is_max {α : Type u_2} [linear_order α] {a : α} :

inf_irred a ↔ ¬is_max a