open import Cat.Prelude

open import Data.Fin.Finite

open import Order.Instances.Elements.Covariant
open import Order.Semilattice.Meet
open import Order.Instances.Props
open import Order.Instances.Upper
open import Order.Diagram.Meet
open import Order.Diagram.Glb
open import Order.Diagram.Top
open import Order.Directed
open import Order.Base

module Order.Filter where

open is-downwards-directed

Filters🔗

A subset $F \subseteq P$ is a filter when it is upwards closed and downwards directed. Explicitly:

If $x \leq y$ and $x \in F,$ then $y \in F .$
There merely exists some $x : P$ with $x \in F .$
If $x \in F$ and $y \in F,$ then there merely exists some $z \in F$ with $z \leq x$ and $z \leq y .$

More abstractly, an upper set $F \subseteq P$ is a filter if its poset of elements is downwards directed.

is-filter : ∀ {o ℓ} {P : Poset o ℓ} → (F : Upper-set P) → Type (o ⊔ ℓ)
is-filter F = is-downwards-directed (∫ F)

record Filter {o ℓ} (P : Poset o ℓ) : Type (o ⊔ ℓ) where
  no-eta-equality
  field
    filter : Upper-set P
    has-is-filter : is-filter filter

  open Monotone filter renaming (pres-≤ to F-≤) public

open Filter

