Commit d565932a authored by Leonard Guetta's avatar Leonard Guetta
Browse files

Kidoush break. I really really ought to wrap up the proof of the main theorem of chapter 1

parent 17e63b7e
......@@ -653,8 +653,8 @@ We can now prove the following proposition, which is the key result of this sect
\]
Since we have identified $\Sigma$ to a subset of the $n$-cells of $\E^*$ via $j$, the above cocartesian square means exactly that $\Sigma$ is an $(n+1)$-basis of $\E^*$.
\end{proof}
\begin{paragr}
Let $C$ be an $(n+1)$-category and $E$ be a subset $E \subseteq C_{n+1}$. This defines a cellular extension
\begin{paragr}\label{paragr:cextfromsubset}
Let $C$ be an $(n+1)$-category and $E$ be a subset $E \subseteq C_{n+1}$. This defines a $n$-cellular extension
\[
\E_E =(\tau_{\leq n}^s(C),E,\src,\trgt),
\]
......@@ -837,7 +837,19 @@ The \emph{size} of a well-formed word $w$, denoted by $\vert w \vert$, is the nu
Hence, by definition, $\E^+$ satisfy all the axioms of $\oo$-categories up to dimension $n$ only. On the other hand, the $(n+1)$-cells of $\E^+$ make it as far as possible as being a $(n+1)$-category as \emph{none} of the axioms of $\oo$-categories are satisfied for cells of dimension $n+1$.
\end{paragr}
%We would like now to quotient the set of $(n+1)$-cells of $\E^+$ as to make it an $(n+1)$-category. In order to do that, we introduce the notion of congruence.
\begin{remark}\label{remark:formalunformal}
Notice that, by definition, we have
\[
w \comp_k w' := (w\fcomp_k w')
\]
for $w$ and $w'$ $k$-composable $(n+1)$-cells of $\E^+$, and we ought to be careful not to confuse the ``real'' composition symbol
\[ \comp_k\]
with the ``formal'' composition symbol
\[
\fcomp_k.\]
As a rule of thumb, it is better not to use both symbols in the same expression. Note also that, since we use the usual symbols
\[(\] and \[)\] as ``formal'' symbols of opening and closing parenthesis, things can get really messy if we don't apply the previous rule because it would be hard to distinguish a formal parenthesis from an ``unformal'' one.
\end{remark}
In the following definition, we consider that a binary relation $\R$ on a set $E$ is nothing but a subset of $E \times E$, and we write $x \; \R \; x'$ to say $(x,x') \in \R$.
\begin{definition}\label{def:congruence}
Let $n\geq 1$. A \emph{congruence} on an $n$-magma $X$ is a binary relation $\R$ on the set of $n$-cells $X_n$ such that:
......@@ -1316,7 +1328,7 @@ In practise, we will use the following criterion to detect discrete Conduché $n
\begin{remark}
Beware that in the previous definition, none of the words were supposed to be well formed. In particular, a subword of a well formed word is not necessarily well formed.
\end{remark}
\begin{paragr} Since a word $w$ is a finite sequence of symbols, it makes sense to write $w(i)$ for the symbol at position $i$ of $w$, with $0 \leq i \leq \mathcal{L}(w)-1$.
\begin{paragr}\label{paragr:lengthandsize} Since a word $w$ is a finite sequence of symbols, it makes sense to write $w(i)$ for the symbol at position $i$ of $w$, with $0 \leq i \leq \mathcal{L}(w)-1$.
For any $0 \leq i \leq \mathcal{L}(w)-1$, define $P_{w}(i)$ to be the number of opening parenthesis in $w$ with position $ \leq i$ minus the number of closing parenthesis in $w$ with position $\leq i$. This defines a function
\[
......@@ -1497,13 +1509,13 @@ is also well formed.
\[
u_1=\tilde{v}e\tilde{w}.
\]
Moreover, we have \[v=(\tilde{v}\] and \[w=\tilde{w}\ast_k u_2).\] By induction hypothesis, the word
Moreover, we have \[v=(\tilde{v}\] and \[w=\tilde{w}\fcomp_k u_2).\] By induction hypothesis, the word
\[
\tilde{v}e'\tilde{w}
\]
is well formed and thus
\[
(\tilde{v}e'\tilde{w}\ast_k u_2)=vew
(\tilde{v}e'\tilde{w}\fcomp_k u_2)=vew
\]
is well formed.
\item[-] $e$ is a subword of $u_2$, which is symmetric to the previous case.\qedhere
......@@ -1561,7 +1573,8 @@ with $w_1$ and $w_2$ well formed words and $0\leq k \leq n$. Then $\src_k(w_1)=\
\end{proof}
\section{Proof of Theorem \ref{thm:conduche}: part II}
Recall that we have seen in Proposition \ref{prop:smallestcategoricalcongruence} that there was a smallest categorical congruence on any $n$-magma $X$ with $n \geq 1$. However, the description of this congruence we obtained when proving its existence was rather abstract. The main goal of this section is to give a more concrete description of the smallest categorical congruence in the case that $X= \E^+$ for an $n$-cellular extension $\E$.
Recall that we have seen in Proposition \ref{prop:smallestcategoricalcongruence} that there exists a smallest categorical congruence on any $n$-magma $X$ with $n \geq 1$. However, the description of this congruence we used for proving its existence was rather abstract. The main goal of this section is to give a more concrete description of the smallest categorical congruence in the case that $X= \E^+$ for an $n$-cellular extension $\E$. This description will turn out to be crucial for the third and last part of the proof of Theorem \ref{thm:conduche}.
\begin{definition}\label{def:elementarymove}
Let $n \geq 0$, $\E=(C,\Sigma,\sigma,\tau)$ be an $n$\nbd-cellular extension and $u,u' \in \T[\E]$. An \emph{elementary move} from $u$ to $u'$ is a quadruple $\mu=(v,w,e,e')$ with $v,w \in \W[\E]$ and $e,e' \in \T[\E]$ such that
\[
......@@ -1628,25 +1641,23 @@ We will use the notation
\]
if they are in the same connected component of $\G[E]$. More precisely, this means that there exists a finite sequence $(u_j)_{0\leq j \leq N}$ of well formed words with $u_0=u$, $u_N=u'$ and $u_j \leftrightarrow u_{j+1}$ for $0 \leq j < N$. The equivalence class of a well formed word $u$ will be denoted by $[u]$.
\end{definition}
We wish now to establish that the equivalence relation $\sim$ defined above is the smallest congruence on $\E^+$. In order to do that, we need to prove several technical results on words.
\begin{lemma}\label{lemmaequivrelationsourcestargets}Let $u,u' \in \T[E]$. If $u \sim u'$ then $u$ and $u'$ are parallel.
\begin{lemma}\label{lemma:equivparallel}Let $u,u' \in \T[\E]$. If $u \sim u'$ then $u$ and $u'$ are parallel.
\end{lemma}
\begin{proof}
Let
\[
\mu =(v,w,e,e') : u \to u'
\]
be an elementary move from $w$ to $w'$. We are going to prove that $s(u)=s(u')$ and $t(u)=t(u')$ with an induction on $\mathcal{L}(v)+\mathcal{L}(w)$(cf.\ \ref{paragrdefinitionwords}). Notice first that, by definition of elementary moves, $|u|\geq 1$ and thus
be an elementary move from $u$ to $u'$. It suffices to prove that $\src(u)=\src(u')$ and $\trgt(u)=\trgt(u')$, which we shall do with an induction on $\mathcal{L}(v)+\mathcal{L}(w)$. Notice first that, by definition of elementary moves, $|u|\geq 1$ and thus
\[
u=(u_1 \ast_k u_2)
u=(u_1 \fcomp_k u_2)
\]
with $u_1,u_2 \in \T[E]$.
with $u_1,u_2 \in \T[\E]$.
\begin{description}
\item[Base case] If $\mathcal{L}(v)+\mathcal{L}(w)=0$, it means that both $v$ and $w$ are both the empty word. It is then straightforward to check the desired property using Definition \ref{definitionelementarymove}.
\item[Inductive step] Suppose now that $\mathcal{L}(v)+\mathcal{L}(w)\geq 0$. Since $e$ is a subword of $u$ that is well formed, from Lemma \ref{lemmasubwords} we are in one of the following cases:
\item[Base case] If $\mathcal{L}(v)+\mathcal{L}(w)=0$, it means that $v$ and $w$ are both the empty word. It is then straightforward to check the desired property using Definition \ref{def:elementarymove}.
\item[Inductive step] Suppose now that $\mathcal{L}(v)+\mathcal{L}(w)\geq 0$. Since $e$ is a subword of $u$ that is well formed, from Proposition \ref{prop:subwords} we are in one of the following cases:
\begin{itemize}
\item[-] $e=u$, which is exactly the base case.
\item[-] $e$ is a subword of $u_1$, which means that there exist $\tilde{v},\tilde{w} \in \T[E]$ such that
......@@ -1659,31 +1670,31 @@ We wish now to establish that the equivalence relation $\sim$ defined above is t
\]
and
\[
w=\tilde{w}\ast_ku_2).
w=\tilde{w}\fcomp_ku_2).
\]
From Corollary \ref{corollarysubwordsubstitution}, the word
From Proposition \ref{prop:subwordsubstitution}, the word
\[
u_1':=\tilde{v}e'\tilde{w}
\]
is well formed. Therefore we can use the induction hypothesis on
is well formed. Since $\mathcal{L}(\tilde{v})+\mathcal{L}(\tilde{w}) < \mathcal{L}(v)+\mathcal{L}(w)$, we can use the induction hypothesis on
\[
\tilde{\mu} :=(\tilde{v},\tilde{w},e,e') : u_1 \to u_1'.
\]
This shows that $s(u_1)=s(u_1')$ and $t(u_1)=t(u_1')$ and since
This shows that $\src(u_1)=\src(u_1')$ and $\trgt(u_1)=\trgt(u_1')$ and since
\[
u=(u_1\ast_k u_2) \text{ and } u'=(u_1' \ast_k u_2)
u=(u_1\fcomp_k u_2) \text{ and } u'=(u_1' \fcomp_k u_2)
\]
it follows easily that $s(u)=s(u')$ and $t(u)=t(u')$.
it follows easily that $\src(u)=\src(u')$ and $\trgt(u)=\trgt(u')$.
\item[-] $e$ is a subword of $u_2$, which is symmetric to the previous case.
\end{itemize}
\end{description}
By definition of $\sim$, this suffices to show the desired properties.
\end{proof}
\begin{lemma}\label{lemmaequivrelationiscongruence}
Let $v_1, v_2, v_1', v_2' \in \T[E]$ and $0 \leq k \leq n$ such that $v_1$ and $v_2$ are $k$-composable, and $v_1'$ and $v_2'$ are $k$-composable. If $v_1 \sim v_2$ and $v_1' \sim v_2'$ then
\begin{lemma}\label{lemma:equivcong}
Let $v_1, v_2, v_1', v_2' \in \T[\E]$ and $0 \leq k \leq n$ such that $v_1$ and $v_2$ are $k$-composable, and $v_1'$ and $v_2'$ are $k$-composable. If $v_1 \sim v_2$ and $v_1' \sim v_2'$ then
\[
(v_1 \ast_k v_2) \sim (v_1' \ast_k v_2').
(v_1 \fcomp_k v_2) \sim (v_1' \fcomp_k v_2').
\]
\end{lemma}
\begin{proof}
......@@ -1697,16 +1708,123 @@ Let
\]
and
\[
\tilde{w} := w\ast_k v_2).
\tilde{w} := w\fcomp_k v_2).
\]
Then, by definition, $(\tilde{v},\tilde{w},e,e')$ is an elementary move from $(v_1 \ast_k v_2)$ to $(v_1' \ast_k v_2)$. Similarly, if we have an elementary move from $v_2$ to $v_2'$, we obtain an elementary move from $(v_1 \ast_k v_2)$ to $(v_1 \ast_k v_2')$.
Then, by definition, $(\tilde{v},\tilde{w},e,e')$ is an elementary move from $(v_1 \fcomp_k v_2)$ to $(v_1' \fcomp_k v_2)$. Similarly, if we have an elementary move from $v_2$ to $v_2'$, we obtain an elementary move from $(v_1 \fcomp_k v_2)$ to $(v_1 \fcomp_k v_2')$.
By definition of $\sim$, this suffices to show the desired property.
\end{proof}
We can now prove the awaited result.
\begin{lemma}\label{lemma:equivsmallestcong}
Let $\R$ be a categorical congruence on $\E^+$ and $u,u' \in \T[\E]$. If $u \sim u'$, then $u \; \R \; u'$.
\end{lemma}
\begin{proof}
The proof is very similar to the proof of Lemma \ref{lemma:equivparallel}. Let
\[
\mu =(v,w,e,e') : u \to u'
\]
be an elementary move from $u$ to $u'$. We are going to prove that $u \; \R \; u'$ with an induction on $\mathcal{L}(v)+\mathcal{L}(w)$. Once again, by definition of elementary moves, $|u|\geq 1$ and thus
\[
u=(u_1 \fcomp_k u_2)
\]
with $u_1,u_2 \in \T[\E]$.
\begin{description}
\item[Base case] If $\mathcal{L}(v)+\mathcal{L}(w)$, it means that $u=e$ and $u'=e'$. In that case, all the different cases of elementary moves from Definition \ref{def:elementarymove} correspond to the different axioms of categorical congruence (Definition \ref{def:categoricalcongruence}). Hence, we have $u \; \R u'$.
\item[Inductive step] Suppose now that $\mathcal{L}(v) + \mathcal{L}(w) \geq 0$. Since $e$ is a subword of $u$, we know from Proposition \ref{prop:subwords} that we are in one of the following cases:
\begin{itemize}[label=-]
\item $e=u$, which is exactly the base case.
\item $e$ is a subword of $u_1$, which means that there exists $\tilde{v},\tilde{w} \in \T[\E]$ such that
\[
u_1=\tilde{v}e\tilde{w}.
\]
Moreover, we have
\[
v=(\tilde{v}
\]
and
\[
w=\tilde{w}\fcomp_k u_2).
\]
From Proposition \ref{prop:subwordsubstitution}, the word
\[
u_1':=\tilde{v}e'\tilde{w}
\]
is well formed and since $\mathcal{L}(\tilde{v})+\mathcal{L}(\tilde{w})<\mathcal{L}(v)+\mathcal{L}(w)$, we can apply the induction hypothesis on
\[
\tilde{\mu} :=(\tilde{v},\tilde{w},e,e') : u_1 \to u_1'.
\]
This proves that $u_1 \; \R \; u_1'$. Now, since we have
\[
u =(u_1 \fcomp_k u_2) =u_1 \comp_k u_2
\]
and
\[
u' =(u_1' \fcomp_k u_2) =u_1' \comp_k u_2
\]
(notice the distinction between the symbol $\fcomp_k$ and the symbol $\comp_k$; see Remark \ref{remark:formalunformal}) and since $\R$ is a congruence, we have
\[
u \; \R \; u'.
\]
\item $e$ is a subword of $u_2$, which is symmetric to the previous case.
\end{itemize}
\end{description}
\end{proof}
Altogether, Lemmas \ref{lemma:equivparallel}, \ref{lemma:equivcong} and \ref{lemma:equivsmallestcong} prove the following proposition, which is what we aimed for.
\begin{proposition}
Let $\E=(C,\Sigma,\sigma,\tau)$ be an $n$-cellular extension. The equivalence relation $\sim$ on $\T[\E]$ (Definition \ref{definitionequivalence}) is the smallest categorical congruence on $\T[\E]$.
Let $\E=(C,\Sigma,\sigma,\tau)$ be an $n$-cellular extension. The equivalence relation $\sim$ on $\T[\E]$ is the smallest categorical congruence on $\E^+$.
\end{proposition}
We end this section with yet another characterisation of $n$-basis of $\oo$-categories.
\begin{paragr}\label{paragr:defrho}
Let $C$ be an $\oo$-category, $n \geq 0$ and $\Sigma$ a subset of $C_{n+1}$ and consider the $n$-cellular extension
\[
\E_{\Sigma}=(\tau^{s}_{\leq n }(C),\Sigma,\src,\trgt)
\]
(see Paragraph \ref{paragr:cextfromsubset}). When there is no ambiguity on the rest of the data, we allow ourselve to write $\W[\Sigma]$, $\T[\Sigma]$ and $\G[\Sigma]$ instead of $\W[\E_{\Sigma}]$, $\T[\E_{\Sigma}]$ and $\G[\E_{\Sigma}]$.
We recursively define a map $\rho_{\Sigma} : \T[\Sigma] \to C_{n+1}$ as
\begin{itemize}[label=-]
\item $\rho_{\Sigma}((\cc_{\alpha}))=\alpha$ for every $\alpha \in \Sigma$,
\item $\rho_{\Sigma}((\ii_x))=1_x$ for every $x \in C_n$,
\item $\rho_{\Sigma} ((w\fcomp_kw'))=\rho(w)\comp_k\rho(w')$ for every $0 \leq k \leq $ and every pair $(w,w')$ of $k$-composable elements of $\T[\Sigma]$.
\end{itemize}
Intuitively speaking, $\rho_{\Sigma}$ is to be understood as an ``evaluation map'': for every $w$ well formed expression on units and formal cells of $\Sigma$, $\rho_{\Sigma}(w)$ is the evaluation of $w$ as an $(n+1)$-cell of $C$.
\end{paragr}
\begin{lemma}\label{lemma:rhosourcetarget}
The map $\rho_{\Sigma}$ is compatible with source and target, i.e.\ for $w \in \T[\Sigma]$, we have
\[
\src(\rho_{\Sigma}(w))=\src(w) \text{ and } \trgt(\rho_{\Sigma}(w))=\trgt(w).
\]
\end{lemma}
\begin{proof}
The fact that $\simeq$ is a congruence follows from
This is proved by an immediate induction left to the reader.
\end{proof}
\begin{lemma}\label{lemma:rhoequiv}
Let $w$ and $w'$ be elements of $\T[\Sigma]$. If $w \sim w'$, then
\[
\rho_{\Sigma}(w)=\rho_{\Sigma}(w').
\]
\end{lemma}
\begin{proof}
From Lemma \ref{lemma:rhosourcetarget} we know that $\rho_{\Sigma}$ is compatible with source and target and, by definition, $\rho_{\Sigma}$ is compatible with composition and units in an obvious sense. Hence, the binary relation $\R$ on $\T[\Sigma]$ defined as \todo{À finir}
\end{proof}
\begin{paragr}
Let $C$ be an $\oo$-category, $\Sigma \subseteq C_{n+1}$ and let $a$ be an $(n+1)$-cell of $C$. We define $\T[\Sigma]_a$ to be the set
\[
\T[\Sigma]_a := \{w\in\T[\Sigma] \quad \vert \quad \rho_{\Sigma}(w)=a\}
\]
Lemma \ref{lemma:rhoequiv} implies that if $v \in \T[\Sigma]_a$ and $v \sim w$ then $w \in \T[\Sigma]_a$.
We define $\G[\Sigma]_a$ to be the full subgraph of $\G[\Sigma]$ whose set of objects is $\T[\Sigma]_a$.
\end{paragr}
\begin{proposition}
Let $C$ be an $\oo$-category, $n\geq 0$ and $\Sigma \subseteq C_{n+1}$. The set $\Sigma$ is an $(n+1)$-basis of $C$ is and only if for every $a \in C_{n+1}$, the graph $\G[\Sigma]_a$ is $0$-connecte (i.e.\ non-empty and connected).
More precisely, this means that for every $a \in C_{n+1}$:
\begin{itemize}[label=-]
\item there exists $w \in \T[\Sigma]$ such that $\rho_{\Sigma}(w)=a$,
\item for every $v,w \in \T[\Sigma]$, if $\rho_{\Sigma}(v)=a=\rho_{\Sigma}(w)$, then $v \sim w$.
\end{itemize}
\end{proposition}
\begin{proof}
\todo{À écrire.}
\end{proof}
\section{Proof of Theorem \ref{thm:conduche}: part III}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment