More gitignore

.gitignore

@@ -1,6 +1,10 @@
 /.lake
-*.out
-*.log
 *.aux
+*.fdb_latexmk
+*.fls
+*.log
 *.gz
-*.toc
+*.out
+*.synctex(busy)
+*.synctex.gz
+*.toc

Paper/macrosetup.tex

@@ -30,6 +30,7 @@
 \newcommand{\FF}{\mathbb{F}}
 \newcommand{\catname}[1]{{\normalfont\textbf{#1}}}
 \newcommand{\C}{\catname{C}}
+\newcommand{\Vect}{\catname{Vect}}
 \newcommand{\catob}[2]{#1 \in \Ob(\catname{#2})}
 \newcommand{\pers}{\catname{Vect}^{(\R, \leq)}}
 \newcommand{\persn}{\catname{Vect}^{(\N, \leq)}}

Paper/sections.tex

@@ -177,3 +177,25 @@ \section{Botnan and Crawley-Boevey}
 A similar condition must hold for any morphism $\alpha : x \rightarrow z \in \mathcal{C}$. In particular, this seems to me like it could yield a set of conditions of the form $n_x \geq m, \forall m \in \N$ in which case the proof no longer works.
 
 
+\section{Simplifying the Botnan and Crawley-Boevey argument}
+
+Let $K$ be a field and $\C$ be a category.
+
+\begin{lem}\label{lem:refinement-finite-height}
+  Let $M$ be a finite dimensional $K$-vector space. Then the refinement order of direct sum decompositions of $M$ has finite height. Precisely,
+  $$\mathrm{height}(\mathrm{DirectSumDecomposition_K(M)}) \le \dim_K(M) - 1$$
+\end{lem}
+\begin{proof}
+  sorry
+\end{proof}
+
+\begin{prop}
+  Let $M$ be a functor $\C \to \Vect$ and $T$ be a chain of direct sum decomposition of $M$. Then $T$ has an upper bound.
+\end{prop}
+\begin{proof}
+  For all $c : \C$, the chain
+  $$T_c := \{t_c | t \in T\}$$
+  is a chain in the refinement order of direct sum decompositions of $M_c$, which has finite height by Lemma \ref{lem:refinement-finite-height}. $T_c$ therefore has a maximal element $u_c$.
+
+  Let's now prove that $u$ is a direct sum decomposition of $M$. All we need to check is that 
+\end{proof}

Paper/theoremsetup.tex

@@ -8,6 +8,7 @@
 \newtheorem*{thm*}{Theorem}
 \newtheorem{cor}{Corollary}
 \newtheorem{lem}{Lemma}
+\newtheorem{prop}{Proposition}
 \newtheorem{deff}{Definition}
 \newtheorem{ex}{Example}
 \theoremstyle{remark}