Can we use the internal logic of a category to do diagram chases "as in $\mathbf{Ab}$" ?

Disclaimer: I'm not yet really comfortable with internal logics, though I know the basics, so the best answer would not be the most technical one.

Suppose you want to prove a diagram lemma (say the snake lemma for instance) in an arbitrary abelian category. As many authors show, one can do this in a purely "categorical way", obviously elements-free. I believe there's a proof in McLane for instance.

You can also use Mitchell's embedding theorem: as the diagram is a small one, the abelian category generated by it is small as well (it can be built in $\omega$ steps), and one can then fully, faithfully, exactly embed it in a category of $R$-modules for some module $R$ , and use the lemma in question in this category (to get the connecting morphism for instance, in the snake lemma), and then go back up to your category, and the properties of the embedding imply what you want.

Of course in categories of $R$-modules, you're allowed to reason like "let $x$ be such that $f(x)=0$. Then $x\in Ker(f)= Im(g)$ so there is $y$ such that blabla", which makes the proofs (usually) somewhat easier.

My question is whether one can use the internal logic of the category to reason exactly as in the $R$-module case, as long as we don't go beyond the logic that we have at hand. For instance, regular logic has an existential quantifier, and so perhaps $f(x)=0\vdash_x \exists y, g(y) = x$ is valid in an abelian category where we have an exact sequence $A\to B \to C$ (that's one part I'm unsure about) and perhaps we could reason as usual (though with a "restricted" logic) to prove some results about arbitrary abelian categories. Is it the case ? Is there a way to use the internal logic to build the connecting morphism in the snake lemma for instance ?

For another example: can we prove, using internal logic, that in the five-lemma, the middle morphism is "injective" ($f(x)=f(y)\vdash_{x,y} x=y$) and "surjective" ($\vdash_{y} \exists x, f(x)=y$) and somehow that would imply that it's both mono and epi, and thus (in an abelian category) iso ? (I'm not typing the sequents, though of course I should)

So to sum up,

Is there a way in which reasoning with the internal logic of an abelian category can help us prove things (such as diagram lemmas) in those, much like we do in the "ordinary ones" (i.e. $R-\mathbf{Mod}, \mathbf{Ab}$) ?

Solution 1:

This MathOverflow question and answer and the referenced slides and the comments both by Ingo Blechschmidt seem directly aimed at your question. See also the nLab page on diagram chasing whose section on diagram chasing in abelian categories addresses the approach you are considering. What you are suggesting is the fourth approach. For your purposes, you may want to look at the other approaches mentioned as well, such as the two element in an abelian category approaches.

As far as I can tell from the above, the "obvious" approach works. Basically, an abelian category is a regular category, so you can definitely interpret regular logic. You can then assert the existence of an abelian group structure for every sort/type, i.e. $\cfrac{\Gamma\vdash t_1:B\qquad \Gamma\vdash t_2:B}{\Gamma\vdash t_1+t_2 : B}$ and so forth. The mentioned "axiom of unique choice", true in any lex category, states that morphisms are equivalent to total functional relations in the internal logic. With the caveat of requiring constructive logic, you can use ordinary element-wise reasoning in this language and the results will be true in any abelian category.

Starting with a regular logic and then asserting every sort has an abelian group structure, should essentially give you the internal language of a regular additive category. However, an abelian category is precisely an exact additive category. Regular categories and exact categories are intimately related. A regular category says all congruences of the form $\Gamma,x:A,y:A\vdash f(x)=f(y)$ for any morphism $f$ have quotients, i.e. coequalizers of the two components of $\{\langle x,y\rangle\in A\times A\mid f(x)=f(y)\}\rightarrowtail A\times A$. This is exactly the image of $f$. An exact category states that every congruence is of the above form for some $f$. (In particular, for the quotient map $q:A\to A/{\sim}$.)

