# 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}$) ?

• I like this question, but it presupposes that we know what the internal logic of an abelian category is. It'll have conjunction and existential quantification (as you noted), but it should have more, since abelian categories are much nicer than just regular. I don't think you'll have genuine disjunction, but instead of $\phi(x)\lor\psi(x)$ you might have something like "$x$ is a sum $y+z$ with $\phi(y)$ and $\psi(z)$." Has this been worked out? (I think the modular law for $\land$ and this pseudo-$\lor$ should hold, though the distributive law shouldn't.) – Andreas Blass May 18 '18 at 1:14
• @AndreasBlass : indeed; but wouldn't it be enough to have an "interesting" 'lower bound' on the logic in question ? If we can do the proof of the five lemma in regular logic and "transport" this in a way, we'd have our five lemma, right ? – Max May 18 '18 at 6:02
• Actually there is another way to prove statements which is somewhere in between internal languages/logic and ordinary category theory, namely generalized elements which allows to prove results in a point-style way using the language if category theory. If you are interested in this I could try to add something. – Giorgio Mossa May 18 '18 at 9:04
• @GiorgioMossa : I am interested indeed ! (I am aware of generalized-elements-type reasoning, but I don't see for instance how it can help when building a connecting morphism, or proving epi-ness for instance, so I would be interested !) – Max May 18 '18 at 9:26
• @Max See this and this for some elaboration and references to Giorgio Mossa's statement in the specific case of abelian categories. – Derek Elkins May 18 '18 at 20:33

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.

• Thank you for your answer ! It'll surely give me a lot to think about – Max May 23 '18 at 17:48

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.

• Please if you need any additional detail or find some part obscure write me in the comments. – Giorgio Mossa May 20 '18 at 11:12
• I'm not yet available and can't really read your answer though I appreciate the effort, I wille read it and get back to you as soon as possible ! – Max May 20 '18 at 14:41
• @MaxMa no problem, unfortunately I couldn't find any way to shorten the answer. – Giorgio Mossa May 20 '18 at 15:24
• Thank you so much for this answer ! It really helps, and it actually gave me a knew way of looking at the Yoneda lemma, so that's great. "Unfortunately", Derek Elkins's answer adresses the question more directly (though yours answers my request from the comments) and so I'll probably accept his over yours – Max May 23 '18 at 17:47
• I'm glad my answer was helpful, and most importantly I absolutely agree Derek Elkins'answer actually address your question. Mine was just a very looong comment. ;-) – Giorgio Mossa May 23 '18 at 20:42

While Andreas raises a very interesting question in the comments, to which I don't know the answer, except to agree that disjunction doesn't work normally in abelian categories since they're not coherent, the restriction to regular logic presents no problems.

For example, given $f:B\to C$, the proposition $f(x)=0$ is simply interpreted as the subobject of $B$ given by all $x$ such that $f(x)=0$. Similarly, $g(y)=x$ is the appropriate subobject of $A\oplus B$, while $\exists y:g(y)=x$ is its image in $B$, which is precisely the image of $g$. Exactness is the assumption that these subobjects are contained in each other, which is how we interpret entailment of propositions.

We can actually prove that this kind of thing will always work using Mitchell's embedding theorem. The embedding is exact and fully faithful, so it preserves and reflects statements of regular logic, and the categorical interpretation of logical statements in a module category is, of course, just the classical interpretation. So any regular statement you can prove in a module category will be true in the internal logic in any abelian category.

• Ok but can such regular reasoning be used to build morphisms ? – Max May 18 '18 at 9:28