mathlib3 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 #

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 #

Closure operator #

structure closure_operator (α : Type u_1) [preorder α] :
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.

Instances for closure_operator
@[protected, instance]
Equations

The identity function as a closure operator.

Equations
@[simp]
theorem closure_operator.id_apply (α : Type u_1) [partial_order α] (a : α) :
@[protected, instance]
Equations
@[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) :

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

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

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

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
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.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
theorem closure_operator.mem_closed_iff {α : 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 : α) :

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

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

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 α] :

The identity function as a lower adjoint to itself.

Equations
@[simp]
theorem lower_adjoint.id_to_fun (α : Type u_1) [preorder α] (x : α) :
@[protected, instance]
Equations
@[protected, instance]
def lower_adjoint.has_coe_to_fun {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β α} :
Equations
def lower_adjoint.simps.apply {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β α} (l : lower_adjoint u) :
α β

See Note [custom simps projection]

Equations
theorem lower_adjoint.gc {α : Type u_1} {β : Type u_4} [preorder α] [preorder β] {u : β α} (l : lower_adjoint 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) :
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) :

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
@[simp]
theorem lower_adjoint.closure_operator_apply {α : Type u_1} {β : Type u_4} [partial_order α] [preorder β] {u : β α} (l : lower_adjoint u) (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
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) :

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

Every Galois connection induces a lower adjoint.

Equations
@[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 : α) :
def galois_connection.closure_operator {α : Type u_1} {β : Type u_4} [partial_order α] [preorder β] {l : α β} {u : β α} (gc : galois_connection l u) :

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

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

Equations
@[simp]

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.