From 61fed4f74a856edd8b029f235f0f1c1d22864569 Mon Sep 17 00:00:00 2001 From: partowp Date: Mon, 20 Jul 2026 19:01:30 +0100 Subject: [PATCH] Barr! --- draft/draft.tex | 45 +++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 43 insertions(+), 2 deletions(-) diff --git a/draft/draft.tex b/draft/draft.tex index a87cf02..c095486 100644 --- a/draft/draft.tex +++ b/draft/draft.tex @@ -2172,7 +2172,24 @@ We take $R=\{(1,1),(1,2),(2,1),(2,2)\}$, and $X=\{1,2,3\}$. $\alpha$ is defined \{1,2\} & x=1 \\ \{2,3\} & x=2\\ \{3\} & x=3 - \end{cases} + \end{cases}\qquad +\begin{tikzpicture}[scale=0.1] + \tikzstyle{every node}+=[inner sep=0pt] + \draw [black] (23.8,-25.2) circle (3); + \draw (23.8,-25.2) node {$1$}; + \draw [black] (42.4,-25.2) circle (3); + \draw (42.4,-25.2) node {$2$}; + \draw [black] (33,-34.6) circle (3); + \draw (33,-34.6) node {$3$}; + \draw [black] (22.477,-22.52) arc (234:-54:2.25); + \fill [black] (25.12,-22.52) -- (26,-22.17) -- (25.19,-21.58); + \draw [black] (41.077,-22.52) arc (234:-54:2.25); + \fill [black] (43.72,-22.52) -- (44.6,-22.17) -- (43.79,-21.58); + \draw [black] (26.8,-25.2) -- (39.4,-25.2); + \fill [black] (39.4,-25.2) -- (38.6,-24.7) -- (38.6,-25.7); + \draw [black] (40.28,-27.32) -- (35.12,-32.48); + \fill [black] (35.12,-32.48) -- (36.04,-32.27) -- (35.33,-31.56); +\end{tikzpicture} \end{gather*} $\sigma$ is defined as below: \begin{gather*} @@ -3138,6 +3155,15 @@ Barr relator is a generalization of the Egli-Milner relator, where the functor i \begin{proof} They all follow in an obvious way from~\autoref{lem:liftable} and~\autoref{lem:coliftable}. The last one needs $\appr\comp\appr=\appr$ that comes from transitivity of $\appr$. \qed \end{proof} +\begin{prop}\label{prop:lax-relator-full-comm} + Assuming the axiom of choice, for a functor $F$ with a liftable order we have: + \begin{gather*} + \bar{F}r\comp\appr=\appr\comp\bar{F} + \end{gather*} +\end{prop} +\begin{proof} + \todo{Write it down. You have it in your notes.} +\end{proof} %\begin{example} % In the category of sets, subset over the powerset functor is an example of a liftable order. Using~\autoref{lem:set-ord-str} we only prove the case for every $h\in\Hom(1,\powf Z)$, $k\in\Hom(1,\powf Y)$. Additionally, for every $g\c Y\to Z$, such that $h\subseteq\powf g(k)$, we define $k'\in\powf Y$ that that $k'=\{y\mid g(y)\in h\}$. We show that $\powf g(k')=h$. % @@ -3259,7 +3285,22 @@ Perhaps if we can relax the definition of liftable by allowing $g$ to be a relat \begin{remark} With a similar argument we can prove that the symmetrization of a right-lax Barr-relator of $F$ is a Barr-relator. \end{remark} -\todo{Try $FX=\powf(X^2)$ to see if the symmetrization of its lax Barr relator is a Barr relator. The order is just the set inclusion.} +\begin{lemma}\label{lem:lax-relator-str} + For a relation $r$, for functions $k_s\c F\pi_1(\bar{F}r)\to\powf FX$ and $k_b\c F\pi_2(\bar{F}r)\to\powf FX$, defined as + \begin{gather*} + k_s(x)=\{(x',y)\mid(x,y)\in\bar{F}r,x'\appr x, (x',y)\notin\bar{F}r\},\\ + k_b(x)=\{(x',y)\mid(x,y)\in\bar{F}r,x\appr x', (x',y)\notin\bar{F}r\}, + \end{gather*} + we have + \begin{gather*} + (\bar{F}r)\comp\appr=\bar{F}r\cup(\bigcup_{x\in F\pi_1(\bar{F}r)} k_s(x)),\\ + (\bar{F}r)\comp\sappr=\bar{F}r\cup(\bigcup_{x\in F\pi_1(\bar{F}r)} k_b(x)). + \end{gather*} +\end{lemma} +\begin{proof} + \todo{Write it down. You have it in your notes.} +\end{proof} +\todo{Try $FX=\powf(X^2)$ to see if the symmetrization of its lax Barr relator is a Barr relator. The order is just the set inclusion. See if~\autoref{prop:lax-relator-full-comm} or~\autoref{lem:lax-relator-str} can help!} \end{document}