mathlib documentation

order.closure

Closure operators on a partial order #

We define (bundled) closure operators on a partial order as an monotone (increasing), extensive (inflationary) and idempotent function. We define closed elements for the operator as elements which are fixed by it.

Note that there is close connection to Galois connections and Galois insertions: every closure operator induces a Galois insertion (from the set of closed elements to the underlying type), and every Galois connection induces a closure operator (namely the composition). In particular, a Galois insertion can be seen as a general case of a closure operator, where the inclusion is given by coercion, see closure_operator.gi.

References #

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

structure closure_operator (α : Type u) [partial_order α] :

Type u

to_preorder_hom : α →ₘ α
le_closure' : ∀ (x : α), x ≤ c.to_preorder_hom.to_fun x
idempotent' : ∀ (x : α), c.to_preorder_hom.to_fun (c.to_preorder_hom.to_fun x) = c.to_preorder_hom.to_fun x

A closure operator on the partial order α is a monotone function which is extensive (every x is less than its closure) and idempotent.

@[instance]

def closure_operator.has_coe_to_fun (α : Type u) [partial_order α] :

has_coe_to_fun (closure_operator α)

Equations

closure_operator.has_coe_to_fun α = {F := λ (c : closure_operator α), α → α, coe := λ (c : closure_operator α), c.to_preorder_hom.to_fun}

def closure_operator.simps.apply (α : Type u) [partial_order α] (f : closure_operator α) :

α → α

See Note [custom simps projection]

Equations

closure_operator.simps.apply α f = ⇑f

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

closure_operator α

The identity function as a closure operator.

Equations

closure_operator.id α = {to_preorder_hom := {to_fun := λ (x : α), x, monotone' := _}, le_closure' := _, idempotent' := _}

@[simp]

theorem closure_operator.id_apply (α : Type u) [partial_order α] (x : α) :

⇑(closure_operator.id α) x = x

@[instance]

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

inhabited (closure_operator α)

Equations

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

@[ext]

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

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

@[simp]

theorem closure_operator.mk'_apply {α : Type u} [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} [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_preorder_hom := {to_fun := f, monotone' := hf₁}, le_closure' := hf₂, idempotent' := _}

@[simp]

theorem closure_operator.mk₂_apply {α : Type u} [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} [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_preorder_hom := {to_fun := f, monotone' := _}, le_closure' := hf, idempotent' := _}

@[simp]

theorem closure_operator.mk₃_apply {α : Type u} [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} [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} [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} [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} [partial_order α] (c : closure_operator α) :

theorem closure_operator.le_closure {α : Type u} [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} [partial_order α] (c : closure_operator α) (x : α) :

⇑c (⇑c x) = ⇑c x

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

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

@[simp]

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

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

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

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

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

def closure_operator.closed {α : Type u} [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} [partial_order α] (c : closure_operator α) (x : α) :

x ∈ c.closed ↔ ⇑c x = x

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

x ∈ c.closed ↔ ⇑c x ≤ x

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

⇑c x = x

@[simp]

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

⇑c x ∈ c.closed

theorem closure_operator.closed_eq_range_close {α : Type u} [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} [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, _⟩

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

⊤ ∈ c.closed

@[simp]

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

⇑c x ≤ y ↔ x ≤ y

theorem closure_operator.eq_mk₃_closed {α : Type u} [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} [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

This lemma shows that the p fed into the mk₃ constructor implies being closed.

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

theorem closure_operator.closure_supr_closure {α : Type u} {ι : Type v} [complete_lattice α] (c : closure_operator α) (x : ι → α) :

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

@[simp]

theorem closure_operator.closure_bsupr_closure {α : Type u} [complete_lattice α] (c : closure_operator α) (p : α → Prop) :

⇑c (⨆ (x : α) (H : p x), ⇑c x) = ⇑c (⨆ (x : α) (H : p x), x)

def closure_operator.gi {α : Type u} [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 galois_connection.closure_operator_apply {α : Type u} [partial_order α] {β : Type u} [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u) (x : α) :

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

def galois_connection.closure_operator {α : Type u} [partial_order α] {β : Type u} [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 = {to_preorder_hom := {to_fun := λ (x : α), u (l x), monotone' := _}, le_closure' := _, idempotent' := _}

@[simp]

theorem closure_operator_gi_self {α : Type u} [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.