I'm just making this up and patching things together, so take this all with a large grain of salt, but combining the presentation of a regular type theory with effective quotients in Maria Maietti's Modular correspondence between dependent type theories and categories including pretopoi and topoi should give a characterization of exactness. Then adding the additive group structure should give a type theory compatible with abelian categories. I adapt Maietti's presentation notationally. I'll use $\Gamma\vdash T\ \mathsf{prop}$ to mean $\Gamma\vdash T\ \mathsf{type}$ and $\Gamma,x:T,y:T\vdash x=y:T$, i.e. that $T$ is a mono type. Terms of mono types correspond to subobjects. As another shorthand, I'll write $\Gamma\vdash T$ when $T$ is a monotype to mean $\Gamma\vdash c:T$ where $c$ is any term of type $T$ in scope (which are necessarily all equal). I'm omitting the usual structural rules and the rules for equality.

Terminal object: $$\cfrac{}{\Gamma\vdash\top\ \mathsf{type}}\top F\qquad\cfrac{}{\Gamma\vdash\star:\top}\top I \qquad\cfrac{\Gamma\vdash t:\top}{\Gamma\vdash t = \star:\top}\top\beta$$

Dependent sum (and thus finite products): $$\cfrac{\Gamma,x:B\vdash C(x)\ \mathsf{type}}{\Gamma\vdash\Sigma x:B.C(x)\ \mathsf{type}}\Sigma F\qquad\cfrac{\Gamma\vdash b:B\qquad\Gamma\vdash c:C(b)\qquad\Sigma x:B.C(x)\ \mathsf{type}}{\Gamma\vdash\langle b,c\rangle:\Sigma x:B.C(x)}\Sigma I$$

$$\cfrac{\Gamma,z:\Sigma x:B.C(x)\vdash M(z)\ \mathsf{type}\qquad \Gamma\vdash d:\Sigma x:B.C(x)\qquad\Gamma,x:B,y:C(x)\vdash m(x,y):M(\langle x,y\rangle)}{\Gamma\vdash\mathsf{elim}_\Sigma(d,x,y.m(x,y)):M(d)}\Sigma E$$

$$\cfrac{\Gamma,z:\Sigma x:B.C(x)\vdash M(z)\ \mathsf{type}\qquad \Gamma\vdash b:B\qquad \Gamma\vdash c:C(b)\qquad\Gamma,x:B,y:C(x)\vdash m(x,y):M(\langle x,y\rangle)}{\Gamma\vdash\mathsf{elim}_\Sigma(\langle b,c\rangle, x,y.m(x,y))=m(b,c):M(\langle b,c\rangle)}\Sigma\beta$$

Extensional equality type (and thus pullbacks given the dependent sum): $$\cfrac{\Gamma\vdash C\ \mathsf{type}\qquad\Gamma\vdash c:C\qquad\Gamma\vdash d:C}{\Gamma\vdash\mathsf{Eq}(C,c,d)\ \mathsf{type}}\mathsf{Eq}F\qquad\cfrac{\Gamma\vdash c:C}{\Gamma\vdash\mathsf{refl}_C(c):\mathsf{Eq}(C,c,c)}\mathsf{Eq}I$$

$$\cfrac{\Gamma\vdash p:\mathsf{Eq}(C,c,d)}{\Gamma\vdash c=d:C}\mathsf{Eq}E\qquad\cfrac{\Gamma\vdash p:\mathsf{Eq}(C,c,d)}{\Gamma\vdash p=\mathsf{refl}_C(c):\mathsf{Eq}(C,c,d)}\mathsf{Eq}\beta$$

Existential type (which can actually be defined as $(\Sigma x:B.C(x))/\top$): $$\cfrac{\Gamma,x:B\vdash C(x)\ \mathsf{prop}}{\Gamma\vdash\exists x:B.C(x)\ \mathsf{type}}\exists F\qquad\cfrac{\Gamma\vdash b:B\qquad\Gamma\vdash c:C(b)\qquad\Gamma\vdash\exists x:B.C(x)\ \mathsf{type}}{\Gamma\vdash(b,c):\exists x:B.C(x)}\exists I$$

$$\cfrac{\Gamma\vdash\exists x:B.C(x)\ \mathsf{type}\qquad\Gamma\vdash b:B\qquad\Gamma\vdash c:C(b)\qquad\Gamma\vdash d:B\qquad\Gamma\vdash t:C(d)}{\Gamma\vdash(b,c)=(d,t):\exists x:B.C(x)}\exists{=}$$

