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

ink

structure ClosureOperator (α : Type u_1) [inst : Preorder α] extends OrderHom : 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.

ink

instance ClosureOperator.instCoeFunClosureOperatorForAll (α : Type u_1) [inst : Preorder α] : CoeFun (ClosureOperator α) fun x => α → α

Equations

• ClosureOperator.instCoeFunClosureOperatorForAll α = { coe := fun c => ↑c.toOrderHom }

ink

@[simp]

theorem ClosureOperator.id_apply (α : Type u_1) [inst : PartialOrder α] (a : α) : ↑(ClosureOperator.id α).toOrderHom a = a

ink

def ClosureOperator.id (α : Type u_1) [inst : PartialOrder α] : ClosureOperator α

The identity function as a closure operator.

Equations

• ClosureOperator.id α = { toOrderHom := OrderHom.id, le_closure' := (_ : ∀ (x : α), x ≤ x), idempotent' := (_ : ∀ (x : α), ↑OrderHom.id (↑OrderHom.id x) = ↑OrderHom.id (↑OrderHom.id x)) }

ink

instance ClosureOperator.instInhabitedClosureOperatorToPreorder (α : Type u_1) [inst : PartialOrder α] : Inhabited (ClosureOperator α)

Equations

• ClosureOperator.instInhabitedClosureOperatorToPreorder α = { default := ClosureOperator.id α }

ink

theorem ClosureOperator.ext {α : Type u_1} [inst : PartialOrder α] (c₁ : ClosureOperator α) (c₂ : ClosureOperator α) : ↑c₁.toOrderHom = ↑c₂.toOrderHom → c₁ = c₂

ink

@[simp]

theorem ClosureOperator.mk'_apply {α : Type u_1} [inst : PartialOrder α] (f : α → α) (hf₁ : Monotone f) (hf₂ : ∀ (x : α), x ≤ f x) (hf₃ : ∀ (x : α), f (f x) ≤ f x) : ∀ (a : α), ↑(ClosureOperator.mk' f hf₁ hf₂ hf₃).toOrderHom a = f a

ink

def ClosureOperator.mk' {α : Type u_1} [inst : 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₃ = { toOrderHom := { toFun := f, monotone' := hf₁ }, le_closure' := hf₂, idempotent' := (_ : ∀ (x : α), f (f x) = f x) }

ink

@[simp]

theorem ClosureOperator.mk₂_apply {α : Type u_1} [inst : PartialOrder α] (f : α → α) (hf : ∀ (x : α), x ≤ f x) (hmin : ∀ ⦃x y : α⦄, x ≤ f y → f x ≤ f y) : ∀ (a : α), ↑(ClosureOperator.mk₂ f hf hmin).toOrderHom a = f a

ink

