Join-semilattices
Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Julian KG, fernabnor and louismntnu.
Created on 2022-04-13.
Last modified on 2024-02-06.
module order-theory.join-semilattices where
Imports
open import foundation.action-on-identifications-functions open import foundation.binary-relations open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.logical-equivalences open import foundation.propositions open import foundation.sets open import foundation.subtypes open import foundation.universe-levels open import group-theory.semigroups open import order-theory.least-upper-bounds-posets open import order-theory.posets open import order-theory.preorders open import order-theory.upper-bounds-posets
Idea
A join-semilattice is a poset in which every pair of elements has a least
binary upper bound. Alternatively, join-semilattices can be defined
algebraically as a set X
equipped with a binary operation ∧ : X → X → X
satisfying
- Asociativity:
(x ∧ y) ∧ z = x ∧ (y ∧ z)
, - Commutativity:
x ∧ y = y ∧ x
, - Idempotency:
x ∧ x = x
.
Note that this definition is identical to the definition of meet-semilattices. We will follow the algebraic approach for our principal definition of join-semilattices, since it requires only one universe level. This is necessary in order to consider the large category of join-semilattices.
Definitions
The predicate on semigroups of being a join-semilattice
module _ {l : Level} (X : Semigroup l) where is-join-semilattice-prop-Semigroup : Prop l is-join-semilattice-prop-Semigroup = product-Prop ( Π-Prop ( type-Semigroup X) ( λ x → Π-Prop ( type-Semigroup X) ( λ y → Id-Prop ( set-Semigroup X) ( mul-Semigroup X x y) ( mul-Semigroup X y x)))) ( Π-Prop ( type-Semigroup X) ( λ x → Id-Prop ( set-Semigroup X) ( mul-Semigroup X x x) ( x))) is-join-semilattice-Semigroup : UU l is-join-semilattice-Semigroup = type-Prop is-join-semilattice-prop-Semigroup is-prop-is-join-semilattice-Semigroup : is-prop is-join-semilattice-Semigroup is-prop-is-join-semilattice-Semigroup = is-prop-type-Prop is-join-semilattice-prop-Semigroup
The algebraic definition of join-semilattices
Join-Semilattice : (l : Level) → UU (lsuc l) Join-Semilattice l = type-subtype is-join-semilattice-prop-Semigroup module _ {l : Level} (X : Join-Semilattice l) where semigroup-Join-Semilattice : Semigroup l semigroup-Join-Semilattice = pr1 X set-Join-Semilattice : Set l set-Join-Semilattice = set-Semigroup semigroup-Join-Semilattice type-Join-Semilattice : UU l type-Join-Semilattice = type-Semigroup semigroup-Join-Semilattice is-set-type-Join-Semilattice : is-set type-Join-Semilattice is-set-type-Join-Semilattice = is-set-type-Semigroup semigroup-Join-Semilattice join-Join-Semilattice : (x y : type-Join-Semilattice) → type-Join-Semilattice join-Join-Semilattice = mul-Semigroup semigroup-Join-Semilattice join-Join-Semilattice' : (x y : type-Join-Semilattice) → type-Join-Semilattice join-Join-Semilattice' x y = join-Join-Semilattice y x private _∨_ = join-Join-Semilattice associative-join-Join-Semilattice : (x y z : type-Join-Semilattice) → ((x ∨ y) ∨ z) = (x ∨ (y ∨ z)) associative-join-Join-Semilattice = associative-mul-Semigroup semigroup-Join-Semilattice is-join-semilattice-Join-Semilattice : is-join-semilattice-Semigroup semigroup-Join-Semilattice is-join-semilattice-Join-Semilattice = pr2 X commutative-join-Join-Semilattice : (x y : type-Join-Semilattice) → (x ∨ y) = (y ∨ x) commutative-join-Join-Semilattice = pr1 is-join-semilattice-Join-Semilattice idempotent-join-Join-Semilattice : (x : type-Join-Semilattice) → (x ∨ x) = x idempotent-join-Join-Semilattice = pr2 is-join-semilattice-Join-Semilattice leq-Join-Semilattice-Prop : (x y : type-Join-Semilattice) → Prop l leq-Join-Semilattice-Prop x y = Id-Prop set-Join-Semilattice (x ∨ y) y leq-Join-Semilattice : (x y : type-Join-Semilattice) → UU l leq-Join-Semilattice x y = type-Prop (leq-Join-Semilattice-Prop x y) is-prop-leq-Join-Semilattice : (x y : type-Join-Semilattice) → is-prop (leq-Join-Semilattice x y) is-prop-leq-Join-Semilattice x y = is-prop-type-Prop (leq-Join-Semilattice-Prop x y) private _≤_ = leq-Join-Semilattice refl-leq-Join-Semilattice : is-reflexive leq-Join-Semilattice refl-leq-Join-Semilattice x = idempotent-join-Join-Semilattice x transitive-leq-Join-Semilattice : is-transitive leq-Join-Semilattice transitive-leq-Join-Semilattice x y z H K = equational-reasoning x ∨ z = x ∨ (y ∨ z) by ap (join-Join-Semilattice x) (inv H) = (x ∨ y) ∨ z by inv (associative-join-Join-Semilattice x y z) = y ∨ z by ap (join-Join-Semilattice' z) K = z by H antisymmetric-leq-Join-Semilattice : is-antisymmetric leq-Join-Semilattice antisymmetric-leq-Join-Semilattice x y H K = equational-reasoning x = y ∨ x by inv K = x ∨ y by commutative-join-Join-Semilattice y x = y by H preorder-Join-Semilattice : Preorder l l pr1 preorder-Join-Semilattice = type-Join-Semilattice pr1 (pr2 preorder-Join-Semilattice) = leq-Join-Semilattice-Prop pr1 (pr2 (pr2 preorder-Join-Semilattice)) = refl-leq-Join-Semilattice pr2 (pr2 (pr2 preorder-Join-Semilattice)) = transitive-leq-Join-Semilattice poset-Join-Semilattice : Poset l l pr1 poset-Join-Semilattice = preorder-Join-Semilattice pr2 poset-Join-Semilattice = antisymmetric-leq-Join-Semilattice is-binary-upper-bound-join-Join-Semilattice : (x y : type-Join-Semilattice) → is-binary-upper-bound-Poset ( poset-Join-Semilattice) ( x) ( y) ( join-Join-Semilattice x y) pr1 (is-binary-upper-bound-join-Join-Semilattice x y) = equational-reasoning x ∨ (x ∨ y) = (x ∨ x) ∨ y by inv (associative-join-Join-Semilattice x x y) = x ∨ y by ap (join-Join-Semilattice' y) (idempotent-join-Join-Semilattice x) pr2 (is-binary-upper-bound-join-Join-Semilattice x y) = equational-reasoning y ∨ (x ∨ y) = (x ∨ y) ∨ y by commutative-join-Join-Semilattice y (x ∨ y) = x ∨ (y ∨ y) by associative-join-Join-Semilattice x y y = x ∨ y by ap (join-Join-Semilattice x) (idempotent-join-Join-Semilattice y) is-least-binary-upper-bound-join-Join-Semilattice : (x y : type-Join-Semilattice) → is-least-binary-upper-bound-Poset ( poset-Join-Semilattice) ( x) ( y) ( join-Join-Semilattice x y) is-least-binary-upper-bound-join-Join-Semilattice x y = prove-is-least-binary-upper-bound-Poset ( poset-Join-Semilattice) ( is-binary-upper-bound-join-Join-Semilattice x y) ( λ z (H , K) → equational-reasoning (x ∨ y) ∨ z = x ∨ (y ∨ z) by associative-join-Join-Semilattice x y z = x ∨ z by ap (join-Join-Semilattice x) K = z by H)
The predicate on posets of being a join-semilattice
module _ {l1 l2 : Level} (P : Poset l1 l2) where is-join-semilattice-Poset-Prop : Prop (l1 ⊔ l2) is-join-semilattice-Poset-Prop = Π-Prop ( type-Poset P) ( λ x → Π-Prop ( type-Poset P) ( has-least-binary-upper-bound-Poset-Prop P x)) is-join-semilattice-Poset : UU (l1 ⊔ l2) is-join-semilattice-Poset = type-Prop is-join-semilattice-Poset-Prop is-prop-is-join-semilattice-Poset : is-prop is-join-semilattice-Poset is-prop-is-join-semilattice-Poset = is-prop-type-Prop is-join-semilattice-Poset-Prop module _ (H : is-join-semilattice-Poset) where join-is-join-semilattice-Poset : type-Poset P → type-Poset P → type-Poset P join-is-join-semilattice-Poset x y = pr1 (H x y) is-least-binary-upper-bound-join-is-join-semilattice-Poset : (x y : type-Poset P) → is-least-binary-upper-bound-Poset P x y ( join-is-join-semilattice-Poset x y) is-least-binary-upper-bound-join-is-join-semilattice-Poset x y = pr2 (H x y)
The order-theoretic definition of join semilattices
Order-Theoretic-Join-Semilattice : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) Order-Theoretic-Join-Semilattice l1 l2 = Σ (Poset l1 l2) is-join-semilattice-Poset module _ {l1 l2 : Level} (A : Order-Theoretic-Join-Semilattice l1 l2) where poset-Order-Theoretic-Join-Semilattice : Poset l1 l2 poset-Order-Theoretic-Join-Semilattice = pr1 A type-Order-Theoretic-Join-Semilattice : UU l1 type-Order-Theoretic-Join-Semilattice = type-Poset poset-Order-Theoretic-Join-Semilattice is-set-type-Order-Theoretic-Join-Semilattice : is-set type-Order-Theoretic-Join-Semilattice is-set-type-Order-Theoretic-Join-Semilattice = is-set-type-Poset poset-Order-Theoretic-Join-Semilattice set-Order-Theoretic-Join-Semilattice : Set l1 set-Order-Theoretic-Join-Semilattice = set-Poset poset-Order-Theoretic-Join-Semilattice leq-Order-Theoretic-Join-Semilattice-Prop : (x y : type-Order-Theoretic-Join-Semilattice) → Prop l2 leq-Order-Theoretic-Join-Semilattice-Prop = leq-Poset-Prop poset-Order-Theoretic-Join-Semilattice leq-Order-Theoretic-Join-Semilattice : (x y : type-Order-Theoretic-Join-Semilattice) → UU l2 leq-Order-Theoretic-Join-Semilattice = leq-Poset poset-Order-Theoretic-Join-Semilattice is-prop-leq-Order-Theoretic-Join-Semilattice : (x y : type-Order-Theoretic-Join-Semilattice) → is-prop (leq-Order-Theoretic-Join-Semilattice x y) is-prop-leq-Order-Theoretic-Join-Semilattice = is-prop-leq-Poset poset-Order-Theoretic-Join-Semilattice refl-leq-Order-Theoretic-Join-Semilattice : (x : type-Order-Theoretic-Join-Semilattice) → leq-Order-Theoretic-Join-Semilattice x x refl-leq-Order-Theoretic-Join-Semilattice = refl-leq-Poset poset-Order-Theoretic-Join-Semilattice antisymmetric-leq-Order-Theoretic-Join-Semilattice : {x y : type-Order-Theoretic-Join-Semilattice} → leq-Order-Theoretic-Join-Semilattice x y → leq-Order-Theoretic-Join-Semilattice y x → x = y antisymmetric-leq-Order-Theoretic-Join-Semilattice {x} {y} = antisymmetric-leq-Poset poset-Order-Theoretic-Join-Semilattice x y transitive-leq-Order-Theoretic-Join-Semilattice : (x y z : type-Order-Theoretic-Join-Semilattice) → leq-Order-Theoretic-Join-Semilattice y z → leq-Order-Theoretic-Join-Semilattice x y → leq-Order-Theoretic-Join-Semilattice x z transitive-leq-Order-Theoretic-Join-Semilattice = transitive-leq-Poset poset-Order-Theoretic-Join-Semilattice is-join-semilattice-Order-Theoretic-Join-Semilattice : is-join-semilattice-Poset poset-Order-Theoretic-Join-Semilattice is-join-semilattice-Order-Theoretic-Join-Semilattice = pr2 A join-Order-Theoretic-Join-Semilattice : (x y : type-Order-Theoretic-Join-Semilattice) → type-Order-Theoretic-Join-Semilattice join-Order-Theoretic-Join-Semilattice = join-is-join-semilattice-Poset poset-Order-Theoretic-Join-Semilattice is-join-semilattice-Order-Theoretic-Join-Semilattice private _∨_ = join-Order-Theoretic-Join-Semilattice is-least-binary-upper-bound-join-Order-Theoretic-Join-Semilattice : (x y : type-Order-Theoretic-Join-Semilattice) → is-least-binary-upper-bound-Poset ( poset-Order-Theoretic-Join-Semilattice) ( x) ( y) ( x ∨ y) is-least-binary-upper-bound-join-Order-Theoretic-Join-Semilattice = is-least-binary-upper-bound-join-is-join-semilattice-Poset poset-Order-Theoretic-Join-Semilattice is-join-semilattice-Order-Theoretic-Join-Semilattice is-binary-upper-bound-join-Order-Theoretic-Join-Semilattice : (x y : type-Order-Theoretic-Join-Semilattice) → is-binary-upper-bound-Poset ( poset-Order-Theoretic-Join-Semilattice) ( x) ( y) ( x ∨ y) is-binary-upper-bound-join-Order-Theoretic-Join-Semilattice x y = is-binary-upper-bound-is-least-binary-upper-bound-Poset ( poset-Order-Theoretic-Join-Semilattice) ( is-least-binary-upper-bound-join-Order-Theoretic-Join-Semilattice ( x) ( y)) leq-left-join-Order-Theoretic-Join-Semilattice : (x y : type-Order-Theoretic-Join-Semilattice) → leq-Order-Theoretic-Join-Semilattice x (x ∨ y) leq-left-join-Order-Theoretic-Join-Semilattice x y = leq-left-is-binary-upper-bound-Poset ( poset-Order-Theoretic-Join-Semilattice) ( is-binary-upper-bound-join-Order-Theoretic-Join-Semilattice x y) leq-right-join-Order-Theoretic-Join-Semilattice : (x y : type-Order-Theoretic-Join-Semilattice) → leq-Order-Theoretic-Join-Semilattice y (x ∨ y) leq-right-join-Order-Theoretic-Join-Semilattice x y = leq-right-is-binary-upper-bound-Poset ( poset-Order-Theoretic-Join-Semilattice) ( is-binary-upper-bound-join-Order-Theoretic-Join-Semilattice x y) leq-join-Order-Theoretic-Join-Semilattice : {x y z : type-Order-Theoretic-Join-Semilattice} → leq-Order-Theoretic-Join-Semilattice x z → leq-Order-Theoretic-Join-Semilattice y z → leq-Order-Theoretic-Join-Semilattice (x ∨ y) z leq-join-Order-Theoretic-Join-Semilattice {x} {y} {z} H K = forward-implication ( is-least-binary-upper-bound-join-Order-Theoretic-Join-Semilattice ( x) ( y) ( z)) ( H , K)
Properties
The join operation of order theoretic join-semilattices is associative
module _ {l1 l2 : Level} (A : Order-Theoretic-Join-Semilattice l1 l2) (x y z : type-Order-Theoretic-Join-Semilattice A) where private _∨_ = join-Order-Theoretic-Join-Semilattice A _≤_ = leq-Order-Theoretic-Join-Semilattice A leq-left-triple-join-Order-Theoretic-Join-Semilattice : x ≤ ((x ∨ y) ∨ z) leq-left-triple-join-Order-Theoretic-Join-Semilattice = calculate-in-Poset ( poset-Order-Theoretic-Join-Semilattice A) chain-of-inequalities x ≤ x ∨ y by leq-left-join-Order-Theoretic-Join-Semilattice A x y in-Poset poset-Order-Theoretic-Join-Semilattice A ≤ (x ∨ y) ∨ z by leq-left-join-Order-Theoretic-Join-Semilattice A (x ∨ y) z in-Poset poset-Order-Theoretic-Join-Semilattice A leq-center-triple-join-Order-Theoretic-Join-Semilattice : y ≤ ((x ∨ y) ∨ z) leq-center-triple-join-Order-Theoretic-Join-Semilattice = calculate-in-Poset ( poset-Order-Theoretic-Join-Semilattice A) chain-of-inequalities y ≤ x ∨ y by leq-right-join-Order-Theoretic-Join-Semilattice A x y in-Poset poset-Order-Theoretic-Join-Semilattice A ≤ (x ∨ y) ∨ z by leq-left-join-Order-Theoretic-Join-Semilattice A (x ∨ y) z in-Poset poset-Order-Theoretic-Join-Semilattice A leq-right-triple-join-Order-Theoretic-Join-Semilattice : z ≤ ((x ∨ y) ∨ z) leq-right-triple-join-Order-Theoretic-Join-Semilattice = leq-right-join-Order-Theoretic-Join-Semilattice A (x ∨ y) z leq-left-triple-join-Order-Theoretic-Join-Semilattice' : x ≤ (x ∨ (y ∨ z)) leq-left-triple-join-Order-Theoretic-Join-Semilattice' = leq-left-join-Order-Theoretic-Join-Semilattice A x (y ∨ z) leq-center-triple-join-Order-Theoretic-Join-Semilattice' : y ≤ (x ∨ (y ∨ z)) leq-center-triple-join-Order-Theoretic-Join-Semilattice' = calculate-in-Poset ( poset-Order-Theoretic-Join-Semilattice A) chain-of-inequalities y ≤ y ∨ z by leq-left-join-Order-Theoretic-Join-Semilattice A y z in-Poset poset-Order-Theoretic-Join-Semilattice A ≤ x ∨ (y ∨ z) by leq-right-join-Order-Theoretic-Join-Semilattice A x (y ∨ z) in-Poset poset-Order-Theoretic-Join-Semilattice A leq-right-triple-join-Order-Theoretic-Join-Semilattice' : z ≤ (x ∨ (y ∨ z)) leq-right-triple-join-Order-Theoretic-Join-Semilattice' = calculate-in-Poset ( poset-Order-Theoretic-Join-Semilattice A) chain-of-inequalities z ≤ y ∨ z by leq-right-join-Order-Theoretic-Join-Semilattice A y z in-Poset poset-Order-Theoretic-Join-Semilattice A ≤ x ∨ (y ∨ z) by leq-right-join-Order-Theoretic-Join-Semilattice A x (y ∨ z) in-Poset poset-Order-Theoretic-Join-Semilattice A leq-associative-join-Order-Theoretic-Join-Semilattice : ((x ∨ y) ∨ z) ≤ (x ∨ (y ∨ z)) leq-associative-join-Order-Theoretic-Join-Semilattice = leq-join-Order-Theoretic-Join-Semilattice A ( leq-join-Order-Theoretic-Join-Semilattice A ( leq-left-triple-join-Order-Theoretic-Join-Semilattice') ( leq-center-triple-join-Order-Theoretic-Join-Semilattice')) ( leq-right-triple-join-Order-Theoretic-Join-Semilattice') leq-associative-join-Order-Theoretic-Join-Semilattice' : (x ∨ (y ∨ z)) ≤ ((x ∨ y) ∨ z) leq-associative-join-Order-Theoretic-Join-Semilattice' = leq-join-Order-Theoretic-Join-Semilattice A ( leq-left-triple-join-Order-Theoretic-Join-Semilattice) ( leq-join-Order-Theoretic-Join-Semilattice A ( leq-center-triple-join-Order-Theoretic-Join-Semilattice) ( leq-right-triple-join-Order-Theoretic-Join-Semilattice)) associative-join-Order-Theoretic-Join-Semilattice : ((x ∨ y) ∨ z) = (x ∨ (y ∨ z)) associative-join-Order-Theoretic-Join-Semilattice = antisymmetric-leq-Order-Theoretic-Join-Semilattice A leq-associative-join-Order-Theoretic-Join-Semilattice leq-associative-join-Order-Theoretic-Join-Semilattice'
The join operation of order theoretic join-semilattices is commutative
module _ {l1 l2 : Level} (A : Order-Theoretic-Join-Semilattice l1 l2) (x y : type-Order-Theoretic-Join-Semilattice A) where private _∨_ = join-Order-Theoretic-Join-Semilattice A _≤_ = leq-Order-Theoretic-Join-Semilattice A leq-commutative-join-Order-Theoretic-Join-Semilattice : (x ∨ y) ≤ (y ∨ x) leq-commutative-join-Order-Theoretic-Join-Semilattice = leq-join-Order-Theoretic-Join-Semilattice A ( leq-right-join-Order-Theoretic-Join-Semilattice A y x) ( leq-left-join-Order-Theoretic-Join-Semilattice A y x) leq-commutative-join-Order-Theoretic-Join-Semilattice' : (y ∨ x) ≤ (x ∨ y) leq-commutative-join-Order-Theoretic-Join-Semilattice' = leq-join-Order-Theoretic-Join-Semilattice A ( leq-right-join-Order-Theoretic-Join-Semilattice A x y) ( leq-left-join-Order-Theoretic-Join-Semilattice A x y) commutative-join-Order-Theoretic-Join-Semilattice : (x ∨ y) = (y ∨ x) commutative-join-Order-Theoretic-Join-Semilattice = antisymmetric-leq-Order-Theoretic-Join-Semilattice A leq-commutative-join-Order-Theoretic-Join-Semilattice leq-commutative-join-Order-Theoretic-Join-Semilattice'
The join operation of order theoretic join-semilattices is idempotent
module _ {l1 l2 : Level} (A : Order-Theoretic-Join-Semilattice l1 l2) (x : type-Order-Theoretic-Join-Semilattice A) where private _∨_ = join-Order-Theoretic-Join-Semilattice A _≤_ = leq-Order-Theoretic-Join-Semilattice A idempotent-join-Order-Theoretic-Join-Semilattice : (x ∨ x) = x idempotent-join-Order-Theoretic-Join-Semilattice = antisymmetric-leq-Order-Theoretic-Join-Semilattice A ( leq-join-Order-Theoretic-Join-Semilattice A ( refl-leq-Order-Theoretic-Join-Semilattice A x) ( refl-leq-Order-Theoretic-Join-Semilattice A x)) ( leq-left-join-Order-Theoretic-Join-Semilattice A x x)
Any order theoretic join-semilattice is an algebraic join semilattice
module _ {l1 l2 : Level} (A : Order-Theoretic-Join-Semilattice l1 l2) where semigroup-Order-Theoretic-Join-Semilattice : Semigroup l1 pr1 semigroup-Order-Theoretic-Join-Semilattice = set-Order-Theoretic-Join-Semilattice A pr1 (pr2 semigroup-Order-Theoretic-Join-Semilattice) = join-Order-Theoretic-Join-Semilattice A pr2 (pr2 semigroup-Order-Theoretic-Join-Semilattice) = associative-join-Order-Theoretic-Join-Semilattice A join-semilattice-Order-Theoretic-Join-Semilattice : Join-Semilattice l1 pr1 join-semilattice-Order-Theoretic-Join-Semilattice = semigroup-Order-Theoretic-Join-Semilattice pr1 (pr2 join-semilattice-Order-Theoretic-Join-Semilattice) = commutative-join-Order-Theoretic-Join-Semilattice A pr2 (pr2 join-semilattice-Order-Theoretic-Join-Semilattice) = idempotent-join-Order-Theoretic-Join-Semilattice A
Recent changes
- 2024-02-06. Fredrik Bakke. Rename
(co)prod
to(co)product
(#1017). - 2023-11-24. Egbert Rijke. Abelianization (#877).
- 2023-06-25. Fredrik Bakke, louismntnu, fernabnor, Egbert Rijke and Julian KG. Posets are categories, and refactor binary relations (#665).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-05-13. Fredrik Bakke. Remove unused imports and fix some unaddressed comments (#621).