Order filters

Main definitions

Throughout this file, P is at least a preorder, but some sections require more structure, such as a bottom element, a top element, or a join-semilattice structure.

• Order.PFilter P: The type of nonempty, downward directed, upward closed subsets of P. This is dual to Order.Ideal, so it simply wraps Order.Ideal Pᵒᵈ.
• Order.IsPFilter P: a predicate for when a Set P is a filter.

Note the relation between Order/Filter and Order/PFilter: for any type α, Filter α represents the same mathematical object as PFilter (Set α).

References

• https://en.wikipedia.org/wiki/Filter_(mathematics)

Tags

pfilter, filter, ideal, dual

structure Order.PFilter (P : Type u_1) [Preorder P] : Type u_1

A filter on a preorder P is a subset of P that is

• nonempty
• downward directed
• upward closed.

• dual : Ideal Pᵒᵈ

def Order.IsPFilter {P : Type u_1} [Preorder P] (F : Set P) : Prop

A predicate for when a subset of P is a filter.

Equations

• Order.IsPFilter F = Order.IsIdeal (⇑OrderDual.ofDual ⁻¹' F)

theorem Order.IsPFilter.of_def {P : Type u_1} [Preorder P] {F : Set P} (nonempty : F.Nonempty) (directed : DirectedOn (fun (x1 x2 : P) => x1 ≥ x2) F) (mem_of_le : ∀ {x y : P}, x ≤ y → x ∈ F → y ∈ F) : IsPFilter F

def Order.IsPFilter.toPFilter {P : Type u_1} [Preorder P] {F : Set P} (h : IsPFilter F) : PFilter P

Create an element of type Order.PFilter from a set satisfying the predicate Order.IsPFilter.

Equations

• h.toPFilter = { dual := Order.IsIdeal.toIdeal h }

instance Order.PFilter.instInhabited {P : Type u_1} [Preorder P] [Inhabited P] : Inhabited (PFilter P)

Equations

• Order.PFilter.instInhabited = { default := { dual := default } }

instance Order.PFilter.instSetLike {P : Type u_1} [Preorder P] : SetLike (PFilter P) P

A filter on P is a subset of P.

Equations

• Order.PFilter.instSetLike = { coe := fun (F : Order.PFilter P) => ⇑OrderDual.toDual ⁻¹' F.dual.carrier, coe_injective' := ⋯ }

theorem Order.PFilter.isPFilter {P : Type u_1} [Preorder P] (F : PFilter P) : IsPFilter ↑F

theorem Order.PFilter.nonempty {P : Type u_1} [Preorder P] (F : PFilter P) : (↑F).Nonempty

theorem Order.PFilter.directed {P : Type u_1} [Preorder P] (F : PFilter P) : DirectedOn (fun (x1 x2 : P) => x1 ≥ x2) ↑F

theorem Order.PFilter.mem_of_le {P : Type u_1} [Preorder P] {x y : P} {F : PFilter P} : x ≤ y → x ∈ F → y ∈ F

theorem Order.PFilter.ext {P : Type u_1} [Preorder P] (s t : PFilter P) (h : ↑s = ↑t) : s = t

Two filters are equal when their underlying sets are equal.

theorem Order.PFilter.mem_of_mem_of_le {P : Type u_1} [Preorder P] {x : P} {F G : PFilter P} (hx : x ∈ F) (hle : F ≤ G) : x ∈ G

def Order.PFilter.principal {P : Type u_1} [Preorder P] (p : P) : PFilter P

The smallest filter containing a given element.

Equations

• Order.PFilter.principal p = { dual := Order.Ideal.principal (OrderDual.toDual p) }

@[simp]

theorem Order.PFilter.mem_mk {P : Type u_1} [Preorder P] (x : P) (I : Ideal Pᵒᵈ) : x ∈ { dual := I } ↔ OrderDual.toDual x ∈ I

@[simp]

theorem Order.PFilter.principal_le_iff {P : Type u_1} [Preorder P] {x : P} {F : PFilter P} : principal x ≤ F ↔ x ∈ F

@[simp]

theorem Order.PFilter.mem_principal {P : Type u_1} [Preorder P] {x y : P} : x ∈ principal y ↔ y ≤ x

theorem Order.PFilter.principal_le_principal_iff {P : Type u_1} [Preorder P] {p q : P} : principal q ≤ principal p ↔ p ≤ q

theorem Order.PFilter.antitone_principal {P : Type u_1} [Preorder P] : Antitone principal

@[simp]

theorem Order.PFilter.top_mem {P : Type u_1} [Preorder P] [OrderTop P] {F : PFilter P} : ⊤ ∈ F

A specific witness of pfilter.nonempty when P has a top element.

instance Order.PFilter.instOrderBot {P : Type u_1} [Preorder P] [OrderTop P] : OrderBot (PFilter P)

There is a bottom filter when P has a top element.

Equations

• Order.PFilter.instOrderBot = OrderBot.mk ⋯

instance Order.PFilter.instOrderTopOfOrderBot {P : Type u_2} [Preorder P] [OrderBot P] : OrderTop (PFilter P)

There is a top filter when P has a bottom element.

Equations

• Order.PFilter.instOrderTopOfOrderBot = OrderTop.mk ⋯

theorem Order.PFilter.inf_mem {P : Type u_1} [SemilatticeInf P] {x y : P} {F : PFilter P} (hx : x ∈ F) (hy : y ∈ F) : x ⊓ y ∈ F

A specific witness of pfilter.directed when P has meets.

@[simp]

theorem Order.PFilter.inf_mem_iff {P : Type u_1} [SemilatticeInf P] {x y : P} {F : PFilter P} : x ⊓ y ∈ F ↔ x ∈ F ∧ y ∈ F

theorem Order.PFilter.sInf_gc {P : Type u_1} [CompleteSemilatticeInf P] : GaloisConnection (fun (x : P) => OrderDual.toDual (principal x)) fun (F : (PFilter P)ᵒᵈ) => sInf ↑(OrderDual.ofDual F)

def Order.PFilter.infGi {P : Type u_1} [CompleteSemilatticeInf P] : GaloisCoinsertion (fun (x : P) => OrderDual.toDual (principal x)) fun (F : (PFilter P)ᵒᵈ) => sInf ↑(OrderDual.ofDual F)

If a poset P admits arbitrary Infs, then principal and Inf form a Galois coinsertion.

Equations

• Order.PFilter.infGi = ⋯.toGaloisCoinsertion ⋯