$$\cfrac{\Gamma,z:\exists x:B.C(x)\vdash M(z)\ \mathsf{prop}\qquad\Gamma\vdash d:\exists x:B.C(x)\qquad\Gamma,x:B,y:C(x)\vdash m(x,y):M((x,y))}{\Gamma\vdash\mathsf{elim}_\exists(d,x,y.m(x,y)):M(d)}\exists E$$

Effective extensional quotient types: $$\cfrac{\Gamma,x:A,y:A\vdash R(x,y)\ \mathsf{prop}\qquad\Gamma,x:A\vdash R(x,x)\qquad\Gamma,x:A,y:A,p:R(x,y)\vdash R(y,x)\qquad\Gamma,x:A,y:A,z:A,p:R(x,y),q:R(y,z)\vdash R(x,z)}{\Gamma\vdash A/R\ \mathsf{type}}QF$$

$$\cfrac{\Gamma\vdash a:A\qquad\Gamma\vdash A/R\ \mathsf{type}}{\Gamma\vdash[a]:A/R}QI\qquad\cfrac{\Gamma\vdash a:A\qquad\Gamma\vdash b:A\qquad\Gamma\vdash A/R\ \mathsf{type}}{\Gamma\vdash [a]=[b]:A/R}Q{=}$$

$$\cfrac{\Gamma,z:A/R\vdash L(z)\ \mathsf{type}\qquad\Gamma\vdash p:A/R\qquad\Gamma,x:A\vdash l(x):L([x])\qquad\Gamma,x:A,y:A,d:R(x,y)\vdash l(x)=l(y):L([x])}{\Gamma\vdash\mathsf{elim}_Q(p, x.l(x)):L(p)}QE$$

$$\cfrac{\Gamma,z:A/R\vdash L(z)\ \mathsf{type}\qquad\Gamma\vdash a:A\qquad\Gamma,x:A\vdash l(x):L([x])\qquad\Gamma,x:A,y:A,d:R(x,y)\vdash l(x)=l(y):L([x])}{\Gamma\vdash\mathsf{elim}_Q([a], x.l(x))=l(a):L([a])}Q\beta$$

$$\cfrac{\Gamma\vdash a:A\qquad\Gamma\vdash b:A\qquad\Gamma\vdash [a]=[b]:A/R}{\Gamma\vdash\mathsf{eff}(a,b):R(a,b)}\mathsf{Eff}$$

Additive structure: $$\cfrac{\vdash A\ \mathsf{type}}{\Gamma\vdash 0_A:A}0I\qquad\cfrac{\vdash A\ \mathsf{type}\qquad\Gamma\vdash a:A\qquad\Gamma\vdash b:A}{\Gamma\vdash a+b:A}{+}I\qquad\cfrac{\vdash A\ \mathsf{type}\qquad\Gamma\vdash a:A}{\Gamma\vdash -a:A}{-}I$$

$$\cfrac{\vdash A\ \mathsf{type}\qquad\Gamma\vdash a:A\qquad\Gamma\vdash b:A}{\Gamma\vdash a+b=b+a:A}{+}\sigma\qquad\cfrac{\vdash A\ \mathsf{type}\qquad\Gamma\vdash a:A}{\Gamma\vdash 0+a=a:A}{+}\lambda$$

$$\cfrac{\vdash A\ \mathsf{type}\qquad\Gamma\vdash a:A\qquad\Gamma\vdash b:A\qquad\Gamma\vdash c:A}{\Gamma\vdash (a+b)+c=a+(b+c):A}{+}\alpha\qquad\cfrac{\vdash A\ \mathsf{type}\qquad\Gamma\vdash a:A}{\Gamma\vdash a+(-a)=0_A:A}{+}i$$

$$\cfrac{\vdash A\ \mathsf{type}\qquad\vdash B\ \mathsf{type}\qquad x:A\vdash t:B}{\Gamma\vdash t[0_A/x]=0_B:B}0c$$