{-# INLINE Filter.constructor #-}
module _ {o ℓ} {P : Poset o ℓ} where
  open Poset P
  private module ↑P = Poset (Upper-sets P)

  instance
    Membership-Filter : Membership ⌞ P ⌟ (Filter P) lzero
    Membership-Filter = record { _∈_ = λ x F → x ∈ Filter.filter F }

    Underlying-Filter : Underlying (Filter P)
    Underlying-Filter = record { ⌞_⌟ = λ F → ∫ₚ F }

    Funlike-Filter : Funlike (Filter P) ⌞ P ⌟ λ _ → Ω
    Funlike-Filter = record { _·_ = λ F x → Filter.filter F · x }

Intuitively, filters are predicates on $P$ that classify elements that are “sufficiently large”. Upwards closure dictates that filters recognize increasingly large elements, and directedness requires that two large elements must contain some large degree of overlap.

We can also turn this thinking on its head, and view of a filter on $P$ as classifying a potentially non-existent element of $P$ by describing all of the elements that lie above it. This perspective is highlighted by the following definition.

Let $x : P .$ The principal filter on $x,$ denoted $↑ x,$ consists of the set ${a : P ∣ x \leq a} .$

  ↑-is-filter : ∀ x → is-filter (↑ P x)
  ↑-is-filter x .inhabited = pure (x , pure ≤-refl)
  ↑-is-filter x .lower-bound (a , x≤a) (b , x≤b) = pure ((x , pure ≤-refl) , □-out! x≤a , □-out! x≤b)

  ↑ᶠ : ⌞ P ⌟ → Filter P
  ↑ᶠ x .filter = ↑ P x
  ↑ᶠ x .has-is-filter = ↑-is-filter x

Principal filters classify the elements of $P$ bounded below by a bona-fide element of $P,$ but this is not always the case.

Filters and meets🔗

module _ {o ℓ} {P : Poset o ℓ} where
  open Poset P

Filters are closed under binary meets and contain top elements (if they exist).

  is-filter→meet-closed
    : {F : Upper-set P} {x y x∧y : ⌞ P ⌟}
    → is-filter F
    → is-meet P x y x∧y
    → x ∈ F → y ∈ F → x∧y ∈ F
  is-filter→meet-closed {F = F} {x = x} {y = y} F-filter x∧y-meet x∈F y∈F =
    case F-filter .lower-bound (x , x∈F) (y , y∈F) of λ where
      z z∈F z≤x z≤y → F .pres-≤ (greatest z z≤x z≤y) z∈F
    where open is-meet x∧y-meet

  is-filter→contains-top
    : {F : Upper-set P} {t : ⌞ P ⌟}
    → is-filter F
    → is-top P t
    → t ∈ F
  is-filter→contains-top {F = F} F-filter t-top =
    case F-filter .inhabited of λ where
      x x∈F → F .pres-≤ (t-top x) x∈F

In particular, this means that filters are closed under finite meets.

  is-filter→finite-glb-closed
    : ∀ {κ} {Ix : Type κ} ⦃ _ : Finite Ix ⦄
    → {F : Upper-set P} {xᵢ : Ix → ⌞ P ⌟} {⋀xᵢ : ⌞ P ⌟}
    → is-filter F
    → is-glb P xᵢ ⋀xᵢ
    → (∀ i → xᵢ i ∈ F) → ⋀xᵢ ∈ F
  is-filter→finite-glb-closed {F = F} {xᵢ = xᵢ} F-filter ⋀xᵢ-glb xᵢ∈F =
    case finite-lower-bound F-filter (λ i → xᵢ i , xᵢ∈F i) of λ where
      z z∈F z≤xᵢ → F .pres-≤ (greatest z z≤xᵢ) z∈F
    where open is-glb ⋀xᵢ-glb

This means that filters preserve finite meets when viewed as monotone maps into the poset of propositions. In particular, this means a filter $F \subseteq L$ on a meet semilattice $L$ induces a meet semilattice homomorphism $F : L \to Ω .$

module _ {o ℓ} {L : Poset o ℓ} (L-slat : is-meet-semilattice L) where
  open Poset L
  open is-meet-semilattice L-slat
  open is-meet-slat-hom

  is-filter→∩-closed
    : {F : Upper-set L} {x y : ⌞ L ⌟}
    → is-filter F
    → x ∈ F → y ∈ F → (x ∩ y) ∈ F
  is-filter→∩-closed {x = x} {y = y} F-filter x∈F y∈F =
    is-filter→meet-closed F-filter (∩-meets x y) x∈F y∈F

  is-filter→is-meet-slat-hom
    : {F : Upper-set L}
    → is-filter F
    → is-meet-slat-hom F L-slat Props-is-meet-slat
  {-# INLINE is-filter→is-meet-slat-hom #-}
  is-filter→is-meet-slat-hom F-filter = record
    { ∩-≤ = λ x y (x∈F , y∈F) → is-filter→∩-closed F-filter x∈F y∈F
    ; top-≤ = λ _ → is-filter→contains-top F-filter (Top.has-top has-top)
    }

Moreover, every filter on a meet semilattice arises this way.

  is-meet-slat-hom→is-filter
    : {F : Monotone L Props}
    → is-meet-slat-hom F L-slat Props-is-meet-slat
    → is-filter F
  {-# INLINE is-meet-slat-hom→is-filter #-}
  is-meet-slat-hom→is-filter F-meet-hom = record
    { inhabited = inc (top , F-meet-hom .top-≤ tt)
    ; lower-bound = λ (x , x∈F) (y , y∈F) →
      inc ((x ∩ y , F-meet-hom .∩-≤ x y (x∈F , y∈F)) , ∩≤l , ∩≤r)
    }

Filter bases🔗

module _ {o ℓ} {P : Poset o ℓ} where
  open Poset P

An $I -indexed$ family $x_{i} : I \to P$ is a filter base of a filter $F \subseteq P$ if:

$x_{i} \in F$ for every $i : I,$ and
if $y \in F$ then there merely exists some $i : I$ such that $x_{i} \leq y .$

  record is-filter-base {κ : Level} {Ix : Type κ} (F : Filter P) (xᵢ : Ix → ⌞ P ⌟) : Type (o ⊔ ℓ ⊔ κ) where
    no-eta-equality
    private
      module F = Filter F
    field
      base∈F : ∀ i → xᵢ i ∈ F
      up-closed : ∀ y → y ∈ F → ∃[ i ∈ Ix ] (xᵢ i ≤ y)

More succinctly, $x_{i}$ is a filter base of $F$ if $F$ is the upwards closure of $x_{i} .$

    F-is-up-closure : ∀ y → y ∈ F ≃ (∃[ i ∈ Ix ] (xᵢ i ≤ y))
    F-is-up-closure y = prop-ext! (up-closed y) (rec! λ i xᵢ≤y → F.F-≤ xᵢ≤y (base∈F i))

  {-# INLINE is-filter-base.constructor #-}
  unquoteDecl H-Level-is-filter-base =
    declare-record-hlevel 1 H-Level-is-filter-base (quote is-filter-base)

  is-up-closure→is-filter-base
    : ∀ {κ} {Ix : Type κ} {F : Filter P}
    → (xᵢ : Ix → ⌞ P ⌟)
    → (∀ y → y ∈ F ≃ (∃[ i ∈ Ix ] (xᵢ i ≤ y)))
    → is-filter-base F xᵢ
  {-# INLINE is-up-closure→is-filter-base #-}
  is-up-closure→is-filter-base xᵢ F-is-up = record
    { base∈F = λ i → F-is-up.from (xᵢ i) (pure (i , ≤-refl))
    ; up-closed = λ y y∈F → F-is-up.to y y∈F
    }
    where
      module F-is-up y = Equiv (F-is-up y)

  is-up-closure≃is-filter-base
    : ∀ {κ} {Ix : Type κ} {F : Filter P}
    → (xᵢ : Ix → ⌞ P ⌟)
    → (∀ y → y ∈ F ≃ (∃[ i ∈ Ix ] (xᵢ i ≤ y))) ≃ is-filter-base F xᵢ
  is-up-closure≃is-filter-base xᵢ = prop-ext!
      (is-up-closure→is-filter-base xᵢ)
      is-filter-base.F-is-up-closure

Every principal filter $↑ x$ has a filter base that consists only of $x .$

  ↑ᶠ-filter-base : ∀ (x : ⌞ P ⌟) → is-filter-base {Ix = ⊤} (↑ᶠ x) (λ _ → x)
  ↑ᶠ-filter-base x .is-filter-base.base∈F _ = inc ≤-refl
  ↑ᶠ-filter-base x .is-filter-base.up-closed = elim! λ y x≤y → inc (tt , x≤y)