module Order.Diagram.Glb where
Greatest lower bounds🔗
A glb (short for greatest lower bound) for a family of elements is, as the name implies, a greatest element among the lower bounds of the . Being a lower bound means that we have for all ; Being the greatest lower bound means that if we’re given some other satisfying (for each ), then we have .
A more common word to use for “greatest lower bound” is “meet”. But since “meet” is a fairly uninformative name, and “glb” (pronounced “glib”) is just plain fun to say, we stick with the non-word for the indexed concept. However, if we’re talking about the glb of a binary family, then we use the word “meet”. The distinction here is entirely artificial, and it’s just because we can’t reuse the identifier is-glb for these two slightly different cases. Summing up: to us, a meet is a glb of two elements.
module _ {ℓ ℓ′} (P : Poset ℓ ℓ′) where private module P = Poset P record is-glb {ℓᵢ} {I : Type ℓᵢ} (F : I → P.Ob) (glb : P.Ob) : Type (ℓ ⊔ ℓ′ ⊔ ℓᵢ) where field glb≤fam : ∀ i → glb P.≤ F i greatest : (lb′ : P.Ob) → (∀ i → lb′ P.≤ F i) → lb′ P.≤ glb
open is-glb private unquoteDecl eqv = declare-record-iso eqv (quote is-glb) instance H-Level-is-glb : ∀ {ℓᵢ} {I : Type ℓᵢ} {F : I → P.Ob} {glb : P.Ob} {n} → H-Level (is-glb F glb) (suc n) H-Level-is-glb = prop-instance $ Iso→is-hlevel 1 eqv (hlevel 1) glb-unique : ∀ {ℓᵢ} {I : Type ℓᵢ} {F : I → P.Ob} → is-prop (Σ P.Ob (is-glb F)) glb-unique (glb , is) (glb′ , is′) = Σ-prop-path! $ P.≤-antisym (is′ .greatest glb (is .glb≤fam)) (is .greatest glb′ (is′ .glb≤fam))
As mentioned before, in the binary case, we refer to glbs as meets: The meet of and is, if it exists, the greatest element satisfying and .
record is-meet (a b : P.Ob) (glb : P.Ob) : Type (ℓ ⊔ ℓ′) where field meet≤l : glb P.≤ a meet≤r : glb P.≤ b greatest : (lb′ : P.Ob) → lb′ P.≤ a → lb′ P.≤ b → lb′ P.≤ glb open is-meet
A shuffling of terms shows that being a meet is precisely being the greatest lower bound of a family of two elements.
is-meet→is-glb : ∀ {a b glb} → is-meet a b glb → is-glb (if_then a else b) glb is-meet→is-glb meet .glb≤fam true = meet .meet≤l is-meet→is-glb meet .glb≤fam false = meet .meet≤r is-meet→is-glb meet .greatest glb′ x = meet .greatest glb′ (x true) (x false) is-glb→is-meet : ∀ {F : Bool → P.Ob} {glb} → is-glb F glb → is-meet (F true) (F false) glb is-glb→is-meet glb .meet≤l = glb .glb≤fam true is-glb→is-meet glb .meet≤r = glb .glb≤fam false is-glb→is-meet glb .greatest lb′ lb′<a lb′<b = glb .greatest lb′ λ where true → lb′<a false → lb′<b
private unquoteDecl eqv′ = declare-record-iso eqv′ (quote is-meet) instance H-Level-is-meet : ∀ {a b glb : P.Ob} {n} → H-Level (is-meet a b glb) (suc n) H-Level-is-meet = prop-instance $ Iso→is-hlevel 1 eqv′ (hlevel 1) open is-iso is-meet≃is-glb : ∀ {a b glb : P.Ob} → is-equiv (is-meet→is-glb {a} {b} {glb}) is-meet≃is-glb = prop-ext! _ is-glb→is-meet .snd meet-unique : ∀ {a b} → is-prop (Σ P.Ob (is-meet a b)) meet-unique {a} {b} = transport (λ i → is-prop (Σ P.Ob λ x → ua (_ , is-meet≃is-glb {a} {b} {x}) (~ i))) glb-unique
An important lemma about meets is that, if , then the greatest lower bound of and is just :
le→is-meet : ∀ {a b} → a P.≤ b → is-meet a b a le→is-meet a≤b .meet≤l = P.≤-refl le→is-meet a≤b .meet≤r = a≤b le→is-meet a≤b .greatest lb′ lb′≤a _ = lb′≤a le-meet : ∀ {a b l} → a P.≤ b → is-meet a b l → a ≡ l le-meet a≤b l = ap fst $ meet-unique (_ , le→is-meet a≤b) (_ , l)
As products🔗
The categorification of meets is products: put another way, if our category has propositional homs, then being given a product diagram is the same as being given a meet.
open is-product open Product is-meet→product : ∀ {a b glb : P.Ob} → is-meet a b glb → Product (poset→category P) a b is-meet→product glb .apex = _ is-meet→product glb .π₁ = glb .is-meet.meet≤l is-meet→product glb .π₂ = glb .is-meet.meet≤r is-meet→product glb .has-is-product .⟨_,_⟩ q<a q<b = glb .is-meet.greatest _ q<a q<b is-meet→product glb .has-is-product .π₁∘factor = prop! is-meet→product glb .has-is-product .π₂∘factor = prop! is-meet→product glb .has-is-product .unique _ _ _ = prop!