Closure operators between preorders #
We define (bundled) closure operators on a preorder as monotone (increasing), extensive (inflationary) and idempotent functions. We define closed elements for the operator as elements which are fixed by it.
Lower adjoints to a function between preorders u : β → α allow to generalise closure operators to
situations where the closure operator we are dealing with naturally decomposes as u ∘ l where l
is a worthy function to have on its own. Typical examples include
l : Set G → Subgroup G := Subgroup.closure, u : Subgroup G → Set G := (↑), where G is a group.
This shows there is a close connection between closure operators, lower adjoints and Galois
connections/insertions: every Galois connection induces a lower adjoint which itself induces a
closure operator by composition (see GaloisConnection.lowerAdjoint and
LowerAdjoint.closureOperator), and every closure operator on a partial order induces a Galois
insertion from the set of closed elements to the underlying type (see ClosureOperator.gi).
Main definitions #
ClosureOperator: A closure operator is a monotone functionf : α → αsuch that∀ x, x ≤ f xand∀ x, f (f x) = f x.LowerAdjoint: A lower adjoint tou : β → αis a functionl : α → βsuch thatlanduform a Galois connection.
Implementation details #
Although LowerAdjoint is technically a generalisation of ClosureOperator (by defining
toFun := id), it is desirable to have both as otherwise ids would be carried all over the
place when using concrete closure operators such as ConvexHull.
LowerAdjoint really is a semibundled structure version of GaloisConnection.
References #
Closure operator #
A closure operator on the preorder α is a monotone function which is extensive (every x
is less than its closure) and idempotent.
- toFun : α → α
An element is less than or equal its closure
Closures are idempotent
- IsClosed (x : α) : Prop
Predicate for an element to be closed.
By default, this is defined as
c.IsClosed x := (c x = x)(seeisClosed_iff). We allow an override to fix definitional equalities.
Equations
- ClosureOperator.instFunLike α = { coe := fun (c : ClosureOperator α) => ⇑c.toOrderHom, coe_injective' := ⋯ }
If c is a closure operator on α and e an order-isomorphism
between α and β then e ∘ c ∘ e⁻¹ is a closure operator on β.
The identity function as a closure operator.
Equations
- ClosureOperator.id α = { toOrderHom := OrderHom.id, le_closure' := ⋯, idempotent' := ⋯, IsClosed := fun (x : α) => True, isClosed_iff := ⋯ }
Equations
- ClosureOperator.instInhabited α = { default := ClosureOperator.id α }
Constructor for a closure operator using the weaker idempotency axiom: f (f x) ≤ f x.
Equations
- ClosureOperator.mk' f hf₁ hf₂ hf₃ = { toFun := f, monotone' := hf₁, le_closure' := hf₂, idempotent' := ⋯, isClosed_iff := ⋯ }
Convenience constructor for a closure operator using the weaker minimality axiom:
x ≤ f y → f x ≤ f y, which is sometimes easier to prove in practice.
Equations
- ClosureOperator.mk₂ f hf hmin = { toFun := f, monotone' := ⋯, le_closure' := hf, idempotent' := ⋯, isClosed_iff := ⋯ }
Construct a closure operator from an inflationary function f and a "closedness" predicate p
witnessing minimality of f x among closed elements greater than x.
Equations
- ClosureOperator.ofPred f p hf hfp hmin = { toOrderHom := (ClosureOperator.mk₂ f hf ⋯).toOrderHom, le_closure' := ⋯, idempotent' := ⋯, IsClosed := p, isClosed_iff := ⋯ }
Every element is less than its closure. This property is sometimes referred to as extensivity or inflationarity.
The type of elements closed under a closure operator.
Send an element to a closed element (by taking the closure).
The set of closed elements for c is exactly its range.
A closure operator is equal to the closure operator obtained by feeding c.closed into the
ofPred constructor.
Define a closure operator from a predicate that's preserved under infima.
Equations
- ClosureOperator.ofCompletePred p hsinf = ClosureOperator.ofPred (fun (a : α) => ⨅ (b : { b : α // a ≤ b ∧ p b }), ↑b) p ⋯ ⋯ ⋯
Conjugating ClosureOperators on α and on β by a fixed isomorphism
e : α ≃o β gives an equivalence ClosureOperator α ≃ ClosureOperator β.
Equations
- e.equivClosureOperator = { toFun := fun (c : ClosureOperator α) => c.conjBy e, invFun := fun (c : ClosureOperator β) => c.conjBy e.symm, left_inv := ⋯, right_inv := ⋯ }
Lower adjoint #
A lower adjoint of u on the preorder α is a function l such that l and u form a Galois
connection. It allows us to define closure operators whose output does not match the input. In
practice, u is often (↑) : β → α.
- toFun : α → β
The underlying function
- gc' : GaloisConnection self.toFun u
The underlying function is a lower adjoint.
The identity function as a lower adjoint to itself.
Equations
- LowerAdjoint.id α = { toFun := fun (x : α) => x, gc' := ⋯ }
Equations
- LowerAdjoint.instInhabitedId = { default := LowerAdjoint.id α }
Equations
- LowerAdjoint.instCoeFunForall = { coe := LowerAdjoint.toFun }
Every element is less than its closure. This property is sometimes referred to as extensivity or inflationarity.
Every lower adjoint induces a closure operator given by the composition. This is the partial order version of the statement that every adjunction induces a monad.
Equations
- l.closureOperator = { toFun := fun (x : α) => u (l.toFun x), monotone' := ⋯, le_closure' := ⋯, idempotent' := ⋯, isClosed_iff := ⋯ }
The set of closed elements for l is the range of u ∘ l.
Send an x to an element of the set of closed elements (by taking the closure).
Translations between GaloisConnection, LowerAdjoint, ClosureOperator #
Every Galois connection induces a lower adjoint.
Equations
- gc.lowerAdjoint = { toFun := l, gc' := gc }
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
The set of closed elements has a Galois insertion to the underlying type.
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.