text:
\begin{document}

\author[Scott Balchin]{Scott Balchin}
\address{Department of Mathematics\\
University of Leicester\\
University Road, Leicester LE1 7RH, England, United Kingdom}
\email{slb76@le.ac.uk}

\title[Factorisation and Cohomology of Higher Categories]{Factorisation and Cohomology of Higher Categories}

\begin{abstract}{We construct an iterative method for factorising small strict $n$-categories into a unique (up to isomorphism) collection of small 1-categories. Following this we develop the theory to include a large class of $\infty$-categories. We use this factorisation to define cohomology theory for higher categories. Finally, we discuss some concrete examples of factorisations of low dimensional categories.}
\end{abstract}

\keywords{Factorisation, Strict $n$-Categories, Cohomology, Dendroidal Set}

\maketitle

\section*{Introduction}

Cohomology theories for small categories were developed by many authors, such as in the work of Watts \cite{watts}, Grothendiek \cite{groth}, Quillen \cite{quillen} and Baues-Wirsching \cite{baues}. Recently G\'alvez-Carrillo, Neumann and Tonks \cite{galvez} developed the theory of Thomason cohomology using Thomason natural systems. This cohomology uses general coefficient systems and was studied in the context of work by Gabriel-Zisman (see \cite{gabriel}).  There has been a recent surge in interest in higher category theory, more specifically that of $\infty$-categories. The goal of this article is to develop cohomology theories for these classes of categories.  Work undertaken by Lurie among others has given such theory for $\infty$-topoi and wider classes of $\infty$-categories, however the latter relies on taking the homotopy category of the $\infty$-category which disregards the higher morphisms \cite{luriebook} \cite{luriebook2}. These cohomology theories use local coefficients, however if we were to utilise the theory of Thomason cohomology we could have cohomology with very general coefficient systems.

In this article we introduce a way to factorise small strict higher categories into a tree like structure of 1-categories, which allows us to use classical methods to construct an $n$-group cohomology for an $n$-category.  Such factorisations have nice functorial properties and uniquely represent the category.  Given such a factorisation, we will look at properties of the shape of the factorisation, where the category of all shapes can be realised as a subcategory of the category of finite rooted trees $\Omega$ which plays a key role in the theory of dendroidal sets, see \cite{dendroidal2}.

The factorisation is given through the use of a shift map which utilises the morphisms in the category, which essentially is a decategorification from the objects up as opposed to the morphisms down as we would if we were taking the homotopy category.  Each shift reduces the categorical dimension by one, we then have reasoning to show that we need not consider each shift, but the homotopy category of each shift, which gives us our collection of 1-categories.

Although this theory was developed to study cohomology with general coefficient systems, it is evident that it may have broader applications, as the factorisation allows us to pass higher categories through classical cohomological machinery intended for 1-categories.

\section{Factorisation of Strict $n$-Categories}
\subsection{Shift Map}
We begin by introducing the so called shift map which allows us to reduce the dimension of a strict $n$-category, let us first introduce the necessary terminology (see \cite{leinster}).

\begin{definition}
A \emph{strict $n$-category} $\Cc$ is a category such that the morphisms are strict $(n-1)$-categories.  We denote by $\Cat_n$ the $(n+1)$-category of strict $n$-categories.
\end{definition}

\begin{remark}
For the rest of the article we will assume that $\Cc$ is a small $n$-category where we index the objects using the natural numbers, $X_i \in \Cc$ for $i \in \mathbb{N}$.
\end{remark}

\begin{definition}
Given $\Cc \in \Cat_n$ we construct a $(n-1)$-category, $s(\Cc)$, from $\Cc$ which we call the \emph{shift} of $\Cc$:

$$s(\Cc)=\coprod_{X_i, X_j \in \mathscr{C}} \Hom(X_i,X_j)$$

\noindent For ease of keeping track of the shifts, instead of writing $s(\Cc)$ we will write $\Cc[1]$.
\end{definition}

\begin{remark}
Note that in the above definition we do not restrict $i$ and $j$ such that $i \leq j$. This is done because $\Hom(X_i,X_j)$ is not necessarily equal to $\Hom(X_j,X_i)$, therefore we need to consider both cases.
\end{remark}

\begin{remark}
If we let $H_1=\Hom(X_i,X_j), H_2=\Hom(X_n,X_m) \in \Cc[1]$, then $\Hom(H_1,H_2)=\emptyset$ unless $i=n$ and $j=m$.  It follows that we get disjoint objects in $\Cc[1]$.  Therefore our above definition has a bit of ambiguity, we have chosen to consider $\Cc[1]$ as just one $(n-1)$-category, however we could consider it as a collection of disjoint ones, which we will be doing when we look at factorisations later.  Although we will use both ways, it should be apparent which one we are using.
\end{remark}

\begin{remark}
We have chosen $\Cc[1]$ to represent the shift map, because if we wanted to consider $s(s(\Cc))$, we can simply refer to it as $(\Cc[1])[1] = \Cc[2]$.  In general the $k$-th shift of $\Cc$ will be denoted by $\Cc[k]$.
\end{remark}

\begin{lemma}
Let $\Cc$ be a small strict $n$-category, then $\Cc[k]$ is defined for all $0 \leq k < n$
\end{lemma}

\begin{proof}
By definition, the shift map reduces the dimension by one each time it is applied.  Therefore it suffices to work out at which shift we get elements which are 1-categories. Clearly $\Cc[n-1]$ would have categorical dimension $n-(n-1)=1$.  Therefore we can only apply the shift map $n-1$ times.
\end{proof}

\subsection{Factorisation Trees and Planes}

Now that we have defined the shift map, we want to be able to use it to construct a factorisation for $\Cc$. $\Cc[1]$ can be regarded as many disjoint $(n-1)$-categories, and this is going to be an essential part of the construction.  The general idea is to factor $\Cc$ into its morphisms which are of one categorical dimension less, we then apply the shift map to each of the $\Cc[1]$ categories to factor each one of them.  We continue this process $(n-1)$ times until we reach a collection of 1-categories.  This process has a clear tree like structure which we will be discussing in detail later.

\begin{definition}
Let $\Cc$ be a strict $n$-category.  We inductively define the \emph{factorisation tree of $\Cc$}, which we denote by $\ff(\Cc)$, by the following procedure:

\begin{itemize}
\item The initial vertex is $\Cc$.
\item The second level has a vertex for each disjoint part of $\Cc[1]$ all of which are connected to the previous vertex.
\item The third level has a vertex for each disjoint part of $\Cc[2]$ which are connected to the vertex in the second level which they are the shift of.
\item Given the $k$-th level which is $\Cc[k-1]$, we attach the $\Cc[k]$ to the above vertices based on which one they are the shift of, which gives us the $(k+1)$-th level.
\end{itemize}
\end{definition}

\begin{remark}
Although in the definition we have said "vertex", we do not disregard what the category in question is, we still want to keep track of the category at each vertex.
\end{remark}

It is clear that $\ff(\Cc)$ uniquely determines $\Cc$, because we still have the initial category as our top vertex, therefore we repeat information. We wish to reduce the amount of information in the factorisation, but for it to still uniquely determine $\Cc$.

The first idea is to consider just the bottom row, however there is no unique way to embed a collection of 1-categories $\Cc_i$ into a strict 2-category $\Dd$ such that $\Dd[1]=\coprod \Cc_i$. An example of this is shown in the appendix. However we can see that if we knew the the objects of $\Dd$ then such an embedding would be unique (up to isomorphism). Therefore what we do is take the homotopy category at all levels of the shift.

\begin{definition}
Let $\Cc$ be a strict $n$-category, then the \emph{factorisation plane of $\Cc$}, denoted by $\pp(\Cc)$ is obtained by taking the homotopy category of every vertex of $\ff(\Cc)$.
\end{definition}

\begin{proposition}
Let $\Cc$ be a strict $n$-category, then $\pp(\Cc)$ uniquely determines $\Cc$ up to isomorphism.
\end{proposition}

\begin{remark}
When considering the factorisation, we took every shift, however we could consider a coarser factorisation by considering every $k$-th shift, although this would not uniquely factorise the category.
\end{remark}

\subsection{Functorial Properties of the Shift Map}
 We want to study the functorial properties of the shift map, and subsequently the factorisation of higher categories \cite{maclane}.

 \begin{proposition}
 Let $F: \Cc \to \Dd$ be a functor between strict $n$-categories, then there is an induced functor $F^\ast : \ff(\Cc) \to \ff(\Dd)$ which acts in a natural way on each vertex
 \end{proposition}

 \begin{proof}
 Functors are defined in such a way that they act nicely on the morphisms of the category, that is given an arrow \xymatrix{A \ar[r]^f & B} in $\mathscr{C}$, there is an arrow \xymatrix{FA \ar[r]^{Ff} & FB}. It follows that we have a naturally induced functor $F^\ast : \Hom(A,B) \to \Hom(FA,FB)$.  We can apply $F^\ast$ to each vertex of the factorisation to get the functor $F^\ast : \ff(\Cc) \to \ff(\Dd)$ as required.
 \end{proof}

 \begin{corollary}
Let $F: \Cc \to \Dd$ be a functor between strict $n$-categories, then there is an induced functor $F^\star : \pp(\Cc) \to \pp(\Dd)$ which acts in a natural way on each vertex
 \end{corollary}

\begin{proof}
This follows from the above theorem, $F^\star$ is $F^\ast$ acting only on the objects and 1-morphisms.
\end{proof}

 \begin{corollary}
 Let $\Cc \simeq \Dd$ be an equivalence of strict $n$-categories, then there is an equivalence $\ff(\Cc) \simeq \ff(\Dd)$
 \end{corollary}

\begin{proof}
If $F:\Cc \to \Dd$ is the functor giving the equivalence, then $F^\ast$ will be an equivalence on each part of the factorisation.
\end{proof}

\subsection{Example: Strict 2 and 3-Groups}

\begin{definition}
A \emph{strict $n$-group} is a group object internal to $(n-1)$-$\Gg rpd$, the $(n-1)$-dimensional category of strict groupoids \cite{garzon}.
\end{definition}

We begin by looking at the factorisations of $2$-groups, this is a relatively simple procedure as we only have one object in $\mathscr{C}$.  Let $\mathscr{G}$ be a strict $2$-group, then $\mathscr{G}[1]= \coprod \Hom(X_i,X_j) = \Hom(X,X)$.  That is the shift of $\mathscr{G}$ only has one category in it, which is a groupoid. If we represent by $\bullet$ a category, then $\mathbb{F}(\mathscr{G})$ has the following shape

