From 459ea284939be269d669c45d54509ee257b1dc4e Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sat, 4 Oct 2025 18:30:18 -0700 Subject: [PATCH 1/3] Progress --- src/order-theory.lagda.md | 1 + src/order-theory/filters-posets.lagda.md | 77 ++++++++++++++++++++++++ src/order-theory/subposets.lagda.md | 5 +- 3 files changed, 81 insertions(+), 2 deletions(-) create mode 100644 src/order-theory/filters-posets.lagda.md diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md index c9e0488eec..44f1f473f1 100644 --- a/src/order-theory.lagda.md +++ b/src/order-theory.lagda.md @@ -36,6 +36,7 @@ open import order-theory.dependent-products-large-posets public open import order-theory.dependent-products-large-preorders public open import order-theory.dependent-products-large-suplattices public open import order-theory.distributive-lattices public +open import order-theory.filters-posets public open import order-theory.finite-coverings-locales public open import order-theory.finite-posets public open import order-theory.finite-preorders public diff --git a/src/order-theory/filters-posets.lagda.md b/src/order-theory/filters-posets.lagda.md new file mode 100644 index 0000000000..fc03f1024c --- /dev/null +++ b/src/order-theory/filters-posets.lagda.md @@ -0,0 +1,77 @@ +# Filters on posets + +```agda +module order-theory.filters-posets where +``` + +
Imports + +```agda +open import foundation.conjunction +open import foundation.dependent-pair-types +open import foundation.existential-quantification +open import foundation.inhabited-subtypes +open import foundation.propositions +open import foundation.subtypes +open import foundation.universe-levels + +open import order-theory.lower-bounds-posets +open import order-theory.posets +open import order-theory.subposets +``` + +
+ +## Idea + +A {{#concept "filter" WDID=Q1052692 WD="filter" Agda=Filter-Poset}} of a +[poset](order-theory.posets.md) `P` is a [subposet](order-theory.subposets.md) +`F` of `P` with the following properties: + +- [Inhabitedness](foundation.inhabited-subtypes.md): `F` is inhabited. +- Downward directedness: any two elements of `F` have a + [lower bound](order-theory.lower-bounds-posets.md) in `F`. +- Upward closure: if `x ∈ F`, `p ∈ P`, and `x ≤ p`, then `p ∈ F`. + +## Definition + +```agda +module _ + {l1 l2 l3 : Level} (P : Poset l1 l2) (F : Subposet l3 P) + where + + is-downward-directed-prop-Subposet : Prop (l1 ⊔ l2 ⊔ l3) + is-downward-directed-prop-Subposet = + Π-Prop + ( type-Subposet P F) + ( λ x → + Π-Prop + ( type-Subposet P F) + ( λ y → + ∃ ( type-Subposet P F) + ( is-binary-lower-bound-Poset-Prop (poset-Subposet P F) x y))) + + is-downward-directed-Subposet : UU (l1 ⊔ l2 ⊔ l3) + is-downward-directed-Subposet = type-Prop is-downward-directed-prop-Subposet + + is-upward-closed-prop-Subposet : Prop (l1 ⊔ l2 ⊔ l3) + is-upward-closed-prop-Subposet = + Π-Prop + ( type-Subposet P F) + ( λ (x , x∈F) → leq-prop-subtype (leq-prop-Poset P x) F) + + is-upward-closed-Subposet : UU (l1 ⊔ l2 ⊔ l3) + is-upward-closed-Subposet = type-Prop is-upward-closed-prop-Subposet + + is-filter-prop-Subposet : Prop (l1 ⊔ l2 ⊔ l3) + is-filter-prop-Subposet = + is-inhabited-subtype-Prop F ∧ is-downward-directed-prop-Subposet ∧ + is-upward-closed-prop-Subposet + + is-filter-Subposet : UU (l1 ⊔ l2 ⊔ l3) + is-filter-Subposet = type-Prop is-filter-prop-Subposet + +Filter-Poset : + {l1 l2 : Level} → (l : Level) → Poset l1 l2 → UU (l1 ⊔ l2 ⊔ lsuc l) +Filter-Poset l P = type-subtype (is-filter-prop-Subposet {l3 = l} P) +``` diff --git a/src/order-theory/subposets.lagda.md b/src/order-theory/subposets.lagda.md index d7cd52162e..fdac02b405 100644 --- a/src/order-theory/subposets.lagda.md +++ b/src/order-theory/subposets.lagda.md @@ -22,8 +22,9 @@ open import order-theory.subpreorders ## Idea -A **subposet** of a poset `P` is a subtype of `P`. By restriction of the -ordering on `P`, subposets have again the structure of a poset. +A {{#concept "subposet" Agda=Subposet}} of a [poset](order-theory.posets.md) `P` +is a [subtype](foundation.subtypes.md) of `P`. By restriction of the ordering on +`P`, subposets have again the structure of a poset. ## Definitions From a47207a9b3e7276ea060708596806861703d609e Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sat, 4 Oct 2025 18:36:48 -0700 Subject: [PATCH 2/3] Define filters on posets --- src/order-theory/filters-posets.lagda.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/order-theory/filters-posets.lagda.md b/src/order-theory/filters-posets.lagda.md index fc03f1024c..6ac526ecd9 100644 --- a/src/order-theory/filters-posets.lagda.md +++ b/src/order-theory/filters-posets.lagda.md @@ -75,3 +75,9 @@ Filter-Poset : {l1 l2 : Level} → (l : Level) → Poset l1 l2 → UU (l1 ⊔ l2 ⊔ lsuc l) Filter-Poset l P = type-subtype (is-filter-prop-Subposet {l3 = l} P) ``` + +## External links + +- [Filter (mathematics)]() + at Wikipedia +- [filter] at $n$Lab From 9d018bb99075eea875b39b605e82b2316ef86abf Mon Sep 17 00:00:00 2001 From: Louis Wasserman Date: Sat, 4 Oct 2025 18:40:05 -0700 Subject: [PATCH 3/3] Fix link --- src/order-theory/filters-posets.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/order-theory/filters-posets.lagda.md b/src/order-theory/filters-posets.lagda.md index 6ac526ecd9..d7843aa4c3 100644 --- a/src/order-theory/filters-posets.lagda.md +++ b/src/order-theory/filters-posets.lagda.md @@ -80,4 +80,4 @@ Filter-Poset l P = type-subtype (is-filter-prop-Subposet {l3 = l} P) - [Filter (mathematics)]() at Wikipedia -- [filter] at $n$Lab +- [filter](https://ncatlab.org/nlab/show/filter) at $n$Lab