Mathlib.Order.Closure

ClosureOperator structure

[Preorder α] extends α →o α

Full source

/-- A closure operator on the preorder `α` is a monotone function which is extensive (every `x`
is less than its closure) and idempotent. -/
structure ClosureOperator [Preorder α] extends α →o α where
  /-- An element is less than or equal its closure -/
  le_closure' : ∀ x, x ≤ toFun x
  /-- Closures are idempotent -/
  idempotent' : ∀ x, toFun (toFun x) = toFun x
  /-- 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 (x : α) : Prop := toFun x = x
  isClosed_iff {x : α} : IsClosed x ↔ toFun x = x := by aesop

Closure operator on a preorder

Informal description

A closure operator on a preorder $\alpha$ is a monotone function $f \colon \alpha \to \alpha$ that is extensive (i.e., $x \leq f(x)$ for all $x \in \alpha$) and idempotent (i.e., $f(f(x)) = f(x)$ for all $x \in \alpha$).

ClosureOperator.instFunLike instance

[Preorder α] : FunLike (ClosureOperator α) α α

Full source

instance [Preorder α] : FunLike (ClosureOperator α) α α where
  coe c := c.1
  coe_injective' := by rintro ⟨⟩ ⟨⟩ h; obtain rfl := DFunLike.ext' h; congr with x; simp_all

Function-Like Structure on Closure Operators

Informal description

For any preorder $\alpha$, the type of closure operators on $\alpha$ can be treated as a function-like type, where each closure operator can be coerced to a function from $\alpha$ to $\alpha$.

ClosureOperator.instOrderHomClass instance

[Preorder α] : OrderHomClass (ClosureOperator α) α α

Full source

instance [Preorder α] : OrderHomClass (ClosureOperator α) α α where
  map_rel f _ _ h := f.mono h

Closure Operators as Order-Preserving Morphisms

Informal description

For any preorder $\alpha$, the type of closure operators on $\alpha$ forms a class of order-preserving morphisms from $\alpha$ to itself. This means that every closure operator $f \colon \alpha \to \alpha$ is monotone (i.e., $x \leq y$ implies $f(x) \leq f(y)$ for all $x, y \in \alpha$).

ClosureOperator.conjBy definition

{α β} [Preorder α] [Preorder β] (c : ClosureOperator α) (e : α ≃o β) : ClosureOperator β

Full source

