# 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 `id`s 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 #

source
structure ClosureOperator (α : Type u_1) [Preorder α] extends α →o α :
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 (x : α) : 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

source
instance ClosureOperator.instFunLike (α : Type u_1) [Preorder α] :
FunLike (ClosureOperator α) α α
Equations

- ClosureOperator.instFunLike α = { coe := fun (c : ClosureOperator α) => ⇑c.toOrderHom, coe_injective' := ⋯ }

source
instance ClosureOperator.instOrderHomClass (α : Type u_1) [Preorder α] :
OrderHomClass (ClosureOperator α) α α
source
def ClosureOperator.conjBy {α : Type u_4} {β : Type u_5} [Preorder α] [Preorder β] (c : ClosureOperator α) (e : α ≃o β) :
ClosureOperator β

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

source
@[simp]
theorem ClosureOperator.conjBy_apply {α : Type u_4} {β : Type u_5} [Preorder α] [Preorder β] (c : ClosureOperator α) (e : α ≃o β) (a : β) :
(c.conjBy e) a = (e.conj ↑c) a
source
theorem ClosureOperator.conjBy_refl {α : Type u_4} [Preorder α] (c : ClosureOperator α) :
c.conjBy (OrderIso.refl α) = c
source
theorem ClosureOperator.conjBy_trans {α : Type u_4} {β : Type u_5} {γ : Type u_6} [Preorder α] [Preorder β] [Preorder γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) (c : ClosureOperator α) :
c.conjBy (e₁.trans e₂) = (c.conjBy e₁).conjBy e₂
source
def ClosureOperator.id (α : Type u_1) [PartialOrder α] :
ClosureOperator α

The identity function as a closure operator.

Equations

- ClosureOperator.id α = { toOrderHom := OrderHom.id, le_closure' := ⋯, idempotent' := ⋯, IsClosed := fun (x : α) => True, isClosed_iff := ⋯ }

Instances For

source
@[simp]
theorem ClosureOperator.id_apply (α : Type u_1) [PartialOrder α] (a : α) :
(id α) a = a
source
@[simp]
theorem ClosureOperator.id_isClosed (α : Type u_1) [PartialOrder α] (x✝ : α) :
(id α).IsClosed x✝ = True
source
instance ClosureOperator.instInhabited (α : Type u_1) [PartialOrder α] :
Inhabited (ClosureOperator α)
Equations

- ClosureOperator.instInhabited α = { default := ClosureOperator.id α }

source
theorem ClosureOperator.ext {α : Type u_1} [PartialOrder α] (c₁ c₂ : ClosureOperator α) :
(∀ (x : α), c₁ x = c₂ x) → c₁ = c₂
source
theorem ClosureOperator.ext_iff {α : Type u_1} [PartialOrder α] {c₁ c₂ : ClosureOperator α} :
c₁ = c₂ ↔ ∀ (x : α), c₁ x = c₂ x
source
def ClosureOperator.mk' {α : Type u_1} [PartialOrder α] (f : α → α) (hf₁ : Monotone f) (hf₂ : ∀ (x : α), x ≤ f x) (hf₃ : ∀ (x : α), f (f x) ≤ f x) :
ClosureOperator α

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 := ⋯ }

Instances For

