PropositionsForAbelianCategories.tex

%\begin{sequent}
%\begin{align*}
%  \alpha:\Mor~|~ &() \\
%  \vdash &\IsIsomorphism\big( \KernelLift( \\
%  &\CokernelProjection( \alpha ), \CokernelColift( \KernelEmbedding( \alpha ), \alpha ))\big)
%\end{align*}
%\end{sequent}

%\begin{sequent}
%\begin{align*}
%  \alpha:\Mor~|~ &() \\
%  \vdash &\IsIsomorphism\big( \CokernelColift( \\
%  &\KernelEmbedding( \alpha ), \KernelLift( \CokernelProjection( \alpha ), \alpha ))\big)
%\end{align*}
%\end{sequent}

\begin{sequent}
\begin{align*}
  \alpha:\Mor~|~ & \IsEpimorphism\big( \alpha \big) \\
  \vdash &\IsIsomorphism\big( \ImageEmbedding( \alpha ) \big)
\end{align*}
\end{sequent}

\begin{sequent}
\begin{align*}
  \alpha:\Mor~|~ & \IsIsomorphism\big( \ImageEmbedding( \alpha ) \big) \\
  \vdash &\IsEpimorphism\big( \alpha \big)
\end{align*}
\end{sequent}

\begin{sequent}
\begin{align*}
  \alpha:\Mor~|~ & \IsEpimorphism\big( \alpha \big) \\
  \vdash &\IsIsomorphism\big( \AstrictionToCoimage( \alpha ) \big)
\end{align*}
\end{sequent}

\begin{sequent}
\begin{align*}
  \alpha:\Mor~|~ & \IsIsomorphism\big( \AstrictionToCoimage( \alpha ) \big) \\
  \vdash &\IsEpimorphism\big( \alpha \big)
\end{align*}
\end{sequent}

\begin{sequent}
\begin{align*}
  \alpha:\Mor~|~ & \IsMonomorphism\big( \alpha \big) \\
  \vdash &\IsIsomorphism\big( \CoimageProjection( \alpha ) \big)
\end{align*}
\end{sequent}

\begin{sequent}
\begin{align*}
  \alpha:\Mor~|~ & \IsIsomorphism\big( \CoimageProjection( \alpha ) \big) \\
  \vdash &\IsMonomorphism\big( \alpha \big)
\end{align*}
\end{sequent}

\begin{sequent}
\begin{align*}
  \alpha:\Mor~|~ & \IsMonomorphism\big( \alpha \big) \\
  \vdash &\IsIsomorphism\big( \CoastrictionToImage( \alpha ) \big)
\end{align*}
\end{sequent}

\begin{sequent}
\begin{align*}
  \alpha:\Mor~|~ & \IsIsomorphism\big( \CoastrictionToImage( \alpha ) \big) \\
  \vdash &\IsMonomorphism\big( \alpha \big)
\end{align*}
\end{sequent}