Publish here. Donate

Difference between revisions of "Funcoid bases/Reduce to meets of applying funcoids to ultrafilters"

From Virtual scientific conference
Jump to: navigation, search
(math typo)
Line 38: Line 38:
  
 
The remaining attempt to prove our conjecture is stalled.
 
The remaining attempt to prove our conjecture is stalled.
 +
 +
The proof above uses the following lemma:
 +
 +
<b>Lemma</b> For every funcoid $f$ and filter $\mathcal{X} \in \mathscr{F} (\operatorname{Src} f)$
 +
$$ \operatorname{up} \langle f \rangle \mathcal{X} = \bigcup_{F \in \operatorname{up} f}
 +
  \operatorname{up} \langle F \rangle \mathcal{X} = \left\{ K \in \operatorname{up} \langle F
 +
  \rangle \mathcal{X} \mid F \in \operatorname{up} f \right\} . $$
 +
 +
<b>Proof</b> $\bigcup_{F \in \operatorname{up} f} \operatorname{up} \langle F \rangle \mathcal{X} = \left\{
 +
K \in \operatorname{up} \langle F \rangle \mathcal{X} \mid F
 +
\in \operatorname{up} f \right\}$ is obvious.
 +
 +
$\bigcup_{F \in \operatorname{up} f} \operatorname{up} \langle F \rangle \mathcal{X} \subseteq
 +
\operatorname{up} \langle f \rangle \mathcal{X}$ is obvious.
 +
 +
Let $G \in \operatorname{up} \langle f \rangle \mathcal{X}$. Then $G \in \operatorname{up}
 +
\bigwedge_{X \in \operatorname{up} \mathcal{X}} \langle f \rangle X$. By properties of
 +
generalized filter bases, there is an $X \in \operatorname{up} \mathcal{X}$ such that
 +
$G \sqsupseteq \langle f \rangle X$. Then $G \sqsupseteq \left\langle \left(
 +
\overline{X} \times^{\mathsf{FCD}} \top \right) \sqcup (X
 +
\times^{\mathsf{FCD}} G) \right\rangle X$.
 +
 +
So $G \in \operatorname{up} \langle F \rangle \mathcal{X}$ where $F = \left(
 +
\overline{X} \times^{\mathsf{FCD}} \top \right) \sqcup (X
 +
\times^{\mathsf{FCD}} G)$ and thus $F \in \operatorname{up} f$. Thus $G \in
 +
\bigcup_{F \in \operatorname{up} f} \operatorname{up} \langle F \rangle \mathcal{X}$.

Revision as of 19:29, 11 April 2017

