From 02b6a8dfd65b97fea5925dfca696a3dcdd02c135 Mon Sep 17 00:00:00 2001 From: partowp Date: Wed, 5 Aug 2026 13:30:03 +0100 Subject: [PATCH] lemma --- draft/draft.tex | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/draft/draft.tex b/draft/draft.tex index 36a2a03..6ffa923 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2489,9 +2489,26 @@ Now, we make the proof more abstract. We prove the statement for set-functors of For sets $X$ and $Y$ in $\powf A$, and a function $f\c A\to B$ the following equation holds: \begin{gather*} %(\powf p_i)^\dagger(R_1\cup R_2)=(\powf p_i)^\dagger(R_1)\cup(\powf p_i)^\dagger(R_2) - \powf f(X\cup Y)=\powf f(X)\cup(\powf f)(Y) + \powf f(X\cup Y)=\powf f(X)\cup \powf f(Y) \end{gather*} \end{lemma} +\begin{proof} + Assuming $b\in\powf f(X_1\cup X_2)$ then exists $z$ that $z\in X_1\cup X_2$ and $f(z)=b$, thus either $z\in X_1$ or $z\in X_2$, so we have $b\in\powf f(X_1)$ or $b\in\powf f(X_2)$, respectively. So, we have $b\in \powf f(X_1)\cup\powf f(X_2)$. + + Now, assuming that $b\in\powf f(X_1)\cup\powf f(X_2)$ then we either have $b\in\powf f(X_1)$ or $b\in\powf f(X_2)$. Without loss of generality, we assume $b\in\powf f(X_j)$, where $j\in\{1,2\}$. + Then there exists $z$ that $z\in X_j$ and $f(z)=b$, so we have $z\in X_1\cup X_2$ that gives $b\in\powf f(X_1\cup X_2)$.\qed + % We prove the lemma for the case that $i=1$. The proof is the same for $i=2$. + % + % First, we prove $(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. + % Assuming $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$ then exists $y_2$ that we have either $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $(y_1,y_2)\in\sigma(x_1,x_2)$. So, we have either $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$ or $y_1\in(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ that means that we have $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$. + % + % Now, we prove $(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)\subseteq(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. Assuming $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s\join(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$ then we have: + % \begin{itemize} + % \item $y_1\in(\powf p_1)^\dagger\comp(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s(x_1,x_2)$. So, $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. + % \item $y_1\in(\powf p_1)^\dagger\comp\sigma(x_1,x_2)$: Then there exists $y_2$ such that $(y_1,y_2)\in\sigma(x_1,x_2)$. So, $(y_1,y_2)\in(\powf s)^\dagger\comp\sigma\comp s\join\sigma(x_1,x_2)$, thus $y_1\in(\powf p_1)^\dagger\comp((\powf s)^\dagger\comp\sigma\comp s\join\sigma)(x_1,x_2)$. + % \end{itemize} \qed + % \todo{Rewrite the proof according to the statement!} +\end{proof} \todo{Finish this proof. With this, you can give the proof for $\powf F$. After you finished this, you can remove the previous sections.} \subsection{Maybe Functor}