\centerline{\xymatrix{ \mathscr{G} & \bullet \ar[d] \\
 \mathscr{G}[1] & \bullet}}

This case is trivial, the more interesting shapes arise when we deal with strict higher groups.  If we consider a strict $3$-group $\mathscr{G}$, then its first shift is the same as in the $2$-group case.  However the category in $\mathscr{G}[1]$ will have more than one object (unless it is the identity 3-group), and therefore $\mathscr{G}[2]$ will have more than one category in it. The shape for it is as in the following diagram:

\centerline{\xymatrix{ \mathscr{G} &&& \bullet \ar[d] \\
 \mathscr{G}[1] &&& \bullet \ar[d]  \ar[dll] \ar[dl] \ar[dr] \ar[drr]\\
 \mathscr{G}[2] & \bullet & \bullet & \cdots & \bullet & \bullet}}

 \begin{remark}
 In the above example we said that if $\mathscr{G}$ was the identity $3$-group, or the strict identity $3$-category, then we will only get one category in $\mathscr{G}[2]$.  This is easily realised for all identity categories.
\end{remark}

 \begin{definition}
 The \emph{strict identity $n$-category} is the category with only identity morphisms in each dimension, we will denote it by $\mathscr{I}_n$
 \end{definition}

 Let $\mathscr{I}_n$ be the identity $n$-category, then $\mathbb{F}(\mathscr{I}_n)$ has the following linear shape

 \centerline{\xymatrix{ \mathscr{I} & \bullet \ar[d] \\
 \mathscr{I}[1] & \bullet \ar[d]\\
 \mathscr{I}[2] & \bullet \ar[d]\\
 &  \vdots \ar[d] \\
 \mathscr{I}[n-1] & \bullet}}

\subsection{Factorisation of $\infty$-Categories}
We can easily extend the previous theory to the notion of $\infty$-categories if we choose the right model for our categories.

\begin{definition}
The category $\Cc at_\infty$ is the $\infty$-category of strict infinity categories.
\end{definition}

\begin{definition}
A \emph{strict $\infty$-category} $\Cc$ is a category such that for any two objects $\Hom(X,Y) \in \Cc at_\infty$.  That is we will consider an $\infty$-category to be a category enriched over the $\infty$-category of strict $\infty$-categories.
\end{definition}

\begin{definition}
The category $\Cc at_{\leq \infty}$ has for objects strict categories of all dimensions with morphisms between objects if and only if they have the same dimension.
\end{definition}

With this type of model considered, we can calculate the factorisation of a strict $\infty$-category, although the main difference will be that the factorisation tree will never terminate, it will be infinite.

\section{The Factorisation Tree in the Tree Category $\Omega$}
\subsection{The Category of Finite Rooted Trees}
We now look at the factorisation tree of a category in a more combinatorial manner. For this we consider their embedding into the category of finite rooted trees which we briefly review here (see \cite{dendroidal2}).

\begin{definition}
A \emph{finite symmetric rooted tree} is a finite poset $(T, \leq)$ such that it satisfies the following:

\begin{itemize}
\item There is a bottom element
\item For each element $e \in T$, the set $\{y \in T | y \leq e\}$ is a linear order under $\leq$
\item It is equipped with a subset $L \subset max(T)$ of the maximal elements of $T$.
\end{itemize}

The category of all all finite symmetric rooted trees is the tree category $\Omega$, where the morphisms are generated by face and degeneracy maps \cite{moerdijk}.
\end{definition}

\begin{notation}
Let $((T,\leq),L)$ be a tree, then:

\begin{itemize}
\item An element $e \in T$ is called an \emph{edge} of the tree
\item The bottom element is called the \emph{root} of the tree
\item An edge in $L \subset T$ is a \emph{leaf} of the tree
\item An edge which is either a leaf or the root is called an \emph{outer edge}
\item An edge which is neither a leaf nor the root is called an \emph{inner edge}
\item Given a non-leaf edge $e$, another edge $e'$ is called an \emph{incoming edge} if it is a direct successor of $e$.  We denote by $in(e)$ the set of incoming edges of $e$
\item Given a non-leaf edge $e$, the subset $v_e := \{e\} \cup in(e)$ is called a \emph{vertex} of $(T, \leq)$, We say that $e$ is the \emph{outgoing edge} of $v$, and we get $in(v_e) := in(e)$
\end{itemize}
\end{notation}

\begin{remark}
Given a finite rooted tree we can obtain a corresponding symmetric operad over $\mathscr{S}et$.  Therefore it follows that we have an inclusion $\Omega \hookrightarrow \mathscr{O}perad$ of the category of finite rooted trees to the category of symmetric operads (see \cite{weissop}).
\end{remark}

\subsection{Factorisation Trees to Finite Rooted Trees}
We now consider a method of embedding factorisation trees into $\Omega$.  We begin by considering degenerate branches of the factorisation tree

\begin{definition}
Let $\mathbb{F}(\mathscr{C})$ be the factorisation tree of a strict $n$-category $\mathscr{C}$.  If $\Hom(X_i,X_j) \in \mathscr{C}[k]$ is the identity $(n-k)$-category, then we say that this element and its successive shifts are a \emph{degenerate branch}.
\end{definition}

\begin{example}
The first example is that of the trivial $n$-category. We saw in an earlier example that the shape of the factorisation of the trivial $n$-category was a single line with $n$ vertices, in this case, the whole branch is degenerate.
\end{example}

\begin{definition}
Denote by $\mathbb{F}act$ the category whose objects are factorisations of categories, and whose morphisms are generated by deleting or inserting categories at vertices.
\end{definition}

\begin{remark}
For an overview of how face and degeneracy maps work in $\Omega$ see \cite{dendroidal2}.
\end{remark}

\begin{remark}
We can consider a factorisation to be a functor $\Cc at_{\leq \infty} \to \mathbb{F}act$.
\end{remark}

\begin{definition}
Let $\Cc$ be a strict $n$-category with factorisation $\mathbb{F}(\Cc)$, we define a quotient map on degenerate branches, where the first vertex of the degeneracy remains, giving it an leaf edge.  We denote this quotient map $Q : \mathbb{F}(\Cc) \to \mathbb{F}(\Cc) / (id)$.
\end{definition}

We now wish to consider the factorisation trees as finite rooted trees. This requires a forgetful functor $u: \mathbb{F}act \to \Omega$, which forgets the category at each vertex.

\begin{definition}
Let $\Cc$ be a strict $n$-category with factorisation $\mathbb{F}(\Cc)$, then the \emph{shape} of $\Cc$ is the tree given by $\mathbb{S}(\Cc)=u(\mathbb{F}(\Cc)/id) \in \Omega$
\end{definition}

\begin{remark}
It should be noted that unlike the factorisation itself, the shape of a category is not unique, there will be infinitely many categories with the same shape, for example all 1-categories have the same shape which is just a single vertex.
\end{remark}

\begin{example}
The identity categories of all dimensions greater than 1 have the same shape. This is because the single branch is degenerate so we quotient out by it and we are left with this shape

\centerline{\xymatrix{ \bullet \ar@{-}[d]\\
&}}
\end{example}

Recall that the simplex category $\Delta$ is a full subcategory of $\Omega$ \cite{moerdijk}. We want to know what families of category have shapes in $\Delta$.  These will be categories that have only one morphism in each dimension apart from the $n$-morphisms which must be non trivial. This gives us a countably infinite set of categories which have shape $[n] \in \Delta$.

\begin{definition}
We denote by $\Cc_{\Delta[n]}$ the collection of $n$-categories which have shape $[n] \in \Delta$, and call them the \emph{categories of $[n]$-shape}.
\end{definition}

\begin{example}
 The following image represents a category in $\Cc_{\Delta[3]}$ where the different line dashings represent different dimensions of morphisms
\vspace{5mm}

\centerline{
\includegraphics[scale=0.08]{delta3}}

\vspace{5mm}
\end{example}

\begin{remark}
For the shape of a category to be truly a finite rooted tree we must specify the root and the direction. This follows quite naturally, the root would be an inward edge on the initial vertex (this is the one obtained from $\Cc$), and the direction would follow the only possible route.
\end{remark}

We now briefly discuss how operations in $\Omega$ affect the shape of a category.  If we consider the categories of simplex shape $\Cc_{\Delta[n]}$, then this is asking how do the face and degeneracy maps affect the category?  The face map $[n] \to [n-1]$ removes a vertex from the tree and merging the two edges which were incident to the vertex and this gives us the shape of $\Cc_{\Delta[n-1]}$ as expected. We have a similar process for the degeneracy maps which gives us a category of one dimension higher.

\section{Cohomology Theories for Strict $n$-Categories}
\subsection{Thomason Cohomology}
We now use Thomason cohomology as introduced in \cite{galvez}. This is a cohomology theory for small categories using general coefficient systems.  Using the factorisation system that we have developed, we apply the tools of Thomason cohomology to define cohomology for strict $n$-categories.  We begin by recalling some definitions from \cite{galvez}.

\begin{definition}
Let $\mathscr{C}$ be a small category, and $T:\Delta/ \mathscr{C} \to \mathscr{A}b$ be a Thomason natural system with values in the category of abelian groups.  The \emph{Thomason cochain complex} $C^\ast_{Th}(\mathscr{C},T)$ is defined as

\begin{center}
\[C^n_{Th}(\mathscr{C},T)= \prod_{([n],f)\in \Delta / \mathscr{C} } T(f) \]
\end{center}

For $n \geq 0$, we have the differential

\begin{center}
\[ d= \sum^{n+1}_{i=1} (-1)^i d_i : \prod_{[n] \to^f \mathscr{C}} T(f) \to \prod_{[n+1] \to^g \mathscr{C}} T(g) \]
\end{center}

induced by the coface maps.

The \emph{$n$-th Thomason cohomology} of $\Cc$ with coefficients $T$ is defined as $H^n_{Th}(\mathscr{C},T):=H^n(C^\ast_{Th}(\mathscr{C},T),d)$
\end{definition}

\begin{remark}
In the definition above we used $\mathscr{A}b$, the category of abelian groups, however the definition works with any abelian category $\Aa$ with some conditions (see \cite{galvez}).
\end{remark}

We now use this, and our factorisation plane to define the Thomason cohomology, but first we introduce some notation

\begin{definition}
Let $\Cc$ be a strict $n$-category with factorisation plane $\mathbb{P}(\Cc)$. We denote by $\mathscr{C}[i,j]$ the category that is placed $i$-th vertically from the top and $j$-th horizontally from the left of $\mathbb{P}(\Cc)$.
\end{definition}