source
@[simp]
theorem ClosureOperator.mk'_apply {α : Type u_1} [PartialOrder α] (f : α → α) (hf₁ : Monotone f) (hf₂ : ∀ (x : α), x ≤ f x) (hf₃ : ∀ (x : α), f (f x) ≤ f x) (a✝ : α) :
(mk' f hf₁ hf₂ hf₃) a✝ = f a✝
source
@[simp]
theorem ClosureOperator.mk'_isClosed {α : Type u_1} [PartialOrder α] (f : α → α) (hf₁ : Monotone f) (hf₂ : ∀ (x : α), x ≤ f x) (hf₃ : ∀ (x : α), f (f x) ≤ f x) (x : α) :
(mk' f hf₁ hf₂ hf₃).IsClosed x = (f x = x)
source
def ClosureOperator.mk₂ {α : Type u_1} [PartialOrder α] (f : α → α) (hf : ∀ (x : α), x ≤ f x) (hmin : ∀ ⦃x y : α⦄, x ≤ f y → f x ≤ f y) :
ClosureOperator α

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 := ⋯ }

Instances For

source
@[simp]
theorem ClosureOperator.mk₂_apply {α : Type u_1} [PartialOrder α] (f : α → α) (hf : ∀ (x : α), x ≤ f x) (hmin : ∀ ⦃x y : α⦄, x ≤ f y → f x ≤ f y) (a✝ : α) :
(mk₂ f hf hmin) a✝ = f a✝
source
@[simp]
theorem ClosureOperator.mk₂_isClosed {α : Type u_1} [PartialOrder α] (f : α → α) (hf : ∀ (x : α), x ≤ f x) (hmin : ∀ ⦃x y : α⦄, x ≤ f y → f x ≤ f y) (x : α) :
(mk₂ f hf hmin).IsClosed x = (f x = x)
source
def ClosureOperator.ofPred {α : Type u_1} [PartialOrder α] (f : α → α) (p : α → Prop) (hf : ∀ (x : α), x ≤ f x) (hfp : ∀ (x : α), p (f x)) (hmin : ∀ ⦃x y : α⦄, x ≤ y → p y → f x ≤ y) :
ClosureOperator α

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 := ⋯ }

Instances For

source
@[simp]
theorem ClosureOperator.ofPred_apply {α : Type u_1} [PartialOrder α] (f : α → α) (p : α → Prop) (hf : ∀ (x : α), x ≤ f x) (hfp : ∀ (x : α), p (f x)) (hmin : ∀ ⦃x y : α⦄, x ≤ y → p y → f x ≤ y) (a✝ : α) :
(ofPred f p hf hfp hmin) a✝ = f a✝
source
@[simp]
theorem ClosureOperator.ofPred_isClosed {α : Type u_1} [PartialOrder α] (f : α → α) (p : α → Prop) (hf : ∀ (x : α), x ≤ f x) (hfp : ∀ (x : α), p (f x)) (hmin : ∀ ⦃x y : α⦄, x ≤ y → p y → f x ≤ y) (a✝ : α) :
(ofPred f p hf hfp hmin).IsClosed a✝ = p a✝
source
theorem ClosureOperator.monotone {α : Type u_1} [PartialOrder α] (c : ClosureOperator α) :
Monotone ⇑c
source
theorem ClosureOperator.le_closure {α : Type u_1} [PartialOrder α] (c : ClosureOperator α) (x : α) :
x ≤ c x

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

source
@[simp]
theorem ClosureOperator.idempotent {α : Type u_1} [PartialOrder α] (c : ClosureOperator α) (x : α) :
c (c x) = c x
source
@[simp]
theorem ClosureOperator.isClosed_closure {α : Type u_1} [PartialOrder α] (c : ClosureOperator α) (x : α) :
c.IsClosed (c x)
source
@[reducible, inline]
abbrev ClosureOperator.Closeds {α : Type u_1} [PartialOrder α] (c : ClosureOperator α) :
Type u_1

The type of elements closed under a closure operator.

Equations