def ClosureOperator.mk₂ {α : Type u_1} [inst : 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 = { toOrderHom := { toFun := f, monotone' := (_ : ∀ (x y : α), x ≤ y → f x ≤ f y) }, le_closure' := hf, idempotent' := (_ : ∀ (x : α), f (f x) = f x) }

ink

@[simp]

theorem ClosureOperator.mk₃_apply {α : Type u_1} [inst : 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 : α), ↑(ClosureOperator.mk₃ f p hf hfp hmin).toOrderHom a = f a

ink

def ClosureOperator.mk₃ {α : Type u_1} [inst : 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 α

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

• ClosureOperator.mk₃ f p hf hfp hmin = ClosureOperator.mk₂ f hf (_ : ∀ (x y : α), x ≤ f y → f x ≤ f y)

ink

theorem ClosureOperator.closure_mem_mk₃ {α : Type u_1} [inst : PartialOrder α] {f : α → α} {p : α → Prop} {hf : ∀ (x : α), x ≤ f x} {hfp : (x : α) → p (f x)} {hmin : ∀ ⦃x y : α⦄, x ≤ y → p y → f 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.

ink

theorem ClosureOperator.closure_le_mk₃_iff {α : Type u_1} [inst : PartialOrder α] {f : α → α} {p : α → Prop} {hf : ∀ (x : α), x ≤ f x} {hfp : (x : α) → p (f x)} {hmin : ∀ ⦃x y : α⦄, x ≤ y → p y → f 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.

ink

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

ink

theorem ClosureOperator.le_closure {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α) (x : α) : x ≤ ↑c.toOrderHom x

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

ink

@[simp]

theorem ClosureOperator.idempotent {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α) (x : α) : ↑c.toOrderHom (↑c.toOrderHom x) = ↑c.toOrderHom x

ink

theorem ClosureOperator.le_closure_iff {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α) (x : α) (y : α) : x ≤ ↑c.toOrderHom y ↔ ↑c.toOrderHom x ≤ ↑c.toOrderHom y

ink

def ClosureOperator.closed {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α) : Set α

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

Equations

• ClosureOperator.closed c x = (↑c.toOrderHom x = x)

ink

theorem ClosureOperator.mem_closed_iff {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α) (x : α) : x ∈ ClosureOperator.closed c ↔ ↑c.toOrderHom x = x

ink

theorem ClosureOperator.mem_closed_iff_closure_le {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α) (x : α) : x ∈ ClosureOperator.closed c ↔ ↑c.toOrderHom x ≤ x

ink

theorem ClosureOperator.closure_eq_self_of_mem_closed {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α) {x : α} (h : x ∈ ClosureOperator.closed c) : ↑c.toOrderHom x = x

ink

@[simp]

theorem ClosureOperator.closure_is_closed {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α) (x : α) : ↑c.toOrderHom x ∈ ClosureOperator.closed c

ink

theorem ClosureOperator.closed_eq_range_close {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α) : ClosureOperator.closed c = Set.range ↑c.toOrderHom

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

ink

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

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

Equations

• ClosureOperator.toClosed c x = { val := ↑c.toOrderHom x, property := (_ : ↑c.toOrderHom x ∈ ClosureOperator.closed c) }

ink

@[simp]

theorem ClosureOperator.closure_le_closed_iff_le {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α) (x : α) {y : α} (hy : ClosureOperator.closed c y) : ↑c.toOrderHom x ≤ y ↔ x ≤ y

ink

theorem ClosureOperator.eq_mk₃_closed {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α) : c = ClosureOperator.mk₃ (↑c.toOrderHom) (ClosureOperator.closed c) (_ : ∀ (x : α), x ≤ ↑c.toOrderHom x) (_ : ∀ (x : α), ↑c.toOrderHom x ∈ ClosureOperator.closed c) (_ : ∀ (x y : α), x ≤ y → ClosureOperator.closed c y → ↑c.toOrderHom x ≤ y)

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

ink

theorem ClosureOperator.mem_mk₃_closed {α : Type u_1} [inst : PartialOrder α] {f : α → α} {p : α → Prop} {hf : ∀ (x : α), x ≤ f x} {hfp : (x : α) → p (f x)} {hmin : ∀ ⦃x y : α⦄, x ≤ y → p y → f x ≤ y} {x : α} (hx : p x) : x ∈ ClosureOperator.closed (ClosureOperator.mk₃ f p hf hfp hmin)

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

ink

@[simp]

theorem ClosureOperator.closure_top {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] (c : ClosureOperator α) : ↑c.toOrderHom ⊤ = ⊤

ink

theorem ClosureOperator.top_mem_closed {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] (c : ClosureOperator α) : ⊤ ∈ ClosureOperator.closed c

ink

theorem ClosureOperator.closure_inf_le {α : Type u_1} [inst : SemilatticeInf α] (c : ClosureOperator α) (x : α) (y : α) : ↑c.toOrderHom (x ⊓ y) ≤ ↑c.toOrderHom x ⊓ ↑c.toOrderHom y

ink

theorem ClosureOperator.closure_sup_closure_le {α : Type u_1} [inst : SemilatticeSup α] (c : ClosureOperator α) (x : α) (y : α) : ↑c.toOrderHom x ⊔ ↑c.toOrderHom y ≤ ↑c.toOrderHom (x ⊔ y)

ink

theorem ClosureOperator.closure_sup_closure_left {α : Type u_1} [inst : SemilatticeSup α] (c : ClosureOperator α) (x : α) (y : α) : ↑c.toOrderHom (↑c.toOrderHom x ⊔ y) = ↑c.toOrderHom (x ⊔ y)

ink

theorem ClosureOperator.closure_sup_closure_right {α : Type u_1} [inst : SemilatticeSup α] (c : ClosureOperator α) (x : α) (y : α) : ↑c.toOrderHom (x ⊔ ↑c.toOrderHom y) = ↑c.toOrderHom (x ⊔ y)

ink

theorem ClosureOperator.closure_sup_closure {α : Type u_1} [inst : SemilatticeSup α] (c : ClosureOperator α) (x : α) (y : α) : ↑c.toOrderHom (↑c.toOrderHom x ⊔ ↑c.toOrderHom y) = ↑c.toOrderHom (x ⊔ y)

ink

@[simp]

theorem ClosureOperator.closure_supᵢ_closure {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] (c : ClosureOperator α) (f : ι → α) : ↑c.toOrderHom (⨆ i, ↑c.toOrderHom (f i)) = ↑c.toOrderHom (⨆ i, f i)

ink

@[simp]

theorem ClosureOperator.closure_supᵢ₂_closure {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [inst : CompleteLattice α] (c : ClosureOperator α) (f : (i : ι) → κ i → α) : ↑c.toOrderHom (⨆ i, ⨆ j, ↑c.toOrderHom (f i j)) = ↑c.toOrderHom (⨆ i, ⨆ j, f i j)

Lower adjoint

ink

structure LowerAdjoint {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] (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 (↑) : β → α.

ink

@[simp]

theorem LowerAdjoint.id_toFun (α : Type u_1) [inst : Preorder α] (x : α) : LowerAdjoint.toFun (LowerAdjoint.id α) x = x

ink

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

The identity function as a lower adjoint to itself.

Equations

• LowerAdjoint.id α = { toFun := fun x => x, gc' := (_ : GaloisConnection id id) }

ink

instance LowerAdjoint.instInhabitedLowerAdjointId {α : Type u_1} [inst : Preorder α] : Inhabited (LowerAdjoint id)

Equations

• LowerAdjoint.instInhabitedLowerAdjointId = { default := LowerAdjoint.id α }

ink

instance LowerAdjoint.instCoeFunLowerAdjointForAll {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {u : β → α} : CoeFun (LowerAdjoint u) fun x => α → β

Equations

• LowerAdjoint.instCoeFunLowerAdjointForAll = { coe := LowerAdjoint.toFun }

ink

theorem LowerAdjoint.gc {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {u : β → α} (l : LowerAdjoint u) : GaloisConnection l.toFun u

ink

theorem LowerAdjoint.ext {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {u : β → α} (l₁ : LowerAdjoint u) (l₂ : LowerAdjoint u) : l₁.toFun = l₂.toFun → l₁ = l₂

ink

theorem LowerAdjoint.monotone {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {u : β → α} (l : LowerAdjoint u) : Monotone (u ∘ l.toFun)

ink

theorem LowerAdjoint.le_closure {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α) : x ≤ u (LowerAdjoint.toFun l x)

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

ink

@[simp]

theorem LowerAdjoint.closureOperator_apply {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α) : ↑(LowerAdjoint.closureOperator l).toOrderHom x = u (LowerAdjoint.toFun l x)

ink

def LowerAdjoint.closureOperator {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : 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

• One or more equations did not get rendered due to their size.

ink

theorem LowerAdjoint.idempotent {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α) : u (LowerAdjoint.toFun l (u (LowerAdjoint.toFun l x))) = u (LowerAdjoint.toFun l x)

ink

theorem LowerAdjoint.le_closure_iff {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α) (y : α) : x ≤ u (LowerAdjoint.toFun l y) ↔ u (LowerAdjoint.toFun l x) ≤ u (LowerAdjoint.toFun l y)

ink

def LowerAdjoint.closed {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : 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

• LowerAdjoint.closed l x = (u (LowerAdjoint.toFun l x) = x)

ink

theorem LowerAdjoint.mem_closed_iff {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α) : x ∈ LowerAdjoint.closed l ↔ u (LowerAdjoint.toFun l x) = x

ink

theorem LowerAdjoint.closure_eq_self_of_mem_closed {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {u : β → α} (l : LowerAdjoint u) {x : α} (h : x ∈ LowerAdjoint.closed l) : u (LowerAdjoint.toFun l x) = x

ink

theorem LowerAdjoint.mem_closed_iff_closure_le {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] {u : β → α} (l : LowerAdjoint u) (x : α) : x ∈ LowerAdjoint.closed l ↔ u (LowerAdjoint.toFun l x) ≤ x

ink

@[simp]

theorem LowerAdjoint.closure_is_closed {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] {u : β → α} (l : LowerAdjoint u) (x : α) : u (LowerAdjoint.toFun l x) ∈ LowerAdjoint.closed l

ink

theorem LowerAdjoint.closed_eq_range_close {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] {u : β → α} (l : LowerAdjoint u) : LowerAdjoint.closed l = Set.range (u ∘ l.toFun)

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

ink

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

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

Equations

• LowerAdjoint.toClosed l x = { val := u (LowerAdjoint.toFun l x), property := (_ : u (LowerAdjoint.toFun l x) ∈ LowerAdjoint.closed l) }

ink

@[simp]

theorem LowerAdjoint.closure_le_closed_iff_le {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] {u : β → α} (l : LowerAdjoint u) (x : α) {y : α} (hy : LowerAdjoint.closed l y) : u (LowerAdjoint.toFun l x) ≤ y ↔ x ≤ y

ink

theorem LowerAdjoint.closure_top {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : OrderTop α] [inst : Preorder β] {u : β → α} (l : LowerAdjoint u) : u (LowerAdjoint.toFun l ⊤) = ⊤

ink

theorem LowerAdjoint.closure_inf_le {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst : Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α) (y : α) : u (LowerAdjoint.toFun l (x ⊓ y)) ≤ u (LowerAdjoint.toFun l x) ⊓ u (LowerAdjoint.toFun l y)

ink

theorem LowerAdjoint.closure_sup_closure_le {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst : Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α) (y : α) : u (LowerAdjoint.toFun l x) ⊔ u (LowerAdjoint.toFun l y) ≤ u (LowerAdjoint.toFun l (x ⊔ y))

ink

theorem LowerAdjoint.closure_sup_closure_left {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst : Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α) (y : α) : u (LowerAdjoint.toFun l (u (LowerAdjoint.toFun l x) ⊔ y)) = u (LowerAdjoint.toFun l (x ⊔ y))

ink

theorem LowerAdjoint.closure_sup_closure_right {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst : Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α) (y : α) : u (LowerAdjoint.toFun l (x ⊔ u (LowerAdjoint.toFun l y))) = u (LowerAdjoint.toFun l (x ⊔ y))

ink

theorem LowerAdjoint.closure_sup_closure {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst : Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α) (y : α) : u (LowerAdjoint.toFun l (u (LowerAdjoint.toFun l x) ⊔ u (LowerAdjoint.toFun l y))) = u (LowerAdjoint.toFun l (x ⊔ y))

ink

theorem LowerAdjoint.closure_supᵢ_closure {α : Type u_1} {ι : Sort u_3} {β : Type u_2} [inst : CompleteLattice α] [inst : Preorder β] {u : β → α} (l : LowerAdjoint u) (f : ι → α) : u (LowerAdjoint.toFun l (⨆ i, u (LowerAdjoint.toFun l (f i)))) = u (LowerAdjoint.toFun l (⨆ i, f i))

ink

theorem LowerAdjoint.closure_supᵢ₂_closure {α : Type u_1} {ι : Sort u_3} {κ : ι → Sort u_4} {β : Type u_2} [inst : CompleteLattice α] [inst : Preorder β] {u : β → α} (l : LowerAdjoint u) (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))

ink

theorem LowerAdjoint.subset_closure {α : Type u_2} {β : Type u_1} [inst : SetLike α β] (l : LowerAdjoint SetLike.coe) (s : Set β) : s ⊆ ↑(LowerAdjoint.toFun l s)

ink

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 ∈ LowerAdjoint.toFun l s) : ¬P ∈ s

ink

theorem LowerAdjoint.le_iff_subset {α : Type u_2} {β : Type u_1} [inst : SetLike α β] (l : LowerAdjoint SetLike.coe) (s : Set β) (S : α) : LowerAdjoint.toFun l s ≤ S ↔ s ⊆ ↑S

ink

theorem LowerAdjoint.mem_iff {α : Type u_2} {β : Type u_1} [inst : SetLike α β] (l : LowerAdjoint SetLike.coe) (s : Set β) (x : β) : x ∈ LowerAdjoint.toFun l s ↔ ∀ (S : α), s ⊆ ↑S → x ∈ S

ink

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 ≤ LowerAdjoint.toFun l s) : LowerAdjoint.toFun l s = S

ink

theorem LowerAdjoint.closure_union_closure_subset {α : Type u_2} {β : Type u_1} [inst : SetLike α β] (l : LowerAdjoint SetLike.coe) (x : α) (y : α) : ↑(LowerAdjoint.toFun l ↑x) ∪ ↑(LowerAdjoint.toFun l ↑y) ⊆ ↑(LowerAdjoint.toFun l (↑x ∪ ↑y))

ink

@[simp]

theorem LowerAdjoint.closure_union_closure_left {α : Type u_1} {β : Type u_2} [inst : SetLike α β] (l : LowerAdjoint SetLike.coe) (x : α) (y : α) : LowerAdjoint.toFun l (↑(LowerAdjoint.toFun l ↑x) ∪ ↑y) = LowerAdjoint.toFun l (↑x ∪ ↑y)

ink

@[simp]

theorem LowerAdjoint.closure_union_closure_right {α : Type u_1} {β : Type u_2} [inst : SetLike α β] (l : LowerAdjoint SetLike.coe) (x : α) (y : α) : LowerAdjoint.toFun l (↑x ∪ ↑(LowerAdjoint.toFun l ↑y)) = LowerAdjoint.toFun l (↑x ∪ ↑y)

ink

theorem LowerAdjoint.closure_union_closure {α : Type u_1} {β : Type u_2} [inst : SetLike α β] (l : LowerAdjoint SetLike.coe) (x : α) (y : α) : LowerAdjoint.toFun l (↑(LowerAdjoint.toFun l ↑x) ∪ ↑(LowerAdjoint.toFun l ↑y)) = LowerAdjoint.toFun l (↑x ∪ ↑y)

ink

@[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))

ink

@[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

ink

@[simp]

theorem GaloisConnection.lowerAdjoint_toFun {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst : Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : ∀ (a : α), LowerAdjoint.toFun (GaloisConnection.lowerAdjoint gc) a = l a

ink

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

Every Galois connection induces a lower adjoint.

Equations

• GaloisConnection.lowerAdjoint gc = { toFun := l, gc' := gc }

ink

@[simp]

theorem GaloisConnection.closureOperator_apply {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (x : α) : ↑(GaloisConnection.closureOperator gc).toOrderHom x = u (l x)

ink

def GaloisConnection.closureOperator {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : 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

• GaloisConnection.closureOperator gc = LowerAdjoint.closureOperator (GaloisConnection.lowerAdjoint gc)

ink

def ClosureOperator.gi {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α) : GaloisInsertion (ClosureOperator.toClosed c) 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.

ink

@[simp]

theorem closureOperator_gi_self {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α) : GaloisConnection.closureOperator (_ : GaloisConnection (ClosureOperator.toClosed c) Subtype.val) = 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.