10
$\begingroup$

While studying topos theory I was wondering if there is something like internal logic of an abelian category. Aparently the answer is yes (by 7º slide in https://www.mimuw.edu.pl/~gael/xxi/files/slides_posters/Blechschmidt.pdf) but I can't see what this weaker variant could be.

Besides that, is there relations between this internal logic and the internal logic of a topos? This relations would be interesting for topos theory? Maybe for homological algebra?

Is there more relations between homological algebra and topos theory beyond Chapther 8 (Cohomology) of "Topos Theory" Johnstone's book? I know that SGA4 is a reference in this topic to.

It's my first time making a question here, sorry for any mistake and thanks in advance

Improve this question
$\endgroup$
1
  • $\begingroup$ You might find some material of interest in the book "Model theory and modules" and other work by Mike Prest. $\endgroup$
    – Neil Strickland
    Commented Apr 25, 2018 at 8:17

1 Answer 1

Reset to default
10
$\begingroup$

I don't know exactly what Blechschmidt had in mind, but an abelian category is in particular a regular category (indeed, a Barr-exact category), and hence it has an internal logic that is a regular logic, having $\exists,\wedge,\top$ but no other connectives (except "$\forall$ and $\Rightarrow$ at top-level" in the sense of an entailment). This regular logic doesn't include the "additiveness" of an abelian category, but you could augment it by axioms making every object an abelian group object and every morphism an abelian group homomorphism.

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ This is exactly what I had in mind, including the augmentation by additional axioms. :-) This approach is to carry element-based proofs by diagram chasing over to general abelian categories. Unlike Freyd–Mitchell's embedding theorem, it works for arbitrary abelian categories (not necessarily small ones, though this obstacle can be removed using set-theoretical reflection principles); unlike the "generalized elements" of Gelfand/Manin, it can also be used to construct morphisms (instead of only verifying properties of already given morphisms); $\endgroup$
    – Ingo Blechschmidt
    Commented Apr 25, 2018 at 19:23
  • 2
    $\begingroup$ "verifying linearity" is never necessary, showing that "for all $x$, there exists a unique $y$ such that ..." suffices; unlike the genuine generalized elements of Bergman, the "stage of definition" is automatically kept track of. This nLab entry lists all the techniques for performing diagram chases in abelian categories I personally know of. $\endgroup$
    – Ingo Blechschmidt
    Commented Apr 25, 2018 at 19:23
  • $\begingroup$ Thanks for both of you! That gives some directions, now I have some idea about the next step. $\endgroup$
    – Ana T
    Commented Apr 25, 2018 at 22:02

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .