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

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

Equations

• SupIrred a = (¬IsMin a ∧ ∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a)

def SupPrime {α : Type u_2} [SemilatticeSup α] (a : α) : Prop

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

Equations

• SupPrime a = (¬IsMin a ∧ ∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c)

theorem SupIrred.not_isMin {α : Type u_2} [SemilatticeSup α] {a : α} (ha : SupIrred a) : ¬IsMin a

theorem SupPrime.not_isMin {α : Type u_2} [SemilatticeSup α] {a : α} (ha : SupPrime a) : ¬IsMin a

theorem IsMin.not_supIrred {α : Type u_2} [SemilatticeSup α] {a : α} (ha : IsMin a) : ¬SupIrred a

theorem IsMin.not_supPrime {α : Type u_2} [SemilatticeSup α] {a : α} (ha : IsMin a) : ¬SupPrime a

@[simp]

theorem not_supIrred {α : Type u_2} [SemilatticeSup α] {a : α} : ¬SupIrred a ↔ IsMin a ∨ ∃ (b : α) (c : α), b ⊔ c = a ∧ b < a ∧ c < a

@[simp]

theorem not_supPrime {α : Type u_2} [SemilatticeSup α] {a : α} : ¬SupPrime a ↔ IsMin a ∨ ∃ (b : α) (c : α), a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c

theorem SupPrime.supIrred {α : Type u_2} [SemilatticeSup α] {a : α} : SupPrime a → SupIrred a

theorem SupPrime.le_sup {α : Type u_2} [SemilatticeSup α] {a b c : α} (ha : SupPrime a) : a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c

@[simp]

theorem not_supIrred_bot {α : Type u_2} [SemilatticeSup α] [OrderBot α] : ¬SupIrred ⊥

@[simp]

theorem not_supPrime_bot {α : Type u_2} [SemilatticeSup α] [OrderBot α] : ¬SupPrime ⊥

theorem SupIrred.ne_bot {α : Type u_2} [SemilatticeSup α] {a : α} [OrderBot α] (ha : SupIrred a) : a ≠ ⊥

theorem SupPrime.ne_bot {α : Type u_2} [SemilatticeSup α] {a : α} [OrderBot α] (ha : SupPrime a) : a ≠ ⊥

theorem SupIrred.finset_sup_eq {ι : Type u_1} {α : Type u_2} [SemilatticeSup α] {a : α} [OrderBot α] {s : Finset ι} {f : ι → α} (ha : SupIrred a) (h : s.sup f = a) : ∃ i ∈ s, f i = a

theorem SupPrime.le_finset_sup {ι : Type u_1} {α : Type u_2} [SemilatticeSup α] {a : α} [OrderBot α] {s : Finset ι} {f : ι → α} (ha : SupPrime a) : a ≤ s.sup f ↔ ∃ i ∈ s, a ≤ f i

theorem exists_supIrred_decomposition {α : Type u_2} [SemilatticeSup α] [OrderBot α] [WellFoundedLT α] (a : α) : ∃ (s : Finset α), s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred 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 InfIrred {α : Type u_2} [SemilatticeInf α] (a : α) : Prop

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

Equations

• InfIrred a = (¬IsMax a ∧ ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a)

def InfPrime {α : Type u_2} [SemilatticeInf α] (a : α) : Prop

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

Equations

• InfPrime a = (¬IsMax a ∧ ∀ ⦃b c : α⦄, b ⊓ c ≤ a → b ≤ a ∨ c ≤ a)

@[simp]

theorem IsMax.not_infIrred {α : Type u_2} [SemilatticeInf α] {a : α} (ha : IsMax a) : ¬InfIrred a

@[simp]

theorem IsMax.not_infPrime {α : Type u_2} [SemilatticeInf α] {a : α} (ha : IsMax a) : ¬InfPrime a

@[simp]

theorem not_infIrred {α : Type u_2} [SemilatticeInf α] {a : α} : ¬InfIrred a ↔ IsMax a ∨ ∃ (b : α) (c : α), b ⊓ c = a ∧ a < b ∧ a < c

@[simp]

theorem not_infPrime {α : Type u_2} [SemilatticeInf α] {a : α} : ¬InfPrime a ↔ IsMax a ∨ ∃ (b : α) (c : α), b ⊓ c ≤ a ∧ ¬b ≤ a ∧ ¬c ≤ a