$$\cfrac{\vdash A \ \mathsf{type}\qquad\vdash B\ \mathsf{type}\qquad\Gamma\vdash a:A\qquad\Gamma\vdash b:A\qquad x:A\vdash t:B}{\Gamma\vdash t[a+b/x]=t[a/x]+t[b/x]:B}{+}c$$

It is not the case that $\top$ and $A\times B(=\Sigma x:A.B)$ correspond to a void/empty/false/$\bot$ type and coproduct type respectively, because initial objects and coproducts in abelian categories are not stable, i.e. preserved by pullback functors. What we can show is that they do behave like void types and coproduct types if we only consider closed types, i.e. the types that correspond to objects of the abelian category rather than objects in a fiber category. All the additive structure is restricted to terms of closed types.

Let $\vdash A\ \mathsf{type}$, $\vdash B\ \mathsf{type}$, and $\vdash C\ \mathsf{type}$, i.e $A$, $B$, and $C$ are closed types, from this point on. Let's show that $\top$ is initial. Clearly, $x:\top\vdash 0_A:A$ shows that there exists an arrow from $\top$ to any (closed) $A$. To show uniqueness, consider a term $x:\top\vdash t(x):A$. Since $x=\star:\top$ via $\top\beta$, this term is the same as $x:\top\vdash t(\star):A$ and so we have $t(x)=t(\star)=t[t'/x]$ for any $t':\top$. In particular, for $t'=0_\top$ we get $t(x)=t[0_\top/x]=0_A$ via $0c$. (Really, we could replace the rule $0c$ with the rule $\frac{\vdash t:A}{\Gamma\vdash t=0_A:A}$ which is to say the only constant term is zero which makes sense as the only constant abelian group homomorphism is the zero morphism.) Next, write $A\oplus B$ for $A\times B$. Define $\mathsf{inl}(a)$ as $\langle a,0_B\rangle$ and $\mathsf{inr}(b)$ as $\langle 0_A,b\rangle$. Define $\mathsf{elim}_\oplus(t,x.f(x),y.g(y))$ as $\mathsf{elim}_\Sigma(t, x,y.f(x)+g(y))$ where $\Gamma\vdash t:A\oplus B$, $\Gamma,x:A\vdash f(x):C$, and $\Gamma,y:B\vdash g(y):C$. It's easy to show that this satisfies the universal property of the coproduct.

The kernel of $\Gamma,x:A\vdash f(x):B$ is $\Sigma x:A.\mathsf{Eq}(B,f(x),0_B)$. The image is $A/R$ where $R(x,y)$ is defined as $\mathsf{Eq}(B,f(x),f(y))$. The cokernel is $B/R$ where $R(x,y)$ is defined as $\exists a:A.\mathsf{Eq}(B,f(a),x-y)$. The coimage is $A/R$ where $R(x,y)$ is defined as $\exists a:A.\mathsf{Eq}(B,f(a),0_B)\times\mathsf{Eq}(A,a,x-y)$. Showing that the image is isomorphic to the kernel of the cokernel using this language is a good exercise. Similarly for the coimage and the cokernel of the kernel. From here it is fairly obvious that the coimage is isomorphic to the image. Either direction is just $\mathsf{elim}_Q(z,x.[x])$ whose well-formedness in both directions just requires $(\exists a:A.f(a)=0\land a = x-y)\iff (f(x)=f(y))$ which clearly holds.

Solution 2:

Since the OP asked for it I will give a sort description of a method for proving the existence of the connecting morphism in the snake lemma, this method will use generalized elements to transport almost verbatim the tradional proof for categories of modules.

In this proof I will follow the diagrams in this pdf (I preferred to use a single pdf instead of putting lots of images, I apologize for the inconvenience). $\DeclareMathOperator{\Ker}{Ker} \DeclareMathOperator{\Coker}{Coker} \DeclareMathOperator{\coker}{coker}$

So assume we have a situation as depicted in diagram (1) in the pdf.

We want to build a morphism from $\Ker \gamma$ into $\Coker \alpha$. The guiding idea to provide such morphism is that a morphism is the same as a natural transformation between the associated presheaves (by Yoneda): so to provide a morphism between two objects $X$ and $Y$ one could provide a family of bijections $\hom[U,X] \to \hom[U,Y]$ natural in $U$.