- c.Closeds = { x : α // c.IsClosed x }

Instances For

source
def ClosureOperator.toCloseds {α : Type u_1} [PartialOrder α] (c : ClosureOperator α) (x : α) :
c.Closeds

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

Equations

- c.toCloseds x = ⟨c x, ⋯⟩

Instances For

source
theorem ClosureOperator.IsClosed.closure_eq {α : Type u_1} [PartialOrder α] {c : ClosureOperator α} {x : α} :
c.IsClosed x → c x = x
source
theorem ClosureOperator.isClosed_iff_closure_le {α : Type u_1} [PartialOrder α] {c : ClosureOperator α} {x : α} :
c.IsClosed x ↔ c x ≤ x
source
theorem ClosureOperator.setOf_isClosed_eq_range_closure {α : Type u_1} [PartialOrder α] {c : ClosureOperator α} :
{x : α | c.IsClosed x} = Set.range ⇑c

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

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

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

source
@[simp]
theorem ClosureOperator.closure_top {α : Type u_1} [PartialOrder α] [OrderTop α] (c : ClosureOperator α) :
c ⊤ = ⊤
source
@[simp]
theorem ClosureOperator.isClosed_top {α : Type u_1} [PartialOrder α] [OrderTop α] (c : ClosureOperator α) :
c.IsClosed ⊤
source
theorem ClosureOperator.closure_inf_le {α : Type u_1} [SemilatticeInf α] (c : ClosureOperator α) (x y : α) :
c (x ⊓ y) ≤ c x ⊓ c y
source
theorem ClosureOperator.closure_sup_closure_le {α : Type u_1} [SemilatticeSup α] (c : ClosureOperator α) (x y : α) :
c x ⊔ c y ≤ c (x ⊔ y)
source
theorem ClosureOperator.closure_sup_closure_left {α : Type u_1} [SemilatticeSup α] (c : ClosureOperator α) (x y : α) :
c (c x ⊔ y) = c (x ⊔ y)
source
theorem ClosureOperator.closure_sup_closure_right {α : Type u_1} [SemilatticeSup α] (c : ClosureOperator α) (x y : α) :
c (x ⊔ c y) = c (x ⊔ y)
source
theorem ClosureOperator.closure_sup_closure {α : Type u_1} [SemilatticeSup α] (c : ClosureOperator α) (x y : α) :
c (c x ⊔ c y) = c (x ⊔ y)
source
def ClosureOperator.ofCompletePred {α : Type u_1} [CompleteLattice α] (p : α → Prop) (hsinf : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)) :
ClosureOperator α

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 ⋯ ⋯ ⋯

Instances For

