order.closure

# 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 := 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 galois_connection.lower_adjoint and 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 closure_operator.gi).

## Main definitions #

• closure_operator: A closure operator is a monotone function f : α → α such that ∀ x, x ≤ f x and ∀ x, f (f x) = f x.
• lower_adjoint: A lower adjoint to u : β → α is a function l : α → β such that l and u form a Galois connection.

## Implementation details #

Although 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 convex_hull.

lower_adjoint really is a semibundled structure version of galois_connection.

## References #

### Closure operator #

structure closure_operator (α : Type u_1) [preorder α] :
Type u_1

A closure operator on the preorder α is a monotone function which is extensive (every x is less than its closure) and idempotent.

Instances for closure_operator
@[protected, instance]
def closure_operator.has_coe_to_fun (α : Type u_1) [preorder α] :
(λ (_x : , α → α)
Equations
def closure_operator.simps.apply (α : Type u_1) [preorder α] (f : closure_operator α) :
α → α
Equations
def closure_operator.id (α : Type u_1)  :

The identity function as a closure operator.

Equations
@[simp]
theorem closure_operator.id_apply (α : Type u_1) (a : α) :
a = a
@[protected, instance]
def closure_operator.inhabited (α : Type u_1)  :
Equations
@[ext]
theorem closure_operator.ext {α : Type u_1} (c₁ c₂ : closure_operator α) :
c₁ = c₂c₁ = c₂
@[simp]
theorem closure_operator.mk'_apply {α : Type u_1} (f : α → α) (hf₁ : monotone f) (hf₂ : ∀ (x : α), x f x) (hf₃ : ∀ (x : α), f (f x) f x) (ᾰ : α) :
hf₁ hf₂ hf₃) = f ᾰ
def closure_operator.mk' {α : Type u_1} (f : α → α) (hf₁ : monotone f) (hf₂ : ∀ (x : α), x f x) (hf₃ : ∀ (x : α), f (f x) f x) :

Constructor for a closure operator using the weaker idempotency axiom: f (f x) ≤ f x.

Equations
@[simp]
theorem closure_operator.mk₂_apply {α : Type u_1} (f : α → α) (hf : ∀ (x : α), x f x) (hmin : ∀ ⦃x y : α⦄, x f yf x f y) (ᾰ : α) :
hf hmin) = f ᾰ
def closure_operator.mk₂ {α : Type u_1} (f : α → α) (hf : ∀ (x : α), x f x) (hmin : ∀ ⦃x y : α⦄, x f yf x f y) :

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
@[simp]
theorem closure_operator.mk₃_apply {α : Type u_1} (f : α → α) (p : α → Prop) (hf : ∀ (x : α), x f x) (hfp : ∀ (x : α), p (f x)) (hmin : ∀ ⦃x y : α⦄, x yp yf x y) (ᾰ : α) :
hf hfp hmin) = f ᾰ
def closure_operator.mk₃ {α : Type u_1} (f : α → α) (p : α → Prop) (hf : ∀ (x : α), x f x) (hfp : ∀ (x : α), p (f x)) (hmin : ∀ ⦃x y : α⦄, x yp yf x y) :

Expanded out version of mk₂. 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.

Equations
• hf hfp hmin = _
theorem closure_operator.closure_mem_mk₃ {α : Type u_1} {f : α → α} {p : α → Prop} {hf : ∀ (x : α), x f x} {hfp : ∀ (x : α), p (f x)} {hmin : ∀ ⦃x y : α⦄, x yp yf x y} (x : α) :
p ( hf hfp hmin) x)

This lemma shows that the image of x of a closure operator built from the mk₃ constructor respects p, the property that was fed into it.

theorem closure_operator.closure_le_mk₃_iff {α : Type u_1} {f : α → α} {p : α → Prop} {hf : ∀ (x : α), x f x} {hfp : ∀ (x : α), p (f x)} {hmin : ∀ ⦃x y : α⦄, x yp yf x y} {x y : α} (hxy : x y) (hy : p y) :
hf hfp hmin) x y

Analogue of closure_le_closed_iff_le but with the p that was fed into the mk₃ constructor.