Using this guiding principle we try to find a function that associates to every generalized element of $\Ker \gamma$, i.e. a morphism $x \colon U \to \Ker \gamma$, a generalized element of $\Coker \alpha$ with the same domain, i.e. a morphism $\delta x \colon U \to \Coker \alpha$.

This function is basically an arrow-version of the mapping provided in the module-proof: in the case of modules the connecting map $\delta$

• picks an $x \in \Ker \gamma$,
• pulls it back through the epimorphism $g$,
• sends in down through $\beta$,
• pulls back again along $f'$
• (finally) pushs it down via $\coker \alpha$.

We will do something similar.

• We start by picking a generalized element $x \colon U \to \Ker \gamma$

• We pull back $(\ker \gamma) \circ x$ along $g$, thus obtaining the generalized element $\bar x \colon P \to B$ and an epimorphism $\pi \colon P \to U$ (by a theorem, in abelian categories pullbacks preserve epimorphisms). The square $(\bar x,\bar g,g,\ker \gamma \circ x)$ is a pullback square (as depicted in the diagram (3)).

• Then we can push down ${\bar x}$ along $\beta$ getting $\beta \circ \bar x$.

By diagram chasing one can easily see that $g' \circ \beta \circ \bar x$ is equal to the null map, hence $\beta \circ \bar x$ factors through the kernel of $g'$, which by the exactness of the lower row is $f'$.

• In this way we get a unique (generalized) element $\bar{\bar x} \colon P \to A'$, as shown in diagram (4), which is the unique morphism that can be obtained by pulling back $\beta \circ \bar x$ along $f$, i.e. the unique morphism such that $f \circ \bar{\bar x}=\beta \circ \bar x$.

• By composition with $\coker \alpha$ we get a generalized element $\coker \alpha \circ \bar{\bar x} \colon P \to \Coker \alpha$.

The problem is that $\coker\alpha \circ \bar{\bar x}$ has domain $P$ while we need a generalized element with domain $U$.

To solve this problem we just need to show that $\coker \alpha \circ \bar {\bar x}$ factors through the epimorphism $\bar g$.

We do this by showing that $\coker \alpha \circ \bar{\bar x} \circ \ker \bar g$ is a null morphism, this implies that $\coker \alpha \circ \bar{\bar x}$ factors through the coker of $\ker \bar g$, which is $\bar g$ by abstract-nonsense.

In diagram (5) we consider have a unique $\bar x$ which makes commute the square (this comes from abstract nonsense) so we have the equality $$f \circ \bar x' = \bar x \circ \ker \bar g\ .$$

From this last equality, by diagram chasing, it follows that $$\bar{\bar x} \circ \ker \bar g = \alpha \circ \bar x'$$ hence that $$\coker \alpha \circ \bar{\bar x} \circ \ker \bar g = 0$$ as we wanted.

From this it follows, as said before, that $\coker \alpha \circ \bar{\bar x}$ factors through $\bar g$, i.e. that there is a generalized element (which is uniquely determined by universal properties) $\delta x \colon U \to \Coker \alpha$ such that $$\coker \alpha \circ \bar{\bar x}=\delta x \circ \bar g\ .$$

Summarizing we basically have build a function $\delta \colon \hom[U,\Ker \gamma] \to \hom[U,\Coker \alpha]$ (which maps generalized elements by the same pulling-pushing game that is used in the module-version with some adjustments).

From this one could proceed by showing the naturality of the functions in $U$, but since we are interested just in the morphism $\delta \colon \ker \gamma \to \Coker \alpha$ (again using yoneda under the hood) we can simply observe that by letting $U=\Ker \gamma$ and $x=\text{id}_{\Ker \gamma}$ the morphism $\delta \text{id} \colon Ker \gamma \to \Coker \alpha$ gives exactly the required morphism.

Some comments: I want to strees that the complications found in order to obtain the morphism $\delta x$ from $\coker \alpha \circ \bar{\bar x}$ are the arrow-version of the well-definition problem that one encounters while defining the connection-morphism $\delta$ in the module case.

I hope this example can give an hint of the power of the use of generalized elements in .... generalizing proofs from the classical set-based cases.