Math-3388 · mathematics · Topology

Math-3388

Outer reloid of restricted funcoid

Status Open · unsolvedmath.comLLM status Open unverified

Top Open Problems Not reported cataloguedOpenOpen

Statement

Definitions and mathematical statement

Shared notation.
$\mathbb N=\{1,2,\ldots\}$, and $\mathbb Z,\mathbb Q,\mathbb R,\mathbb C$ denote the integers, rationals, reals and complex numbers. Any other conventions are specified locally.

For a set $X$, let $\mathcal F(X)$ be all filters on $\mathcal P(X)$, including the improper filter $\bot_X=\mathcal P(X)$. A filter is a nonempty family closed under finite intersections and supersets. Order filters by $\mathcal A\sqsubseteq\mathcal B$ when $\mathcal A\supseteq\mathcal B$ as families. Thus $\bigsqcup$ is intersection of filter families and $\bigsqcap$ is the filter generated by their union; the empty join is $\bot_X$ and the empty meet is $\top_X=\{X\}$. For $E\subseteq X$, $\uparrow E=\{U\subseteq X:E\subseteq U\}$ is its principal filter. Write $\mathcal A\mathrel{\#}\mathcal B$ when every $U\in\mathcal A$ and $V\in\mathcal B$ have $U\cap V\ne\varnothing$, equivalently $\mathcal A\sqcap\mathcal B\ne\bot_X$.

A funcoid $f:X\to Y$ is a pair of maps $\alpha_f:\mathcal F(X)\to\mathcal F(Y)$ and $\beta_f:\mathcal F(Y)\to\mathcal F(X)$ satisfying \[ \mathcal B\mathrel{\#}\alpha_f(\mathcal A) \quad\Longleftrightarrow\quad \mathcal A\mathrel{\#}\beta_f(\mathcal B) \qquad(\mathcal A\in\mathcal F(X),\ \mathcal B\in\mathcal F(Y)). \] Its reverse interchanges $\alpha_f,\beta_f$. Composition satisfies $\alpha_{g\circ f}=\alpha_g\circ\alpha_f$ and $\beta_{g\circ f}=\beta_f\circ\beta_g$. The identity has both maps equal to the identity. The order on $\mathsf{FCD}(X,Y)$ is pointwise order on $\alpha_f$; its meets and joins mean greatest lower bounds and least upper bounds within this complete lattice. A relation $R\subseteq X\times Y$ induces the principal funcoid $\widehat R$ with $\alpha_{\widehat R}(\mathcal A)$ the filter generated by $\{R[U]:U\in\mathcal A\}$ and the analogous inverse-image formula for $\beta$. Here $R[U]=\{y:\exists x\in U,(x,y)\in R\}$.

A reloid $f:X\to Y$ is a filter on $X\times Y$, ordered by reverse inclusion of filter families. For a relation $R\subseteq X\times Y$, its principal reloid is $\uparrow R$. The reloid $g\circ f:X\to Z$ is generated by $G\circ F$ for $F\in f,G\in g$, where $G\circ F=\{(x,z):\exists y,(x,y)\in F,(y,z)\in G\}$. The reverse $f^{-1}$ is generated by $F^{-1}=\{(y,x):(x,y)\in F\}$ for $F\in f$. The identity $1_X$ is $\uparrow\Delta_X$, where $\Delta_X=\{(x,x):x\in X\}$.

For $\mathcal A\in\mathcal F(X),\mathcal B\in\mathcal F(Y)$, $\mathcal A\times^{\mathsf{RLD}}\mathcal B$ is generated by all rectangles $U\times V$ with $U\in\mathcal A,V\in\mathcal B$. Their funcoidal product $\mathcal A\times^{\mathsf{FCD}}\mathcal B$ has first map $\mathcal L\mapsto\mathcal B$ if $\mathcal L\mathrel{\#}\mathcal A$, and $\mathcal L\mapsto\bot_Y$ otherwise; its reverse map has the corresponding formula with $\mathcal A,\mathcal B$ interchanged.

For a funcoid $f:X\to Y$, define its outward reloid and inward reloid by \[ O(f)=\bigsqcap^{\mathsf{RLD}}\{\uparrow R:R\subseteq X\times Y,\ f\sqsubseteq\widehat R\}, \] \[ I(f)=\bigsqcup^{\mathsf{RLD}}\{\mathcal A\times^{\mathsf{RLD}}\mathcal B: \mathcal A\times^{\mathsf{FCD}}\mathcal B\sqsubseteq f\}. \] These are the source's $(\mathsf{RLD})_{\mathrm{out}}f$ and $(\mathsf{RLD})_{\mathrm{in}}f$; meets in the first formula generate a filter, and joins in the second intersect filter families.

Statement recorded in the supplied source.
For every funcoid $f:X\to Y$ and filters $\mathcal A\in\mathcal F(X),\mathcal B\in\mathcal F(Y)$, is \[ O\left(f\sqcap^{\mathsf{FCD}}(\mathcal A\times^{\mathsf{FCD}}\mathcal B)\right) =O(f)\sqcap^{\mathsf{RLD}}(\mathcal A\times^{\mathsf{RLD}}\mathcal B)? \] The superscripts specify the two different lattice meets. [S2][S3]

Short English statement

Does restricting a funcoid to a product of filters commute with passage to its outward reloid?

Sources

Catalogue entry

Statement licence: CC-BY-4.0 · Source file

Contributions 0

No attempts yet. Significant partial results and substantial reductions are welcome. Contribute an attempt.