Operator Generated by Image of Closure Operator is Closure Operator

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.

Let $c: S \to S$ be a closure operator on $L$.


Then $\map {\operatorname {operator} } {\struct {c \sqbrk S, \precsim} } = c$

where

$\mathord \precsim = \mathord \preceq \cap \paren {c \sqbrk S \times c \sqbrk S}$
$\map {\operatorname {operator} } {\struct {c \sqbrk S, \precsim} }$ denotes the operator generated by $\struct {c \sqbrk S, \precsim}$


Proof

Let $x \in S$.

By definition of closure operator/inflationary:

$x \preceq \map c x$

By definition of upper closure of element:

$\map c x \in x^\succeq$

By definition of image of mapping:

$\map c x \in c \sqbrk S$

By definition of intersection:

$\map c x \in x^\succeq \cap c \sqbrk S$

By definitions of infimum and lower bound:

$\map {\inf_L} {x^\succeq \cap c \sqbrk S} \preceq \map c x$

We will prove that

$\map c x$ is lower bound for $x^\succeq \cap c \sqbrk S$

Let $y \in x^\succeq \cap c \sqbrk S$

By definition of intersection:

$y \in x^\succeq$ and $y \in c \sqbrk S$

By definition of image of mapping:

$\exists z \in S: y = \map c z$

By definition of closure operator/idempotent:

$y = \map c y$

By definition of upper closure of element:

$x \preceq y$

Thus by definition of closure operator/increasing:

$\map c x \preceq y$

$\Box$


By definition of infimum:

$\map c x \preceq \map {\inf_L} {x^\succeq \cap c \sqbrk S}$

By definition of antisymmetry:

$\map c x = \map {\inf_L} {x^\succeq \cap c \sqbrk S}$

Thus by definition of operator generated by $\struct {c \sqbrk S, \precsim}$:

$\map {\map {\operatorname {operator} } {\struct {c \sqbrk S, \precsim} } } x = \map c x$

Hence by Equality of Mappings:

$\map {\operatorname {operator} } {\struct {c \sqbrk S, \precsim} } = c$

$\blacksquare$


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Operator_Generated_by_Image_of_Closure_Operator_is_Closure_Operator&oldid=479688"