theorem InfPrime.infIrred {α : Type u_2} [SemilatticeInf α] {a : α} : InfPrime a → InfIrred a

theorem InfPrime.inf_le {α : Type u_2} [SemilatticeInf α] {a b c : α} (ha : InfPrime a) : b ⊓ c ≤ a ↔ b ≤ a ∨ c ≤ a

theorem not_infIrred_top {α : Type u_2} [SemilatticeInf α] [OrderTop α] : ¬InfIrred ⊤

theorem not_infPrime_top {α : Type u_2} [SemilatticeInf α] [OrderTop α] : ¬InfPrime ⊤

theorem InfIrred.ne_top {α : Type u_2} [SemilatticeInf α] {a : α} [OrderTop α] (ha : InfIrred a) : a ≠ ⊤

theorem InfPrime.ne_top {α : Type u_2} [SemilatticeInf α] {a : α} [OrderTop α] (ha : InfPrime a) : a ≠ ⊤

theorem InfIrred.finset_inf_eq {ι : Type u_1} {α : Type u_2} [SemilatticeInf α] {a : α} [OrderTop α] {s : Finset ι} {f : ι → α} : InfIrred a → s.inf f = a → ∃ i ∈ s, f i = a

theorem InfPrime.finset_inf_le {ι : Type u_1} {α : Type u_2} [SemilatticeInf α] {a : α} [OrderTop α] {s : Finset ι} {f : ι → α} (ha : InfPrime a) : s.inf f ≤ a ↔ ∃ i ∈ s, f i ≤ a

theorem exists_infIrred_decomposition {α : Type u_2} [SemilatticeInf α] [OrderTop α] [WellFoundedGT α] (a : α) : ∃ (s : Finset α), s.inf id = a ∧ ∀ ⦃b : α⦄, b ∈ s → InfIrred 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 infIrred_toDual {α : Type u_2} [SemilatticeSup α] {a : α} : InfIrred (OrderDual.toDual a) ↔ SupIrred a

@[simp]

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

@[simp]

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

@[simp]

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

theorem SupIrred.dual {α : Type u_2} [SemilatticeSup α] {a : α} : SupIrred a → InfIrred (OrderDual.toDual a)

Alias of the reverse direction of infIrred_toDual.

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

Alias of the reverse direction of infPrime_toDual.

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

Alias of the reverse direction of supIrred_ofDual.

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

Alias of the reverse direction of supPrime_ofDual.

@[simp]

theorem supIrred_toDual {α : Type u_2} [SemilatticeInf α] {a : α} : SupIrred (OrderDual.toDual a) ↔ InfIrred a

@[simp]

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

@[simp]

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

@[simp]

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

theorem InfIrred.dual {α : Type u_2} [SemilatticeInf α] {a : α} : InfIrred a → SupIrred (OrderDual.toDual a)

Alias of the reverse direction of supIrred_toDual.

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

Alias of the reverse direction of supPrime_toDual.

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

Alias of the reverse direction of infIrred_ofDual.

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

Alias of the reverse direction of infPrime_ofDual.

@[simp]

theorem supPrime_iff_supIrred {α : Type u_2} [DistribLattice α] {a : α} : SupPrime a ↔ SupIrred a

@[simp]

theorem infPrime_iff_infIrred {α : Type u_2} [DistribLattice α] {a : α} : InfPrime a ↔ InfIrred a

theorem SupIrred.supPrime {α : Type u_2} [DistribLattice α] {a : α} : SupIrred a → SupPrime a

Alias of the reverse direction of supPrime_iff_supIrred.

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

Alias of the reverse direction of infPrime_iff_infIrred.

theorem supPrime_iff_not_isMin {α : Type u_2} [LinearOrder α] {a : α} : SupPrime a ↔ ¬IsMin a

theorem infPrime_iff_not_isMax {α : Type u_2} [LinearOrder α] {a : α} : InfPrime a ↔ ¬IsMax a

@[simp]

theorem supIrred_iff_not_isMin {α : Type u_2} [LinearOrder α] {a : α} : SupIrred a ↔ ¬IsMin a

@[simp]

theorem infIrred_iff_not_isMax {α : Type u_2} [LinearOrder α] {a : α} : InfIrred a ↔ ¬IsMax a