Closure operators between preorders #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
is a worthy function to have on its own. Typical examples include
l : set G → subgroup G := subgroup.closure,
u : subgroup G → set G := coe, 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
lower_adjoint.closure_operator), and every closure operator on a partial order induces a Galois
insertion from the set of closed elements to the underlying type (see
Main definitions #
closure_operator: A closure operator is a monotone function
f : α → αsuch that
∀ x, x ≤ f xand
∀ x, f (f x) = f x.
lower_adjoint: A lower adjoint to
u : β → αis a function
l : α → βsuch that
uform a Galois connection.
Implementation details #
lower_adjoint is technically a generalisation of
closure_operator (by defining
to_fun := id), it is desirable to have both as otherwise
ids would be carried all over the
place when using concrete closure operators such as
Closure operator #
- to_order_hom : α →o α
- le_closure' : ∀ (x : α), x ≤ self.to_order_hom.to_fun x
- idempotent' : ∀ (x : α), self.to_order_hom.to_fun (self.to_order_hom.to_fun x) = self.to_order_hom.to_fun x
A closure operator on the preorder
α is a monotone function which is extensive (every
is less than its closure) and idempotent.
Constructor for a closure operator using the weaker idempotency axiom:
f (f x) ≤ f x.
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.
Expanded out version of
p implies being closed. This constructor should be used when
you already know a sufficient condition for being closed and using
mem_mk₃_closed will avoid you
the (slight) hassle of having to prove it both inside and outside the constructor.
This lemma shows that the image of
x of a closure operator built from the
p, the property that was fed into it.
closure_le_closed_iff_le but with the
p that was fed into the
p fed into the
mk₃ constructor implies being closed.
Lower adjoint #
A lower adjoint of
u on the preorder
α is a function
l such that
u form a Galois
connection. It allows us to define closure operators whose output does not match the input. In
u is often
coe : β → α.
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.
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.
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.