open import Cat.Prelude

open import Order.Diagram.Bottom
open import Order.Diagram.Join
open import Order.Diagram.Meet
open import Order.Diagram.Lub
open import Order.Diagram.Top
open import Order.Morphism
open import Order.Base

import Order.Reasoning

module Order.Subposet where

SubposetsπŸ”—

Let be a poset, and be a predicate on We can form a subposet of by restricting to the elements of where holds.

module _ {o β„“} (A : Poset o β„“) where
  open Order.Reasoning A

  Subposet : βˆ€ {β„“'} β†’ (P : Ob β†’ Prop β„“') β†’ Poset (o βŠ” β„“') β„“
  Subposet P .Poset.Ob = βˆ«β‚š P
  Subposet P .Poset._≀_ (a , _) (b , _) = a ≀ b
  Subposet P .Poset.≀-thin = ≀-thin
  Subposet P .Poset.≀-refl = ≀-refl
  Subposet P .Poset.≀-trans = ≀-trans
  Subposet P .Poset.≀-antisym p q =
    Ξ£-prop-path! (≀-antisym p q)

Every subposet includes into the original order it was constructed from, and this inclusion is an order embedding.

module _ {o β„“ β„“'} {A : Poset o β„“} (P : ⌞ A ⌟ β†’ Prop β„“') where
  open Order.Reasoning A

  subposet-inc : Monotone (Subposet A P) A
  subposet-inc .hom = fst
  subposet-inc .pres-≀ p = p

  subposet-inc-is-order-embedding
    : is-order-embedding (Subposet A P) A (apply subposet-inc)
  subposet-inc-is-order-embedding = _ , id-equiv

module _ {o β„“ β„“'} {A : Poset o β„“} {P : ⌞ A ⌟ β†’ Prop β„“'} where
  open Order.Reasoning A

  subposet-inc-inj
    : {x y : βˆ«β‚š P}
    β†’ subposet-inc {A = A} P # x ≑ subposet-inc {A = A} P # y
    β†’ x ≑ y
  subposet-inc-inj p = Ξ£-prop-path! p

Joins and Meets in SubposetsπŸ”—

If has joins or meets, and is closed under those joins and meets, then the subposet induced by also has those joins and meets.

  open is-meet
  open is-join
  open is-lub

  subposet-has-top
    : βˆ€ {x}
    β†’ (px : x ∈ P)
    β†’ is-top A x
    β†’ is-top (Subposet A P) (x , px)
  subposet-has-top px x-top (y , _) = x-top y

  subposet-has-bottom
    : βˆ€ {x}
    β†’ (px : x ∈ P)
    β†’ is-bottom A x
    β†’ is-bottom (Subposet A P) (x , px)
  subposet-has-bottom px x-bottom (y , _) = x-bottom y

  subposet-has-meet
    : βˆ€ {x y z}
    β†’ (px : x ∈ P) (py : y ∈ P) (pz : z ∈ P)
    β†’ is-meet A x y z
    β†’ is-meet (Subposet A P) (x , px) (y , py) (z , pz)
  subposet-has-meet px py pz z-meet .meet≀l = z-meet .meet≀l
  subposet-has-meet px py pz z-meet .meet≀r = z-meet .meet≀r
  subposet-has-meet px py pz z-meet .greatest (lb , _) = z-meet .greatest lb

  subposet-has-join
    : βˆ€ {x y z}
    β†’ (px : x ∈ P) (py : y ∈ P) (pz : z ∈ P)
    β†’ is-join A x y z
    β†’ is-join (Subposet A P) (x , px) (y , py) (z , pz)
  subposet-has-join px py pz z-join .l≀join = z-join .l≀join
  subposet-has-join px py pz z-join .r≀join = z-join .r≀join
  subposet-has-join px py pz z-join .least (lb , _) = z-join .least lb

  subposet-has-lub
    : βˆ€ {β„“α΅’} {I : Type β„“α΅’}
    β†’ {k : I β†’ Ob} {x : Ob}
    β†’ (pk : βˆ€ i β†’ k i ∈ P)
    β†’ (px : x ∈ P)
    β†’ is-lub A k x
    β†’ is-lub (Subposet A P) (Ξ» i β†’ k i , pk i) (x , px)
  subposet-has-lub pk px has-lub .fam≀lub i =
    has-lub .fam≀lub i
  subposet-has-lub pk px has-lub .least ub fam≀ub =
    has-lub .least (ub .fst) fam≀ub

  subposet-top
    : (has-top : Top A)
    β†’ Top.top has-top ∈ P
    β†’ Top (Subposet A P)
  subposet-top has-top top∈P .Top.top =
    Top.top has-top , top∈P
  subposet-top has-top top∈P .Top.has-top =
    subposet-has-top  top∈P (Top.has-top has-top)

  subposet-bottom
    : (has-bottom : Bottom A)
    β†’ Bottom.bot has-bottom ∈ P
    β†’ Bottom (Subposet A P)
  subposet-bottom has-bottom bottom∈P .Bottom.bot =
    Bottom.bot has-bottom , bottom∈P
  subposet-bottom has-bottom bottom∈P .Bottom.has-bottom =
    subposet-has-bottom bottom∈P (Bottom.has-bottom has-bottom)

  subposet-meets
    : (has-meets : Has-meets A)
    β†’ (meet∈P : βˆ€ {x y} β†’ x ∈ P β†’ y ∈ P β†’ Meet.glb (has-meets x y) ∈ P)
    β†’ (βˆ€ {x y} β†’ (px : x ∈ P) β†’ (py : y ∈ P) β†’ Meet (Subposet A P) (x , px) (y , py))
  subposet-meets has-meets meet∈P {x} {y} x∈P y∈P .Meet.glb =
    Meet.glb (has-meets x y) , meet∈P x∈P y∈P
  subposet-meets has-meets meet∈P {x} {y} x∈P y∈P .Meet.has-meet =
    subposet-has-meet x∈P y∈P (meet∈P x∈P y∈P) (Meet.has-meet (has-meets x y))

  subposet-joins
    : (has-joins : Has-joins A)
    β†’ (join∈P : βˆ€ {x y} β†’ x ∈ P β†’ y ∈ P β†’ Join.lub (has-joins x y) ∈ P)
    β†’ (βˆ€ {x y} β†’ (px : x ∈ P) β†’ (py : y ∈ P) β†’ Join (Subposet A P) (x , px) (y , py))
  subposet-joins has-joins join∈P {x} {y} x∈P y∈P .Join.lub =
    Join.lub (has-joins x y) , join∈P x∈P y∈P
  subposet-joins has-joins join∈P {x} {y} x∈P y∈P .Join.has-join =
    subposet-has-join x∈P y∈P (join∈P x∈P y∈P) (Join.has-join (has-joins x y))