From c56fde7def0733b0f3f67b3abb4b1b60b29d9683 Mon Sep 17 00:00:00 2001 From: Gabriel Lisboa Conegero Date: Mon, 8 Sep 2025 17:03:26 -0400 Subject: [PATCH 1/3] [ADD]: Add IsFilter and IsIdeal --- src/Relation/Binary/Filter.agda | 89 +++++++++++++++++++++++++++++++++ 1 file changed, 89 insertions(+) create mode 100644 src/Relation/Binary/Filter.agda diff --git a/src/Relation/Binary/Filter.agda b/src/Relation/Binary/Filter.agda new file mode 100644 index 0000000000..595a635b9d --- /dev/null +++ b/src/Relation/Binary/Filter.agda @@ -0,0 +1,89 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Structures for order-theoretic filters +------------------------------------------------------------------------ +-- As per our discussion, we should add the definition of a filter to +-- agda-stdlib. + +-- ## Background + +-- First, some background. Let (P, ≤) be a preorder (or more generally, I +-- guess just a relation `R : P → P → Set`). A *filter* of size κ in P consists of +-- a predicate `F : P → Set κ` that satisfies the following conditions: + +-- - `F` is upwards closed: if x ≤ y and F(x), then F(y) +-- - `F` is downwards directed: there exists some x with F(x), and for +-- - every x, y : P with F(x) and F(y), there exists some z : P with +-- F(z) × z ≤ x × z ≤ y + +-- Some useful facts: + +-- - If P is a meet semilattice, then conditions 1 and 2 jointly imply that +-- F(⊤), and conditions 1 and 3 mean that F(x) × F(y) → F(x ∧ y), where ∧ +-- is the meet. +-- - Alternatively, if P is a meet semilattice, then a κ-small filter is +-- equivalent to a meet semilattice homomorphism P → Type κ, where the +-- unit type is the top element, and meets are given by products of +-- types. + +-- ## Programming + +-- There does need to be some thought as to organization. We should go with +-- the definition I listed first as our primary definition, as it is the +-- most general. The useful facts would be nice to prove as theorems. + +-- Moreover, I think we should place the definition either in it's own file +-- `Relation.Binary.Filter`, or inside of a folder like +-- `Relation.Binary.Diagram.Filter`; not sure here. Theorems would be +-- somewhere in Relation.Binary.Lattice.Filter or something. + +-- We might want to factor out the "downward directed" and "upwards closed" bits into their own +-- definitions? Could also place all of this in `Relation.Binary.Subset` or +-- something, as they are all definitions regarding subsets of binary +-- relations? Note that there are also "downwards closed" and "upwards +-- directed" sets, so be careful with names! + +-- PS: for bonus points, you could also add *ideals* in a preorder: these +-- are the duals of filters; IE: downwards-closed, upwards directed. + +-- Hope that makes sense, +-- Reed :) +{-# OPTIONS --cubical-compatible --safe #-} + +module Relation.Binary.Filter where + +open import Relation.Binary.Core using (Rel) +open import Data.Product.Base using (∃-syntax; _×_; _,_) +open import Level +open import Relation.Binary.Structures using (IsPreorder) +open import Function.Base using (flip) + +private + variable + a κ ℓ₁ ℓ₂ : Level + A : Set a + +UpwardClosure : (A → Set ℓ₁) → Rel A ℓ₂ → Set _ +UpwardClosure {A = A} F _≤_ = ∀ (x y : A) → (x ≤ y) × (F x) → F y + +DownwardDirectdness : (A → Set ℓ₁) → Rel A ℓ₂ → Set _ +DownwardDirectdness {A = A} F _≤_ = (∃[ x ] F x) × (∀ x y → (F x) × (F y) → ∃[ z ] (F z × z ≤ x × z ≤ y)) + +DownwardClosure : (A → Set ℓ₁) → Rel A ℓ₂ → Set _ +DownwardClosure {A = A} F _≤_ = UpwardClosure F (flip _≤_) + +UpwardDirectdness : (A → Set ℓ₁) → Rel A ℓ₂ → Set _ +UpwardDirectdness {A = A} F _≤_ = DownwardDirectdness F (flip _≤_) + +record IsFilter {a κ ℓ} {A : Set κ} (F : A → Set κ) (_≤_ : Rel A ℓ) : Set (a ⊔ κ ⊔ ℓ) where + field + upClosed : UpwardClosure F _≤_ + downDirected : DownwardDirectdness F _≤_ + +record IsIdeal {a κ ℓ} {A : Set κ} (F : A → Set κ) (_≤_ : Rel A ℓ) : Set (a ⊔ κ ⊔ ℓ) where + field + downClosed : DownwardClosure F _≤_ + upDirected : UpwardDirectdness F _≤_ + + From 95bc37fc27c206d02890d34b0bab9e296341e04c Mon Sep 17 00:00:00 2001 From: Gabriel Lisboa Conegero Date: Mon, 8 Sep 2025 17:04:07 -0400 Subject: [PATCH 2/3] [ADD]: Add fact 0 and 1 about lattice and filters --- src/Relation/Binary/Lattice/Filter.agda | 41 +++++++++++++++++++++++++ 1 file changed, 41 insertions(+) create mode 100644 src/Relation/Binary/Lattice/Filter.agda diff --git a/src/Relation/Binary/Lattice/Filter.agda b/src/Relation/Binary/Lattice/Filter.agda new file mode 100644 index 0000000000..2779543f76 --- /dev/null +++ b/src/Relation/Binary/Lattice/Filter.agda @@ -0,0 +1,41 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties satisfied by meet semilattices +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Relation.Binary.Lattice + +module Relation.Binary.Lattice.Filter + {κ ℓ₁ ℓ₂} (P : BoundedMeetSemilattice κ ℓ₁ ℓ₂) where + +open import Function.Base using (flip; _∘_) +open import Relation.Binary.Structures using (IsDecPartialOrder) +open import Relation.Binary.Definitions using (Decidable) +open import Relation.Binary.Filter using (IsFilter) +open import Data.Product.Base using (∃-syntax; _×_; _,_; proj₁; proj₂) + +open BoundedMeetSemilattice P + +open import Relation.Binary.Lattice.Properties.MeetSemilattice meetSemilattice + +open import Relation.Binary.Properties.Poset poset using (≥-isPartialOrder) +import Relation.Binary.Lattice.Properties.JoinSemilattice as J + +-- The dual construction is a join semilattice. + +fact0 : (F : Carrier → Set κ) → IsFilter F _≤_ → F ⊤ +fact0 F filter = + let (x , Fx) = downDirected .proj₁ + in upClosed x ⊤ (maximum x , Fx) + where + open IsFilter filter + +fact1 : (F : Carrier → Set κ) → IsFilter F _≤_ → (∀ x y → F x × F y → F (x ∧ y)) +fact1 F filter x y (Fx , Fy) = + let (z , Fz , z≤x , z≤y) = downDirected .proj₂ x y (Fx , Fy) + in upClosed z (x ∧ y) (∧-greatest z≤x z≤y , Fz) + where + open IsFilter filter From 52cab95c29152bc0a961d4e62c77ae8e461ff39d Mon Sep 17 00:00:00 2001 From: Gabriel Lisboa Conegero Date: Fri, 19 Sep 2025 14:26:30 -0400 Subject: [PATCH 3/3] [REFAC]: Use Respect in upClosure definition --- src/Relation/Binary/Filter.agda | 3 ++- src/Relation/Binary/Lattice/Filter.agda | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Relation/Binary/Filter.agda b/src/Relation/Binary/Filter.agda index 595a635b9d..6f43ea74f6 100644 --- a/src/Relation/Binary/Filter.agda +++ b/src/Relation/Binary/Filter.agda @@ -57,6 +57,7 @@ open import Relation.Binary.Core using (Rel) open import Data.Product.Base using (∃-syntax; _×_; _,_) open import Level open import Relation.Binary.Structures using (IsPreorder) +open import Relation.Binary.Definitions using (_Respects_) open import Function.Base using (flip) private @@ -65,7 +66,7 @@ private A : Set a UpwardClosure : (A → Set ℓ₁) → Rel A ℓ₂ → Set _ -UpwardClosure {A = A} F _≤_ = ∀ (x y : A) → (x ≤ y) × (F x) → F y +UpwardClosure F _≤_ = F Respects _≤_ DownwardDirectdness : (A → Set ℓ₁) → Rel A ℓ₂ → Set _ DownwardDirectdness {A = A} F _≤_ = (∃[ x ] F x) × (∀ x y → (F x) × (F y) → ∃[ z ] (F z × z ≤ x × z ≤ y)) diff --git a/src/Relation/Binary/Lattice/Filter.agda b/src/Relation/Binary/Lattice/Filter.agda index 2779543f76..ba5c293afa 100644 --- a/src/Relation/Binary/Lattice/Filter.agda +++ b/src/Relation/Binary/Lattice/Filter.agda @@ -29,13 +29,13 @@ import Relation.Binary.Lattice.Properties.JoinSemilattice as J fact0 : (F : Carrier → Set κ) → IsFilter F _≤_ → F ⊤ fact0 F filter = let (x , Fx) = downDirected .proj₁ - in upClosed x ⊤ (maximum x , Fx) + in upClosed {x = x} {y = ⊤} (maximum x) Fx where open IsFilter filter fact1 : (F : Carrier → Set κ) → IsFilter F _≤_ → (∀ x y → F x × F y → F (x ∧ y)) fact1 F filter x y (Fx , Fy) = let (z , Fz , z≤x , z≤y) = downDirected .proj₂ x y (Fx , Fy) - in upClosed z (x ∧ y) (∧-greatest z≤x z≤y , Fz) + in upClosed {x = z} {y = x ∧ y} (∧-greatest z≤x z≤y) Fz where open IsFilter filter