# Documentation

Mathlib.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 := (↑), 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 function f : α → α such that ∀ x, x ≤ f x and ∀ x, f (f x) = f x.
• LowerAdjoint: A lower adjoint to u : β → α is a function l : α → β such that l and u form 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 #

• https://en.wikipedia.org/wiki/Closure_operator#Closure_operators_on_partially_ordered_sets

### Closure operator #

structure ClosureOperator (α : Type u_1) [inst : ] extends :
Type u_1
• An element is less than or equal its closure

le_closure' : ∀ (x : α), x toOrderHom x
• Closures are idempotent

idempotent' : ∀ (x : α), toOrderHom (toOrderHom x) = toOrderHom x

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

Instances For
instance ClosureOperator.instCoeFunClosureOperatorForAll (α : Type u_1) [inst : ] :
CoeFun () fun x => αα
Equations
• = { coe := fun c => c.toOrderHom }
@[simp]
theorem ClosureOperator.id_apply (α : Type u_1) [inst : ] (a : α) :
().toOrderHom a = a
def ClosureOperator.id (α : Type u_1) [inst : ] :

The identity function as a closure operator.

Equations
• = { toOrderHom := OrderHom.id, le_closure' := (_ : ∀ (x : α), x x), idempotent' := (_ : ∀ (x : α), OrderHom.id (OrderHom.id x) = OrderHom.id (OrderHom.id x)) }
Equations
• = { default := }
theorem ClosureOperator.ext {α : Type u_1} [inst : ] (c₁ : ) (c₂ : ) :
c₁.toOrderHom = c₂.toOrderHomc₁ = c₂
@[simp]
theorem ClosureOperator.mk'_apply {α : Type u_1} [inst : ] (f : αα) (hf₁ : ) (hf₂ : ∀ (x : α), x f x) (hf₃ : ∀ (x : α), f (f x) f x) :
∀ (a : α), (ClosureOperator.mk' f hf₁ hf₂ hf₃).toOrderHom a = f a
def ClosureOperator.mk' {α : Type u_1} [inst : ] (f : αα) (hf₁ : ) (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
• ClosureOperator.mk' f hf₁ hf₂ hf₃ = { toOrderHom := { toFun := f, monotone' := hf₁ }, le_closure' := hf₂, idempotent' := (_ : ∀ (x : α), f (f x) = f x) }
@[simp]
theorem ClosureOperator.mk₂_apply {α : Type u_1} [inst : ] (f : αα) (hf : ∀ (x : α), x f x) (hmin : ∀ ⦃x y : α⦄, x f yf x f y) :
∀ (a : α), (ClosureOperator.mk₂ f hf hmin).toOrderHom a = f a
def ClosureOperator.mk₂ {α : Type u_1} [inst : ] (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
• ClosureOperator.mk₂ f hf hmin = { toOrderHom := { toFun := f, monotone' := (_ : ∀ (x y : α), x yf x f y) }, le_closure' := hf, idempotent' := (_ : ∀ (x : α), f (f x) = f x) }
@[simp]
theorem ClosureOperator.mk₃_apply {α : Type u_1} [inst : ] (f : αα) (p : αProp) (hf : ∀ (x : α), x f x) (hfp : (x : α) → p (f x)) (hmin : ∀ ⦃x y : α⦄, x yp yf x y) :
∀ (a : α), (ClosureOperator.mk₃ f p hf hfp hmin).toOrderHom a = f a
def ClosureOperator.mk₃ {α : Type u_1} [inst : ] (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
theorem ClosureOperator.closure_mem_mk₃ {α : Type u_1} [inst : ] {f : αα} {p : αProp} {hf : ∀ (x : α), x f x} {hfp : (x : α) → p (f x)} {hmin : ∀ ⦃x y : α⦄, x yp yf x y} (x : α) :
p ((ClosureOperator.mk₃ f p hf hfp hmin).toOrderHom 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 ClosureOperator.closure_le_mk₃_iff {α : Type u_1} [inst : ] {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) :
(ClosureOperator.mk₃ f p hf hfp hmin).toOrderHom x y

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

theorem ClosureOperator.monotone {α : Type u_1} [inst : ] (c : ) :
Monotone c.toOrderHom
theorem ClosureOperator.le_closure {α : Type u_1} [inst : ] (c : ) (x : α) :
x c.toOrderHom x

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

@[simp]
theorem ClosureOperator.idempotent {α : Type u_1} [inst : ] (c : ) (x : α) :
c.toOrderHom (c.toOrderHom x) = c.toOrderHom x
theorem ClosureOperator.le_closure_iff {α : Type u_1} [inst : ] (c : ) (x : α) (y : α) :
x c.toOrderHom y c.toOrderHom x c.toOrderHom y
def ClosureOperator.closed {α : Type u_1} [inst : ] (c : ) :
Set α

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

Equations
• = (c.toOrderHom x = x)
theorem ClosureOperator.mem_closed_iff {α : Type u_1} [inst : ] (c : ) (x : α) :
c.toOrderHom x = x
theorem ClosureOperator.mem_closed_iff_closure_le {α : Type u_1} [inst : ] (c : ) (x : α) :
c.toOrderHom x x
theorem ClosureOperator.closure_eq_self_of_mem_closed {α : Type u_1} [inst : ] (c : ) {x : α} (h : ) :
c.toOrderHom x = x
@[simp]
theorem ClosureOperator.closure_is_closed {α : Type u_1} [inst : ] (c : ) (x : α) :
c.toOrderHom x
theorem ClosureOperator.closed_eq_range_close {α : Type u_1} [inst : ] (c : ) :
= Set.range c.toOrderHom

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

def ClosureOperator.toClosed {α : Type u_1} [inst : ] (c : ) (x : α) :

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

Equations
• = { val := c.toOrderHom x, property := (_ : c.toOrderHom x ) }
@[simp]
theorem ClosureOperator.closure_le_closed_iff_le {α : Type u_1} [inst : ] (c : ) (x : α) {y : α} (hy : ) :
c.toOrderHom x y x y
theorem ClosureOperator.eq_mk₃_closed {α : Type u_1} [inst : ] (c : ) :
c = ClosureOperator.mk₃ (c.toOrderHom) () (_ : ∀ (x : α), x c.toOrderHom x) (_ : ∀ (x : α), c.toOrderHom x ) (_ : ∀ (x y : α), x yc.toOrderHom x y)

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

theorem ClosureOperator.mem_mk₃_closed {α : Type u_1} [inst : ] {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) :

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

@[simp]
theorem ClosureOperator.closure_top {α : Type u_1} [inst : ] [inst : ] (c : ) :
c.toOrderHom =
theorem ClosureOperator.top_mem_closed {α : Type u_1} [inst : ] [inst : ] (c : ) :
theorem ClosureOperator.closure_inf_le {α : Type u_1} [inst : ] (c : ) (x : α) (y : α) :
c.toOrderHom (x y) c.toOrderHom x c.toOrderHom y
theorem ClosureOperator.closure_sup_closure_le {α : Type u_1} [inst : ] (c : ) (x : α) (y : α) :
c.toOrderHom x c.toOrderHom y c.toOrderHom (x y)
theorem ClosureOperator.closure_sup_closure_left {α : Type u_1} [inst : ] (c : ) (x : α) (y : α) :
c.toOrderHom (c.toOrderHom x y) = c.toOrderHom (x y)
theorem ClosureOperator.closure_sup_closure_right {α : Type u_1} [inst : ] (c : ) (x : α) (y : α) :
c.toOrderHom (x c.toOrderHom y) = c.toOrderHom (x y)
theorem ClosureOperator.closure_sup_closure {α : Type u_1} [inst : ] (c : ) (x : α) (y : α) :
c.toOrderHom (c.toOrderHom x c.toOrderHom y) = c.toOrderHom (x y)
@[simp]
theorem ClosureOperator.closure_supᵢ_closure {α : Type u_1} {ι : Sort u_2} [inst : ] (c : ) (f : ια) :
c.toOrderHom (i, c.toOrderHom (f i)) = c.toOrderHom (i, f i)
@[simp]
theorem ClosureOperator.closure_supᵢ₂_closure {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [inst : ] (c : ) (f : (i : ι) → κ iα) :
c.toOrderHom (i, j, c.toOrderHom (f i j)) = c.toOrderHom (i, j, f i j)

structure LowerAdjoint {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (u : βα) :
Type (maxu_1u_2)
• The underlying function

toFun : αβ
• The underlying function is a lower adjoint.

gc' : GaloisConnection toFun 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 (↑) : β → α.

Instances For
@[simp]
theorem LowerAdjoint.id_toFun (α : Type u_1) [inst : ] (x : α) :
def LowerAdjoint.id (α : Type u_1) [inst : ] :

The identity function as a lower adjoint to itself.

Equations
Equations
instance LowerAdjoint.instCoeFunLowerAdjointForAll {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} :
CoeFun () fun x => αβ
Equations
theorem LowerAdjoint.gc {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) :
theorem LowerAdjoint.ext {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l₁ : ) (l₂ : ) :
l₁.toFun = l₂.toFunl₁ = l₂
theorem LowerAdjoint.monotone {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) :
Monotone (u l.toFun)
theorem LowerAdjoint.le_closure {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) (x : α) :
x u ()

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

@[simp]
theorem LowerAdjoint.closureOperator_apply {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) (x : α) :
().toOrderHom x = u ()
def LowerAdjoint.closureOperator {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) :

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
• One or more equations did not get rendered due to their size.
theorem LowerAdjoint.idempotent {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) (x : α) :
u (LowerAdjoint.toFun l (u ())) = u ()
theorem LowerAdjoint.le_closure_iff {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) (x : α) (y : α) :
x u () u () u ()
def LowerAdjoint.closed {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) :
Set α

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

Equations
• = (u () = x)
theorem LowerAdjoint.mem_closed_iff {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) (x : α) :
u () = x
theorem LowerAdjoint.closure_eq_self_of_mem_closed {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) {x : α} (h : ) :
u () = x
theorem LowerAdjoint.mem_closed_iff_closure_le {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) (x : α) :
u () x
@[simp]
theorem LowerAdjoint.closure_is_closed {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) (x : α) :
u ()
theorem LowerAdjoint.closed_eq_range_close {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) :
= Set.range (u l.toFun)

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

def LowerAdjoint.toClosed {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) (x : α) :
↑()

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

Equations
• = { val := u (), property := (_ : u () ) }
@[simp]
theorem LowerAdjoint.closure_le_closed_iff_le {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) (x : α) {y : α} (hy : ) :
u () y x y
theorem LowerAdjoint.closure_top {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : ] {u : βα} (l : ) :
u () =
theorem LowerAdjoint.closure_inf_le {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) (x : α) (y : α) :
u (LowerAdjoint.toFun l (x y)) u () u ()
theorem LowerAdjoint.closure_sup_closure_le {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) (x : α) (y : α) :
u () u () u (LowerAdjoint.toFun l (x y))
theorem LowerAdjoint.closure_sup_closure_left {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) (x : α) (y : α) :
u (LowerAdjoint.toFun l (u () y)) = u (LowerAdjoint.toFun l (x y))
theorem LowerAdjoint.closure_sup_closure_right {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) (x : α) (y : α) :
u (LowerAdjoint.toFun l (x u ())) = u (LowerAdjoint.toFun l (x y))
theorem LowerAdjoint.closure_sup_closure {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) (x : α) (y : α) :
u (LowerAdjoint.toFun l (u () u ())) = u (LowerAdjoint.toFun l (x y))
theorem LowerAdjoint.closure_supᵢ_closure {α : Type u_1} {ι : Sort u_3} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) (f : ια) :
theorem LowerAdjoint.closure_supᵢ₂_closure {α : Type u_1} {ι : Sort u_3} {κ : ιSort u_4} {β : Type u_2} [inst : ] [inst : ] {u : βα} (l : ) (f : (i : ι) → κ iα) :
u (LowerAdjoint.toFun l (i, j, u (LowerAdjoint.toFun l (f i j)))) = u (LowerAdjoint.toFun l (i, j, f i j))
theorem LowerAdjoint.subset_closure {α : Type u_2} {β : Type u_1} [inst : SetLike α β] (l : LowerAdjoint SetLike.coe) (s : Set β) :
s ↑()
theorem LowerAdjoint.not_mem_of_not_mem_closure {α : Type u_2} {β : Type u_1} [inst : SetLike α β] (l : LowerAdjoint SetLike.coe) {s : Set β} {P : β} (hP : ¬P ) :
¬P s
theorem LowerAdjoint.le_iff_subset {α : Type u_2} {β : Type u_1} [inst : SetLike α β] (l : LowerAdjoint SetLike.coe) (s : Set β) (S : α) :
S s S
theorem LowerAdjoint.mem_iff {α : Type u_2} {β : Type u_1} [inst : SetLike α β] (l : LowerAdjoint SetLike.coe) (s : Set β) (x : β) :
x ∀ (S : α), s Sx S
theorem LowerAdjoint.eq_of_le {α : Type u_2} {β : Type u_1} [inst : SetLike α β] (l : LowerAdjoint SetLike.coe) {s : Set β} {S : α} (h₁ : s S) (h₂ : S ) :
= S
theorem LowerAdjoint.closure_union_closure_subset {α : Type u_2} {β : Type u_1} [inst : SetLike α β] (l : LowerAdjoint SetLike.coe) (x : α) (y : α) :
↑() ↑() ↑(LowerAdjoint.toFun l (x y))
@[simp]
theorem LowerAdjoint.closure_union_closure_left {α : Type u_1} {β : Type u_2} [inst : SetLike α β] (l : LowerAdjoint SetLike.coe) (x : α) (y : α) :
@[simp]
theorem LowerAdjoint.closure_union_closure_right {α : Type u_1} {β : Type u_2} [inst : SetLike α β] (l : LowerAdjoint SetLike.coe) (x : α) (y : α) :
theorem LowerAdjoint.closure_union_closure {α : Type u_1} {β : Type u_2} [inst : SetLike α β] (l : LowerAdjoint SetLike.coe) (x : α) (y : α) :
@[simp]
theorem LowerAdjoint.closure_unionᵢ_closure {α : Type u_1} {ι : Sort u_3} {β : Type u_2} [inst : SetLike α β] (l : LowerAdjoint SetLike.coe) (f : ια) :
LowerAdjoint.toFun l (Set.unionᵢ fun i => ↑(LowerAdjoint.toFun l ↑(f i))) = LowerAdjoint.toFun l (Set.unionᵢ fun i => ↑(f i))
@[simp]
theorem LowerAdjoint.closure_unionᵢ₂_closure {α : Type u_1} {ι : Sort u_3} {κ : ιSort u_4} {β : Type u_2} [inst : SetLike α β] (l : LowerAdjoint SetLike.coe) (f : (i : ι) → κ iα) :
LowerAdjoint.toFun l (Set.unionᵢ fun i => Set.unionᵢ fun j => ↑(LowerAdjoint.toFun l ↑(f i j))) = LowerAdjoint.toFun l (Set.unionᵢ fun i => Set.unionᵢ fun j => ↑(f i j))

### Translations between GaloisConnection, LowerAdjoint, ClosureOperator#

@[simp]
theorem GaloisConnection.lowerAdjoint_toFun {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {l : αβ} {u : βα} (gc : ) :
∀ (a : α),
def GaloisConnection.lowerAdjoint {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {l : αβ} {u : βα} (gc : ) :

Every Galois connection induces a lower adjoint.

Equations
• = { toFun := l, gc' := gc }
@[simp]
theorem GaloisConnection.closureOperator_apply {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {l : αβ} {u : βα} (gc : ) (x : α) :
().toOrderHom x = u (l x)
def GaloisConnection.closureOperator {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {l : αβ} {u : βα} (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
def ClosureOperator.gi {α : Type u_1} [inst : ] (c : ) :
GaloisInsertion () Subtype.val

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

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem closureOperator_gi_self {α : Type u_1} [inst : ] (c : ) :

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.