The idea behind this attempted proof is to reduce behavior of funcoids $\langle f\rangle$ with better known behavior of filters $\langle f\rangle x$ for an arbitrary ultrafilter $x$ (I remind that knowing $\langle f\rangle x$ for all ultrafilters $x$ on the domain, it's possible to restore funcoid $f$) and then to replace $\langle X_0 \sqcap^{\mathsf{FCD}} \ldots \sqcap^{\mathsf{FCD}} X_n\rangle x$ with $\langle X_0 \rangle x \sqcap \dots \sqcap \langle X_n \rangle x$.

The below is my attempted proof (trying to reduce the statement for $n$ to the statement for $n-1$):

Let $X_i\in S$. We need to prove for every binary relations $Q \in \operatorname{up} (X_0 \sqcap^{\mathsf{FCD}} \ldots \sqcap^{\mathsf{FCD}} X_n)$ that is $\langle Q \rangle x \sqsupseteq \langle X_0 \rangle x \sqcap \ldots \sqcap \langle X_n \rangle x$ that is $\operatorname{up} \langle Q \rangle x \subseteq \left\{ K_0 \sqcap \ldots \sqcap K_n \mid \forall i : K_i \in \operatorname{up} \langle X_i \rangle x \right\}$ that $Q \in S$.

The below is a chain of equalities attempting the proof:

$\operatorname{up} \langle Q \rangle x \subseteq \left\{ K_0 \sqcap \ldots \sqcap K_n \mid \forall i : K_i \in \operatorname{up} \langle X_i \rangle x \right\} = \\ \left\{ P \sqcap K_n \mid P \in \operatorname{up} (\langle X_0 \rangle x \sqcap \ldots \sqcap \langle X_{n - 1} \rangle x) \wedge K_n \in \operatorname{up} \langle X_n \rangle x \right\} = \\ \left\{ P \sqcap K_n \mid P \in \operatorname{up} \langle X_0 \sqcap^{\mathsf{FCD}} \ldots \sqcap^{\mathsf{FCD}} X_{n - 1} \rangle x \wedge K_n \in \operatorname{up} \langle X_n \rangle x \right\} = \\ \left\{ P \sqcap K_n \mid K \in \operatorname{up} (X_0 \sqcap^{\mathsf{FCD}} \ldots \sqcap^{\mathsf{FCD}} X_{n - 1}), P \in \operatorname{up} \langle K \rangle x \wedge K_n \in \operatorname{up} \langle X_n \rangle x \right\} = \\ \bigcup_{K \in \operatorname{up} (X_0 \sqcap^{\mathsf{FCD}} \ldots \sqcap^{\mathsf{FCD}} X_{n - 1})} \left\{ P \sqcap K_n \mid P \in \operatorname{up} \langle K \rangle x \wedge K_n \in \operatorname{up} \langle X_n \rangle x \right\} = \\ \bigcup_{K \in \operatorname{up} (X_0 \sqcap^{\mathsf{FCD}} \ldots \sqcap^{\mathsf{FCD}} X_{n - 1})} \operatorname{up} (\langle K \rangle x \sqcap \langle X_n \rangle x) = \\ \bigcup_{K \in \operatorname{up} (X_0 \sqcap^{\mathsf{FCD}} \ldots \sqcap^{\mathsf{FCD}} X_{n - 1})} \operatorname{up} \langle K \sqcap^{\mathsf{FCD}} X_n \rangle x \subseteq \bigcup_{K \in \operatorname{up} (X_0 \sqcap^{\mathsf{FCD}} \ldots \sqcap^{\mathsf{FCD}} X_{n - 1})} Q_K$

because $\langle K \rangle x \sqcap \langle X_n \rangle x = \langle K \sqcap^{\mathsf{FCD}} X_n \rangle x \sqsupseteq Q_K$ for $Q_K \in S$

The remaining attempt to prove our conjecture is stalled.

The proof above uses the following lemma:

Lemma For every funcoid $f$ and filter $\mathcal{X} \in \mathscr{F} (\operatorname{Src} f)$ $$ \operatorname{up} \langle f \rangle \mathcal{X} = \bigcup_{F \in \operatorname{up} f} \operatorname{up} \langle F \rangle \mathcal{X} = \left\{ K \in \operatorname{up} \langle F \rangle \mathcal{X} \mid F \in \operatorname{up} f \right\} . $$

Proof $\bigcup_{F \in \operatorname{up} f} \operatorname{up} \langle F \rangle \mathcal{X} = \left\{ K \in \operatorname{up} \langle F \rangle \mathcal{X} \mid F \in \operatorname{up} f \right\}$ is obvious.

$\bigcup_{F \in \operatorname{up} f} \operatorname{up} \langle F \rangle \mathcal{X} \subseteq \operatorname{up} \langle f \rangle \mathcal{X}$ is obvious.

Let $G \in \operatorname{up} \langle f \rangle \mathcal{X}$. Then $G \in \operatorname{up} \bigwedge_{X \in \operatorname{up} \mathcal{X}} \langle f \rangle X$. By properties of generalized filter bases, there is an $X \in \operatorname{up} \mathcal{X}$ such that $G \sqsupseteq \langle f \rangle X$. Then $G \sqsupseteq \left\langle \left( \overline{X} \times^{\mathsf{FCD}} \top \right) \sqcup (X \times^{\mathsf{FCD}} G) \right\rangle X$.

So $G \in \operatorname{up} \langle F \rangle \mathcal{X}$ where $F = \left( \overline{X} \times^{\mathsf{FCD}} \top \right) \sqcup (X \times^{\mathsf{FCD}} G)$ and thus $F \in \operatorname{up} f$. Thus $G \in \bigcup_{F \in \operatorname{up} f} \operatorname{up} \langle F \rangle \mathcal{X}$.