module Order.Diagram.Meet where
Meets🔗
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 (P : Poset o ℓ) (a b glb : ⌞ P ⌟) : Type (o ⊔ ℓ) where
no-eta-equality
open Poset P
field
: glb ≤ a
meet≤l : glb ≤ b
meet≤r : (lb' : Ob) → lb' ≤ a → lb' ≤ b → lb' ≤ glb
greatest
record Meet (P : Poset o ℓ) (a b : ⌞ P ⌟) : Type (o ⊔ ℓ) where
no-eta-equality
field
: ⌞ P ⌟
glb : is-meet P a b glb
has-meet open is-meet has-meet public
open is-meet
: Poset o ℓ → Type (o ⊔ ℓ)
Has-meets = ∀ x y → Meet P x y Has-meets P
A shuffling of terms shows that being a meet is precisely being the greatest lower bound of a family of two elements.
: ∀ {a b glb} → is-meet P a b glb → is-glb P (if_then a else b) glb
is-meet→is-glb .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-meet→is-glb meet
: ∀ {F : Bool → Ob} {glb} → is-glb P F glb → is-meet P (F true) (F false) glb
is-glb→is-meet .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
is-glb→is-meet glb → lb'<a
true → lb'<b false
An important lemma about meets is that, if then the greatest lower bound of and is just
: ∀ {a b} → a ≤ b → is-meet P a b a
le→is-meet .meet≤l = ≤-refl
le→is-meet a≤b .meet≤r = a≤b
le→is-meet a≤b .greatest lb' lb'≤a _ = lb'≤a
le→is-meet a≤b
: ∀ {a b l} → a ≤ b → is-meet P a b l → a ≡ l
le-meet = meet-unique (le→is-meet a≤b) l le-meet a≤b l
As products🔗
When passing from posets to categories, meets become products: coming from the other direction, if a category has each a proposition, then products in are simply meets.
open is-product
open Product
: ∀ {a b glb : Ob} → is-meet P a b glb → Product (poset→category P) a b
is-meet→product .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 =
is-meet→product glb .is-meet.greatest _ q<a q<b
glb .has-is-product .π₁∘⟨⟩ = prop!
is-meet→product glb .has-is-product .π₂∘⟨⟩ = prop!
is-meet→product glb .has-is-product .unique _ _ = prop! is-meet→product glb