theorem closure_operator.monotone {α : Type u_1} (c : closure_operator α) :
theorem closure_operator.le_closure {α : Type u_1} (c : closure_operator α) (x : α) :
x c x

Every element is less than its closure. This property is sometimes referred to as extensivity or inflationarity.

@[simp]
theorem closure_operator.idempotent {α : Type u_1} (c : closure_operator α) (x : α) :
c (c x) = c x
theorem closure_operator.le_closure_iff {α : Type u_1} (c : closure_operator α) (x y : α) :
x c y c x c y
def closure_operator.closed {α : Type u_1} (c : closure_operator α) :
set α

An element x is closed for the closure operator c if it is a fixed point for it.

Equations
theorem closure_operator.mem_closed_iff {α : Type u_1} (c : closure_operator α) (x : α) :
x c.closed c x = x
theorem closure_operator.mem_closed_iff_closure_le {α : Type u_1} (c : closure_operator α) (x : α) :
x c.closed c x x
theorem closure_operator.closure_eq_self_of_mem_closed {α : Type u_1} (c : closure_operator α) {x : α} (h : x c.closed) :
c x = x
@[simp]
theorem closure_operator.closure_is_closed {α : Type u_1} (c : closure_operator α) (x : α) :
theorem closure_operator.closed_eq_range_close {α : Type u_1} (c : closure_operator α) :

The set of closed elements for c is exactly its range.

def closure_operator.to_closed {α : Type u_1} (c : closure_operator α) (x : α) :

Send an x to an element of the set of closed elements (by taking the closure).

Equations
@[simp]
theorem closure_operator.closure_le_closed_iff_le {α : Type u_1} (c : closure_operator α) (x : α) {y : α} (hy : c.closed y) :
c x y x y
theorem closure_operator.eq_mk₃_closed {α : Type u_1} (c : closure_operator α) :
c = _ _

A closure operator is equal to the closure operator obtained by feeding c.closed into the mk₃ constructor.

theorem closure_operator.mem_mk₃_closed {α : Type u_1} {f : α → α} {p : α → Prop} {hf : ∀ (x : α), x f x} {hfp : ∀ (x : α), p (f x)} {hmin : ∀ ⦃x y : α⦄, x yp yf x y} {x : α} (hx : p x) :
x hf hfp hmin).closed

The property p fed into the mk₃ constructor implies being closed.

@[simp]
theorem closure_operator.closure_top {α : Type u_1} [order_top α] (c : closure_operator α) :
theorem closure_operator.top_mem_closed {α : Type u_1} [order_top α] (c : closure_operator α) :
theorem closure_operator.closure_inf_le {α : Type u_1} (c : closure_operator α) (x y : α) :
c (x y) c x c y
theorem closure_operator.closure_sup_closure_le {α : Type u_1} (c : closure_operator α) (x y : α) :
c x c y c (x y)
theorem closure_operator.closure_sup_closure_left {α : Type u_1} (c : closure_operator α) (x y : α) :
c (c x y) = c (x y)
theorem closure_operator.closure_sup_closure_right {α : Type u_1} (c : closure_operator α) (x y : α) :
c (x c y) = c (x y)
theorem closure_operator.closure_sup_closure {α : Type u_1} (c : closure_operator α) (x y : α) :
c (c x c y) = c (x y)
@[simp]
theorem closure_operator.closure_supr_closure {α : Type u_1} {ι : Sort u_2} (c : closure_operator α) (f : ι → α) :
c (⨆ (i : ι), c (f i)) = c (⨆ (i : ι), f i)
@[simp]
theorem closure_operator.closure_supr₂_closure {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} (c : closure_operator α) (f : Π (i : ι), κ i → α) :
c (⨆ (i : ι) (j : κ i), c (f i j)) = c (⨆ (i : ι) (j : κ i), f i j)

structure lower_adjoint {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] (u : β → α) :
Type (max u_1 u_4)
• to_fun : α → β
• gc' : u

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 coe : β → α.

Instances for lower_adjoint
@[protected]
def lower_adjoint.id (α : Type u_1) [preorder α] :

The identity function as a lower adjoint to itself.

