Closure operators on a partial order #
We define (bundled) closure operators on a partial order as an monotone (increasing), extensive (inflationary) and idempotent function. We define closed elements for the operator as elements which are fixed by it.
Note that there is close connection to Galois connections and Galois insertions: every closure
operator induces a Galois insertion (from the set of closed elements to the underlying type), and
every Galois connection induces a closure operator (namely the composition). In particular,
a Galois insertion can be seen as a general case of a closure operator, where the inclusion is given
by coercion, see closure_operator.gi
.
References #
- to_preorder_hom : α →ₘ α
- le_closure' : ∀ (x : α), x ≤ c.to_preorder_hom.to_fun x
- idempotent' : ∀ (x : α), c.to_preorder_hom.to_fun (c.to_preorder_hom.to_fun x) = c.to_preorder_hom.to_fun x
A closure operator on the partial order α
is a monotone function which is extensive (every x
is less than its closure) and idempotent.
Equations
- closure_operator.has_coe_to_fun α = {F := λ (c : closure_operator α), α → α, coe := λ (c : closure_operator α), c.to_preorder_hom.to_fun}
The identity function as a closure operator.
Equations
- closure_operator.id α = {to_preorder_hom := {to_fun := λ (x : α), x, monotone' := _}, le_closure' := _, idempotent' := _}
Equations
- closure_operator.inhabited α = {default := closure_operator.id α _inst_1}
Constructor for a closure operator using the weaker idempotency axiom: f (f x) ≤ f x
.
Equations
- closure_operator.mk' f hf₁ hf₂ hf₃ = {to_preorder_hom := {to_fun := f, monotone' := hf₁}, le_closure' := hf₂, idempotent' := _}
Every element is less than its closure. This property is sometimes referred to as extensivity or inflationary.
An element x
is closed for the closure operator c
if it is a fixed point for it.
The set of closed elements for c
is exactly its range.
Send an x
to an element of the set of closed elements (by taking the closure).
The set of closed elements has a Galois insertion to the underlying type.
Every Galois connection induces a closure operator given by the composition. This is the partial order version of the statement that every adjunction induces a monad.
Equations
- gc.closure_operator = {to_preorder_hom := {to_fun := λ (x : α), u (l x), monotone' := _}, le_closure' := _, idempotent' := _}
The Galois insertion associated to a closure operator can be used to reconstruct the closure operator.
Note that the inverse in the opposite direction does not hold in general.