diagram chasing in abelian categories

Stream: maths

[Kevin Buzzard]

Someone pointed me to this talk about "constructive category theory" which made me wonder whether we could use such tricks to do e.g. snake lemma in a general abelian category via these "generalised morphisms".

[Adam Topaz]

I don't know if this would be any easier than working, e.g., with docs#category_theory.abelian.pseudoelement

[Adam Topaz]

But we probably should have some API for categorical spans in mathlib...

[Chris Hughes]

Are there interesting results on decidability of particular questions about particular categories, in a similar vein to the fact that the first order theory of real-closed fields is decidable? Does it make sense to ask about whether the theory of the category of real finite dimensional vector spaces is decidable, I guess there are a lot of interpretations of that statement.

[Adam Topaz]

That's an interesting question. I don't recall ever seeing anything about the model theory of categories.

[Adam Topaz]

But whatever that means, decidability should be invariant under categorical equivalence and not just isomorphisms... Its hard to even imagine such a notion!

[Adam Topaz]

This so-called Rezk completion probably has something to do with this

[Chris Hughes]

I just looked at Rezk completion on nlab and I don't understand it because I don't understand what the difference between a precategory and a category is.

[Johan Commelin]

Adam Topaz said:

But whatever that means, decidability should be invariant under categorical equivalence and not just isomorphisms... Its hard to even imagine such a notion!

I guess that depends on what you mean by isomorphism? Decidable equality isn't invariant under bijections, only under equiv.
But I'm not an expert.

[David Wärn]

I think as long as your language doesn't allow to talk about equality of objects, you can't tell the difference between equivalences of categories and isomorphisms of categories, or between a category and its Rezk completion (all the Rezk completion does is to change "equality of objects" into "isomorphism of objects")

[Chris Hughes]

Johan Commelin said:

Adam Topaz said:

But whatever that means, decidability should be invariant under categorical equivalence and not just isomorphisms... Its hard to even imagine such a notion!

I guess that depends on what you mean by isomorphism? Decidable equality isn't invariant under bijections, only under equiv.
But I'm not an expert.

There's a distinction between decidable equality and decidability of the first order theory. e.g. the reals have undecidable equality and a decidable first order theory in the language of rings, but the integers have decidable equality and an undecidable first order theory. Decidability of the first order theory is preserved under bijective homomorphisms.

[David Wärn]

Actually if you allow quantification over objects, then you can encode Peano arithmetic in the theory of the category of fin dim real vector spaces (edit: is this true? you can define addition, but what about multiplication?). If you only quantify over morphisms, then you should get decidability since a morphism is just a matrix of numbers

[David Wärn]

Let me elaborate on the answer above. Consider a first-order theory of categories, with two sorts "objects" and "morphisms", where you can quantify over either one, you have symbols for the domain/codomain of a morphism, and for identity morphisms and composition. I claim that the theory of the category of (finite-dimensional) vector spaces over any field of char 0 is thus undecidable (for stupid reasons, basically). Note that you can define what it means for an object to be zero-dimensional (say, it has a unique endomorphism), for a morphism to be zero, for an object to be one-dimensional (every endomorphism is zero or an iso), and what it means for a diagram to be a (co)product diagram. There is a common trick to defining addition in a category with biproducts, which lets you define addition (and hence subtraction) of morphisms. We can define a "scalar" to be a morphism R -> R where R is our favourite one-dimensional object. Note that we can define arithmetic on scalars. I claim that we can also define what it means for a scalar to be a natural number. Then you can interpret Peano arithmetic, so you get undecidability. Note that x is a natural number if and only if it is the trace of some identity morphism. As it turns out, a matrix is traceless iff it is a commutator, so we can define what it means for two endomorphisms of V to have the same trace (their difference is a commutator). Given an inclusion i : R -> V together with a retraction j : V -> R, you can define a trace-preserving embedding End R -> End V, so you can define what it means for a scalar to be the trace of a given endomorphism, as needed.

[Adam Topaz]

David Wärn said:

I think as long as your language doesn't allow to talk about equality of objects, you can't tell the difference between equivalences of categories and isomorphisms of categories, or between a category and its Rezk completion (all the Rezk completion does is to change "equality of objects" into "isomorphism of objects")

As far as I know, equality is always part of a first order language. So if you encode a category as two sorts (one for objects and one for morphisms), then at least in usual first order logic you will be talking about equality of objects by default.

[David Wärn]

True, in most presentations of first-order logic, equality is included by default. But you can just remove it! It means that you can't define $f : A \to B$ to mean $(A, B) = (\textup{dom} f, \textup{cod} f)$, but you can use dependent types for hom-sets like in mathlib.

[David Wärn]

https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf this might be relevant