\begin{example}
Consider a category with the following factorisation
\vspace{5mm}

\centerline{\xymatrix{ &&& \bullet \ar[dl] \ar[dr] \\
& & \bullet \ar[dl] \ar[dr] & & \bullet \ar[d] \\
& \bullet & & \star &  \bullet}}
\vspace{5mm}

Then the category denoted by $\star$ would be $\Cc[3,2]$

\end{example}

\begin{definition}
Let $\Cc$ be a strict $n$-category with factorisation plane $\mathbb{P}(\Cc)$.  Then a Thomason natural system on $\Cc$ is a collection of functors $T_{[i,j]}:\Delta/( \Cc[i,j] )\to \Aa b$
\end{definition}

\begin{definition}
Let $\Cc$ be a strict $m$-category with factorisation plane $\mathbb{P}(\Cc)$.  Then the Thomason cohomology group of $\Cc$ is the strict $m$-group whose $k$-morphisms are the collection are groups $H^n_{Th}(\mathscr{C}[k,j],T_{[k,j]})$ where $j$ ranges over the obvious domain.  We attach the $k$ morphisms to the $k-1$ morphisms by respecting the shape of the tree. That is, we attach $H^n_{Th}(\mathscr{C}[k,j],T_{[k,j]})$ as $k$-morphisms of $H^n_{Th}(\mathscr{C}[k-1,j'],T_{[k-1,j']})$ if there is an edge from $\mathscr{C}[k-1,j']$ to $\mathscr{C}[k,j]$ in $\mathbb{P}(\Cc)$.

We will denote the $m$-group $n$-th cohomology by $H^{m,n}_{Th}(\mathscr{C},T)$
\end{definition}

\begin{remark}
We can easily apply the above procedure to the class of $\infty$-categories that were discussed earlier, in this case we would get a strict $\infty$-group for the cohomology.
\end{remark}

We can use the functorial properties of the cohomology theory and the factorisations to give some results about the cohomology of higher categories.

\begin{proposition}

Let $\Cc$ and $\Dd$ be strict $n$-categories, and $(\phi,\psi)$ a pair of adjoint strict $n$-functors

\begin{center}
$ \phi : \Dd \rightleftarrows \Cc : \psi$
\end{center}

Then there is a natural isomorphism $H^{n,\ast}_{Th}(\Dd,\phi^\ast(T)) \cong H^{n,\ast}_{Th(n)}(\Cc,T)$
\end{proposition}

\begin{proof}
Using corollary $1.14$ we can lift $\phi$ and $\psi$ to $\phi^\star$ and $\psi^\star$ respectively. These are a pair of adjoint functors between $\mathbb{P}(\Cc)$ and $\mathbb{P}(\Dd)$ which act on each node in the factorisaion tree in the obvious way.  Then using results from \cite{galvez} concerning the functorial properties of Thomason cohomology, we can conclude our result.
\end{proof}

Using the methods outlined in \cite{galvez}, it is possible to give similar definitions for Baues-Wirsching cohomology and other classical cohomology theories for strict $n$-categories.

\section{Example: A $3$-Groupoid}
\subsection{Factorisation Tree and Plane}
In this section we will be considering a strict 3-groupoid $\Cc$ which is the following category

\centerline{
\includegraphics[scale=0.08]{3cat}}

Here the double lines are 2-morphisms and the triple line is a 3-morphism.  The identity 1-, 2- and 3-morphisms are not included in the image.  The first step in calculating the factorisation of $\Cc$ is to calculate $\Cc[1]$.  As $\Cc$ is a groupoid which is fully connected with two objects, we have $2^2=4$ 2-categories in $\Cc[1]$. Let us call the left object $X_1$ and the right object $X_2$

Begin by noting that $\Hom(X_1,X_1)=\Hom(X_2,X_2)=\mathscr{I}_2$, where $\mathscr{I}_2$ is the identity 2-category.  Also, because of the symmetry of the category we will have that $\Hom(X_1,X_2)=\Hom(X_2,X_1)$, we just need to find out what 2-category this is. An easy way to do this is to regard the morphisms as the new objects, and then the 2-morphisms as the new 1-morphisms and so on. It follows that $\Hom(X_1,X_2)$ is the following category

\vspace{5mm}

\centerline{
\xymatrix{\mathscr{C}'= &\bullet\rtwocell{=} & \bullet \ltwocell{=} }}
\vspace{5mm}

These categories make up $\Cc[1]$, we now need to work out the shift of each of these categories so that we can calculate $\Cc[2]$. Clearly $\mathscr{I}_2[1]=\mathscr{I}_1$, so we need only consider $\Cc'[1]$ in any detail.  As with $\Cc$ we have two objects which are connected, so we will get four 1-categories in $\Cc'[1]$.  If we label the left object of $\Cc'$ $Y_1$ and the right object $Y_2$, then we have that $\Hom(Y_1,Y_1)=\Hom(Y_2,Y_2)=\mathscr{I}_1$, and $\Hom(Y_1,Y_2)=\Hom(Y_2,Y_1)=\Cc''$ where $\Cc''$ is given by the following category

\vspace{5mm}

\centerline{
\xymatrix{\mathscr{C}''= &\bullet \ar[r] & \bullet \ar[l] }}
\vspace{5mm}

We now have all of the parts required to derive the factorisation of $\Cc$. $\mathbb{F}(\Cc)$ is given by the following tree:

\vspace{5mm}

\centerline{
\xymatrix{\Cc &&&&&& \Cc \ar[ddlllll] \ar[ddrrrrr] \ar[ddll] \ar[ddrr]\\
\\
\Cc[1] & \mathscr{I}_2 \ar[dd] &&& \Cc' \ar[ddll] \ar[ddl] \ar[dd] \ar[ddr]  &&&& \Cc' \ar[ddl] \ar[dd] \ar[ddr] \ar[ddrr] &&& \mathscr{I}_2 \ar[dd]\\
\\
\Cc[2] & \mathscr{I}_1 & \mathscr{I}_1 & \Cc'' & \Cc'' & \mathscr{I}_1 && \mathscr{I}_1 & \Cc'' & \Cc'' & \mathscr{I}_1 & \mathscr{I}_1}}
\vspace{5mm}

The next task is to find the factorisation plane of $\Cc$, so this requires us to find the homotopy categories of the involved higher categories.  Note that $h(\mathscr{I}_2)=\mathscr{I}_1$ and that $h(\Cc)=h(\Cc')=\Cc''$, so that $\mathbb{P}(\Cc)$ is the following tree

\vspace{5mm}

\centerline{
\xymatrix{h(\Cc) &&&&&& \Cc'' \ar[ddlllll] \ar[ddrrrrr] \ar[ddll] \ar[ddrr]\\
\\
h(\Cc[1]) & \mathscr{I}_1 \ar[dd] &&& \Cc'' \ar[ddll] \ar[ddl] \ar[dd] \ar[ddr]  &&&& \Cc'' \ar[ddl] \ar[dd] \ar[ddr] \ar[ddrr] &&& \mathscr{I}_1 \ar[dd]\\
\\
\Cc[2] & \mathscr{I}_1 & \mathscr{I}_1 & \Cc'' & \Cc'' & \mathscr{I}_1 && \mathscr{I}_1 & \Cc'' & \Cc'' & \mathscr{I}_1 & \mathscr{I}_1}}
\vspace{5mm}

Finally we would like to know the shape of $\Cc$. This requires us to quotient out the degenerate branches. We have two branches that are degenerate, both of which start at $\mathscr{I}_2$. When we quotient out these and use the forgetful functor (from definition 2.9) we get the following rooted tree in $\Omega$

\vspace{5mm}

\centerline{
\xymatrix{ &&&&& \ar[d]\\
&&&&& \bullet \ar[ddlllll] \ar[ddrrrrr] \ar[ddll] \ar[ddrr]\\
\\
  \bullet \ar[dd] &&& \bullet \ar[ddll] \ar[ddl] \ar[dd] \ar[ddr]  &&&& \bullet \ar[ddl] \ar[dd] \ar[ddr] \ar[ddrr] &&& \bullet \ar[dd]\\
\\
 & \bullet & \bullet & \bullet & \bullet && \bullet & \bullet & \bullet & \bullet & }}
\vspace{5mm}

We now have derived $\mathbb{F}(\Cc)$, $\mathbb{P}(\Cc)$ and $\mathbb{S}(\Cc)$.  Now we consider $\mathbb{P}(\Cc)$ so we can calculate the cohomology of $\Cc$. We will not explicitly calculate each homology group, but just leave them as $H^n_{Th}(\mathscr{C}[k,j],T_{[k,j]})$, where $k=1,2,3$ and $j$ can take a range of values respective of the value of $k$. Then we have $H^{3,n}(\Cc,T)$ using the following form, if a group has an arrow to another group, then it indicates that that group acts on the group it is incident to, and the $\bullet$ represents an object.  We will also shorten $H^n_{Th}(\mathscr{C}[k,j],T_{[k,j]})$ to $H^n(k,j)$ for space purposes

\vspace{5mm}

\centerline{\resizebox{35em}{0.8em}{
\xymatrix{ H^n(3,1) \ar[d] & H^n(3,2) \ar[drr] & H^n(3,3) \ar[dr] & H^n(3,4) \ar[d] & H^n(3,5) \ar[dl] && H^n(3,6) \ar[dr] & H^n(3,7) \ar[d] & H^n(3,8) \ar[dl] &  H^n(3,9) \ar[dll] & H^n(3,10)\ar[d] \\
H^n(2,1) \ar[drrrrr] &&& H^n(2,2) \ar[drr] &&&& H^n(2,3)\ar[dll] &&& H^n(2,4) \ar[dlllll]\\
&&&&& H^n(1,1) \ar[d] \\
&&&&& \bullet}}}

\vspace{5mm}

\appendix
\section{Unique Embedding of 1-Categories into Strict 2-Categories}

We will first show that there is always a trivial embedding of a 1-category into a strict 2-category, such that the shift of the 2-category is our collection of 1-categories.

Suppose that we start with the 2-groupoid $\mathscr{C}$ displayed below discarding the identity 2 morphisms.
\vspace{5mm}

\centerline{
\xymatrix{\mathscr{C}= &\bullet \ar@(ul,dl) \ar@(dl,ul) \rtwocell{=} & \bullet \ltwocell{=} \ar@(ur,dr) \ar@(dr,ur)}}
\vspace{5mm}

We want to derive $\mathscr{C}[1]$, as the category is connected, and we have two objects, we will get four 1-categories from the shift. This gives us the following shift $\Cc[1]$:
\vspace{5mm}

\centerline{\xymatrix{\mathscr{C}[1]= & \bullet \ar@(ul,dl) \ar@(dl,ul) & \bullet \ar@(ul,dl) \ar@(dl,ul) \ar[r] & \bullet \ar[l] \ar@(ur,dr) \ar@(dr,ur) & & \bullet \ar@(ul,dl) \ar@(dl,ul) \ar[r] & \bullet \ar[l] \ar@(ur,dr) \ar@(dr,ur) &  \bullet \ar@(ur,dr) \ar@(dr,ur)}}

\vspace{5mm}

Now we want to show that this factorisation is not unique in the sense that another 2-category could have this collection of 1-categories as its shift.  The procedure is easy, we can just take four disjoint objects, and embed each shift category above as a set of morphisms going from the object to itself.  Then if we take the shift of this 2-category, because the objects are disjoint, we get four 1-categories and they are exactly as we require.

\noindent We will now look at another example, where there is a non-trivial embedding of a collection of 1-categories into two different 2-categories.  The 2-category in question has three objects and looks like this, where we have excluded the identity 1 morphisms as well as the identity 2-morphisms to make the diagram less cluttered.
\vspace{5mm}

\centerline{
\xymatrix{\mathscr{C}= & \bullet  \rrtwocell{=} \ddrtwocell{=} && \bullet \lltwocell{=} \ddltwocell{=}\\
& \\
&& \bullet \uurtwocell{=} \uultwocell{=}  }}

\vspace{5mm}

The shift of $\mathscr{C}$ has two different types of structure, with multiplicity 3 and 6 which we will denote by $"3 \times"$ and $"6 \times"$.  Note that we have $9 = 3^2$ categories as all objects are linked by morphisms in both directions.

\vspace{5mm}

\centerline{
\xymatrix{\mathscr{C}[1] = & 3 \times & \bullet \ar@(ul,dl) \ar@(dl,ul) & 6 \times & \bullet \ar@(ul,dl) \ar@(dl,ul) \ar[r] & \bullet \ar[l] \ar@(ur,dr) \ar@(dr,ur)}}

\vspace{5mm}

We want to find another category $\mathscr{D}$ which has $\mathscr{C}[1]=\mathscr{D}[1]$.  As we have nine segments above, it would make sense to look at a one category with five objects, which is split into three parts, with one object on its own and two sets of two, this gives us $1^2+2^2+2^2=9$ segments in the shift.  Such a category is given below, and it can be easily verified that this satisfies $\mathscr{C}[1]=\mathscr{D}[1]$, again, excluding all identity morphisms.

\vspace{5mm}

\centerline{
\includegraphics[scale=0.3]{bicategory}}

\noindent This is a non trivial embedding, so given a collection of 1-categories, we do not have a unique way to embed them into a 2-category, and therefore the entire factorisation tree cannot be determined from a subset of levels from the whole tree.  Given the homotopy category of the above level we know the number of objects in the category. This tells us how many objects we are embedding our category into, and how connected they are.  Given this information, we get a unique embedding, which leads to the reasoning that $\mathbb{P}(\Cc)$ represents the same information as $\mathbb{F}(\Cc)$.

\vspace*{0.3cm} {\it Acknowledgements.}
I would like to thank Frank Neumann for his encouragement and suggestions and also for the initial motivation to study higher category theory.

\bibliographystyle{amsplain}
\bibliography{shiftbib}
\end{document}


text:
We established in the last section that the shadow of the negative gradient $\mathbf{d}_{\x_t}^\Pi$ is indeed the best ``local'' direction of descent (Lemma \ref{best local direction}), and a true measure of the primal gap since convergence in $\|\mathbf{d}_{\mathbf{x}_t} ^\Pi\|$ implies optimality (Lemma \ref{primal gap optimality}). Having characterized the parametric projections curve, the natural question is if a shadow-descent algorithm that walks along the directional derivative with respect to negative gradient at iterate $\x_t$
, converge linearly? We start by answering that question positively for  continuous-time dynamics.

We now present the continuous-time dynamics for moving along the shadow of the gradient in the polytope. In this section we let $\mathcal{D}^*$ be the dual space
of $\mathcal{D}$ (in our case since $\mathcal{D} \subseteq \mathbb{R}^n$, $\mathcal{D}^*$ can also be identified with $\mathbb{R}^n$).
Let $\phi: \mathcal{D} \rightarrow \mathbb{R}$ be a strongly convex and differentiable function.
This function will be used as the {\it mirror-map} in a generalization of \hme{the} projected gradient descent algorithm, known as {\it mirror descent} \cite{Nemirovski1983}. \hme{We now briefly discuss the mirror descent algorithm and review simple preliminaries needed for what follows.} Let $\phi^*$ be the Fenchel-conjugate of $\phi$ with effective domain $P$, that is $\phi^*(\mathbf{y}) = \max_{\mathbf{x} \in P} \{\innerprod{\mathbf{y}}{\mathbf{x} } - \phi(\mathbf{x} )\}$. From Danskin's theorem (see e.g., \cite{Bertsekas_2003}), we know that $\nabla \phi^*(\mathbf{y}) = \argmax_{\mathbf{x}  \in P}\{ \innerprod{\mathbf{y}}{\mathbf{x} } - \phi(\x)\}$,
so that $\nabla \phi^* : \mathcal{D}^* \to P$ is the mirror-map operator mapping from $\mathcal{D}^*$ to $\mathcal{D}$. We use $\nabla^2 \phi^* (\cdot)$ to denote the Hessian of $\phi^*$. \hme{The mirror descent algorithm is iterative and starts with any point $\x_0 \in P$. Then for any $t \geq 1$, the algorithm first performs \emph{unconstrained} gradient descent steps in the dual space:
\begin{equation*}
  \mathbf{z}_{t} = \nabla \phi (\x_t) - \gamma_t \nabla f(\x_t) \text{ for some step size $\gamma_t \geq 0$,}
\end{equation*}
and then maps back these descent steps to the primal space by computing a so-called \emph{Bregman projection}: $\x_{t+1} =  \nabla \phi^*(\mathbf{z}_{t})$.}

\subsection{ODE for Moving in the Shadow of the Gradient}
Let $X(t)$ denote the continuous-time trajectory of our dynamics and $\dot{X}$ denote the time-derivative of $X(t)$, i.e., $\dot{X}(t) = \frac{d}{dt}X(t)$. In \cite{Krichene_2015}, Krichene et. al propose the following coupled dynamics $(X(t), Z(t))$ for mirror descent, where $X(t)$ evolves in the primal space $\mathcal{D}$, and $Z(t)$ evolves in the dual space $\mathcal{D}^*$, as follows, initialized with $Z(0) = \mathbf{z}_0 \text{ with } \nabla \phi^*(\mathbf{z}_0) = \x_0 \in P$:
\begin{equation} \label{MD ODE}

    \dot{Z}(t) = -\nabla f(X(t)), \quad X(t) = \nabla \phi^*(Z(t)).

\end{equation}
Let $\mathbf{d}_{X(t)}^{\phi}$ be the directional derivative with respect to the Bregman projections in the mirror descent algorithm, i.e., $\mathbf{d}_{X(t)}^{\phi}= \lim_{\epsilon \downarrow 0}  \frac{\nabla \phi^* (\nabla \phi(X(t)) - \epsilon \nabla f(X(t))) - X(t)}{\epsilon}$. The continuous time dynamics of tracing this directional derivative are simply \begin{equation}
    \dot{X}(t) = \mathbf{d}_{X(t)}^\phi. \label{ODe for shadow}
\end{equation}
\hme{These dynamics in \eqref{ODe for shadow}} solely operate in the primal space and one can initialize them with $X(0) = \x_0\in P$

and show that they are equivalent to \eqref{MD ODE} under mild technical conditions as specified below (the proof is in Appendix \ref{sec: app ode theorem}):

\begin{restatable}{theorem}{odetheorem}
\label{ode theorem}
Let $\phi: \mathcal{D} \rightarrow \mathbb{R}$ be a mirror map that is strongly convex and differentiable, and assume that the directional derivative $\mathbf{d}_{X(t)}^\phi$ exists for all $t \geq 0$. Then, the dynamics for mirror descent \eqref{MD ODE} are equivalent to the shadow dynamics $\dot{X}(t) = \mathbf{d}_{X(t)}^\phi$ with the same initial conditions $X(0) = \x_0\in P$.
\end{restatable}

Although the results of Theorem \ref{ode theorem} hold for general mirror-maps, in this work we focus on the case when $\phi = \frac{1}{2} \|\cdot\|^2$ to exploit the piecewise linear structure of the projections curve (with respect to the gradient) proved in Theorem \ref{elephant}. Note that when the mirror map $\phi = \frac{1}{2} \|\cdot\|^2$, we have
\begin{align*}
    \nabla \phi^*(\mathbf{y}) &= \argmax_{\mathbf{x}  \in P}\{ \innerprod{\mathbf{y}}{\mathbf{x} } - \phi(\x)\}
    = \argmin_{\mathbf{x}  \in P}\left\{ \frac{1}{2}\|\x\| -  \innerprod{\mathbf{y}}{\mathbf{x} }\right\}

    = \argmin_{\mathbf{x}  \in P} \frac{1}{2} \|\y - \x\|^2,
\end{align*}
so that we recover a Euclidean projection onto $P$. This implies
\begin{align*}
  \mathbf{d}_{X(t)}^\phi &= \lim_{\epsilon \downarrow 0}  \frac{\nabla \phi^* (X(t) - \epsilon \nabla f(X(t))) - X(t)}{\epsilon} && (\text{$\nabla \phi(X(t)) = X(t)$)}\\
    & = \lim_{\epsilon \downarrow 0} \frac{\argmin_{\x \in P} \frac{1}{2} \|X(t) - \epsilon \nabla f(X(t)) - \x\|^2 - X(t)}{\epsilon}&& (\text{by definition of $\nabla \phi^*$})\\
    &= \mathbf{d}_{X(t)}^\Pi.
\end{align*}
Therefore, Theorem \ref{ode theorem} shows that the continuous-time dynamics of moving in the (Euclidean) shadow of the gradient are equivalent to those of PGD. Moreover, we also show the following convergence result of those dynamics (proof in Appendix \ref{proof of ode conver theorem}):
\begin{restatable}{theorem}{odeconver}
\label{ode_conver}
Let $P \subseteq \mathbb{R}^n$ be a polytope and suppose that $f : P \rightarrow \mathbb{R}$ is differentiable and $\mu$-strongly convex over $P$. Consider the shadow dynamics $\dot{X}(t) = \mathbf{d}_{X(t)}^\Pi$ with initial conditions $X(0) = \x_0\in P$. Then for each $t \geq 0$, we have $X(t) \in P$. Moreover, the primal gap $h(X(t))\coloneq f(X(t)) - f(\mathbf{x}^*)$ associated with the shadow dynamics decreases as: $h(X(t)) \leq e^{-2\mu t} h(\x_0)$.
\end{restatable}

\subsection{Shadow-Walk Method}
Although the continuous-dynamics of moving along the shadow are the same as those of PGD and achieve linear convergence, it is unclear how to discretize this continuous-time process and obtain a linearly convergent algorithm. To ensure feasibility we may have arbitrarily small step-sizes, and therefore, cannot show sufficient progress in such cases. This is a phenomenon similar to that in the Away-Step and Pairwise CG variants, where the maximum step-size that one can take might not be big enough to show sufficient progress. In \cite{Lacoste2015}, the authors overcome this problem by bounding the number of such `bad' steps using dimension reduction arguments crucially relying on the fact that these algorithms maintain their iterates as a convex combination of vertices. However, unlike away-steps in CG variants, we consider shadow directions {($\mathbf{d}_{\mathbf{x}}^\Pi$, $\hat{\mathbf{d}}_{\mathbf{x}}^\Pi$)} for descent, which are independent from the vertices of $P$ and thus eliminating the need to maintain active sets for the iterates of the algorithm. In general, the shadow ODE might revisit a fixed facet a large number times (see Figure \ref{fig:proj}) with decreasing step-sizes. This problem does not occur when discretizing PGD's continuous time dynamics since we can take {\it unconstrained} gradient steps and then the projections ensure feasibility.

Inspired by PGD's discretization and the structure of the parametric projections curve, we propose a {\sc Shadow-Walk} algorithm (Algorithm \ref{alg:shadowwalk}) with a slight twist: \hme{trace the projections curve by walking along the shadow at an iterate $\x_t$ until enough progress is ensured. To do this, we use the {\sc Trace-Opt} procedure, which chains \hme{together} consecutive short descent steps and uses line-search until it minimizes the function $f$ over the linear segments of projections curve. The complete description of the algorithm is given in Algorithm \ref{alg: tracing PW proj opt} in Appendix \ref{app: trace opt}.}
One important property of {\sc Trace-Opt} is that it only requires one gradient oracle call. Also, if we know the smoothness constant $L$, then {\sc Trace-Opt} can be terminated early once we have traced the projections curve until we reach the PGD step with a fixed $1/L$ step size. This results in linear convergence, as long as the number of steps \hme{taken by the} {\sc Trace-Opt} \hme{procedure} are bounded, i.e., the number of ``bad'' boundary cases. Using fundamental properties of normal cones attained in the projections curve, we are able bound these steps to be at most the number of faces of the polytope (Theorem \ref{breakpoints}). We thus establish the following result (proof in Appendix \ref{sec:app proof of theorem alg convg 1}):

\begin{algorithm}[t]
\caption{{\sc Shadow-Walk} Algorithm}
\label{alg:shadowwalk}
\begin{algorithmic}[1]
\INPUT Polytope $P \subseteq \mathbb{R}^n$, function $f : P \to \mathbb{R}$ and initialization $\x_0 \in P$.
\For{$t = 0, \dots. T$}
    \State Update $\mathbf{x}_{t+1} \coloneq$ \textsc{Trace-Opt}$(\mathbf{x}_t, \nabla f(\mathbf{x}_t))$ . \Comment{ \texttt{trace projections curve}}
\EndFor
\RETURN $\x_{T+1}$
\end{algorithmic}
\end{algorithm}

\begin{restatable}{theorem}{shadowwalkconver} \label{alg converg1}
Let $P \subseteq \mathbb{R}^n$ be a polytope and suppose that $f : P \rightarrow \mathbb{R}$ is $L$-smooth and $\mu$-strongly convex over $P$. Then the primal gap $h(\mathbf{x}_t)\coloneq f(\mathbf{x}_t) - f(\mathbf{x}^*)$ of the {\sc Shadow Walk} algorithm decreases geometrically:
$$h(\mathbf{x}_{t+1}) \leq \left(1- \frac{\mu}{ L}\right)h(\mathbf{x}_t)$$
with each iteration of the {\sc Shadow Walk} algorithm (assuming {\sc Trace-Opt} is a single step). Moreover, the number of oracle calls to shadow, {in-face shadow} and line-search oracles to obtain an $\epsilon$-accurate solution is $O\left(\beta \frac{L}{\mu} \log (\frac{1}{\epsilon}) \right)$, where $\beta$ is the maximum number of breakpoints of the parametric projections curve that the \textsc{Trace-Opt} method visits.
\end{restatable}

This result is the key interpolation between PGD and CGD methods, attaining geometric constant independent rates. Comparing this convergence rate with the one in Theorem \ref{ode_conver}, we see that we pay for discretization of the ODE with the constants $L$ and $\beta$. Although the constant $\beta$ depends on the number of facets $m$ and in fact the combinatorial structure of the face-lattice of the polytope, it is invariant under any deformations of the actual geometry of the polytope preserving the face-lattice (in contrast to vertex-facet distance and pyramidal width) as we discuss next. Although we show $\beta \leq O(2^m)$, we conjecture that it can be much smaller (i.e., $O(nm)$) for structured polytopes. Moreover, computationally we see much fewer
\hme{fewer than $O(2^m)$ calls to the oracle}.

\subsection{A  Note on the Linear Convergence Rate}
Although our linear convergence rate depends on the number of facet inequalities $m$, it eliminates the dependence on the geometry of the domain that is needed in CG variants. For example, Jaggi and Lacoste-Julien \cite{Lacoste2015} prove a linear rate of $\left(1 - \frac{\mu}{L} \left( \frac{\delta}{D}\right)^2 \right)$ to get an $\epsilon-$accurate solution for the away step FW algorithm, where $\delta$ is the pyramidal width of the domain. Now, consider the example in Figure \ref{fig:pyramidal width} showing how the pyramidal width $\delta$ of a simple triangle domain changes as the angle $\theta$ changes. In particular, the pyramidal width will be arbitrarily small for small $\theta$. However, note that the number of facets for this triangle domain is $m = 3$, and the number of breakpoints of the projections curve $\beta$ is not dependent on the angle $\theta$. Therefore, we smoothly interpolate between the $\left(1 - \frac{\mu}{L} \right)$ rate for PGD and the rates for CG variants (see Table \ref{summary} for a summary of these rates).

config: arxiv


TITLE: Show that $\sum_{n=1}^\infty nx^{n-1}$ converges uniformly on $[0,\frac{9}{10}]$
QUESTION [0 upvotes]: Show that $\sum_{n=1}^\infty nx^{n-1}$ converges uniformly on $[0,\frac{9}{10}]$

First I think we need to show pointwise convergence:
$$\sum_{n=1}^\infty nx^{n-1} = \lim_{N\to\infty} \sum_{n=1}^N nx^{n-1}$$
Since it's a finite sum we can do the following:
$$= \lim_{N\to\infty} \sum_{n=1}^N (x^n)' =  \lim_{N\to\infty} \left(\sum_{n=1}^N x^n\right)^{'} = \lim_{N\to\infty}  \frac{x^N-1}{x-1} = \frac{1-1}{x-1} = 0$$

REPLY [0 votes]: Using geometric series we know exactly what your series should be
$$ \sum_{n=1}^\infty n x^{n-1} = \frac{1}{(1-x)^2}$$
Uniform convergence asked about the remaining terms and you can try to give uniform estimate
$$ \sum_{n=N+1}^\infty n x^{n-1} = x^N \left( \frac{1}{(1-x)^2}
+ \frac{N}{1-x} \right) \leq  (\tfrac{9}{10})^N \left( \frac{1}{(1-\frac{9}{10})^2}
+ \frac{N}{1-\frac{9}{10}} \right) \to 0 $$
for all $0 \leq x \leq \frac{9}{10}$.


text:
/-
Copyright (c) 2021 Anatole Dedecker. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Anatole Dedecker, Eric Wieser
-/
import analysis.specific_limits.basic
import analysis.analytic.basic
import analysis.complex.basic
import data.nat.choose.cast
import data.finset.noncomm_prod

/-!
# Exponential in a Banach algebra

In this file, we define `exp 𝕂 : 𝔸 → 𝔸`, the exponential map in a topological algebra `𝔸` over a
field `𝕂`.

While for most interesting results we need `𝔸` to be normed algebra, we do not require this in the
definition in order to make `exp` independent of a particular choice of norm. The definition also
does not require that `𝔸` be complete, but we need to assume it for most results.

We then prove some basic results, but we avoid importing derivatives here to minimize dependencies.
Results involving derivatives and comparisons with `real.exp` and `complex.exp` can be found in
`analysis/special_functions/exponential`.

## Main results

We prove most result for an arbitrary field `𝕂`, and then specialize to `𝕂 = ℝ` or `𝕂 = ℂ`.

### General case

- `exp_add_of_commute_of_mem_ball` : if `𝕂` has characteristic zero, then given two commuting
  elements `x` and `y` in the disk of convergence, we have
  `exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)`
- `exp_add_of_mem_ball` : if `𝕂` has characteristic zero and `𝔸` is commutative, then given two
  elements `x` and `y` in the disk of convergence, we have
  `exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)`
- `exp_neg_of_mem_ball` : if `𝕂` has characteristic zero and `𝔸` is a division ring, then given an
  element `x` in the disk of convergence, we have `exp 𝕂 (-x) = (exp 𝕂 x)⁻¹`.

### `𝕂 = ℝ` or `𝕂 = ℂ`

- `exp_series_radius_eq_top` : the `formal_multilinear_series` defining `exp 𝕂` has infinite
  radius of convergence
- `exp_add_of_commute` : given two commuting elements `x` and `y`, we have
  `exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)`
- `exp_add` : if `𝔸` is commutative, then we have `exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)`
  for any `x` and `y`
- `exp_neg` : if `𝔸` is a division ring, then we have `exp 𝕂 (-x) = (exp 𝕂 x)⁻¹`.
- `exp_sum_of_commute` : the analogous result to `exp_add_of_commute` for `finset.sum`.
- `exp_sum` : the analogous result to `exp_add` for `finset.sum`.
- `exp_nsmul` : repeated addition in the domain corresponds to repeated multiplication in the
  codomain.
- `exp_zsmul` : repeated addition in the domain corresponds to repeated multiplication in the
  codomain.

### Other useful compatibility results

- `exp_eq_exp` : if `𝔸` is a normed algebra over two fields `𝕂` and `𝕂'`, then `exp 𝕂 = exp 𝕂' 𝔸`

-/

open filter is_R_or_C continuous_multilinear_map normed_field asymptotics
open_locale nat topological_space big_operators ennreal

section topological_algebra

variables (𝕂 𝔸 : Type*) [field 𝕂] [ring 𝔸] [algebra 𝕂 𝔸] [topological_space 𝔸]
  [topological_ring 𝔸]

/-- `exp_series 𝕂 𝔸` is the `formal_multilinear_series` whose `n`-th term is the map
`(xᵢ) : 𝔸ⁿ ↦ (1/n! : 𝕂) • ∏ xᵢ`. Its sum is the exponential map `exp 𝕂 : 𝔸 → 𝔸`. -/
def exp_series : formal_multilinear_series 𝕂 𝔸 𝔸 :=
λ n, (n!⁻¹ : 𝕂) • continuous_multilinear_map.mk_pi_algebra_fin 𝕂 n 𝔸

variables {𝔸}

/-- `exp 𝕂 : 𝔸 → 𝔸` is the exponential map determined by the action of `𝕂` on `𝔸`.
It is defined as the sum of the `formal_multilinear_series` `exp_series 𝕂 𝔸`.

Note that when `𝔸 = matrix n n 𝕂`, this is the **Matrix Exponential**; see
[`analysis.normed_space.matrix_exponential`](../matrix_exponential) for lemmas specific to that
case. -/
noncomputable def exp (x : 𝔸) : 𝔸 := (exp_series 𝕂 𝔸).sum x

variables {𝕂}

lemma exp_series_apply_eq (x : 𝔸) (n : ℕ) : exp_series 𝕂 𝔸 n (λ _, x) = (n!⁻¹ : 𝕂) • x^n :=
by simp [exp_series]

lemma exp_series_apply_eq' (x : 𝔸) :
  (λ n, exp_series 𝕂 𝔸 n (λ _, x)) = (λ n, (n!⁻¹ : 𝕂) • x^n) :=
funext (exp_series_apply_eq x)

lemma exp_series_sum_eq (x : 𝔸) : (exp_series 𝕂 𝔸).sum x = ∑' (n : ℕ), (n!⁻¹ : 𝕂) • x^n :=
tsum_congr (λ n, exp_series_apply_eq x n)

lemma exp_eq_tsum : exp 𝕂 = (λ x : 𝔸, ∑' (n : ℕ), (n!⁻¹ : 𝕂) • x^n) :=
funext exp_series_sum_eq

@[simp] lemma exp_zero [t2_space 𝔸] : exp 𝕂 (0 : 𝔸) = 1 :=
begin
  suffices : (λ x : 𝔸, ∑' (n : ℕ), (n!⁻¹ : 𝕂) • x^n) 0 = ∑' (n : ℕ), if n = 0 then 1 else 0,
  { have key : ∀ n ∉ ({0} : finset ℕ), (if n = 0 then (1 : 𝔸) else 0) = 0,
      from λ n hn, if_neg (finset.not_mem_singleton.mp hn),
    rw [exp_eq_tsum, this, tsum_eq_sum key, finset.sum_singleton],
    simp },
  refine tsum_congr (λ n, _),
  split_ifs with h h;
  simp [h]
end

@[simp] lemma exp_op [t2_space 𝔸] (x : 𝔸) :
  exp 𝕂 (mul_opposite.op x) = mul_opposite.op (exp 𝕂 x) :=
by simp_rw [exp, exp_series_sum_eq, ←mul_opposite.op_pow, ←mul_opposite.op_smul, tsum_op]

@[simp] lemma exp_unop [t2_space 𝔸] (x : 𝔸ᵐᵒᵖ) :
  exp 𝕂 (mul_opposite.unop x) = mul_opposite.unop (exp 𝕂 x) :=
by simp_rw [exp, exp_series_sum_eq, ←mul_opposite.unop_pow, ←mul_opposite.unop_smul, tsum_unop]

lemma star_exp [t2_space 𝔸] [star_ring 𝔸] [has_continuous_star 𝔸] (x : 𝔸) :
  star (exp 𝕂 x) = exp 𝕂 (star x) :=
by simp_rw [exp_eq_tsum, ←star_pow, ←star_inv_nat_cast_smul, ←tsum_star]

variables (𝕂)

lemma commute.exp_right [t2_space 𝔸] {x y : 𝔸} (h : commute x y) : commute x (exp 𝕂 y) :=
begin
  rw exp_eq_tsum,
  exact commute.tsum_right x (λ n, (h.pow_right n).smul_right _),
end

lemma commute.exp_left [t2_space 𝔸] {x y : 𝔸} (h : commute x y) : commute (exp 𝕂 x) y :=
(h.symm.exp_right 𝕂).symm

lemma commute.exp [t2_space 𝔸] {x y : 𝔸} (h : commute x y) : commute (exp 𝕂 x) (exp 𝕂 y) :=
(h.exp_left _).exp_right _

end topological_algebra

section topological_division_algebra
variables {𝕂 𝔸 : Type*} [field 𝕂] [division_ring 𝔸] [algebra 𝕂 𝔸] [topological_space 𝔸]
  [topological_ring 𝔸]

lemma exp_series_apply_eq_div (x : 𝔸) (n : ℕ) : exp_series 𝕂 𝔸 n (λ _, x) = x^n / n! :=
by rw [div_eq_mul_inv, ←(nat.cast_commute n! (x ^ n)).inv_left₀.eq, ←smul_eq_mul,
    exp_series_apply_eq, inv_nat_cast_smul_eq _ _ _ _]

lemma exp_series_apply_eq_div' (x : 𝔸) : (λ n, exp_series 𝕂 𝔸 n (λ _, x)) = (λ n, x^n / n!) :=
funext (exp_series_apply_eq_div x)

lemma exp_series_sum_eq_div (x : 𝔸) : (exp_series 𝕂 𝔸).sum x = ∑' (n : ℕ), x^n / n! :=
tsum_congr (exp_series_apply_eq_div x)

lemma exp_eq_tsum_div : exp 𝕂 = (λ x : 𝔸, ∑' (n : ℕ), x^n / n!) :=
funext exp_series_sum_eq_div

end topological_division_algebra

section normed

section any_field_any_algebra

variables {𝕂 𝔸 𝔹 : Type*} [nontrivially_normed_field 𝕂]
variables [normed_ring 𝔸] [normed_ring 𝔹] [normed_algebra 𝕂 𝔸] [normed_algebra 𝕂 𝔹]

lemma norm_exp_series_summable_of_mem_ball (x : 𝔸)
  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
  summable (λ n, ∥exp_series 𝕂 𝔸 n (λ _, x)∥) :=
(exp_series 𝕂 𝔸).summable_norm_apply hx

lemma norm_exp_series_summable_of_mem_ball' (x : 𝔸)
  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
  summable (λ n, ∥(n!⁻¹ : 𝕂) • x^n∥) :=
begin
  change summable (norm ∘ _),
  rw ← exp_series_apply_eq',
  exact norm_exp_series_summable_of_mem_ball x hx
end

section complete_algebra

variables [complete_space 𝔸]

lemma exp_series_summable_of_mem_ball (x : 𝔸)
  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
  summable (λ n, exp_series 𝕂 𝔸 n (λ _, x)) :=
summable_of_summable_norm (norm_exp_series_summable_of_mem_ball x hx)

lemma exp_series_summable_of_mem_ball' (x : 𝔸)
  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
  summable (λ n, (n!⁻¹ : 𝕂) • x^n) :=
summable_of_summable_norm (norm_exp_series_summable_of_mem_ball' x hx)

lemma exp_series_has_sum_exp_of_mem_ball (x : 𝔸)
  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
  has_sum (λ n, exp_series 𝕂 𝔸 n (λ _, x)) (exp 𝕂 x) :=
formal_multilinear_series.has_sum (exp_series 𝕂 𝔸) hx

lemma exp_series_has_sum_exp_of_mem_ball' (x : 𝔸)
  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
  has_sum (λ n, (n!⁻¹ : 𝕂) • x^n) (exp 𝕂 x):=
begin
  rw ← exp_series_apply_eq',
  exact exp_series_has_sum_exp_of_mem_ball x hx
end

lemma has_fpower_series_on_ball_exp_of_radius_pos (h : 0 < (exp_series 𝕂 𝔸).radius) :
  has_fpower_series_on_ball (exp 𝕂) (exp_series 𝕂 𝔸) 0 (exp_series 𝕂 𝔸).radius :=
(exp_series 𝕂 𝔸).has_fpower_series_on_ball h

lemma has_fpower_series_at_exp_zero_of_radius_pos (h : 0 < (exp_series 𝕂 𝔸).radius) :
  has_fpower_series_at (exp 𝕂) (exp_series 𝕂 𝔸) 0 :=
(has_fpower_series_on_ball_exp_of_radius_pos h).has_fpower_series_at

lemma continuous_on_exp :
  continuous_on (exp 𝕂 : 𝔸 → 𝔸) (emetric.ball 0 (exp_series 𝕂 𝔸).radius) :=
formal_multilinear_series.continuous_on

lemma analytic_at_exp_of_mem_ball (x : 𝔸) (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
  analytic_at 𝕂 (exp 𝕂) x:=
begin
  by_cases h : (exp_series 𝕂 𝔸).radius = 0,
  { rw h at hx, exact (ennreal.not_lt_zero hx).elim },
  { have h := pos_iff_ne_zero.mpr h,
    exact (has_fpower_series_on_ball_exp_of_radius_pos h).analytic_at_of_mem hx }
end

/-- In a Banach-algebra `𝔸` over a normed field `𝕂` of characteristic zero, if `x` and `y` are
in the disk of convergence and commute, then `exp 𝕂 (x + y) = (exp 𝕂 x) * (exp 𝕂 y)`. -/
lemma exp_add_of_commute_of_mem_ball [char_zero 𝕂]
  {x y : 𝔸} (hxy : commute x y) (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius)
  (hy : y ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
  exp 𝕂 (x + y) = (exp 𝕂 x) * (exp 𝕂 y) :=
begin
  rw [exp_eq_tsum, tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm
        (norm_exp_series_summable_of_mem_ball' x hx) (norm_exp_series_summable_of_mem_ball' y hy)],
  dsimp only,
  conv_lhs {congr, funext, rw [hxy.add_pow' _, finset.smul_sum]},
  refine tsum_congr (λ n, finset.sum_congr rfl $ λ kl hkl, _),
  rw [nsmul_eq_smul_cast 𝕂, smul_smul, smul_mul_smul, ← (finset.nat.mem_antidiagonal.mp hkl),
      nat.cast_add_choose, (finset.nat.mem_antidiagonal.mp hkl)],
  congr' 1,
  have : (n! : 𝕂) ≠ 0 := nat.cast_ne_zero.mpr n.factorial_ne_zero,
  field_simp [this]
end

/-- `exp 𝕂 x` has explicit two-sided inverse `exp 𝕂 (-x)`. -/
noncomputable def invertible_exp_of_mem_ball [char_zero 𝕂] {x : 𝔸}
  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) : invertible (exp 𝕂 x) :=
{ inv_of := exp 𝕂 (-x),
  inv_of_mul_self := begin
    have hnx : -x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius,
    { rw [emetric.mem_ball, ←neg_zero, edist_neg_neg],
      exact hx },
    rw [←exp_add_of_commute_of_mem_ball (commute.neg_left $ commute.refl x) hnx hx, neg_add_self,
      exp_zero],
  end,
  mul_inv_of_self := begin
    have hnx : -x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius,
    { rw [emetric.mem_ball, ←neg_zero, edist_neg_neg],
      exact hx },
    rw [←exp_add_of_commute_of_mem_ball (commute.neg_right $ commute.refl x) hx hnx, add_neg_self,
      exp_zero],
  end }

lemma is_unit_exp_of_mem_ball [char_zero 𝕂] {x : 𝔸}
  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) : is_unit (exp 𝕂 x) :=
@is_unit_of_invertible _ _ _ (invertible_exp_of_mem_ball hx)

lemma inv_of_exp_of_mem_ball [char_zero 𝕂] {x : 𝔸}
  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) [invertible (exp 𝕂 x)] :
  ⅟(exp 𝕂 x) = exp 𝕂 (-x) :=
by { letI := invertible_exp_of_mem_ball hx, convert (rfl : ⅟(exp 𝕂 x) = _) }

/-- Any continuous ring homomorphism commutes with `exp`. -/
lemma map_exp_of_mem_ball {F} [ring_hom_class F 𝔸 𝔹] (f : F) (hf : continuous f) (x : 𝔸)
  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
  f (exp 𝕂 x) = exp 𝕂 (f x) :=
begin
  rw [exp_eq_tsum, exp_eq_tsum],
  refine ((exp_series_summable_of_mem_ball' _ hx).has_sum.map f hf).tsum_eq.symm.trans _,
  dsimp only [function.comp],
  simp_rw [one_div, map_inv_nat_cast_smul f 𝕂 𝕂, map_pow],
end

end complete_algebra

lemma algebra_map_exp_comm_of_mem_ball [complete_space 𝕂] (x : 𝕂)
  (hx : x ∈ emetric.ball (0 : 𝕂) (exp_series 𝕂 𝕂).radius) :
  algebra_map 𝕂 𝔸 (exp 𝕂 x) = exp 𝕂 (algebra_map 𝕂 𝔸 x) :=
map_exp_of_mem_ball _ (algebra_map_clm _ _).continuous _ hx

end any_field_any_algebra

section any_field_division_algebra

variables {𝕂 𝔸 : Type*} [nontrivially_normed_field 𝕂] [normed_division_ring 𝔸] [normed_algebra 𝕂 𝔸]

variables (𝕂)

lemma norm_exp_series_div_summable_of_mem_ball (x : 𝔸)
  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
  summable (λ n, ∥x^n / n!∥) :=
begin
  change summable (norm ∘ _),
  rw ← exp_series_apply_eq_div' x,
  exact norm_exp_series_summable_of_mem_ball x hx
end

lemma exp_series_div_summable_of_mem_ball [complete_space 𝔸] (x : 𝔸)
  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) : summable (λ n, x^n / n!) :=
summable_of_summable_norm (norm_exp_series_div_summable_of_mem_ball 𝕂 x hx)

lemma exp_series_div_has_sum_exp_of_mem_ball [complete_space 𝔸] (x : 𝔸)
  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) : has_sum (λ n, x^n / n!) (exp 𝕂 x) :=
begin
  rw ← exp_series_apply_eq_div' x,
  exact exp_series_has_sum_exp_of_mem_ball x hx
end

variables {𝕂}

lemma exp_neg_of_mem_ball [char_zero 𝕂] [complete_space 𝔸] {x : 𝔸}
  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
  exp 𝕂 (-x) = (exp 𝕂 x)⁻¹ :=
begin
  letI := invertible_exp_of_mem_ball hx,
  exact inv_of_eq_inv (exp 𝕂 x),
end

end any_field_division_algebra

section any_field_comm_algebra

variables {𝕂 𝔸 : Type*} [nontrivially_normed_field 𝕂] [normed_comm_ring 𝔸] [normed_algebra 𝕂 𝔸]
  [complete_space 𝔸]

/-- In a commutative Banach-algebra `𝔸` over a normed field `𝕂` of characteristic zero,
`exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)` for all `x`, `y` in the disk of convergence. -/
lemma exp_add_of_mem_ball [char_zero 𝕂] {x y : 𝔸}
  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius)
  (hy : y ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
  exp 𝕂 (x + y) = (exp 𝕂 x) * (exp 𝕂 y) :=
exp_add_of_commute_of_mem_ball (commute.all x y) hx hy

end any_field_comm_algebra

section is_R_or_C

section any_algebra

variables (𝕂 𝔸 𝔹 : Type*) [is_R_or_C 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸]
variables [normed_ring 𝔹] [normed_algebra 𝕂 𝔹]

/-- In a normed algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`, the series defining the exponential map
has an infinite radius of convergence. -/
lemma exp_series_radius_eq_top : (exp_series 𝕂 𝔸).radius = ∞ :=
begin
  refine (exp_series 𝕂 𝔸).radius_eq_top_of_summable_norm (λ r, _),
  refine summable_of_norm_bounded_eventually _ (real.summable_pow_div_factorial r) _,
  filter_upwards [eventually_cofinite_ne 0] with n hn,
  rw [norm_mul, norm_norm (exp_series 𝕂 𝔸 n), exp_series, norm_smul, norm_inv, norm_pow,
      nnreal.norm_eq, norm_eq_abs, abs_cast_nat, mul_comm, ←mul_assoc, ←div_eq_mul_inv],
  have : ∥continuous_multilinear_map.mk_pi_algebra_fin 𝕂 n 𝔸∥ ≤ 1 :=
    norm_mk_pi_algebra_fin_le_of_pos (nat.pos_of_ne_zero hn),
  exact mul_le_of_le_one_right (div_nonneg (pow_nonneg r.coe_nonneg n) n!.cast_nonneg) this
