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) [Preorder α] extends OrderHom : 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

instance ClosureOperator.instFunLikeClosureOperator (α : Type u_1) [Preorder α] : FunLike (ClosureOperator α) α α

Equations

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

instance ClosureOperator.instOrderHomClassClosureOperatorToLEInstFunLikeClosureOperator (α : Type u_1) [Preorder α] : OrderHomClass (ClosureOperator α) α α

Equations

• ⋯ = ⋯

@[simp]

theorem ClosureOperator.id_isClosed (α : Type u_1) [PartialOrder α] : ∀ (x : α), (ClosureOperator.id α).IsClosed x = True

@[simp]

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

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

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

Equations

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

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

@[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 : α) : (ClosureOperator.mk' f hf₁ hf₂ hf₃).IsClosed x = (f x = x)

@[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 : α), (ClosureOperator.mk' f hf₁ hf₂ hf₃) a = f a

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₃ = { toOrderHom := { toFun := f, monotone' := hf₁ }, le_closure' := hf₂, idempotent' := ⋯, IsClosed := fun (x : α) => f x = x, isClosed_iff := ⋯ }

@[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 : α), (ClosureOperator.mk₂ f hf hmin) a = f a

@[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 : α) : (ClosureOperator.mk₂ f hf hmin).IsClosed x = (f x = x)

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 = { toOrderHom := { toFun := f, monotone' := ⋯ }, le_closure' := hf, idempotent' := ⋯, IsClosed := fun (x : α) => f x = x, isClosed_iff := ⋯ }

@[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 : α), (ClosureOperator.ofPred f p hf hfp hmin).IsClosed a = p a

@[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 : α), (ClosureOperator.ofPred f p hf hfp hmin) a = f a

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

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

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

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.

@[simp]

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

@[simp]

theorem ClosureOperator.isClosed_closure {α : Type u_1} [PartialOrder α] (c : ClosureOperator α) (x : α) : c.IsClosed (c x)

@[inline, reducible]

abbrev ClosureOperator.Closeds {α : Type u_1} [PartialOrder α] (c : ClosureOperator α) : Type u_1

The type of elements closed under a closure operator.

Equations

• ClosureOperator.Closeds c = { x : α // c.IsClosed x }

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

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

Equations

• ClosureOperator.toCloseds c x = { val := c x, property := ⋯ }

theorem ClosureOperator.IsClosed.closure_eq {α : Type u_1} [PartialOrder α] {c : ClosureOperator α} {x : α} : c.IsClosed x → c x = x

theorem ClosureOperator.isClosed_iff_closure_le {α : Type u_1} [PartialOrder α] {c : ClosureOperator α} {x : α} : c.IsClosed x ↔ c x ≤ x

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.

theorem ClosureOperator.le_closure_iff {α : Type u_1} [PartialOrder α] {c : ClosureOperator α} {x : α} {y : α} : x ≤ c y ↔ c x ≤ c y

@[simp]

theorem ClosureOperator.IsClosed.closure_le_iff {α : Type u_1} [PartialOrder α] {c : ClosureOperator α} {x : α} {y : α} (hy : c.IsClosed y) : c x ≤ y ↔ x ≤ y

theorem ClosureOperator.closure_min {α : Type u_1} [PartialOrder α] {c : ClosureOperator α} {x : α} {y : α} (hxy : x ≤ y) (hy : c.IsClosed y) : c x ≤ y

theorem ClosureOperator.eq_ofPred_closed {α : Type u_1} [PartialOrder α] (c : ClosureOperator α) : 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} [PartialOrder α] [OrderTop α] (c : ClosureOperator α) : c ⊤ = ⊤

@[simp]

theorem ClosureOperator.isClosed_top {α : Type u_1} [PartialOrder α] [OrderTop α] (c : ClosureOperator α) : c.IsClosed ⊤

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

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

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

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

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

@[simp]

theorem ClosureOperator.ofCompletePred_isClosed {α : Type u_1} [CompleteLattice α] (p : α → Prop) (hsinf : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)) : ∀ (a : α), (ClosureOperator.ofCompletePred p hsinf).IsClosed a = p a

@[simp]

theorem ClosureOperator.ofCompletePred_apply {α : Type u_1} [CompleteLattice α] (p : α → Prop) (hsinf : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)) (a : α) : (ClosureOperator.ofCompletePred p hsinf) a = ⨅ (b : { b : α // a ≤ b ∧ p b }), ↑b

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

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

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

Lower adjoint

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.

@[simp]

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

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

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

Equations

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

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

Equations

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

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

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

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

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.

@[simp]

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

@[simp]

theorem LowerAdjoint.closureOperator_isClosed {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α) : (LowerAdjoint.closureOperator l).IsClosed x = (u (l.toFun x) = x)

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

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

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)

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)

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

• LowerAdjoint.closed l = {x : α | u (l.toFun x) = x}

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

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

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

@[simp]

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

theorem LowerAdjoint.closed_eq_range_close {α : Type u_1} {β : Type u_4} [PartialOrder α] [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.

def LowerAdjoint.toClosed {α : Type u_1} {β : Type u_4} [PartialOrder α] [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 (l.toFun x), property := ⋯ }

@[simp]

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

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

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)

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

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

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

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

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

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

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 : P ∉ l.toFun s) : P ∉ s

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 ⊆ ↑S → x ∈ 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} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : ∀ (a : α), (GaloisConnection.lowerAdjoint gc).toFun a = l a

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

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

@[simp]

theorem GaloisConnection.closureOperator_isClosed {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (x : α) : (GaloisConnection.closureOperator gc).IsClosed x = (u (l x) = x)

@[simp]

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

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

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

def ClosureOperator.gi {α : Type u_1} [PartialOrder α] (c : ClosureOperator α) : GaloisInsertion (ClosureOperator.toCloseds c) Subtype.val

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

Equations

• ClosureOperator.gi c = { choice := fun (x : α) (hx : ↑(ClosureOperator.toCloseds c x) ≤ x) => { val := x, property := ⋯ }, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

@[simp]

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