source
@[simp]
theorem ClosureOperator.ofCompletePred_apply {α : Type u_1} [CompleteLattice α] (p : α → Prop) (hsinf : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)) (a : α) :
(ofCompletePred p hsinf) a = ⨅ (b : { b : α // a ≤ b ∧ p b }), ↑b
source
@[simp]
theorem ClosureOperator.ofCompletePred_isClosed {α : Type u_1} [CompleteLattice α] (p : α → Prop) (hsinf : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)) (a✝ : α) :
(ofCompletePred p hsinf).IsClosed a✝ = p a✝
source
theorem ClosureOperator.sInf_isClosed {α : Type u_1} [CompleteLattice α] {c : ClosureOperator α} {S : Set α} (H : ∀ x ∈ S, c.IsClosed x) :
c.IsClosed (sInf S)
source
@[simp]
theorem ClosureOperator.closure_iSup_closure {α : Type u_1} {ι : Sort u_2} [CompleteLattice α] (c : ClosureOperator α) (f : ι → α) :
c (⨆ (i : ι), c (f i)) = c (⨆ (i : ι), f i)
source
@[simp]
theorem ClosureOperator.closure_iSup₂_closure {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [CompleteLattice α] (c : ClosureOperator α) (f : (i : ι) → κ i → α) :
c (⨆ (i : ι), ⨆ (j : κ i), c (f i j)) = c (⨆ (i : ι), ⨆ (j : κ i), f i j)
source
def OrderIso.equivClosureOperator {α : Type u_4} {β : Type u_5} [Preorder α] [Preorder β] (e : α ≃o β) :
ClosureOperator α ≃ ClosureOperator β

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 := ⋯ }

Instances For

source
@[simp]
theorem OrderIso.equivClosureOperator_apply {α : Type u_4} {β : Type u_5} [Preorder α] [Preorder β] (e : α ≃o β) (c : ClosureOperator α) :
e.equivClosureOperator c = c.conjBy e
source
@[simp]
theorem OrderIso.equivClosureOperator_symm_apply {α : Type u_4} {β : Type u_5} [Preorder α] [Preorder β] (e : α ≃o β) (c : ClosureOperator β) :
e.equivClosureOperator.symm c = c.conjBy e.symm

### Lower adjoint #

source
structure LowerAdjoint {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] (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

source
def LowerAdjoint.id (α : Type u_1) [Preorder α] :
LowerAdjoint id

The identity function as a lower adjoint to itself.

Equations

- LowerAdjoint.id α = { toFun := fun (x : α) => x, gc' := ⋯ }

Instances For

source
@[simp]
theorem LowerAdjoint.id_toFun (α : Type u_1) [Preorder α] (x : α) :
(LowerAdjoint.id α).toFun x = x
source
instance LowerAdjoint.instInhabitedId {α : Type u_1} [Preorder α] :
Inhabited (LowerAdjoint id)
Equations

- LowerAdjoint.instInhabitedId = { default := LowerAdjoint.id α }

source
instance LowerAdjoint.instCoeFunForall {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : β → α} :
CoeFun (LowerAdjoint u) fun (x : LowerAdjoint u) => α → β
Equations

- LowerAdjoint.instCoeFunForall = { coe := LowerAdjoint.toFun }

source
theorem LowerAdjoint.gc {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : β → α} (l : LowerAdjoint u) :
GaloisConnection l.toFun u
source
theorem LowerAdjoint.ext {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : β → α} (l₁ l₂ : LowerAdjoint u) :
l₁.toFun = l₂.toFun → l₁ = l₂
source
theorem LowerAdjoint.ext_iff {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : β → α} {l₁ l₂ : LowerAdjoint u} :
l₁ = l₂ ↔ l₁.toFun = l₂.toFun
source
theorem LowerAdjoint.monotone {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : β → α} (l : LowerAdjoint u) :
Monotone (u ∘ l.toFun)
source
theorem LowerAdjoint.le_closure {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α) :
x ≤ u (l.toFun x)

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

source
def LowerAdjoint.closureOperator {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {u : β → α} (l : LowerAdjoint u) :
ClosureOperator α

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 := ⋯ }

Instances For

source
@[simp]
theorem LowerAdjoint.closureOperator_isClosed {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α) :
l.closureOperator.IsClosed x = ((fun (x : α) => u (l.toFun x)) x = x)
source
@[simp]
theorem LowerAdjoint.closureOperator_apply {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α) :
l.closureOperator x = u (l.toFun x)
source
theorem LowerAdjoint.idempotent {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α) :
u (l.toFun (u (l.toFun x))) = u (l.toFun x)
source
theorem LowerAdjoint.le_closure_iff {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {u : β → α} (l : LowerAdjoint u) (x y : α) :
x ≤ u (l.toFun y) ↔ u (l.toFun x) ≤ u (l.toFun y)
source
def LowerAdjoint.closed {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : β → α} (l : LowerAdjoint u) :
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

source
theorem LowerAdjoint.mem_closed_iff {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α) :
x ∈ l.closed ↔ u (l.toFun x) = x
source
theorem LowerAdjoint.closure_eq_self_of_mem_closed {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : β → α} (l : LowerAdjoint u) {x : α} (h : x ∈ l.closed) :
u (l.toFun x) = x
source
theorem LowerAdjoint.mem_closed_iff_closure_le {α : Type u_1} {β : Type u_4} [PartialOrder α] [PartialOrder β] {u : β → α} (l : LowerAdjoint u) (x : α) :
x ∈ l.closed ↔ u (l.toFun x) ≤ x
source
@[simp]
theorem LowerAdjoint.closure_is_closed {α : Type u_1} {β : Type u_4} [PartialOrder α] [PartialOrder β] {u : β → α} (l : LowerAdjoint u) (x : α) :
u (l.toFun x) ∈ l.closed
source
theorem LowerAdjoint.closed_eq_range_close {α : Type u_1} {β : Type u_4} [PartialOrder α] [PartialOrder β] {u : β → α} (l : LowerAdjoint u) :
l.closed = Set.range (u ∘ l.toFun)

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

source
def LowerAdjoint.toClosed {α : Type u_1} {β : Type u_4} [PartialOrder α] [PartialOrder β] {u : β → α} (l : LowerAdjoint u) (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

source
@[simp]
theorem LowerAdjoint.closure_le_closed_iff_le {α : Type u_1} {β : Type u_4} [PartialOrder α] [PartialOrder β] {u : β → α} (l : LowerAdjoint u) (x : α) {y : α} (hy : l.closed y) :
u (l.toFun x) ≤ y ↔ x ≤ y
source
theorem LowerAdjoint.closure_top {α : Type u_1} {β : Type u_4} [PartialOrder α] [OrderTop α] [Preorder β] {u : β → α} (l : LowerAdjoint u) :
u (l.toFun ⊤) = ⊤
source
theorem LowerAdjoint.closure_inf_le {α : Type u_1} {β : Type u_4} [SemilatticeInf α] [Preorder β] {u : β → α} (l : LowerAdjoint u) (x y : α) :
u (l.toFun (x ⊓ y)) ≤ u (l.toFun x) ⊓ u (l.toFun y)
source
theorem LowerAdjoint.closure_sup_closure_le {α : Type u_1} {β : Type u_4} [SemilatticeSup α] [Preorder β] {u : β → α} (l : LowerAdjoint u) (x y : α) :
u (l.toFun x) ⊔ u (l.toFun y) ≤ u (l.toFun (x ⊔ y))
source
theorem LowerAdjoint.closure_sup_closure_left {α : Type u_1} {β : Type u_4} [SemilatticeSup α] [Preorder β] {u : β → α} (l : LowerAdjoint u) (x y : α) :
u (l.toFun (u (l.toFun x) ⊔ y)) = u (l.toFun (x ⊔ y))
source
theorem LowerAdjoint.closure_sup_closure_right {α : Type u_1} {β : Type u_4} [SemilatticeSup α] [Preorder β] {u : β → α} (l : LowerAdjoint u) (x y : α) :
u (l.toFun (x ⊔ u (l.toFun y))) = u (l.toFun (x ⊔ y))
source
theorem LowerAdjoint.closure_sup_closure {α : Type u_1} {β : Type u_4} [SemilatticeSup α] [Preorder β] {u : β → α} (l : LowerAdjoint u) (x y : α) :
u (l.toFun (u (l.toFun x) ⊔ u (l.toFun y))) = u (l.toFun (x ⊔ y))
source
theorem LowerAdjoint.closure_iSup_closure {α : Type u_1} {ι : Sort u_2} {β : Type u_4} [CompleteLattice α] [Preorder β] {u : β → α} (l : LowerAdjoint u) (f : ι → α) :
u (l.toFun (⨆ (i : ι), u (l.toFun (f i)))) = u (l.toFun (⨆ (i : ι), f i))
source
theorem LowerAdjoint.closure_iSup₂_closure {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} {β : Type u_4} [CompleteLattice α] [Preorder β] {u : β → α} (l : LowerAdjoint u) (f : (i : ι) → κ i → α) :
u (l.toFun (⨆ (i : ι), ⨆ (j : κ i), u (l.toFun (f i j)))) = u (l.toFun (⨆ (i : ι), ⨆ (j : κ i), f i j))
source
theorem LowerAdjoint.subset_closure {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (s : Set β) :
s ⊆ ↑(l.toFun s)
source
theorem LowerAdjoint.notMem_of_notMem_closure {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) {s : Set β} {P : β} (hP : P ∉ l.toFun s) :
P ∉ s
source
@[deprecated LowerAdjoint.notMem_of_notMem_closure (since := "2025-05-23")]
theorem LowerAdjoint.not_mem_of_not_mem_closure {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) {s : Set β} {P : β} (hP : P ∉ l.toFun s) :
P ∉ s

Alias of `LowerAdjoint.notMem_of_notMem_closure`.

source
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
source
theorem LowerAdjoint.mem_iff {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (s : Set β) (x : β) :
x ∈ l.toFun s ↔ ∀ (S : α), s ⊆ ↑S → x ∈ S
source
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
source
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))
source
@[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)
source
@[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)
source
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)
source
@[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))
source
@[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` #

source
def GaloisConnection.lowerAdjoint {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) :
LowerAdjoint u

Every Galois connection induces a lower adjoint.

Equations

- gc.lowerAdjoint = { toFun := l, gc' := gc }

Instances For

source
@[simp]
theorem GaloisConnection.lowerAdjoint_toFun {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (a✝ : α) :
gc.lowerAdjoint.toFun a✝ = l a✝
source
def GaloisConnection.closureOperator {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) :
ClosureOperator α

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

- gc.closureOperator = gc.lowerAdjoint.closureOperator

Instances For

source
@[simp]
theorem GaloisConnection.closureOperator_isClosed {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (x : α) :
gc.closureOperator.IsClosed x = (u (l x) = x)
source
@[simp]
theorem GaloisConnection.closureOperator_apply {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (x : α) :
gc.closureOperator x = u (l x)
source
def ClosureOperator.gi {α : Type u_1} [PartialOrder α] (c : ClosureOperator α) :
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

source
@[simp]
theorem closureOperator_gi_self {α : Type u_1} [PartialOrder α] (c : ClosureOperator α) :
⋯.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.