end

lemma exp_series_radius_pos : 0 < (exp_series 𝕂 𝔸).radius :=
begin
  rw exp_series_radius_eq_top,
  exact with_top.zero_lt_top
end

variables {𝕂 𝔸 𝔹}

lemma norm_exp_series_summable (x : 𝔸) : summable (λ n, ∥exp_series 𝕂 𝔸 n (λ _, x)∥) :=
norm_exp_series_summable_of_mem_ball x ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

lemma norm_exp_series_summable' (x : 𝔸) : summable (λ n, ∥(n!⁻¹ : 𝕂) • x^n∥) :=
norm_exp_series_summable_of_mem_ball' x ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

section complete_algebra

variables [complete_space 𝔸]

lemma exp_series_summable (x : 𝔸) : summable (λ n, exp_series 𝕂 𝔸 n (λ _, x)) :=
summable_of_summable_norm (norm_exp_series_summable x)

lemma exp_series_summable' (x : 𝔸) : summable (λ n, (n!⁻¹ : 𝕂) • x^n) :=
summable_of_summable_norm (norm_exp_series_summable' x)

lemma exp_series_has_sum_exp (x : 𝔸) : has_sum (λ n, exp_series 𝕂 𝔸 n (λ _, x)) (exp 𝕂 x) :=
exp_series_has_sum_exp_of_mem_ball x ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

lemma exp_series_has_sum_exp' (x : 𝔸) : has_sum (λ n, (n!⁻¹ : 𝕂) • x^n) (exp 𝕂 x):=
exp_series_has_sum_exp_of_mem_ball' x ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

lemma exp_has_fpower_series_on_ball :
  has_fpower_series_on_ball (exp 𝕂) (exp_series 𝕂 𝔸) 0 ∞ :=
exp_series_radius_eq_top 𝕂 𝔸 ▸
  has_fpower_series_on_ball_exp_of_radius_pos (exp_series_radius_pos _ _)

lemma exp_has_fpower_series_at_zero :
  has_fpower_series_at (exp 𝕂) (exp_series 𝕂 𝔸) 0 :=
exp_has_fpower_series_on_ball.has_fpower_series_at

lemma exp_continuous : continuous (exp 𝕂 : 𝔸 → 𝔸) :=
begin
  rw [continuous_iff_continuous_on_univ, ← metric.eball_top_eq_univ (0 : 𝔸),
      ← exp_series_radius_eq_top 𝕂 𝔸],
  exact continuous_on_exp
end

lemma exp_analytic (x : 𝔸) :
  analytic_at 𝕂 (exp 𝕂) x :=
analytic_at_exp_of_mem_ball x ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

/-- In a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`, if `x` and `y` commute, then
`exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)`. -/
lemma exp_add_of_commute
  {x y : 𝔸} (hxy : commute x y) :
  exp 𝕂 (x + y) = (exp 𝕂 x) * (exp 𝕂 y) :=
exp_add_of_commute_of_mem_ball hxy ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
  ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

section
variables (𝕂)

/-- `exp 𝕂 x` has explicit two-sided inverse `exp 𝕂 (-x)`. -/
noncomputable def invertible_exp (x : 𝔸) : invertible (exp 𝕂 x) :=
invertible_exp_of_mem_ball $ (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

lemma is_unit_exp (x : 𝔸) : is_unit (exp 𝕂 x) :=
is_unit_exp_of_mem_ball $ (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

lemma inv_of_exp (x : 𝔸) [invertible (exp 𝕂 x)] :
  ⅟(exp 𝕂 x) = exp 𝕂 (-x) :=
inv_of_exp_of_mem_ball $ (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

lemma ring.inverse_exp (x : 𝔸) : ring.inverse (exp 𝕂 x) = exp 𝕂 (-x) :=
begin
  letI := invertible_exp 𝕂 x,
  exact ring.inverse_invertible _,
end

end

/-- In a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`, if a family of elements `f i` mutually
commute then `exp 𝕂 (∑ i, f i) = ∏ i, exp 𝕂 (f i)`. -/
lemma exp_sum_of_commute {ι} (s : finset ι) (f : ι → 𝔸)
  (h : ∀ (i ∈ s) (j ∈ s), commute (f i) (f j)) :
  exp 𝕂 (∑ i in s, f i) = s.noncomm_prod (λ i, exp 𝕂 (f i))
    (λ i hi j hj, (h i hi j hj).exp 𝕂) :=