/-- If `c` is a closure operator on `α` and `e` an order-isomorphism
between `α` and `β` then `e ∘ c ∘ e⁻¹` is a closure operator on `β`. -/
@[simps apply]
def conjBy {α β} [Preorder α] [Preorder β] (c : ClosureOperator α)
    (e : α ≃o β) : ClosureOperator β where
  toFun := e.conj c
  IsClosed b := c.IsClosed (e.symm b)
  monotone' _ _ h :=
    (map_le_map_iff e).mpr <| c.monotone <| (map_le_map_iff e.symm).mpr h
  le_closure' _ := e.symm_apply_le.mp (c.le_closure' _)
  idempotent' _ :=
    congrArg e <| Eq.trans (congrArg c (e.symm_apply_apply _)) (c.idempotent' _)
  isClosed_iff := Iff.trans c.isClosed_iff e.eq_symm_apply

Conjugation of a closure operator by an order isomorphism

Informal description

Given a closure operator $c$ on a preorder $\alpha$ and an order isomorphism $e \colon \alpha \simeq_o \beta$ between preorders $\alpha$ and $\beta$, the function `ClosureOperator.conjBy` constructs a closure operator on $\beta$ defined by the composition $e \circ c \circ e^{-1}$. The resulting closure operator satisfies: 1. **Monotonicity**: For any $x, y \in \beta$, if $x \leq y$, then $(e \circ c \circ e^{-1})(x) \leq (e \circ c \circ e^{-1})(y)$. 2. **Extensivity**: For any $x \in \beta$, $x \leq (e \circ c \circ e^{-1})(x)$. 3. **Idempotence**: For any $x \in \beta$, $(e \circ c \circ e^{-1})((e \circ c \circ e^{-1})(x)) = (e \circ c \circ e^{-1})(x)$. 4. **Closed Elements**: An element $b \in \beta$ is closed under this operator if and only if $e^{-1}(b)$ is closed under $c$.

ClosureOperator.conjBy_refl theorem

{α} [Preorder α] (c : ClosureOperator α) : c.conjBy (OrderIso.refl α) = c

Full source

lemma conjBy_refl {α} [Preorder α] (c : ClosureOperator α) :
    c.conjBy (OrderIso.refl α) = c := rfl

Conjugation by Identity Preserves Closure Operator

Informal description

Let $\alpha$ be a preorder and $c$ be a closure operator on $\alpha$. Then the conjugation of $c$ by the identity order isomorphism $\text{id} \colon \alpha \to \alpha$ equals $c$ itself, i.e., $c \circ \text{id} \circ \text{id}^{-1} = c$.

ClosureOperator.conjBy_trans theorem

 {α β γ} [Preorder α] [Preorder β] [Preorder γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) (c : ClosureOperator α) :
  c.conjBy (e₁.trans e₂) = (c.conjBy e₁).conjBy e₂

Full source

lemma conjBy_trans {α β γ} [Preorder α] [Preorder β] [Preorder γ]
    (e₁ : α ≃o β) (e₂ : β ≃o γ) (c : ClosureOperator α) :
    c.conjBy (e₁.trans e₂) = (c.conjBy e₁).conjBy e₂ := rfl

Composition Property of Conjugated Closure Operators

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be preorders, and let $e_1 \colon \alpha \simeq_o \beta$ and $e_2 \colon \beta \simeq_o \gamma$ be order isomorphisms. For any closure operator $c$ on $\alpha$, the conjugation of $c$ by the composition $e_1 \circ e_2$ is equal to the conjugation of the conjugation of $c$ by $e_1$ by $e_2$. In other words, \[ c.\text{conjBy}(e_1 \circ e_2) = (c.\text{conjBy}(e_1)).\text{conjBy}(e_2). \]

ClosureOperator.id definition

: ClosureOperator α

Full source

/-- The identity function as a closure operator. -/
@[simps!]
def id : ClosureOperator α where
  toOrderHom := OrderHom.id
  le_closure' _ := le_rfl
  idempotent' _ := rfl
  IsClosed _ := True

Identity closure operator

Informal description

The identity function on a preorder $\alpha$ is a closure operator, where for every element $x \in \alpha$, the closure of $x$ is $x$ itself. This operator is trivially monotone, extensive (since $x \leq x$), and idempotent (since applying the identity function twice yields the same result as applying it once).

ClosureOperator.instInhabited instance

: Inhabited (ClosureOperator α)

Full source

instance : Inhabited (ClosureOperator α) :=
  ⟨id α⟩

Existence of Closure Operators on Preorders

Informal description

For any preorder $\alpha$, the type of closure operators on $\alpha$ is inhabited.

ClosureOperator.ext theorem

: ∀ c₁ c₂ : ClosureOperator α, (∀ x, c₁ x = c₂ x) → c₁ = c₂

Full source

@[ext]
theorem ext : ∀ c₁ c₂ : ClosureOperator α, (∀ x, c₁ x = c₂ x) → c₁ = c₂ :=
  DFunLike.ext

Extensionality of Closure Operators

Informal description

For any two closure operators $c_1$ and $c_2$ on a preorder $\alpha$, if $c_1(x) = c_2(x)$ for all $x \in \alpha$, then $c_1 = c_2$.

ClosureOperator.mk' definition

(f : α → α) (hf₁ : Monotone f) (hf₂ : ∀ x, x ≤ f x) (hf₃ : ∀ x, f (f x) ≤ f x) : ClosureOperator α

Full source

/-- Constructor for a closure operator using the weaker idempotency axiom: `f (f x) ≤ f x`. -/
@[simps]
def mk' (f : α → α) (hf₁ : Monotone f) (hf₂ : ∀ x, x ≤ f x) (hf₃ : ∀ x, f (f x) ≤ f x) :
    ClosureOperator α where
  toFun := f
  monotone' := hf₁
  le_closure' := hf₂
  idempotent' x := (hf₃ x).antisymm (hf₁ (hf₂ x))

Construction of a closure operator from monotonicity, extensivity, and weak idempotency

Informal description

Given a function $f \colon \alpha \to \alpha$ on a preorder $\alpha$ that is monotone, extensive (i.e., $x \leq f(x)$ for all $x \in \alpha$), and weakly idempotent (i.e., $f(f(x)) \leq f(x)$ for all $x \in \alpha$), then $f$ defines a closure operator on $\alpha$.

ClosureOperator.mk₂ definition

(f : α → α) (hf : ∀ x, x ≤ f x) (hmin : ∀ ⦃x y⦄, x ≤ f y → f x ≤ f y) : ClosureOperator α

Full source

/-- 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. -/
@[simps]
def mk₂ (f : α → α) (hf : ∀ x, x ≤ f x) (hmin : ∀ ⦃x y⦄, x ≤ f y → f x ≤ f y) :
    ClosureOperator α where
  toFun := f
  monotone' _ y hxy := hmin (hxy.trans (hf y))
  le_closure' := hf
  idempotent' _ := (hmin le_rfl).antisymm (hf _)

Construction of a closure operator from extensivity and minimality conditions

Informal description

Given a function $f \colon \alpha \to \alpha$ on a preorder $\alpha$ such that: 1. (Extensivity) For all $x \in \alpha$, $x \leq f(x)$. 2. (Minimality) For all $x, y \in \alpha$, if $x \leq f(y)$, then $f(x) \leq f(y)$. Then $f$ defines a closure operator on $\alpha$, i.e., a monotone, extensive, and idempotent function.

ClosureOperator.ofPred definition

 (f : α → α) (p : α → Prop) (hf : ∀ x, x ≤ f x) (hfp : ∀ x, p (f x)) (hmin : ∀ ⦃x y⦄, x ≤ y → p y → f x ≤ y) :
  ClosureOperator α

Full source

/-- 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`. -/
@[simps!]
def ofPred (f : α → α) (p : α → Prop) (hf : ∀ x, x ≤ f x) (hfp : ∀ x, p (f x))
    (hmin : ∀ ⦃x y⦄, x ≤ y → p y → f x ≤ y) : ClosureOperator α where
  __ := mk₂ f hf fun _ y hxy => hmin hxy (hfp y)
  IsClosed := p
  isClosed_iff := ⟨fun hx ↦ (hmin le_rfl hx).antisymm <| hf _, fun hx ↦ hx ▸ hfp _⟩

Construction of a closure operator from a closedness predicate

Informal description

Given a function $f \colon \alpha \to \alpha$ on a preorder $\alpha$ and a predicate $p \colon \alpha \to \mathrm{Prop}$ (representing "closedness"), if: 1. (Extensivity) For all $x \in \alpha$, $x \leq f(x)$. 2. (Closedness of image) For all $x \in \alpha$, $p(f(x))$ holds. 3. (Minimality) For all $x, y \in \alpha$, if $x \leq y$ and $p(y)$ holds, then $f(x) \leq y$. Then $f$ defines a closure operator on $\alpha$, where the closed elements are precisely those satisfying $p$. Moreover, for any $x \in \alpha$, $f(x)$ is the smallest closed element greater than or equal to $x$.

ClosureOperator.monotone theorem

: Monotone c

Full source

@[mono]
theorem monotone : Monotone c :=
  c.monotone'

Monotonicity of Closure Operators

Informal description

For any closure operator $c$ on a preorder $\alpha$, the function $c$ is monotone, i.e., for all $x, y \in \alpha$, if $x \leq y$ then $c(x) \leq c(y)$.

ClosureOperator.le_closure theorem

(x : α) : x ≤ c x

Full source

/-- Every element is less than its closure. This property is sometimes referred to as extensivity or
inflationarity. -/
theorem le_closure (x : α) : x ≤ c x :=
  c.le_closure' x

Extensivity of Closure Operators: $x \leq c(x)$

Informal description

For any element $x$ in a preorder $\alpha$ and any closure operator $c$ on $\alpha$, the element $x$ is less than or equal to its closure under $c$, i.e., $x \leq c(x)$.

ClosureOperator.idempotent theorem

(x : α) : c (c x) = c x

Full source

@[simp]
theorem idempotent (x : α) : c (c x) = c x :=
  c.idempotent' x

Idempotence of Closure Operators: $c(c(x)) = c(x)$

Informal description

For any closure operator $c$ on a preorder $\alpha$ and any element $x \in \alpha$, the operator is idempotent, i.e., $c(c(x)) = c(x)$.

ClosureOperator.isClosed_closure theorem

(x : α) : c.IsClosed (c x)

Full source

@[simp] lemma isClosed_closure (x : α) : c.IsClosed (c x) := c.isClosed_iff.2 <| c.idempotent x

Closure of an Element is Closed

Informal description

For any closure operator $c$ on a preorder $\alpha$ and any element $x \in \alpha$, the closure $c(x)$ is closed under $c$, i.e., $c(c(x)) = c(x)$.

ClosureOperator.Closeds abbrev

Full source

/-- The type of elements closed under a closure operator. -/
abbrev Closeds := {x // c.IsClosed x}

Closed Elements under a Closure Operator

Informal description

The type of elements in a preorder $\alpha$ that are closed under a closure operator $c \colon \alpha \to \alpha$, i.e., elements $x \in \alpha$ satisfying $c(x) = x$.

ClosureOperator.toCloseds definition

(x : α) : c.Closeds

Full source

/-- Send an element to a closed element (by taking the closure). -/
def toCloseds (x : α) : c.Closeds := ⟨c x, c.isClosed_closure x⟩

Closure of an element as a closed element

Informal description

Given a closure operator $c$ on a preorder $\alpha$ and an element $x \in \alpha$, the function maps $x$ to its closure $c(x)$, viewed as a closed element (i.e., an element satisfying $c(c(x)) = c(x)$).

ClosureOperator.IsClosed.closure_eq theorem

: c.IsClosed x → c x = x

Full source

theorem IsClosed.closure_eq : c.IsClosed x → c x = x := c.isClosed_iff.1

Fixed Point Property of Closed Elements under a Closure Operator

Informal description

If an element $x$ in a preorder $\alpha$ is closed under a closure operator $c \colon \alpha \to \alpha$, then $c(x) = x$.

ClosureOperator.isClosed_iff_closure_le theorem

: c.IsClosed x ↔ c x ≤ x

Full source

theorem isClosed_iff_closure_le : c.IsClosed x ↔ c x ≤ x :=
  ⟨fun h ↦ h.closure_eq.le, fun h ↦ c.isClosed_iff.2 <| h.antisymm <| c.le_closure x⟩

Characterization of Closed Elements via Closure Operator: $c(x) \leq x$

Informal description

An element $x$ in a preorder $\alpha$ is closed under a closure operator $c \colon \alpha \to \alpha$ if and only if its closure $c(x)$ is less than or equal to $x$.

ClosureOperator.setOf_isClosed_eq_range_closure theorem

: {x | c.IsClosed x} = Set.range c

Full source

/-- The set of closed elements for `c` is exactly its range. -/
theorem setOf_isClosed_eq_range_closure : {x | c.IsClosed x} = Set.range c := by
  ext x; exact ⟨fun hx ↦ ⟨x, hx.closure_eq⟩, by rintro ⟨y, rfl⟩; exact c.isClosed_closure _⟩

Closed Elements of a Closure Operator Coincide with Its Range

Informal description

For a closure operator $c$ on a preorder $\alpha$, the set of closed elements $\{x \in \alpha \mid c(x) = x\}$ is equal to the range of $c$, i.e., $\{c(x) \mid x \in \alpha\}$.

ClosureOperator.le_closure_iff theorem

: x ≤ c y ↔ c x ≤ c y

Full source

theorem le_closure_iff : x ≤ c y ↔ c x ≤ c y :=
  ⟨fun h ↦ c.idempotent y ▸ c.monotone h, (c.le_closure x).trans⟩

Characterization of Closure Ordering: $x \leq c(y) \leftrightarrow c(x) \leq c(y)$

Informal description

For any elements $x, y$ in a preorder $\alpha$ and any closure operator $c$ on $\alpha$, the inequality $x \leq c(y)$ holds if and only if $c(x) \leq c(y)$.

ClosureOperator.IsClosed.closure_le_iff theorem

(hy : c.IsClosed y) : c x ≤ y ↔ x ≤ y

Full source

@[simp]
theorem IsClosed.closure_le_iff (hy : c.IsClosed y) : c x ≤ y ↔ x ≤ y := by
  rw [← hy.closure_eq, ← le_closure_iff]

Characterization of Closure Inequality for Closed Elements: $c(x) \leq y \leftrightarrow x \leq y$ when $y$ is closed

Informal description

For any closure operator $c$ on a preorder $\alpha$ and any element $y \in \alpha$ that is closed under $c$ (i.e., $c(y) = y$), the inequality $c(x) \leq y$ holds if and only if $x \leq y$.

ClosureOperator.closure_min theorem

(hxy : x ≤ y) (hy : c.IsClosed y) : c x ≤ y

Full source

lemma closure_min (hxy : x ≤ y) (hy : c.IsClosed y) : c x ≤ y := hy.closure_le_iff.2 hxy

Closure Operator Minimality Property: $c(x) \leq y$ for $x \leq y$ with $y$ closed

Informal description

Let $c$ be a closure operator on a preorder $\alpha$, and let $x, y \in \alpha$ such that $x \leq y$ and $y$ is closed under $c$ (i.e., $c(y) = y$). Then the closure of $x$ satisfies $c(x) \leq y$.

ClosureOperator.closure_isGLB theorem

(x : α) : IsGLB {y | x ≤ y ∧ c.IsClosed y} (c x)

Full source

lemma closure_isGLB (x : α) : IsGLB { y | x ≤ y ∧ c.IsClosed y } (c x) where
  left _ := and_imp.mpr closure_min
  right _ h := h ⟨c.le_closure x, c.isClosed_closure x⟩

Closure as Greatest Lower Bound of Closed Elements Above

Informal description

For any closure operator $c$ on a preorder $\alpha$ and any element $x \in \alpha$, the closure $c(x)$ is the greatest lower bound of the set $\{y \in \alpha \mid x \leq y \text{ and } c(y) = y\}$ of all closed elements above $x$.

ClosureOperator.ext_isClosed theorem

(c₁ c₂ : ClosureOperator α) (h : ∀ x, c₁.IsClosed x ↔ c₂.IsClosed x) : c₁ = c₂

Full source

theorem ext_isClosed (c₁ c₂ : ClosureOperator α)
    (h : ∀ x, c₁.IsClosed x ↔ c₂.IsClosed x) : c₁ = c₂ :=
  ext c₁ c₂ <| fun x => IsGLB.unique (c₁.closure_isGLB x) <|
    (Set.ext (and_congr_right' <| h ·)).substr (c₂.closure_isGLB x)

Equality of Closure Operators via Closed Elements

Informal description

For any two closure operators $c_1$ and $c_2$ on a preorder $\alpha$, if an element $x \in \alpha$ is closed under $c_1$ if and only if it is closed under $c_2$ (i.e., $c_1(x) = x \leftrightarrow c_2(x) = x$ for all $x \in \alpha$), then $c_1 = c_2$.

ClosureOperator.closure_top theorem

: c ⊤ = ⊤

Full source

@[simp]
theorem closure_top : c ⊤ = ⊤ :=
  le_top.antisymm (c.le_closure _)

Closure of Top Element is Top

Informal description

For any closure operator $c$ on a preorder $\alpha$ with a greatest element $\top$, the closure of $\top$ is $\top$ itself, i.e., $c(\top) = \top$.

ClosureOperator.isClosed_top theorem

: c.IsClosed ⊤

Full source

@[simp] lemma isClosed_top : c.IsClosed ⊤ := c.isClosed_iff.2 c.closure_top

Top Element is Closed Under Closure Operator

Informal description

For any closure operator $c$ on a preorder $\alpha$ with a greatest element $\top$, the element $\top$ is closed under $c$, i.e., $c(\top) = \top$.

ClosureOperator.closure_inf_le theorem

[SemilatticeInf α] (c : ClosureOperator α) (x y : α) : c (x ⊓ y) ≤ c x ⊓ c y

Full source

theorem closure_inf_le [SemilatticeInf α] (c : ClosureOperator α) (x y : α) :
    c (x ⊓ y) ≤ c x ⊓ c y :=
  c.monotone.map_inf_le _ _

Closure Operator Preserves Meet Inequality

Informal description

Let $\alpha$ be a meet-semilattice and $c$ a closure operator on $\alpha$. For any elements $x, y \in \alpha$, the closure of their meet is less than or equal to the meet of their closures, i.e., $c(x \sqcap y) \leq c(x) \sqcap c(y)$.

ClosureOperator.closure_sup_closure_le theorem

(x y : α) : c x ⊔ c y ≤ c (x ⊔ y)

Full source

theorem closure_sup_closure_le (x y : α) : c x ⊔ c y ≤ c (x ⊔ y) :=
  c.monotone.le_map_sup _ _

Closure Operator Preserves Supremum Inequality

Informal description

For any closure operator $c$ on a preorder $\alpha$ and any elements $x, y \in \alpha$, the supremum of $c(x)$ and $c(y)$ is less than or equal to $c$ applied to the supremum of $x$ and $y$, i.e., $c(x) \sqcup c(y) \leq c(x \sqcup y)$.

ClosureOperator.closure_sup_closure_left theorem

(x y : α) : c (c x ⊔ y) = c (x ⊔ y)

Full source

theorem closure_sup_closure_left (x y : α) : c (c x ⊔ y) = c (x ⊔ y) :=
  (le_closure_iff.1
        (sup_le (c.monotone le_sup_left) (le_sup_right.trans (c.le_closure _)))).antisymm
    (c.monotone (sup_le_sup_right (c.le_closure _) _))

Closure Operator Preserves Supremum with Left Closure: $c(c(x) \sqcup y) = c(x \sqcup y)$

Informal description

For any elements $x, y$ in a preorder $\alpha$ and any closure operator $c$ on $\alpha$, the closure of the supremum of $c(x)$ and $y$ equals the closure of the supremum of $x$ and $y$, i.e., $c(c(x) \sqcup y) = c(x \sqcup y)$.

ClosureOperator.closure_sup_closure_right theorem

(x y : α) : c (x ⊔ c y) = c (x ⊔ y)

Full source

theorem closure_sup_closure_right (x y : α) : c (x ⊔ c y) = c (x ⊔ y) := by
  rw [sup_comm, closure_sup_closure_left, sup_comm (a := x)]

Closure Operator Preserves Supremum with Right Closure: $c(x \sqcup c(y)) = c(x \sqcup y)$

Informal description

For any elements $x, y$ in a preorder $\alpha$ and any closure operator $c$ on $\alpha$, the closure of the supremum of $x$ and $c(y)$ equals the closure of the supremum of $x$ and $y$, i.e., $c(x \sqcup c(y)) = c(x \sqcup y)$.

ClosureOperator.closure_sup_closure theorem

(x y : α) : c (c x ⊔ c y) = c (x ⊔ y)

Full source

theorem closure_sup_closure (x y : α) : c (c x ⊔ c y) = c (x ⊔ y) := by
  rw [closure_sup_closure_left, closure_sup_closure_right]

Closure Operator Preserves Supremum with Both Closures: $c(c(x) \sqcup c(y)) = c(x \sqcup y)$

Informal description

For any elements $x, y$ in a preorder $\alpha$ and any closure operator $c$ on $\alpha$, the closure of the supremum of $c(x)$ and $c(y)$ equals the closure of the supremum of $x$ and $y$, i.e., $c(c(x) \sqcup c(y)) = c(x \sqcup y)$.

ClosureOperator.ofCompletePred definition

(p : α → Prop) (hsinf : ∀ s, (∀ a ∈ s, p a) → p (sInf s)) : ClosureOperator α

Full source

/-- Define a closure operator from a predicate that's preserved under infima. -/
@[simps!]
def ofCompletePred (p : α → Prop) (hsinf : ∀ s, (∀ a ∈ s, p a) → p (sInf s)) : ClosureOperator α :=
  ofPred (fun a ↦ ⨅ b : {b // a ≤ b ∧ p b}, b) p
    (fun a ↦ by simp +contextual)
    (fun _ ↦ hsinf _ <| forall_mem_range.2 fun b ↦ b.2.2)
    (fun _ b hab hb ↦ iInf_le_of_le ⟨b, hab, hb⟩ le_rfl)

Closure operator from infimum-preserving predicate

Informal description

Given a preorder $\alpha$ and a predicate $p \colon \alpha \to \mathrm{Prop}$ that is preserved under infima (i.e., for any subset $S \subseteq \alpha$ where every element satisfies $p$, the infimum $\bigsqcap S$ also satisfies $p$), the function that maps each $a \in \alpha$ to the infimum of all upper bounds of $a$ that satisfy $p$ defines a closure operator on $\alpha$. The closed elements of this operator are precisely those satisfying $p$.

ClosureOperator.sInf_isClosed theorem

{c : ClosureOperator α} {S : Set α} (H : ∀ x ∈ S, c.IsClosed x) : c.IsClosed (sInf S)

Full source

theorem sInf_isClosed {c : ClosureOperator α} {S : Set α}
    (H : ∀ x ∈ S, c.IsClosed x) : c.IsClosed (sInf S) :=
  isClosed_iff_closure_le.mpr <| le_of_le_of_eq c.monotone.map_sInf_le <|
    Eq.trans (biInf_congr (c.isClosed_iff.mp <| H · ·)) sInf_eq_iInf.symm

Infimum of Closed Elements is Closed under a Closure Operator

Informal description

Let $\alpha$ be a preorder, $c$ a closure operator on $\alpha$, and $S$ a subset of $\alpha$ such that every element of $S$ is closed under $c$ (i.e., $c(x) \leq x$ for all $x \in S$). Then the infimum of $S$ is also closed under $c$, i.e., $c(\bigsqcap S) \leq \bigsqcap S$.

ClosureOperator.closure_iSup_closure theorem

(f : ι → α) : c (⨆ i, c (f i)) = c (⨆ i, f i)

Full source

@[simp]
theorem closure_iSup_closure (f : ι → α) : c (⨆ i, c (f i)) = c (⨆ i, f i) :=
  le_antisymm (le_closure_iff.1 <| iSup_le fun i => c.monotone <| le_iSup f i) <|
    c.monotone <| iSup_mono fun _ => c.le_closure _

Closure Commutes with Supremum of Closures: $c(\bigsqcup_i c(f_i)) = c(\bigsqcup_i f_i)$

Informal description

For any closure operator $c$ on a preorder $\alpha$ and any indexed family of elements $f \colon \iota \to \alpha$, the closure of the supremum of the closures equals the closure of the supremum, i.e., $$ c\left(\bigsqcup_{i} c(f_i)\right) = c\left(\bigsqcup_{i} f_i\right). $$

ClosureOperator.closure_iSup₂_closure theorem

(f : ∀ i, κ i → α) : c (⨆ (i) (j), c (f i j)) = c (⨆ (i) (j), f i j)

Full source

@[simp]
theorem closure_iSup₂_closure (f : ∀ i, κ i → α) :
    c (⨆ (i) (j), c (f i j)) = c (⨆ (i) (j), f i j) :=
  le_antisymm (le_closure_iff.1 <| iSup₂_le fun i j => c.monotone <| le_iSup₂ i j) <|
    c.monotone <| iSup₂_mono fun _ _ => c.le_closure _

Closure of Supremum of Closures Equals Closure of Supremum for Doubly Indexed Family

Informal description

Let $\alpha$ be a preorder and $c$ be a closure operator on $\alpha$. For any doubly indexed family of elements $(f_{i,j})_{i \in \iota, j \in \kappa_i}$ in $\alpha$, the closure of the supremum of the closures satisfies: \[ c\left(\bigsqcup_{i,j} c(f_{i,j})\right) = c\left(\bigsqcup_{i,j} f_{i,j}\right). \]

OrderIso.equivClosureOperator definition

{α β} [Preorder α] [Preorder β] (e : α ≃o β) : ClosureOperator α ≃ ClosureOperator β

Full source

/-- Conjugating `ClosureOperators` on `α` and on `β` by a fixed isomorphism
`e : α ≃o β` gives an equivalence `ClosureOperator α ≃ ClosureOperator β`. -/
@[simps apply symm_apply]
def OrderIso.equivClosureOperator {α β} [Preorder α] [Preorder β] (e : α ≃o β) :
    ClosureOperatorClosureOperator α ≃ ClosureOperator β where
  toFun     c := c.conjBy e
  invFun    c := c.conjBy e.symm
  left_inv  c := Eq.trans (c.conjBy_trans _ _).symm
                 <| Eq.trans (congrArg _ e.self_trans_symm) c.conjBy_refl
  right_inv c := Eq.trans (c.conjBy_trans _ _).symm
                 <| Eq.trans (congrArg _ e.symm_trans_self) c.conjBy_refl

Equivalence of closure operators via order isomorphism

Informal description

Given an order isomorphism $e \colon \alpha \simeq_o \beta$ between preorders $\alpha$ and $\beta$, the function `OrderIso.equivClosureOperator` constructs an equivalence between the types of closure operators on $\alpha$ and $\beta$. Specifically, it maps a closure operator $c$ on $\alpha$ to the closure operator $e \circ c \circ e^{-1}$ on $\beta$, and conversely maps a closure operator $d$ on $\beta$ to $e^{-1} \circ d \circ e$ on $\alpha$. These operations are mutual inverses, establishing a bijective correspondence between closure operators on $\alpha$ and $\beta$.

LowerAdjoint structure

[Preorder α] [Preorder β] (u : β → α)

Full source

/-- 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 `(↑) : β → α`. -/
structure LowerAdjoint [Preorder α] [Preorder β] (u : β → α) where
  /-- The underlying function -/
  toFun : α → β
  /-- The underlying function is a lower adjoint. -/
  gc' : GaloisConnection toFun u

Lower adjoint function forming a Galois connection

Informal description

A lower adjoint to a function $u : \beta \to \alpha$ between preorders is a function $l : \alpha \to \beta$ such that $l$ and $u$ form a Galois connection. This structure allows defining closure operators where the output type differs from the input type, with $u$ often being a coercion like $(↑) : \beta \to \alpha$.

LowerAdjoint.id definition

[Preorder α] : LowerAdjoint (id : α → α)

Full source

/-- The identity function as a lower adjoint to itself. -/
@[simps]
protected def id [Preorder α] : LowerAdjoint (id : α → α) where
  toFun x := x
  gc' := GaloisConnection.id

Identity as a lower adjoint

Informal description

The identity function on a preorder $\alpha$ is a lower adjoint to itself, forming a trivial Galois connection where both the lower adjoint and the upper adjoint are the identity function.

LowerAdjoint.instInhabitedId instance

[Preorder α] : Inhabited (LowerAdjoint (id : α → α))

Full source

instance [Preorder α] : Inhabited (LowerAdjoint (id : α → α)) :=
  ⟨LowerAdjoint.id α⟩

Inhabited Lower Adjoints to the Identity Function

Informal description

For any preorder $\alpha$, the identity function $\mathrm{id} : \alpha \to \alpha$ has a lower adjoint structure, making the type of lower adjoints to $\mathrm{id}$ inhabited.

LowerAdjoint.instCoeFunForall instance

: CoeFun (LowerAdjoint u) fun _ => α → β

Full source

instance : CoeFun (LowerAdjoint u) fun _ => α → β where coe := toFun

Coercion of Lower Adjoint to Function

Informal description

For any lower adjoint function $l$ associated with $u : \beta \to \alpha$ between preorders, $l$ can be treated as a function from $\alpha$ to $\beta$ via a coercion.

LowerAdjoint.gc theorem

: GaloisConnection l u

Full source

theorem gc : GaloisConnection l u :=
  l.gc'

Galois Connection Property of Lower Adjoint

Informal description

For a lower adjoint function $l : \alpha \to \beta$ and a function $u : \beta \to \alpha$ between preorders, $l$ and $u$ form a Galois connection. That is, for all $x \in \alpha$ and $y \in \beta$, we have $l(x) \leq y \leftrightarrow x \leq u(y)$.

LowerAdjoint.ext theorem

: ∀ l₁ l₂ : LowerAdjoint u, (l₁ : α → β) = (l₂ : α → β) → l₁ = l₂

Full source

@[ext]
theorem ext : ∀ l₁ l₂ : LowerAdjoint u, (l₁ : α → β) = (l₂ : α → β) → l₁ = l₂
  | ⟨l₁, _⟩, ⟨l₂, _⟩, h => by
    congr

Extensionality of Lower Adjoints

Informal description

For any two lower adjoints $l_1$ and $l_2$ to a function $u : \beta \to \alpha$ between preorders, if the underlying functions $l_1, l_2 : \alpha \to \beta$ are equal, then $l_1 = l_2$ as lower adjoints.

LowerAdjoint.monotone theorem

: Monotone (u ∘ l)

Full source

@[mono]
theorem monotone : Monotone (u ∘ l) :=
  l.gc.monotone_u.comp l.gc.monotone_l

Monotonicity of the Composition of a Lower Adjoint and its Upper Adjoint

Informal description

For a lower adjoint function $l \colon \alpha \to \beta$ and a function $u \colon \beta \to \alpha$ between preorders that form a Galois connection, the composition $u \circ l$ is a monotone function from $\alpha$ to itself. That is, for any $x, y \in \alpha$, if $x \leq y$, then $u(l(x)) \leq u(l(y))$.

LowerAdjoint.le_closure theorem

(x : α) : x ≤ u (l x)

Full source

/-- Every element is less than its closure. This property is sometimes referred to as extensivity or
inflationarity. -/
theorem le_closure (x : α) : x ≤ u (l x) :=
  l.gc.le_u_l _

Extensivity of Closure: $x \leq u(l(x))$

Informal description

For any element $x$ in a preorder $\alpha$, and given a lower adjoint function $l \colon \alpha \to \beta$ and a function $u \colon \beta \to \alpha$ forming a Galois connection, the element $x$ is less than or equal to its closure under the composition $u \circ l$, i.e., $x \leq u(l(x))$.

LowerAdjoint.closureOperator definition

: ClosureOperator α

Full source

/-- 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. -/
@[simps]
def closureOperator : ClosureOperator α where
  toFun x := u (l x)
  monotone' := l.monotone
  le_closure' := l.le_closure
  idempotent' x := l.gc.u_l_u_eq_u (l x)

Closure operator induced by a lower adjoint

Informal description

Given a lower adjoint function $l \colon \alpha \to \beta$ and a monotone function $u \colon \beta \to \alpha$ between preorders that form a Galois connection, the composition $u \circ l$ defines a closure operator on $\alpha$. This operator is monotone, extensive (satisfying $x \leq u(l(x))$ for all $x \in \alpha$), and idempotent (satisfying $u(l(u(l(x)))) = u(l(x))$ for all $x \in \alpha$).

LowerAdjoint.idempotent theorem

(x : α) : u (l (u (l x))) = u (l x)

Full source

theorem idempotent (x : α) : u (l (u (l x))) = u (l x) :=
  l.closureOperator.idempotent _

Idempotence of Closure Operator Induced by Lower Adjoint: $u \circ l \circ u \circ l = u \circ l$

Informal description

For any element $x$ in a preorder $\alpha$, and given a lower adjoint function $l \colon \alpha \to \beta$ and a function $u \colon \beta \to \alpha$ forming a Galois connection, the composition $u \circ l$ is idempotent, i.e., $u(l(u(l(x)))) = u(l(x))$.

LowerAdjoint.le_closure_iff theorem

(x y : α) : x ≤ u (l y) ↔ u (l x) ≤ u (l y)

Full source

theorem le_closure_iff (x y : α) : x ≤ u (l y) ↔ u (l x) ≤ u (l y) :=
  l.closureOperator.le_closure_iff

Characterization of Closure Ordering via Lower Adjoint: $x \leq u(l(y)) \leftrightarrow u(l(x)) \leq u(l(y))$

Informal description

For any elements $x, y$ in a preorder $\alpha$ and a lower adjoint function $l \colon \alpha \to \beta$ with corresponding function $u \colon \beta \to \alpha$, the inequality $x \leq u(l(y))$ holds if and only if $u(l(x)) \leq u(l(y))$.

LowerAdjoint.closed definition

: Set α

Full source

/-- An element `x` is closed for `l : LowerAdjoint u` if it is a fixed point: `u (l x) = x` -/
def closed : Set α := {x | u (l x) = x}

Set of closed elements for a lower adjoint

Informal description

The set of closed elements for a lower adjoint function `l : α → β` with respect to `u : β → α` consists of all elements `x ∈ α` that are fixed points of the composition `u ∘ l`, i.e., satisfying `u (l x) = x`.

LowerAdjoint.mem_closed_iff theorem

(x : α) : x ∈ l.closed ↔ u (l x) = x

Full source

theorem mem_closed_iff (x : α) : x ∈ l.closedx ∈ l.closed ↔ u (l x) = x :=
  Iff.rfl

Characterization of Closed Elements via Lower Adjoint Fixpoint Condition

Informal description

For any element $x$ in a preorder $\alpha$, $x$ belongs to the set of closed elements of a lower adjoint $l$ (with respect to $u : \beta \to \alpha$) if and only if the composition $u \circ l$ fixes $x$, i.e., $u(l(x)) = x$.

LowerAdjoint.closure_eq_self_of_mem_closed theorem

{x : α} (h : x ∈ l.closed) : u (l x) = x

Full source

theorem closure_eq_self_of_mem_closed {x : α} (h : x ∈ l.closed) : u (l x) = x :=
  h

Fixed Point Property for Closed Elements under Lower Adjoint Composition

Informal description

For any element $x$ in the set of closed elements of a lower adjoint $l$ (i.e., $x \in l.\text{closed}$), the composition $u \circ l$ fixes $x$, that is, $u(l(x)) = x$.

LowerAdjoint.mem_closed_iff_closure_le theorem

(x : α) : x ∈ l.closed ↔ u (l x) ≤ x

Full source

theorem mem_closed_iff_closure_le (x : α) : x ∈ l.closedx ∈ l.closed ↔ u (l x) ≤ x :=
  l.closureOperator.isClosed_iff_closure_le

Characterization of Closed Elements via Lower Adjoint Inequality: $u(l(x)) \leq x$

Informal description

For any element $x$ in a preorder $\alpha$, $x$ belongs to the set of closed elements of a lower adjoint $l$ (with respect to $u : \beta \to \alpha$) if and only if the composition $u \circ l$ applied to $x$ is less than or equal to $x$, i.e., $u(l(x)) \leq x$.

LowerAdjoint.closure_is_closed theorem

(x : α) : u (l x) ∈ l.closed

Full source

@[simp]
theorem closure_is_closed (x : α) : u (l x) ∈ l.closed :=
  l.idempotent x

Closure of Any Element is Closed under Lower Adjoint Composition

Informal description

For any element $x$ in a preorder $\alpha$, the image of $x$ under the composition $u \circ l$ of a lower adjoint $l \colon \alpha \to \beta$ and a function $u \colon \beta \to \alpha$ forming a Galois connection is a closed element, i.e., $u(l(x)) \in l.\text{closed}$.

LowerAdjoint.closed_eq_range_close theorem

: l.closed = Set.range (u ∘ l)

Full source

/-- The set of closed elements for `l` is the range of `u ∘ l`. -/
theorem closed_eq_range_close : l.closed = Set.range (u ∘ l) :=
  l.closureOperator.setOf_isClosed_eq_range_closure

Closed Elements as Range of Closure Operator Induced by Lower Adjoint

Informal description

For a lower adjoint function $l \colon \alpha \to \beta$ with respect to $u \colon \beta \to \alpha$ between preorders, the set of closed elements $\{x \in \alpha \mid u(l(x)) = x\}$ is equal to the range of the composition $u \circ l \colon \alpha \to \alpha$.

LowerAdjoint.toClosed definition

(x : α) : l.closed

Full source

/-- Send an `x` to an element of the set of closed elements (by taking the closure). -/
def toClosed (x : α) : l.closed :=
  ⟨u (l x), l.closure_is_closed x⟩

Closure of an element under a lower adjoint

Informal description

Given a lower adjoint function `l : α → β` with respect to `u : β → α` between preorders, the function maps an element `x : α` to the closed element `u (l x)` in the set of closed elements of `l`.

LowerAdjoint.closure_le_closed_iff_le theorem

(x : α) {y : α} (hy : l.closed y) : u (l x) ≤ y ↔ x ≤ y

Full source

@[simp]
theorem closure_le_closed_iff_le (x : α) {y : α} (hy : l.closed y) : u (l x) ≤ y ↔ x ≤ y :=
  (show l.closureOperator.IsClosed y from hy).closure_le_iff

Characterization of Closure Inequality for Closed Elements: $u(l(x)) \leq y \leftrightarrow x \leq y$ when $y$ is closed

Informal description

Let $\alpha$ and $\beta$ be preorders, $u \colon \beta \to \alpha$ a monotone function, and $l \colon \alpha \to \beta$ a lower adjoint to $u$. For any $x \in \alpha$ and any closed element $y \in \alpha$ (i.e., $u(l(y)) = y$), the inequality $u(l(x)) \leq y$ holds if and only if $x \leq y$.

LowerAdjoint.closure_top theorem

[PartialOrder α] [OrderTop α] [Preorder β] {u : β → α} (l : LowerAdjoint u) : u (l ⊤) = ⊤

Full source

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

Closure of Top Element under Lower Adjoint Equals Top

Informal description

Let $\alpha$ be a partial order with a greatest element $\top$, and $\beta$ be a preorder. For any lower adjoint function $l \colon \alpha \to \beta$ to a monotone function $u \colon \beta \to \alpha$, the closure of $\top$ under the induced closure operator $u \circ l$ equals $\top$, i.e., $u(l(\top)) = \top$.

LowerAdjoint.closure_inf_le theorem

 [SemilatticeInf α] [Preorder β] {u : β → α} (l : LowerAdjoint u) (x y : α) : u (l (x ⊓ y)) ≤ u (l x) ⊓ u (l y)

Full source

theorem closure_inf_le [SemilatticeInf α] [Preorder β] {u : β → α} (l : LowerAdjoint u) (x y : α) :
    u (l (x ⊓ y)) ≤ u (l x) ⊓ u (l y) :=
  l.closureOperator.closure_inf_le x y

Closure of Meet Under Lower Adjoint is Bounded by Meet of Closures

Informal description

Let $\alpha$ be a meet-semilattice and $\beta$ a preorder. Given a lower adjoint function $l \colon \alpha \to \beta$ and a monotone function $u \colon \beta \to \alpha$ forming a Galois connection, for any elements $x, y \in \alpha$, the closure of their meet satisfies $u(l(x \sqcap y)) \leq u(l(x)) \sqcap u(l(y))$.

LowerAdjoint.closure_sup_closure_le theorem

(x y : α) : u (l x) ⊔ u (l y) ≤ u (l (x ⊔ y))

Full source

theorem closure_sup_closure_le (x y : α) : u (l x) ⊔ u (l y) ≤ u (l (x ⊔ y)) :=
  l.closureOperator.closure_sup_closure_le x y

Closure Inequality for Suprema under Lower Adjoint Composition

Informal description

Let $\alpha$ and $\beta$ be preorders, $u \colon \beta \to \alpha$ a monotone function, and $l \colon \alpha \to \beta$ its lower adjoint forming a Galois connection. For any elements $x, y$ in a join-semilattice $\alpha$, the supremum of the closures $u(l(x))$ and $u(l(y))$ is less than or equal to the closure of their supremum, i.e., \[ u(l(x)) \sqcup u(l(y)) \leq u(l(x \sqcup y)). \]

LowerAdjoint.closure_sup_closure_left theorem

(x y : α) : u (l (u (l x) ⊔ y)) = u (l (x ⊔ y))

Full source

theorem closure_sup_closure_left (x y : α) : u (l (u (l x) ⊔ y)) = u (l (x ⊔ y)) :=
  l.closureOperator.closure_sup_closure_left x y

Closure of Supremum with Left Closure under Lower Adjoint: $u(l(u(l(x)) \sqcup y)) = u(l(x \sqcup y))$

Informal description

Let $\alpha$ and $\beta$ be preorders, $u \colon \beta \to \alpha$ a monotone function, and $l \colon \alpha \to \beta$ its lower adjoint forming a Galois connection. For any elements $x, y \in \alpha$ where $\alpha$ is a join-semilattice, the closure of the supremum of the closure of $x$ and $y$ equals the closure of the supremum of $x$ and $y$, i.e., \[ u(l(u(l(x)) \sqcup y)) = u(l(x \sqcup y)). \]

LowerAdjoint.closure_sup_closure_right theorem

(x y : α) : u (l (x ⊔ u (l y))) = u (l (x ⊔ y))

Full source

theorem closure_sup_closure_right (x y : α) : u (l (x ⊔ u (l y))) = u (l (x ⊔ y)) :=
  l.closureOperator.closure_sup_closure_right x y

Closure of Supremum with Right Closure under Lower Adjoint: $u(l(x \sqcup u(l(y)))) = u(l(x \sqcup y))$

Informal description

Let $\alpha$ and $\beta$ be preorders, $u \colon \beta \to \alpha$ a monotone function, and $l \colon \alpha \to \beta$ its lower adjoint forming a Galois connection. For any elements $x, y \in \alpha$ where $\alpha$ is a join-semilattice, the closure of the supremum of $x$ and the closure of $y$ equals the closure of the supremum of $x$ and $y$, i.e., \[ u(l(x \sqcup u(l(y)))) = u(l(x \sqcup y)). \]

LowerAdjoint.closure_sup_closure theorem

(x y : α) : u (l (u (l x) ⊔ u (l y))) = u (l (x ⊔ y))

Full source

theorem closure_sup_closure (x y : α) : u (l (u (l x) ⊔ u (l y))) = u (l (x ⊔ y)) :=
  l.closureOperator.closure_sup_closure x y

Closure Operator Preserves Supremum of Closures: $u(l(u(l(x)) \sqcup u(l(y)))) = u(l(x \sqcup y))$

Informal description

Let $\alpha$ and $\beta$ be preorders, $u \colon \beta \to \alpha$ a monotone function, and $l \colon \alpha \to \beta$ its lower adjoint forming a Galois connection. For any elements $x, y \in \alpha$ where $\alpha$ is a join-semilattice, the closure of the supremum of the closures of $x$ and $y$ equals the closure of the supremum of $x$ and $y$, i.e., \[ u(l(u(l(x)) \sqcup u(l(y)))) = u(l(x \sqcup y)). \]

LowerAdjoint.closure_iSup_closure theorem

(f : ι → α) : u (l (⨆ i, u (l (f i)))) = u (l (⨆ i, f i))

Full source

theorem closure_iSup_closure (f : ι → α) : u (l (⨆ i, u (l (f i)))) = u (l (⨆ i, f i)) :=
  l.closureOperator.closure_iSup_closure _

Closure Commutes with Supremum of Closures: $u(l(\bigsqcup_i u(l(f_i)))) = u(l(\bigsqcup_i f_i))$

Informal description

For any lower adjoint function $l \colon \alpha \to \beta$ and monotone function $u \colon \beta \to \alpha$ forming a Galois connection, and for any indexed family of elements $f \colon \iota \to \alpha$, the following equality holds: $$ u\left(l\left(\bigsqcup_{i} u(l(f_i))\right)\right) = u\left(l\left(\bigsqcup_{i} f_i\right)\right). $$ This states that the composition $u \circ l$ commutes with suprema of $u \circ l$-closures.

LowerAdjoint.closure_iSup₂_closure theorem

(f : ∀ i, κ i → α) : u (l <| ⨆ (i) (j), u (l <| f i j)) = u (l <| ⨆ (i) (j), f i j)

Full source

theorem closure_iSup₂_closure (f : ∀ i, κ i → α) :
    u (l <| ⨆ (i) (j), u (l <| f i j)) = u (l <| ⨆ (i) (j), f i j) :=
  l.closureOperator.closure_iSup₂_closure _

Closure Operator Preserves Supremum of Doubly Indexed Family under Lower Adjoint

Informal description

Let $\alpha$ and $\beta$ be preorders, $u \colon \beta \to \alpha$ a monotone function, and $l \colon \alpha \to \beta$ its lower adjoint forming a Galois connection. For any doubly indexed family of elements $(f_{i,j})_{i \in \iota, j \in \kappa_i}$ in $\alpha$, the closure operator $u \circ l$ satisfies: \[ u\left(l\left(\bigsqcup_{i,j} u(l(f_{i,j}))\right)\right) = u\left(l\left(\bigsqcup_{i,j} f_{i,j}\right)\right). \]

LowerAdjoint.subset_closure theorem

(s : Set β) : s ⊆ l s

Full source

theorem subset_closure (s : Set β) : s ⊆ l s :=
  l.le_closure s

Extensivity of Lower Adjoint Closure: $s \subseteq l(s)$

Informal description

For any set $s$ in a preorder $\beta$, and given a lower adjoint function $l \colon \text{Set } \beta \to \alpha$, the set $s$ is a subset of its closure under $l$, i.e., $s \subseteq l(s)$.

LowerAdjoint.not_mem_of_not_mem_closure theorem

{s : Set β} {P : β} (hP : P ∉ l s) : P ∉ s

Full source

theorem not_mem_of_not_mem_closure {s : Set β} {P : β} (hP : P ∉ l s) : P ∉ s := fun h =>
  hP (subset_closure _ s h)

Non-membership in closure implies non-membership in original set

Informal description

For any subset $s$ of a preorder $\beta$ and any element $P \in \beta$, if $P$ does not belong to the closure $l(s)$ of $s$ under the lower adjoint $l$, then $P$ does not belong to $s$.

LowerAdjoint.le_iff_subset theorem

(s : Set β) (S : α) : l s ≤ S ↔ s ⊆ S

Full source

theorem le_iff_subset (s : Set β) (S : α) : l s ≤ S ↔ s ⊆ S :=
  l.gc s S

Lower Adjoint Order-Subset Equivalence

Informal description

For a lower adjoint function $l : \mathcal{P}(\beta) \to \alpha$ and a subset $s \subseteq \beta$ and an element $S \in \alpha$, we have $l(s) \leq S$ if and only if $s \subseteq S$ (where $\leq$ is the preorder on $\alpha$ and $\subseteq$ is the subset relation on $\beta$).

LowerAdjoint.mem_iff theorem

(s : Set β) (x : β) : x ∈ l s ↔ ∀ S : α, s ⊆ S → x ∈ S

Full source

theorem mem_iff (s : Set β) (x : β) : x ∈ l sx ∈ l s ↔ ∀ S : α, s ⊆ S → x ∈ S := by
  simp_rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← l.le_iff_subset]
  exact ⟨fun h S => h.trans, fun h => h _ le_rfl⟩

Characterization of Closure Membership via Lower Adjoints

Informal description

For a lower adjoint function $l \colon \mathcal{P}(\beta) \to \alpha$ and a subset $s \subseteq \beta$, an element $x \in \beta$ belongs to the closure $l(s)$ if and only if for every subset $S \in \alpha$ containing $s$, $x$ is also in $S$.

LowerAdjoint.closure_union_closure_subset theorem

(x y : α) : (l x : Set β) ∪ l y ⊆ l (x ∪ y)

Full source

theorem closure_union_closure_subset (x y : α) : (l x : Set β) ∪ l y(l x : Set β) ∪ l y ⊆ l (x ∪ y) :=
  l.closure_sup_closure_le x y

Closure of Union Contains Union of Closures for Lower Adjoints

Informal description

Let $\alpha$ and $\beta$ be preorders, $u \colon \beta \to \alpha$ a monotone function, and $l \colon \alpha \to \beta$ its lower adjoint forming a Galois connection. For any elements $x, y$ in $\alpha$, the union of the closures $l(x)$ and $l(y)$ (viewed as sets in $\beta$) is contained in the closure of their union, i.e., \[ l(x) \cup l(y) \subseteq l(x \cup y). \]

LowerAdjoint.closure_union_closure_left theorem

(x y : α) : l (l x ∪ y) = l (x ∪ y)

Full source

@[simp]
theorem closure_union_closure_left (x y : α) : l (l x ∪ y) = l (x ∪ y) :=
  SetLike.coe_injective (l.closure_sup_closure_left x y)

Closure of Union with Left Closure under Lower Adjoint: $l(l(x) \cup y) = l(x \cup y)$

Informal description

Let $\alpha$ and $\beta$ be preorders, $u \colon \beta \to \alpha$ a monotone function, and $l \colon \alpha \to \beta$ its lower adjoint forming a Galois connection. For any elements $x, y \in \alpha$, the closure of the union of the closure of $x$ and $y$ equals the closure of the union of $x$ and $y$, i.e., \[ l(l(x) \cup y) = l(x \cup y). \]

LowerAdjoint.closure_union_closure_right theorem

(x y : α) : l (x ∪ l y) = l (x ∪ y)

Full source

@[simp]
theorem closure_union_closure_right (x y : α) : l (x ∪ l y) = l (x ∪ y) :=
  SetLike.coe_injective (l.closure_sup_closure_right x y)

Closure of Union with Right Closure under Lower Adjoint: $l(x \cup l(y)) = l(x \cup y)$

Informal description

Let $\alpha$ and $\beta$ be preorders, $u \colon \beta \to \alpha$ a monotone function, and $l \colon \alpha \to \beta$ its lower adjoint forming a Galois connection. For any elements $x, y \in \alpha$, the closure of the union of $x$ and the closure of $y$ equals the closure of the union of $x$ and $y$, i.e., \[ l(x \cup l(y)) = l(x \cup y). \]

LowerAdjoint.closure_union_closure theorem

(x y : α) : l (l x ∪ l y) = l (x ∪ y)

Full source

theorem closure_union_closure (x y : α) : l (l x ∪ l y) = l (x ∪ y) := by
  rw [closure_union_closure_right, closure_union_closure_left]

Closure of Union of Closures under Lower Adjoint: $l(l(x) \cup l(y)) = l(x \cup y)$

Informal description

Let $\alpha$ and $\beta$ be preorders, $u \colon \beta \to \alpha$ a monotone function, and $l \colon \alpha \to \beta$ its lower adjoint forming a Galois connection. For any elements $x, y \in \alpha$, the closure of the union of the closures of $x$ and $y$ equals the closure of the union of $x$ and $y$, i.e., \[ l(l(x) \cup l(y)) = l(x \cup y). \]

LowerAdjoint.closure_iUnion_closure theorem

(f : ι → α) : l (⋃ i, l (f i)) = l (⋃ i, f i)

Full source

@[simp]
theorem closure_iUnion_closure (f : ι → α) : l (⋃ i, l (f i)) = l (⋃ i, f i) :=
  SetLike.coe_injective <| l.closure_iSup_closure _

Lower Adjoint Commutes with Union of Closures: $l(\bigcup_i l(f_i)) = l(\bigcup_i f_i)$

Informal description

For any lower adjoint function $l \colon \alpha \to \beta$ and monotone function $u \colon \beta \to \alpha$ forming a Galois connection, and for any indexed family of sets $f \colon \iota \to \alpha$, the following equality holds: $$ l\left(\bigcup_{i} l(f_i)\right) = l\left(\bigcup_{i} f_i\right). $$ This states that the lower adjoint $l$ commutes with unions of $l$-closures.

LowerAdjoint.closure_iUnion₂_closure theorem

(f : ∀ i, κ i → α) : l (⋃ (i) (j), l (f i j)) = l (⋃ (i) (j), f i j)

Full source

@[simp]
theorem closure_iUnion₂_closure (f : ∀ i, κ i → α) :
    l (⋃ (i) (j), l (f i j)) = l (⋃ (i) (j), f i j) :=
  SetLike.coe_injective <| l.closure_iSup₂_closure _

Closure Operator Preserves Union of Doubly Indexed Family under Lower Adjoint

Informal description

Let $\alpha$ and $\beta$ be preorders, $u \colon \beta \to \alpha$ a monotone function, and $l \colon \alpha \to \beta$ its lower adjoint forming a Galois connection. For any doubly indexed family of elements $(f_{i,j})_{i \in \iota, j \in \kappa_i}$ in $\alpha$, the closure operator $u \circ l$ satisfies: \[ l\left(\bigcup_{i,j} l(f_{i,j})\right) = l\left(\bigcup_{i,j} f_{i,j}\right). \]

GaloisConnection.lowerAdjoint definition

[Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : LowerAdjoint u

Full source

/-- Every Galois connection induces a lower adjoint. -/
@[simps]
def GaloisConnection.lowerAdjoint [Preorder α] [Preorder β] {l : α → β} {u : β → α}
    (gc : GaloisConnection l u) : LowerAdjoint u where
  toFun := l
  gc' := gc

Lower adjoint induced by a Galois connection

Informal description

Given a Galois connection between preorders $\alpha$ and $\beta$ consisting of functions $l : \alpha \to \beta$ and $u : \beta \to \alpha$, the function $l$ defines a lower adjoint to $u$. This means $l$ and $u$ satisfy the Galois connection property: for all $x \in \alpha$ and $y \in \beta$, $l(x) \leq y$ if and only if $x \leq u(y)$.

GaloisConnection.closureOperator definition

[PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : ClosureOperator α

Full source

/-- 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. -/
@[simps!]
def GaloisConnection.closureOperator [PartialOrder α] [Preorder β] {l : α → β} {u : β → α}
    (gc : GaloisConnection l u) : ClosureOperator α :=
  gc.lowerAdjoint.closureOperator

Closure operator induced by a Galois connection

Informal description

Given a Galois connection between a partial order $\alpha$ and a preorder $\beta$ consisting of functions $l \colon \alpha \to \beta$ and $u \colon \beta \to \alpha$, the composition $u \circ l$ defines a closure operator on $\alpha$. This operator is monotone, extensive (satisfying $x \leq u(l(x))$ for all $x \in \alpha$), and idempotent (satisfying $u(l(u(l(x)))) = u(l(x))$ for all $x \in \alpha$).

ClosureOperator.gi definition

[PartialOrder α] (c : ClosureOperator α) : GaloisInsertion c.toCloseds (↑)

Full source

/-- The set of closed elements has a Galois insertion to the underlying type. -/
def ClosureOperator.gi [PartialOrder α] (c : ClosureOperator α) :
    GaloisInsertion c.toCloseds (↑) where
  choice x hx := ⟨x, isClosed_iff_closure_le.2 hx⟩
  gc _ y := y.2.closure_le_iff
  le_l_u _ := c.le_closure _
  choice_eq x hx := le_antisymm (c.le_closure x) hx

Galois insertion induced by a closure operator

Informal description

Given a closure operator $c$ on a partial order $\alpha$, there is a Galois insertion between the set of closed elements (i.e., elements $x \in \alpha$ satisfying $c(x) = x$) and $\alpha$ itself. The insertion is given by the map sending an element to its closure (viewed as a closed element) and the inclusion map from closed elements back to $\alpha$.

closureOperator_gi_self theorem

[PartialOrder α] (c : ClosureOperator α) : c.gi.gc.closureOperator = c

Full source

/-- 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. -/
@[simp]
theorem closureOperator_gi_self [PartialOrder α] (c : ClosureOperator α) :
    c.gi.gc.closureOperator = c := by
  ext x
  rfl

Closure Operator Reconstruction via Galois Insertion

Informal description

For any closure operator $c$ on a partial order $\alpha$, the closure operator induced by the Galois insertion associated to $c$ is equal to $c$ itself. That is, if we construct a Galois insertion from $c$ and then derive a closure operator from this insertion, we recover the original closure operator $c$.

Mathlib.Order.Closure

Main definitions

Implementation details

References