Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: topos theory

Topic: internalization

Reid Barton (Dec 28 2020 at 12:06):

If $f : A \to B$ is (injective, surjective) then so is the induced map between the free abelian groups on $A$ and $B$. Is this the sort of statement where I can get an internal version in any (Grothendieck) topos for free by some Barr's theorem argument?

Morgan Rogers (he/him) (Dec 28 2020 at 12:47):

I believe so, since the proof that the algebraic construction of the free group has the required universal property is constructive, so you should be able to use that description in the internal language. From there, the proof that injectivity/surjectivity lifts is also constructive, and should be valid in any topos. There are some subtleties to check, no doubt.

Reid Barton (Dec 28 2020 at 12:58):

So this is the kind of argument that I used to convince myself that the statement is at least true internally, but as you say it is a bit subtle. Let's take injectivity because it is more difficult. Then classically one might prove it like this: identify the free abelian group on $A$ with finitely supported functions from $A$ to the integers, and the map induced by $f$ with "extension by zero". Then injectivity becomes obvious. But this requires LEM (already to write down the unit map from $A$ to finitely supported functions on $A$, and possibly elsewhere as well).

Reid Barton (Dec 28 2020 at 13:01):

But I think you can indeed also prove injectivity constructively by arguing that if a formal sum of images equals zero, we can pick some way of cancelling terms $f(a_i) - f(a'_i) = 0$ which witnesses this, and each of these cancellations gives a corresponding cancellation $a_i - a'_i = 0$.

Morgan Rogers (he/him) (Dec 28 2020 at 13:05):

Finiteness of sums should make that valid, but I've always been a little uncertain about how automatically finitary arguments lift to arbitrary toposes

Reid Barton (Dec 28 2020 at 13:05):

The key fact seems to be that the free groups is presented as the quotient of a finitary inductive type by a finitary equivalence relation--so maybe there's some extension of "any geometric sequent which is true classically is also true constructively" to a language which contains such constructions?

Reid Barton (Dec 28 2020 at 13:10):

In reality I want statements slightly more complicated than these (involving the free abelian group on a pointed set) and so the subtleties become slightly more subtle... and it would be nice to have a hammer which says I don't have to worry.