mathlib documentation

order.closure

Closure operators between preorders #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 := coe, 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 galois_connection.lower_adjoint and lower_adjoint.closure_operator), and every closure operator on a partial order induces a Galois insertion from the set of closed elements to the underlying type (see closure_operator.gi).

Main definitions #

closure_operator: A closure operator is a monotone function f : α → α such that ∀ x, x ≤ f x and ∀ x, f (f x) = f x.
lower_adjoint: A lower adjoint to u : β → α is a function l : α → β such that l and u form a Galois connection.

Implementation details #

Although lower_adjoint is technically a generalisation of closure_operator (by defining to_fun := id), it is desirable to have both as otherwise ids would be carried all over the place when using concrete closure operators such as convex_hull.

lower_adjoint really is a semibundled structure version of galois_connection.

References #

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

Closure operator #

structure closure_operator (α : Type u_1) [preorder α] :

Type u_1

to_order_hom : α →o α
le_closure' : ∀ (x : α), x ≤ self.to_order_hom.to_fun x
idempotent' : ∀ (x : α), self.to_order_hom.to_fun (self.to_order_hom.to_fun x) = self.to_order_hom.to_fun 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 closure_operator

@[protected, instance]

def closure_operator.has_coe_to_fun (α : Type u_1) [preorder α] :

has_coe_to_fun (closure_operator α) (λ (_x : closure_operator α), α → α)

Equations

closure_operator.has_coe_to_fun α = {coe := λ (c : closure_operator α), c.to_order_hom.to_fun}

def closure_operator.simps.apply (α : Type u_1) [preorder α] (f : closure_operator α) :

α → α

See Note [custom simps projection]

Equations

closure_operator.simps.apply α f = ⇑f

def closure_operator.id (α : Type u_1) [partial_order α] :

closure_operator α

The identity function as a closure operator.

Equations

closure_operator.id α = {to_order_hom := order_hom.id (partial_order.to_preorder α), le_closure' := _, idempotent' := _}

@[simp]

theorem closure_operator.id_apply (α : Type u_1) [partial_order α] (a : α) :

⇑(closure_operator.id α) a = a

@[protected, instance]

def closure_operator.inhabited (α : Type u_1) [partial_order α] :

inhabited (closure_operator α)

Equations

closure_operator.inhabited α = {default := closure_operator.id α _inst_1}

@[ext]

theorem closure_operator.ext {α : Type u_1} [partial_order α] (c₁ c₂ : closure_operator α) :

⇑c₁ = ⇑c₂ → c₁ = c₂

@[simp]

theorem closure_operator.mk'_apply {α : Type u_1} [partial_order α] (f : α → α) (hf₁ : monotone f) (hf₂ : ∀ (x : α), x ≤ f x) (hf₃ : ∀ (x : α), f (f x) ≤ f x) (ᾰ : α) :

⇑(closure_operator.mk' f hf₁ hf₂ hf₃) ᾰ = f ᾰ

def closure_operator.mk' {α : Type u_1} [partial_order α] (f : α → α) (hf₁ : monotone f) (hf₂ : ∀ (x : α), x ≤ f x) (hf₃ : ∀ (x : α), f (f x) ≤ f x) :

closure_operator α

Constructor for a closure operator using the weaker idempotency axiom: f (f x) ≤ f x.

Equations

closure_operator.mk' f hf₁ hf₂ hf₃ = {to_order_hom := {to_fun := f, monotone' := hf₁}, le_closure' := hf₂, idempotent' := _}

@[simp]

theorem closure_operator.mk₂_apply {α : Type u_1} [partial_order α] (f : α → α) (hf : ∀ (x : α), x ≤ f x) (hmin : ∀ ⦃x y : α⦄, x ≤ f y → f x ≤ f y) (ᾰ : α) :

⇑(closure_operator.mk₂ f hf hmin) ᾰ = f ᾰ

def closure_operator.mk₂ {α : Type u_1} [partial_order α] (f : α → α) (hf : ∀ (x : α), x ≤ f x) (hmin : ∀ ⦃x y : α⦄, x ≤ f y → f x ≤ f y) :

closure_operator α

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

