# 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) [] extends :
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.

• toFun : αα
• monotone' : Monotone self.toFun
• le_closure' : ∀ (x : α), x self.toFun x

An element is less than or equal its closure

• idempotent' : ∀ (x : α), self.toFun (self.toFun x) = self.toFun x

Closures are idempotent

• IsClosed : αProp

Predicate for an element to be closed.

By default, this is defined as c.IsClosed x := (c x = x) (see isClosed_iff). We allow an override to fix definitional equalities.

• isClosed_iff : ∀ {x : α}, self.IsClosed x self.toFun x = x
Instances For
theorem ClosureOperator.le_closure' {α : Type u_1} [] (self : ) (x : α) :
x self.toFun x

An element is less than or equal its closure

theorem ClosureOperator.idempotent' {α : Type u_1} [] (self : ) (x : α) :
self.toFun (self.toFun x) = self.toFun x

Closures are idempotent

theorem ClosureOperator.isClosed_iff {α : Type u_1} [] (self : ) {x : α} :
self.IsClosed x self.toFun x = x
instance ClosureOperator.instFunLike (α : Type u_1) [] :
FunLike () α α
Equations
• = { coe := fun (c : ) => c.toOrderHom, coe_injective' := }
instance ClosureOperator.instOrderHomClass (α : Type u_1) [] :
Equations
• =
@[simp]
theorem ClosureOperator.conjBy_apply {α : Type u_4} {β : Type u_5} [] [] (c : ) (e : α ≃o β) (a : β) :
(c.conjBy e) a = (e.conj c) a
def ClosureOperator.conjBy {α : Type u_4} {β : Type u_5} [] [] (c : ) (e : α ≃o β) :

If c is a closure operator on α and e an order-isomorphism between α and β then e ∘ c ∘ e⁻¹ is a closure operator on β.

Equations
• c.conjBy e = { toFun := (e.conj c), monotone' := , le_closure' := , idempotent' := , IsClosed := fun (b : β) => c.IsClosed (e.symm b), isClosed_iff := }
Instances For
theorem ClosureOperator.conjBy_refl {α : Type u_4} [] (c : ) :
c.conjBy () = c
theorem ClosureOperator.conjBy_trans {α : Type u_4} {β : Type u_5} {γ : Type u_6} [] [] [] (e₁ : α ≃o β) (e₂ : β ≃o γ) (c : ) :
c.conjBy (e₁.trans e₂) = (c.conjBy e₁).conjBy e₂
@[simp]
theorem ClosureOperator.id_isClosed (α : Type u_1) [] :
∀ (x : α), .IsClosed x = True
@[simp]
theorem ClosureOperator.id_apply (α : Type u_1) [] (a : α) :
a = a
def ClosureOperator.id (α : Type u_1) [] :

The identity function as a closure operator.

Equations
• = { toOrderHom := OrderHom.id, le_closure' := , idempotent' := , IsClosed := fun (x : α) => True, isClosed_iff := }
Instances For
instance ClosureOperator.instInhabited (α : Type u_1) [] :
Equations
• = { default := }
theorem ClosureOperator.ext {α : Type u_1} [] (c₁ : ) (c₂ : ) :
(∀ (x : α), c₁ x = c₂ x)c₁ = c₂
@[simp]
theorem ClosureOperator.mk'_isClosed {α : Type u_1} [] (f : αα) (hf₁ : ) (hf₂ : ∀ (x : α), x f x) (hf₃ : ∀ (x : α), f (f x) f x) (x : α) :
(ClosureOperator.mk' f hf₁ hf₂ hf₃).IsClosed x = (f x = x)
@[simp]
theorem ClosureOperator.mk'_apply {α : Type u_1} [] (f : αα) (hf₁ : ) (hf₂ : ∀ (x : α), x f x) (hf₃ : ∀ (x : α), f (f x) f x) :
∀ (a : α), (ClosureOperator.mk' f hf₁ hf₂ hf₃) a = f a
def ClosureOperator.mk' {α : Type u_1} [] (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₃ = { toFun := f, monotone' := hf₁, le_closure' := hf₂, idempotent' := , IsClosed := fun (x : α) => f x = x, isClosed_iff := }
Instances For
@[simp]
theorem ClosureOperator.mk₂_isClosed {α : Type u_1} [] (f : αα) (hf : ∀ (x : α), x f x) (hmin : ∀ ⦃x y : α⦄, x f yf x f y) (x : α) :
(ClosureOperator.mk₂ f hf hmin).IsClosed x = (f x = x)
@[simp]
theorem ClosureOperator.mk₂_apply {α : Type u_1} [] (f : αα) (hf : ∀ (x : α), x f x) (hmin : ∀ ⦃x y : α⦄, x f yf x f y) :
∀ (a : α), (ClosureOperator.mk₂ f hf hmin) a = f a
def ClosureOperator.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
• ClosureOperator.mk₂ f hf hmin = { toFun := f, monotone' := , le_closure' := hf, idempotent' := , IsClosed := fun (x : α) => f x = x, isClosed_iff := }
Instances For
@[simp]
theorem ClosureOperator.ofPred_isClosed {α : Type u_1} [] (f : αα) (p : αProp) (hf : ∀ (x : α), x f x) (hfp : ∀ (x : α), p (f x)) (hmin : ∀ ⦃x y : α⦄, x yp yf x y) :
∀ (a : α), (ClosureOperator.ofPred f p hf hfp hmin).IsClosed a = p a
@[simp]
theorem ClosureOperator.ofPred_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) :
∀ (a : α), (ClosureOperator.ofPred f p hf hfp hmin) a = f a
def ClosureOperator.ofPred {α : Type u_1} [] (f : αα) (p : αProp) (hf : ∀ (x : α), x f x) (hfp : ∀ (x : α), p (f x)) (hmin : ∀ ⦃x y : α⦄, x yp yf x y) :

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
• One or more equations did not get rendered due to their size.
Instances For
theorem ClosureOperator.monotone {α : Type u_1} [] (c : ) :
theorem ClosureOperator.le_closure {α : Type u_1} [] (c : ) (x : α) :
x c 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} [] (c : ) (x : α) :
c (c x) = c x
@[simp]
theorem ClosureOperator.isClosed_closure {α : Type u_1} [] (c : ) (x : α) :
c.IsClosed (c x)
@[reducible, inline]
abbrev ClosureOperator.Closeds {α : Type u_1} [] (c : ) :
Type u_1

The type of elements closed under a closure operator.

Equations
• c.Closeds = { x : α // c.IsClosed x }
Instances For
def ClosureOperator.toCloseds {α : Type u_1} [] (c : ) (x : α) :
c.Closeds

Send an element to a closed element (by taking the closure).

Equations
• c.toCloseds x = c x,
Instances For
theorem ClosureOperator.IsClosed.closure_eq {α : Type u_1} [] {c : } {x : α} :
c.IsClosed xc x = x
theorem ClosureOperator.isClosed_iff_closure_le {α : Type u_1} [] {c : } {x : α} :
c.IsClosed x c x x
theorem ClosureOperator.setOf_isClosed_eq_range_closure {α : Type u_1} [] {c : } :
{x : α | c.IsClosed x} =

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

theorem ClosureOperator.le_closure_iff {α : Type u_1} [] {c : } {x : α} {y : α} :
x c y c x c y
@[simp]
theorem ClosureOperator.IsClosed.closure_le_iff {α : Type u_1} [] {c : } {x : α} {y : α} (hy : c.IsClosed y) :
c x y x y
theorem ClosureOperator.closure_min {α : Type u_1} [] {c : } {x : α} {y : α} (hxy : x y) (hy : c.IsClosed y) :
c x y
theorem ClosureOperator.closure_isGLB {α : Type u_1} [] {c : } (x : α) :
IsGLB {y : α | x y c.IsClosed y} (c x)
theorem ClosureOperator.ext_isClosed {α : Type u_1} [] (c₁ : ) (c₂ : ) (h : ∀ (x : α), c₁.IsClosed x c₂.IsClosed x) :
c₁ = c₂
theorem ClosureOperator.eq_ofPred_closed {α : Type u_1} [] (c : ) :
c = ClosureOperator.ofPred (c) c.IsClosed

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

@[simp]
theorem ClosureOperator.closure_top {α : Type u_1} [] [] (c : ) :
@[simp]
theorem ClosureOperator.isClosed_top {α : Type u_1} [] [] (c : ) :
c.IsClosed
theorem ClosureOperator.closure_inf_le {α : Type u_1} [] (c : ) (x : α) (y : α) :
c (x y) c x c y
theorem ClosureOperator.closure_sup_closure_le {α : Type u_1} [] (c : ) (x : α) (y : α) :
c x c y c (x y)
theorem ClosureOperator.closure_sup_closure_left {α : Type u_1} [] (c : ) (x : α) (y : α) :
c (c x y) = c (x y)
theorem ClosureOperator.closure_sup_closure_right {α : Type u_1} [] (c : ) (x : α) (y : α) :
c (x c y) = c (x y)
theorem ClosureOperator.closure_sup_closure {α : Type u_1} [] (c : ) (x : α) (y : α) :
c (c x c y) = c (x y)
@[simp]
theorem ClosureOperator.ofCompletePred_apply {α : Type u_1} [] (p : αProp) (hsinf : ∀ (s : Set α), (as, p a)p (sInf s)) (a : α) :
() a = ⨅ (b : { b : α // a b p b }), b
@[simp]
theorem ClosureOperator.ofCompletePred_isClosed {α : Type u_1} [] (p : αProp) (hsinf : ∀ (s : Set α), (as, p a)p (sInf s)) :
∀ (a : α), ().IsClosed a = p a
def ClosureOperator.ofCompletePred {α : Type u_1} [] (p : αProp) (hsinf : ∀ (s : Set α), (as, p a)p (sInf s)) :

Define a closure operator from a predicate that's preserved under infima.

Equations
Instances For
theorem ClosureOperator.sInf_isClosed {α : Type u_1} [] {c : } {S : Set α} (H : xS, c.IsClosed x) :
c.IsClosed (sInf S)
@[simp]
theorem ClosureOperator.closure_iSup_closure {α : Type u_1} {ι : Sort u_2} [] (c : ) (f : ια) :
c (⨆ (i : ι), c (f i)) = c (⨆ (i : ι), f i)
@[simp]
theorem ClosureOperator.closure_iSup₂_closure {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [] (c : ) (f : (i : ι) → κ iα) :
c (⨆ (i : ι), ⨆ (j : κ i), c (f i j)) = c (⨆ (i : ι), ⨆ (j : κ i), f i j)
@[simp]
theorem OrderIso.equivClosureOperator_apply {α : Type u_4} {β : Type u_5} [] [] (e : α ≃o β) (c : ) :
e.equivClosureOperator c = c.conjBy e
@[simp]
theorem OrderIso.equivClosureOperator_symm_apply {α : Type u_4} {β : Type u_5} [] [] (e : α ≃o β) (c : ) :
e.equivClosureOperator.symm c = c.conjBy e.symm
def OrderIso.equivClosureOperator {α : Type u_4} {β : Type u_5} [] [] (e : α ≃o β) :

Conjugating ClosureOperators on α and on β by a fixed isomorphism e : α ≃o β gives an equivalence ClosureOperator α ≃ ClosureOperator β.

Equations
• e.equivClosureOperator = { toFun := fun (c : ) => c.conjBy e, invFun := fun (c : ) => c.conjBy e.symm, left_inv := , right_inv := }
Instances For

structure LowerAdjoint {α : Type u_1} {β : Type u_4} [] [] (u : βα) :
Type (max u_1 u_4)

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.

Instances For
theorem LowerAdjoint.gc' {α : Type u_1} {β : Type u_4} [] [] {u : βα} (self : ) :
GaloisConnection self.toFun u

The underlying function is a lower adjoint.

@[simp]
theorem LowerAdjoint.id_toFun (α : Type u_1) [] (x : α) :
().toFun x = x
def LowerAdjoint.id (α : Type u_1) [] :

The identity function as a lower adjoint to itself.

Equations
• = { toFun := fun (x : α) => x, gc' := }
Instances For
instance LowerAdjoint.instInhabitedId {α : Type u_1} [] :
Equations
• LowerAdjoint.instInhabitedId = { default := }
instance LowerAdjoint.instCoeFunForall {α : Type u_1} {β : Type u_4} [] [] {u : βα} :
CoeFun () fun (x : ) => αβ
Equations
theorem LowerAdjoint.gc {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l : ) :
theorem LowerAdjoint.ext {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l₁ : ) (l₂ : ) :
l₁.toFun = l₂.toFunl₁ = l₂
theorem LowerAdjoint.monotone {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l : ) :
Monotone (u l.toFun)
theorem LowerAdjoint.le_closure {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l : ) (x : α) :
x u (l.toFun x)

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

@[simp]
theorem LowerAdjoint.closureOperator_isClosed {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l : ) (x : α) :
l.closureOperator.IsClosed x = (u (l.toFun x) = x)
@[simp]
theorem LowerAdjoint.closureOperator_apply {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l : ) (x : α) :
l.closureOperator x = u (l.toFun x)
def LowerAdjoint.closureOperator {α : Type u_1} {β : Type u_4} [] [] {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
• l.closureOperator = { toFun := fun (x : α) => u (l.toFun x), monotone' := , le_closure' := , idempotent' := , IsClosed := fun (x : α) => u (l.toFun x) = x, isClosed_iff := }
Instances For
theorem LowerAdjoint.idempotent {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l : ) (x : α) :
u (l.toFun (u (l.toFun x))) = u (l.toFun x)
theorem LowerAdjoint.le_closure_iff {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l : ) (x : α) (y : α) :
x u (l.toFun y) u (l.toFun x) u (l.toFun y)
def LowerAdjoint.closed {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l : ) :
Set α

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

Equations
• l.closed = {x : α | u (l.toFun x) = x}
Instances For
theorem LowerAdjoint.mem_closed_iff {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l : ) (x : α) :
x l.closed u (l.toFun x) = x
theorem LowerAdjoint.closure_eq_self_of_mem_closed {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l : ) {x : α} (h : x l.closed) :
u (l.toFun x) = x
theorem LowerAdjoint.mem_closed_iff_closure_le {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l : ) (x : α) :
x l.closed u (l.toFun x) x
@[simp]
theorem LowerAdjoint.closure_is_closed {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l : ) (x : α) :
u (l.toFun x) l.closed
theorem LowerAdjoint.closed_eq_range_close {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l : ) :
l.closed = 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_4} [] [] {u : βα} (l : ) (x : α) :
l.closed

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

Equations
• l.toClosed x = u (l.toFun x),
Instances For
@[simp]
theorem LowerAdjoint.closure_le_closed_iff_le {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l : ) (x : α) {y : α} (hy : l.closed y) :
u (l.toFun x) y x y
theorem LowerAdjoint.closure_top {α : Type u_1} {β : Type u_4} [] [] [] {u : βα} (l : ) :
u (l.toFun ) =
theorem LowerAdjoint.closure_inf_le {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l : ) (x : α) (y : α) :
u (l.toFun (x y)) u (l.toFun x) u (l.toFun y)
theorem LowerAdjoint.closure_sup_closure_le {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l : ) (x : α) (y : α) :
u (l.toFun x) u (l.toFun y) u (l.toFun (x y))
theorem LowerAdjoint.closure_sup_closure_left {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l : ) (x : α) (y : α) :
u (l.toFun (u (l.toFun x) y)) = u (l.toFun (x y))
theorem LowerAdjoint.closure_sup_closure_right {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l : ) (x : α) (y : α) :
u (l.toFun (x u (l.toFun y))) = u (l.toFun (x y))
theorem LowerAdjoint.closure_sup_closure {α : Type u_1} {β : Type u_4} [] [] {u : βα} (l : ) (x : α) (y : α) :
u (l.toFun (u (l.toFun x) u (l.toFun y))) = u (l.toFun (x y))
theorem LowerAdjoint.closure_iSup_closure {α : Type u_1} {ι : Sort u_2} {β : Type u_4} [] [] {u : βα} (l : ) (f : ια) :
u (l.toFun (⨆ (i : ι), u (l.toFun (f i)))) = u (l.toFun (⨆ (i : ι), f i))
theorem LowerAdjoint.closure_iSup₂_closure {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {β : Type u_4} [] [] {u : βα} (l : ) (f : (i : ι) → κ iα) :
u (l.toFun (⨆ (i : ι), ⨆ (j : κ i), u (l.toFun (f i j)))) = u (l.toFun (⨆ (i : ι), ⨆ (j : κ i), f i j))
theorem LowerAdjoint.subset_closure {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (s : Set β) :
s (l.toFun s)
theorem LowerAdjoint.not_mem_of_not_mem_closure {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) {s : Set β} {P : β} (hP : Pl.toFun s) :
Ps
theorem LowerAdjoint.le_iff_subset {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (s : Set β) (S : α) :
l.toFun s S s S
theorem LowerAdjoint.mem_iff {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (s : Set β) (x : β) :
x l.toFun s ∀ (S : α), s Sx S
theorem LowerAdjoint.eq_of_le {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) {s : Set β} {S : α} (h₁ : s S) (h₂ : S l.toFun s) :
l.toFun s = S
theorem LowerAdjoint.closure_union_closure_subset {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (x : α) (y : α) :
(l.toFun x) (l.toFun y) (l.toFun (x y))
@[simp]
theorem LowerAdjoint.closure_union_closure_left {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (x : α) (y : α) :
l.toFun ((l.toFun x) y) = l.toFun (x y)
@[simp]
theorem LowerAdjoint.closure_union_closure_right {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (x : α) (y : α) :
l.toFun (x (l.toFun y)) = l.toFun (x y)
theorem LowerAdjoint.closure_union_closure {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (x : α) (y : α) :
l.toFun ((l.toFun x) (l.toFun y)) = l.toFun (x y)
@[simp]
theorem LowerAdjoint.closure_iUnion_closure {α : Type u_1} {ι : Sort u_2} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (f : ια) :
l.toFun (⋃ (i : ι), (l.toFun (f i))) = l.toFun (⋃ (i : ι), (f i))
@[simp]
theorem LowerAdjoint.closure_iUnion₂_closure {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (f : (i : ι) → κ iα) :
l.toFun (⋃ (i : ι), ⋃ (j : κ i), (l.toFun (f i j))) = l.toFun (⋃ (i : ι), ⋃ (j : κ i), (f i j))

### Translations between GaloisConnection, LowerAdjoint, ClosureOperator#

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

Every Galois connection induces a lower adjoint.

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

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

Equations
• c.gi = { choice := fun (x : α) (hx : (c.toCloseds x) x) => x, , gc := , le_l_u := , choice_eq := }
Instances For
@[simp]
theorem closureOperator_gi_self {α : Type u_1} [] (c : ) :
.closureOperator = 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.