Equations
@[simp]
theorem lower_adjoint.id_to_fun (α : Type u_1) [preorder α] (x : α) :
x = x
@[protected, instance]
def lower_adjoint.inhabited {α : Type u_1} [preorder α] :
Equations
@[protected, instance]
def lower_adjoint.has_coe_to_fun {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β → α} :
(λ (_x : , α → β)
Equations
def lower_adjoint.simps.apply {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β → α} (l : lower_adjoint u) :
α → β
Equations
theorem lower_adjoint.gc {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β → α} (l : lower_adjoint u) :
@[ext]
theorem lower_adjoint.ext {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β → α} (l₁ l₂ : lower_adjoint u) :
l₁ = l₂l₁ = l₂
theorem lower_adjoint.monotone {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β → α} (l : lower_adjoint u) :
theorem lower_adjoint.le_closure {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β → α} (l : lower_adjoint u) (x : α) :
x u (l x)

Every element is less than its closure. This property is sometimes referred to as extensivity or inflationarity.

def lower_adjoint.closure_operator {α : Type u_1} {β : Type u_4} [preorder β] {u : β → α} (l : lower_adjoint u) :

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
@[simp]
theorem lower_adjoint.closure_operator_apply {α : Type u_1} {β : Type u_4} [preorder β] {u : β → α} (l : lower_adjoint u) (x : α) :
theorem lower_adjoint.idempotent {α : Type u_1} {β : Type u_4} [preorder β] {u : β → α} (l : lower_adjoint u) (x : α) :
u (l (u (l x))) = u (l x)
theorem lower_adjoint.le_closure_iff {α : Type u_1} {β : Type u_4} [preorder β] {u : β → α} (l : lower_adjoint u) (x y : α) :
x u (l y) u (l x) u (l y)
def lower_adjoint.closed {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β → α} (l : lower_adjoint u) :
set α

An element x is closed for l : lower_adjoint u if it is a fixed point: u (l x) = x

Equations
theorem lower_adjoint.mem_closed_iff {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β → α} (l : lower_adjoint u) (x : α) :
x l.closed u (l x) = x
theorem lower_adjoint.closure_eq_self_of_mem_closed {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β → α} (l : lower_adjoint u) {x : α} (h : x l.closed) :
u (l x) = x
theorem lower_adjoint.mem_closed_iff_closure_le {α : Type u_1} {β : Type u_4} {u : β → α} (l : lower_adjoint u) (x : α) :
x l.closed u (l x) x
@[simp]
theorem lower_adjoint.closure_is_closed {α : Type u_1} {β : Type u_4} {u : β → α} (l : lower_adjoint u) (x : α) :
u (l x) l.closed
theorem lower_adjoint.closed_eq_range_close {α : Type u_1} {β : Type u_4} {u : β → α} (l : lower_adjoint u) :

The set of closed elements for l is the range of u ∘ l.

def lower_adjoint.to_closed {α : Type u_1} {β : Type u_4} {u : β → α} (l : lower_adjoint u) (x : α) :

Send an x to an element of the set of closed elements (by taking the closure).

Equations
@[simp]
theorem lower_adjoint.closure_le_closed_iff_le {α : Type u_1} {β : Type u_4} {u : β → α} (l : lower_adjoint u) (x : α) {y : α} (hy : l.closed y) :
u (l x) y x y
theorem lower_adjoint.closure_top {α : Type u_1} {β : Type u_4} [order_top α] [preorder β] {u : β → α} (l : lower_adjoint u) :
u (l ) =
theorem lower_adjoint.closure_inf_le {α : Type u_1} {β : Type u_4} [preorder β] {u : β → α} (l : lower_adjoint u) (x y : α) :
u (l (x y)) u (l x) u (l y)
theorem lower_adjoint.closure_sup_closure_le {α : Type u_1} {β : Type u_4} [preorder β] {u : β → α} (l : lower_adjoint u) (x y : α) :
u (l x) u (l y) u (l (x y))
theorem lower_adjoint.closure_sup_closure_left {α : Type u_1} {β : Type u_4} [preorder β] {u : β → α} (l : lower_adjoint u) (x y : α) :
u (l (u (l x) y)) = u (l (x y))
theorem lower_adjoint.closure_sup_closure_right {α : Type u_1} {β : Type u_4} [preorder β] {u : β → α} (l : lower_adjoint u) (x y : α) :
u (l (x u (l y))) = u (l (x y))
theorem lower_adjoint.closure_sup_closure {α : Type u_1} {β : Type u_4} [preorder β] {u : β → α} (l : lower_adjoint u) (x y : α) :
u (l (u (l x) u (l y))) = u (l (x y))
theorem lower_adjoint.closure_supr_closure {α : Type u_1} {ι : Sort u_2} {β : Type u_4} [preorder β] {u : β → α} (l : lower_adjoint u) (f : ι → α) :
u (l (⨆ (i : ι), u (l (f i)))) = u (l (⨆ (i : ι), f i))
theorem lower_adjoint.closure_supr₂_closure {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} {β : Type u_4} [preorder β] {u : β → α} (l : lower_adjoint u) (f : Π (i : ι), κ i → α) :
u (l (⨆ (i : ι) (j : κ i), u (l (f i j)))) = u (l (⨆ (i : ι) (j : κ i), f i j))
theorem lower_adjoint.subset_closure {α : Type u_1} {β : Type u_4} [ β] (l : lower_adjoint coe) (s : set β) :
s (l s)
theorem lower_adjoint.not_mem_of_not_mem_closure {α : Type u_1} {β : Type u_4} [ β] (l : lower_adjoint coe) {s : set β} {P : β} (hP : P l s) :
P s
theorem lower_adjoint.le_iff_subset {α : Type u_1} {β : Type u_4} [ β] (l : lower_adjoint coe) (s : set β) (S : α) :
l s S s S
theorem lower_adjoint.mem_iff {α : Type u_1} {β : Type u_4} [ β] (l : lower_adjoint coe) (s : set β) (x : β) :
x l s ∀ (S : α), s Sx S
theorem lower_adjoint.eq_of_le {α : Type u_1} {β : Type u_4} [ β] (l : lower_adjoint coe) {s : set β} {S : α} (h₁ : s S) (h₂ : S l s) :
l s = S
theorem lower_adjoint.closure_union_closure_subset {α : Type u_1} {β : Type u_4} [ β] (l : lower_adjoint coe) (x y : α) :
@[simp]
theorem lower_adjoint.closure_union_closure_left {α : Type u_1} {β : Type u_4} [ β] (l : lower_adjoint coe) (x y : α) :
(l ((l x) y)) = (l (x y))
@[simp]
theorem lower_adjoint.closure_union_closure_right {α : Type u_1} {β : Type u_4} [ β] (l : lower_adjoint coe) (x y : α) :
l (x (l y)) = l (x y)
@[simp]
theorem lower_adjoint.closure_union_closure {α : Type u_1} {β : Type u_4} [ β] (l : lower_adjoint coe) (x y : α) :
l ((l x) (l y)) = l (x y)
@[simp]
theorem lower_adjoint.closure_Union_closure {α : Type u_1} {ι : Sort u_2} {β : Type u_4} [ β] (l : lower_adjoint coe) (f : ι → α) :
l (⋃ (i : ι), (l (f i))) = l (⋃ (i : ι), (f i))
@[simp]
theorem lower_adjoint.closure_Union₂_closure {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} {β : Type u_4} [ β] (l : lower_adjoint coe) (f : Π (i : ι), κ i → α) :
l (⋃ (i : ι) (j : κ i), (l (f i j))) = l (⋃ (i : ι) (j : κ i), (f i j))

### Translations between galois_connection, lower_adjoint, closure_operator#

def galois_connection.lower_adjoint {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : u) :

Every Galois connection induces a lower adjoint.

Equations
@[simp]
theorem galois_connection.lower_adjoint_to_fun {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : u) (ᾰ : α) :
@[simp]
theorem galois_connection.closure_operator_apply {α : Type u_1} {β : Type u_4} [preorder β] {l : α → β} {u : β → α} (gc : u) (x : α) :
def galois_connection.closure_operator {α : Type u_1} {β : Type u_4} [preorder β] {l : α → β} {u : β → α} (gc : u) :

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
def closure_operator.gi {α : Type u_1} (c : closure_operator α) :

The set of closed elements has a Galois insertion to the underlying type.

Equations
@[simp]
theorem closure_operator_gi_self {α : Type u_1} (c : closure_operator α) :

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.