closure_operator.mk₂ f hf hmin = {to_order_hom := {to_fun := f, monotone' := _}, le_closure' := hf, idempotent' := _}

@[simp]

theorem closure_operator.mk₃_apply {α : Type u_1} [partial_order α] (f : α → α) (p : α → Prop) (hf : ∀ (x : α), x ≤ f x) (hfp : ∀ (x : α), p (f x)) (hmin : ∀ ⦃x y : α⦄, x ≤ y → p y → f x ≤ y) (ᾰ : α) :

⇑(closure_operator.mk₃ f p hf hfp hmin) ᾰ = f ᾰ

def closure_operator.mk₃ {α : Type u_1} [partial_order α] (f : α → α) (p : α → Prop) (hf : ∀ (x : α), x ≤ f x) (hfp : ∀ (x : α), p (f x)) (hmin : ∀ ⦃x y : α⦄, x ≤ y → p y → f x ≤ y) :

closure_operator α

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

closure_operator.mk₃ f p hf hfp hmin = closure_operator.mk₂ f hf _

theorem closure_operator.closure_mem_mk₃ {α : Type u_1} [partial_order α] {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 (⇑(closure_operator.mk₃ f p hf hfp hmin) 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 closure_operator.closure_le_mk₃_iff {α : Type u_1} [partial_order α] {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) :

⇑(closure_operator.mk₃ f p hf hfp hmin) x ≤ y

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

theorem closure_operator.monotone {α : Type u_1} [partial_order α] (c : closure_operator α) :

theorem closure_operator.le_closure {α : Type u_1} [partial_order α] (c : closure_operator α) (x : α) :

x ≤ ⇑c x

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

@[simp]

theorem closure_operator.idempotent {α : Type u_1} [partial_order α] (c : closure_operator α) (x : α) :

⇑c (⇑c x) = ⇑c x

theorem closure_operator.le_closure_iff {α : Type u_1} [partial_order α] (c : closure_operator α) (x y : α) :

x ≤ ⇑c y ↔ ⇑c x ≤ ⇑c y

def closure_operator.closed {α : Type u_1} [partial_order α] (c : closure_operator α) :

set α

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

Equations

c.closed = λ (x : α), ⇑c x = x

theorem closure_operator.mem_closed_iff {α : Type u_1} [partial_order α] (c : closure_operator α) (x : α) :

x ∈ c.closed ↔ ⇑c x = x

theorem closure_operator.mem_closed_iff_closure_le {α : Type u_1} [partial_order α] (c : closure_operator α) (x : α) :

x ∈ c.closed ↔ ⇑c x ≤ x

theorem closure_operator.closure_eq_self_of_mem_closed {α : Type u_1} [partial_order α] (c : closure_operator α) {x : α} (h : x ∈ c.closed) :

⇑c x = x

@[simp]

theorem closure_operator.closure_is_closed {α : Type u_1} [partial_order α] (c : closure_operator α) (x : α) :

⇑c x ∈ c.closed

theorem closure_operator.closed_eq_range_close {α : Type u_1} [partial_order α] (c : closure_operator α) :

c.closed = set.range ⇑c

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

def closure_operator.to_closed {α : Type u_1} [partial_order α] (c : closure_operator α) (x : α) :

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

Equations

c.to_closed x = ⟨⇑c x, _⟩

@[simp]

theorem closure_operator.closure_le_closed_iff_le {α : Type u_1} [partial_order α] (c : closure_operator α) (x : α) {y : α} (hy : c.closed y) :

⇑c x ≤ y ↔ x ≤ y

theorem closure_operator.eq_mk₃_closed {α : Type u_1} [partial_order α] (c : closure_operator α) :

c = closure_operator.mk₃ ⇑c c.closed _ _ _

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

theorem closure_operator.mem_mk₃_closed {α : Type u_1} [partial_order α] {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 ∈ (closure_operator.mk₃ f p hf hfp hmin).closed

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

@[simp]

theorem closure_operator.closure_top {α : Type u_1} [partial_order α] [order_top α] (c : closure_operator α) :

theorem closure_operator.top_mem_closed {α : Type u_1} [partial_order α] [order_top α] (c : closure_operator α) :

⊤ ∈ c.closed

theorem closure_operator.closure_inf_le {α : Type u_1} [semilattice_inf α] (c : closure_operator α) (x y : α) :

⇑c (x ⊓ y) ≤ ⇑c x ⊓ ⇑c y

theorem closure_operator.closure_sup_closure_le {α : Type u_1} [semilattice_sup α] (c : closure_operator α) (x y : α) :

⇑c x ⊔ ⇑c y ≤ ⇑c (x ⊔ y)

theorem closure_operator.closure_sup_closure_left {α : Type u_1} [semilattice_sup α] (c : closure_operator α) (x y : α) :

⇑c (⇑c x ⊔ y) = ⇑c (x ⊔ y)

theorem closure_operator.closure_sup_closure_right {α : Type u_1} [semilattice_sup α] (c : closure_operator α) (x y : α) :

⇑c (x ⊔ ⇑c y) = ⇑c (x ⊔ y)

theorem closure_operator.closure_sup_closure {α : Type u_1} [semilattice_sup α] (c : closure_operator α) (x y : α) :

⇑c (⇑c x ⊔ ⇑c y) = ⇑c (x ⊔ y)

@[simp]

theorem closure_operator.closure_supr_closure {α : Type u_1} {ι : Sort u_2} [complete_lattice α] (c : closure_operator α) (f : ι → α) :

⇑c (⨆ (i : ι), ⇑c (f i)) = ⇑c (⨆ (i : ι), f i)

@[simp]

theorem closure_operator.closure_supr₂_closure {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} [complete_lattice α] (c : closure_operator α) (f : Π (i : ι), κ i → α) :

⇑c (⨆ (i : ι) (j : κ i), ⇑c (f i j)) = ⇑c (⨆ (i : ι) (j : κ i), f i j)

Lower adjoint #

structure lower_adjoint {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] (u : β → α) :

Type (max u_1 u_4)

to_fun : α → β
gc' : galois_connection self.to_fun 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 coe : β → α.

Instances for lower_adjoint

@[protected]

def lower_adjoint.id (α : Type u_1) [preorder α] :

lower_adjoint id

The identity function as a lower adjoint to itself.

Equations

lower_adjoint.id α = {to_fun := λ (x : α), x, gc' := _}

@[simp]

theorem lower_adjoint.id_to_fun (α : Type u_1) [preorder α] (x : α) :

(lower_adjoint.id α).to_fun x = x

@[protected, instance]

def lower_adjoint.inhabited {α : Type u_1} [preorder α] :

inhabited (lower_adjoint id)

Equations

lower_adjoint.inhabited = {default := lower_adjoint.id α _inst_1}

@[protected, instance]

def lower_adjoint.has_coe_to_fun {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β → α} :

has_coe_to_fun (lower_adjoint u) (λ (_x : lower_adjoint u), α → β)

Equations

lower_adjoint.has_coe_to_fun = {coe := lower_adjoint.to_fun u}

def lower_adjoint.simps.apply {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β → α} (l : lower_adjoint u) :

α → β

See Note [custom simps projection]

Equations

lower_adjoint.simps.apply l = ⇑l

theorem lower_adjoint.gc {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β → α} (l : lower_adjoint u) :

galois_connection ⇑l u

@[ext]

theorem lower_adjoint.ext {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β → α} (l₁ l₂ : lower_adjoint u) :

⇑l₁ = ⇑l₂ → l₁ = l₂

theorem lower_adjoint.monotone {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β → α} (l : lower_adjoint u) :

monotone (u ∘ ⇑l)

theorem lower_adjoint.le_closure {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β → α} (l : lower_adjoint u) (x : α) :

x ≤ u (⇑l x)

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

def lower_adjoint.closure_operator {α : Type u_1} {β : Type u_4} [partial_order α] [preorder β] {u : β → α} (l : lower_adjoint u) :

closure_operator α

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.closure_operator = {to_order_hom := {to_fun := λ (x : α), u (⇑l x), monotone' := _}, le_closure' := _, idempotent' := _}

@[simp]

theorem lower_adjoint.closure_operator_apply {α : Type u_1} {β : Type u_4} [partial_order α] [preorder β] {u : β → α} (l : lower_adjoint u) (x : α) :

⇑(l.closure_operator) x = u (⇑l x)

theorem lower_adjoint.idempotent {α : Type u_1} {β : Type u_4} [partial_order α] [preorder β] {u : β → α} (l : lower_adjoint u) (x : α) :

u (⇑l (u (⇑l x))) = u (⇑l x)

theorem lower_adjoint.le_closure_iff {α : Type u_1} {β : Type u_4} [partial_order α] [preorder β] {u : β → α} (l : lower_adjoint u) (x y : α) :

x ≤ u (⇑l y) ↔ u (⇑l x) ≤ u (⇑l y)

def lower_adjoint.closed {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β → α} (l : lower_adjoint u) :

set α

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

Equations

l.closed = λ (x : α), u (⇑l x) = x

theorem lower_adjoint.mem_closed_iff {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β → α} (l : lower_adjoint u) (x : α) :

x ∈ l.closed ↔ u (⇑l x) = x

theorem lower_adjoint.closure_eq_self_of_mem_closed {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β → α} (l : lower_adjoint u) {x : α} (h : x ∈ l.closed) :

u (⇑l x) = x

theorem lower_adjoint.mem_closed_iff_closure_le {α : Type u_1} {β : Type u_4} [partial_order α] [partial_order β] {u : β → α} (l : lower_adjoint u) (x : α) :

x ∈ l.closed ↔ u (⇑l x) ≤ x

@[simp]

theorem lower_adjoint.closure_is_closed {α : Type u_1} {β : Type u_4} [partial_order α] [partial_order β] {u : β → α} (l : lower_adjoint u) (x : α) :

u (⇑l x) ∈ l.closed

theorem lower_adjoint.closed_eq_range_close {α : Type u_1} {β : Type u_4} [partial_order α] [partial_order β] {u : β → α} (l : lower_adjoint u) :

l.closed = set.range (u ∘ ⇑l)

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

def lower_adjoint.to_closed {α : Type u_1} {β : Type u_4} [partial_order α] [partial_order β] {u : β → α} (l : lower_adjoint u) (x : α) :

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

Equations

l.to_closed x = ⟨u (⇑l x), _⟩

@[simp]

theorem lower_adjoint.closure_le_closed_iff_le {α : Type u_1} {β : Type u_4} [partial_order α] [partial_order β] {u : β → α} (l : lower_adjoint u) (x : α) {y : α} (hy : l.closed y) :

u (⇑l x) ≤ y ↔ x ≤ y

theorem lower_adjoint.closure_top {α : Type u_1} {β : Type u_4} [partial_order α] [order_top α] [preorder β] {u : β → α} (l : lower_adjoint u) :

u (⇑l ⊤) = ⊤

theorem lower_adjoint.closure_inf_le {α : Type u_1} {β : Type u_4} [semilattice_inf α] [preorder β] {u : β → α} (l : lower_adjoint u) (x y : α) :

u (⇑l (x ⊓ y)) ≤ u (⇑l x) ⊓ u (⇑l y)

theorem lower_adjoint.closure_sup_closure_le {α : Type u_1} {β : Type u_4} [semilattice_sup α] [preorder β] {u : β → α} (l : lower_adjoint u) (x y : α) :

u (⇑l x) ⊔ u (⇑l y) ≤ u (⇑l (x ⊔ y))

theorem lower_adjoint.closure_sup_closure_left {α : Type u_1} {β : Type u_4} [semilattice_sup α] [preorder β] {u : β → α} (l : lower_adjoint u) (x y : α) :

u (⇑l (u (⇑l x) ⊔ y)) = u (⇑l (x ⊔ y))

theorem lower_adjoint.closure_sup_closure_right {α : Type u_1} {β : Type u_4} [semilattice_sup α] [preorder β] {u : β → α} (l : lower_adjoint u) (x y : α) :

u (⇑l (x ⊔ u (⇑l y))) = u (⇑l (x ⊔ y))

theorem lower_adjoint.closure_sup_closure {α : Type u_1} {β : Type u_4} [semilattice_sup α] [preorder β] {u : β → α} (l : lower_adjoint u) (x y : α) :

u (⇑l (u (⇑l x) ⊔ u (⇑l y))) = u (⇑l (x ⊔ y))

theorem lower_adjoint.closure_supr_closure {α : Type u_1} {ι : Sort u_2} {β : Type u_4} [complete_lattice α] [preorder β] {u : β → α} (l : lower_adjoint u) (f : ι → α) :

u (⇑l (⨆ (i : ι), u (⇑l (f i)))) = u (⇑l (⨆ (i : ι), f i))

theorem lower_adjoint.closure_supr₂_closure {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} {β : Type u_4} [complete_lattice α] [preorder β] {u : β → α} (l : lower_adjoint u) (f : Π (i : ι), κ i → α) :

u (⇑l (⨆ (i : ι) (j : κ i), u (⇑l (f i j)))) = u (⇑l (⨆ (i : ι) (j : κ i), f i j))

theorem lower_adjoint.subset_closure {α : Type u_1} {β : Type u_4} [set_like α β] (l : lower_adjoint coe) (s : set β) :

s ⊆ ↑(⇑l s)

theorem lower_adjoint.not_mem_of_not_mem_closure {α : Type u_1} {β : Type u_4} [set_like α β] (l : lower_adjoint coe) {s : set β} {P : β} (hP : P ∉ ⇑l s) :

P ∉ s

theorem lower_adjoint.le_iff_subset {α : Type u_1} {β : Type u_4} [set_like α β] (l : lower_adjoint coe) (s : set β) (S : α) :

⇑l s ≤ S ↔ s ⊆ ↑S

theorem lower_adjoint.mem_iff {α : Type u_1} {β : Type u_4} [set_like α β] (l : lower_adjoint coe) (s : set β) (x : β) :

x ∈ ⇑l s ↔ ∀ (S : α), s ⊆ ↑S → x ∈ S

theorem lower_adjoint.eq_of_le {α : Type u_1} {β : Type u_4} [set_like α β] (l : lower_adjoint coe) {s : set β} {S : α} (h₁ : s ⊆ ↑S) (h₂ : S ≤ ⇑l s) :

⇑l s = S

theorem lower_adjoint.closure_union_closure_subset {α : Type u_1} {β : Type u_4} [set_like α β] (l : lower_adjoint coe) (x y : α) :

↑(⇑l ↑x) ∪ ↑(⇑l ↑y) ⊆ ↑(⇑l (↑x ∪ ↑y))

@[simp]

theorem lower_adjoint.closure_union_closure_left {α : Type u_1} {β : Type u_4} [set_like α β] (l : lower_adjoint coe) (x y : α) :

⇑l (↑(⇑l ↑x) ∪ ↑y) = ⇑l (↑x ∪ ↑y)

@[simp]

theorem lower_adjoint.closure_union_closure_right {α : Type u_1} {β : Type u_4} [set_like α β] (l : lower_adjoint coe) (x y : α) :

⇑l (↑x ∪ ↑(⇑l ↑y)) = ⇑l (↑x ∪ ↑y)

theorem lower_adjoint.closure_union_closure {α : Type u_1} {β : Type u_4} [set_like α β] (l : lower_adjoint coe) (x y : α) :

⇑l (↑(⇑l ↑x) ∪ ↑(⇑l ↑y)) = ⇑l (↑x ∪ ↑y)

@[simp]

theorem lower_adjoint.closure_Union_closure {α : Type u_1} {ι : Sort u_2} {β : Type u_4} [set_like α β] (l : lower_adjoint coe) (f : ι → α) :

⇑l (⋃ (i : ι), ↑(⇑l ↑(f i))) = ⇑l (⋃ (i : ι), ↑(f i))

@[simp]

theorem lower_adjoint.closure_Union₂_closure {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} {β : Type u_4} [set_like α β] (l : lower_adjoint coe) (f : Π (i : ι), κ i → α) :

⇑l (⋃ (i : ι) (j : κ i), ↑(⇑l ↑(f i j))) = ⇑l (⋃ (i : ι) (j : κ i), ↑(f i j))

Translations between `galois_connection`, `lower_adjoint`, `closure_operator` #

def galois_connection.lower_adjoint {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) :

lower_adjoint u

Every Galois connection induces a lower adjoint.

Equations

gc.lower_adjoint = {to_fun := l, gc' := gc}

@[simp]

theorem galois_connection.lower_adjoint_to_fun {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) (ᾰ : α) :

gc.lower_adjoint.to_fun ᾰ = l ᾰ

@[simp]

theorem galois_connection.closure_operator_apply {α : Type u_1} {β : Type u_4} [partial_order α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) (x : α) :

⇑(gc.closure_operator) x = u (⇑(gc.lower_adjoint) x)

def galois_connection.closure_operator {α : Type u_1} {β : Type u_4} [partial_order α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) :

closure_operator α

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.closure_operator = gc.lower_adjoint.closure_operator

def closure_operator.gi {α : Type u_1} [partial_order α] (c : closure_operator α) :

galois_insertion c.to_closed coe

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

Equations

c.gi = {choice := λ (x : α) (hx : ↑(c.to_closed x) ≤ x), ⟨x, _⟩, gc := _, le_l_u := _, choice_eq := _}

@[simp]

theorem closure_operator_gi_self {α : Type u_1} [partial_order α] (c : closure_operator α) :

_.closure_operator = 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.