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 #

Irreducible and prime elements #

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

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

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

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

    Equations
    Instances For
      theorem SupIrred.not_isMin {α : Type u_2} [SemilatticeSup α] {a : α} (ha : SupIrred a) :
      theorem SupPrime.not_isMin {α : Type u_2} [SemilatticeSup α] {a : α} (ha : SupPrime a) :
      theorem IsMin.not_supIrred {α : Type u_2} [SemilatticeSup α] {a : α} (ha : IsMin a) :
      theorem IsMin.not_supPrime {α : Type u_2} [SemilatticeSup α] {a : α} (ha : IsMin 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 : α} :
      theorem SupPrime.le_sup {α : Type u_2} [SemilatticeSup α] {a : α} {b : α} {c : α} (ha : SupPrime a) :
      a b c a b a c
      @[simp]
      @[simp]
      theorem SupIrred.ne_bot {α : Type u_2} [SemilatticeSup α] {a : α} [OrderBot α] (ha : SupIrred a) :
      theorem SupPrime.ne_bot {α : Type u_2} [SemilatticeSup α] {a : α} [OrderBot α] (ha : SupPrime 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) :
      is, 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 is, a f i
      theorem exists_supIrred_decomposition {α : Type u_2} [SemilatticeSup α] [OrderBot α] [WellFoundedLT α] (a : α) :
      ∃ (s : Finset α), s.sup id = a ∀ ⦃b : α⦄, b sSupIrred 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 : α) :

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

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

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

        Equations
        Instances For
          @[simp]
          theorem IsMax.not_infIrred {α : Type u_2} [SemilatticeInf α] {a : α} (ha : IsMax a) :
          @[simp]
          theorem IsMax.not_infPrime {α : Type u_2} [SemilatticeInf α] {a : α} (ha : IsMax 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 : α} :
          theorem InfPrime.inf_le {α : Type u_2} [SemilatticeInf α] {a : α} {b : α} {c : α} (ha : InfPrime a) :
          b c a b a c a
          theorem InfIrred.ne_top {α : Type u_2} [SemilatticeInf α] {a : α} [OrderTop α] (ha : InfIrred a) :
          theorem InfPrime.ne_top {α : Type u_2} [SemilatticeInf α] {a : α} [OrderTop α] (ha : InfPrime a) :
          theorem InfIrred.finset_inf_eq {ι : Type u_1} {α : Type u_2} [SemilatticeInf α] {a : α} [OrderTop α] {s : Finset ι} {f : ια} :
          InfIrred as.inf f = ais, 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 is, f i a
          theorem exists_infIrred_decomposition {α : Type u_2} [SemilatticeInf α] [OrderTop α] [WellFoundedGT α] (a : α) :
          ∃ (s : Finset α), s.inf id = a ∀ ⦃b : α⦄, b sInfIrred 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 aInfIrred (OrderDual.toDual a)

          Alias of the reverse direction of infIrred_toDual.

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

          Alias of the reverse direction of infPrime_toDual.

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

          Alias of the reverse direction of supIrred_ofDual.

          theorem InfPrime.ofDual {α : Type u_2} [SemilatticeSup α] {a : αᵒᵈ} :
          InfPrime aSupPrime (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 aSupIrred (OrderDual.toDual a)

          Alias of the reverse direction of supIrred_toDual.

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

          Alias of the reverse direction of supPrime_toDual.

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

          Alias of the reverse direction of infIrred_ofDual.

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

          Alias of the reverse direction of infPrime_ofDual.

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

          Alias of the reverse direction of supPrime_iff_supIrred.

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

          Alias of the reverse direction of infPrime_iff_infIrred.

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