begin
  classical,
  induction s using finset.induction_on with a s ha ih,
  { simp },
  rw [finset.noncomm_prod_insert_of_not_mem _ _ _ _ ha, finset.sum_insert ha,
      exp_add_of_commute, ih],
  refine commute.sum_right _ _ _ _,
  intros i hi,
  exact h _ (finset.mem_insert_self _ _) _ (finset.mem_insert_of_mem hi),
end

lemma exp_nsmul (n : ℕ) (x : 𝔸) :
  exp 𝕂 (n • x) = exp 𝕂 x ^ n :=
begin
  induction n with n ih,
  { rw [zero_smul, pow_zero, exp_zero], },
  { rw [succ_nsmul, pow_succ, exp_add_of_commute ((commute.refl x).smul_right n), ih] }
end

variables (𝕂)

/-- Any continuous ring homomorphism commutes with `exp`. -/
lemma map_exp {F} [ring_hom_class F 𝔸 𝔹] (f : F) (hf : continuous f) (x : 𝔸) :
  f (exp 𝕂 x) = exp 𝕂 (f x) :=
map_exp_of_mem_ball f hf x $ (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

lemma exp_smul {G} [monoid G] [mul_semiring_action G 𝔸] [has_continuous_const_smul G 𝔸]
  (g : G) (x : 𝔸) :
  exp 𝕂 (g • x) = g • exp 𝕂 x :=
(map_exp 𝕂 (mul_semiring_action.to_ring_hom G 𝔸 g) (continuous_const_smul _) x).symm

lemma exp_units_conj (y : 𝔸ˣ) (x : 𝔸)  :
  exp 𝕂 (y * x * ↑(y⁻¹) : 𝔸) = y * exp 𝕂 x * ↑(y⁻¹) :=
exp_smul _ (conj_act.to_conj_act y) x

lemma exp_units_conj' (y : 𝔸ˣ) (x : 𝔸)  :
  exp 𝕂 (↑(y⁻¹) * x * y) = ↑(y⁻¹) * exp 𝕂 x * y :=
exp_units_conj _ _ _

@[simp] lemma prod.fst_exp [complete_space 𝔹] (x : 𝔸 × 𝔹) : (exp 𝕂 x).fst = exp 𝕂 x.fst :=
map_exp _ (ring_hom.fst 𝔸 𝔹) continuous_fst x

@[simp] lemma prod.snd_exp [complete_space 𝔹] (x : 𝔸 × 𝔹) : (exp 𝕂 x).snd = exp 𝕂 x.snd :=
map_exp _ (ring_hom.snd 𝔸 𝔹) continuous_snd x

@[simp] lemma pi.exp_apply {ι : Type*} {𝔸 : ι → Type*} [fintype ι]
  [Π i, normed_ring (𝔸 i)] [Π i, normed_algebra 𝕂 (𝔸 i)] [Π i, complete_space (𝔸 i)]
  (x : Π i, 𝔸 i) (i : ι) :
  exp 𝕂 x i = exp 𝕂 (x i) :=
begin
  -- Lean struggles to infer this instance due to it wanting `[Π i, semi_normed_ring (𝔸 i)]`
  letI : normed_algebra 𝕂 (Π i, 𝔸 i) := pi.normed_algebra _,
  exact map_exp _ (pi.eval_ring_hom 𝔸 i) (continuous_apply _) x
end

lemma pi.exp_def {ι : Type*} {𝔸 : ι → Type*} [fintype ι]
  [Π i, normed_ring (𝔸 i)] [Π i, normed_algebra 𝕂 (𝔸 i)] [Π i, complete_space (𝔸 i)]
  (x : Π i, 𝔸 i) :
  exp 𝕂 x = λ i, exp 𝕂 (x i) :=
funext $ pi.exp_apply 𝕂 x

lemma function.update_exp {ι : Type*} {𝔸 : ι → Type*} [fintype ι] [decidable_eq ι]
  [Π i, normed_ring (𝔸 i)] [Π i, normed_algebra 𝕂 (𝔸 i)] [Π i, complete_space (𝔸 i)]
  (x : Π i, 𝔸 i) (j : ι) (xj : 𝔸 j) :
  function.update (exp 𝕂 x) j (exp 𝕂 xj) = exp 𝕂 (function.update x j xj) :=
begin
  ext i,
  simp_rw [pi.exp_def],
  exact (function.apply_update (λ i, exp 𝕂) x j xj i).symm,
end

end complete_algebra

lemma algebra_map_exp_comm (x : 𝕂) :
  algebra_map 𝕂 𝔸 (exp 𝕂 x) = exp 𝕂 (algebra_map 𝕂 𝔸 x) :=
algebra_map_exp_comm_of_mem_ball x $
  (exp_series_radius_eq_top 𝕂 𝕂).symm ▸ edist_lt_top _ _

end any_algebra

section division_algebra

variables {𝕂 𝔸 : Type*} [is_R_or_C 𝕂] [normed_division_ring 𝔸] [normed_algebra 𝕂 𝔸]

variables (𝕂)

lemma norm_exp_series_div_summable (x : 𝔸) : summable (λ n, ∥x^n / n!∥) :=
norm_exp_series_div_summable_of_mem_ball 𝕂 x
  ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

variables [complete_space 𝔸]

lemma exp_series_div_summable (x : 𝔸) : summable (λ n, x^n / n!) :=
summable_of_summable_norm (norm_exp_series_div_summable 𝕂 x)

lemma exp_series_div_has_sum_exp (x : 𝔸) : has_sum (λ n, x^n / n!) (exp 𝕂 x):=
exp_series_div_has_sum_exp_of_mem_ball 𝕂 x
  ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

variables {𝕂}

lemma exp_neg (x : 𝔸) : exp 𝕂 (-x) = (exp 𝕂 x)⁻¹ :=
exp_neg_of_mem_ball $ (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _

lemma exp_zsmul (z : ℤ) (x : 𝔸) : exp 𝕂 (z • x) = (exp 𝕂 x) ^ z :=
begin
  obtain ⟨n, rfl | rfl⟩ := z.eq_coe_or_neg,
  { rw [zpow_coe_nat, coe_nat_zsmul, exp_nsmul] },
  { rw [zpow_neg, zpow_coe_nat, neg_smul, exp_neg, coe_nat_zsmul, exp_nsmul] },
end

lemma exp_conj (y : 𝔸) (x : 𝔸) (hy : y ≠ 0) :
  exp 𝕂 (y * x * y⁻¹) = y * exp 𝕂 x * y⁻¹ :=
exp_units_conj _ (units.mk0 y hy) x

lemma exp_conj' (y : 𝔸) (x : 𝔸)  (hy : y ≠ 0) :
  exp 𝕂 (y⁻¹ * x * y) = y⁻¹ * exp 𝕂 x * y :=
exp_units_conj' _ (units.mk0 y hy) x

end division_algebra

section comm_algebra

variables {𝕂 𝔸 : Type*} [is_R_or_C 𝕂] [normed_comm_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸]

/-- In a commutative Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`,
`exp 𝕂 (x+y) = (exp 𝕂 x) * (exp 𝕂 y)`. -/
lemma exp_add {x y : 𝔸} : exp 𝕂 (x + y) = (exp 𝕂 x) * (exp 𝕂 y) :=
exp_add_of_mem_ball ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
  ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)

/-- A version of `exp_sum_of_commute` for a commutative Banach-algebra. -/
lemma exp_sum {ι} (s : finset ι) (f : ι → 𝔸) :
  exp 𝕂 (∑ i in s, f i) = ∏ i in s, exp 𝕂 (f i) :=
begin
  rw [exp_sum_of_commute, finset.noncomm_prod_eq_prod],
  exact λ i hi j hj, commute.all _ _,
end

end comm_algebra

end is_R_or_C

end normed

section scalar_tower

variables (𝕂 𝕂' 𝔸 : Type*) [field 𝕂] [field 𝕂'] [ring 𝔸] [algebra 𝕂 𝔸] [algebra 𝕂' 𝔸]
  [topological_space 𝔸] [topological_ring 𝔸]

/-- If a normed ring `𝔸` is a normed algebra over two fields, then they define the same
`exp_series` on `𝔸`. -/
lemma exp_series_eq_exp_series (n : ℕ) (x : 𝔸) :
  (exp_series 𝕂 𝔸 n (λ _, x)) = (exp_series 𝕂' 𝔸 n (λ _, x)) :=
by rw [exp_series_apply_eq, exp_series_apply_eq, inv_nat_cast_smul_eq 𝕂 𝕂']

/-- If a normed ring `𝔸` is a normed algebra over two fields, then they define the same
exponential function on `𝔸`. -/
lemma exp_eq_exp : (exp 𝕂 : 𝔸 → 𝔸) = exp 𝕂' :=
begin
  ext,
  rw [exp, exp],
  refine tsum_congr (λ n, _),
  rw exp_series_eq_exp_series 𝕂 𝕂' 𝔸 n x
end

lemma exp_ℝ_ℂ_eq_exp_ℂ_ℂ : (exp ℝ : ℂ → ℂ) = exp ℂ :=
exp_eq_exp ℝ ℂ ℂ

end scalar_tower

subset_name: curated


TITLE: Why do bubbles group when one pops?
QUESTION [1 upvotes]: I was recently observing the way bubbles move as they pop and disappear. I noticed that when bubbles destabilize and pop, the remaining bubbles immediately surrounding it will move to fill its place. I was wondering what the driving cause is here.
At first, I figured that stickiness was the cause. But, I don't think this would be a driving force unless perhaps the bubbles are clustered (i.e. they share at least 1 membrane).
I've also noticed this behavior in groups of individual, non-clustered bubbles. As an introductory physics student, I'm curious: what causes this phenomenon?

REPLY [1 votes]: The blubbles exerce pressure forces with their neighboor through the shared membranes. Pressure is higher in blubbles than in free air, when within a field of bubbles it is balanced on each sides of bubble wall... as long as there is a neighbor. When this one pops, the rest of the pack around push towards the empty space.

REPLY [0 votes]: The Nature is Smart; it prefers the state with the lowest energy (maximum entropy) in different manifestations.(surface tension in this case). Please refer to this link already answered. (Why does the nature always prefer low energy and maximum entropy?)