Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 18 of 18
Is is constructively true (to be more precise, is it true in a topos with NNO) that every object embeds in an abelian group object?
This came up in discussion under an MO answer I gave a while back – I’ve also brought up the claim in the nForum – but Peter LeFanu Lumsdaine brought up the point that I’m asking about now. It’s not immediately clear that the answer is ’yes’ if the object doesn’t have decidable equality.
I would imagine it can be proven constructively as long as one has that coprojections into a coproduct are monic. For I think one can give a constructively valid construction of the free abelian group on a set as (of course one needs to define the multiplication map as well, but I think all is fine), and then one can use the coprojection from into the component of the coproduct.
That gives the free monoid, but not the free abelian group. Am I missing something?
Ah yes, good point! Can we not just use instead of as the indexing set? Edit (posted before I saw Todd’s comment in #5): actually, I think this will be tricky, because for this kind of idea to work out, one will need to take a quotient, and then I think it will be difficult to show that we have a monomorphism into it.
I don’t see how.
I think it can be done, e.g. one defines for as the quotient of by the relation identifying if , i.e. this is a kind of categorification of the usual construction of the integers as equivalence classes as natural numbers.
The problem for your question, as noted in #4, is that it is not obvious (to me at least) how to show monicity of the canonical arrow from into the quotient.
On the other hand, presumably it can be shown constructively that the natural numbers embed in the integers defined in this way (as equivalence classes of pairs of natural numbers), and such a proof might categorify (constructively).
Edit 1: it seems ’obvious’ if one uses elements. The map would come from the canonical one sending to and sending the latter into the coproduct of which is a quotient, and then we just observe that (I am mixing notation a bit here, using 1 for the empty tuple) implies that . Presumably one can also reformulate this in an element-free way.
Edit 2: one also will presumably need a quotient of the products by the action of the symmetric group as well to get abelian-ness. But I don’t think this affects the proof, using elements, of monicity of the canonical map of Edit 1.
A comment on the MO question notes that the singleton map of into its powerset is an injection and is an abelian monoid under or , but that it’s not clear whether this helps with injecting into an abelian group. Classically, is also an abelian group under the symmetric difference operation (the addition operation of its Boolean ring structure), and hence also under its dual operation “if and only if”. It’s not clear to me whether either of these is true constructively (and they are no longer strictly dual, either); but it’s at least something else to think about.
I am led to wonder if the construction in #6 (disregarding Edit 2) is some kind of unusual construction of the free group on . If the construction is correct, has anybody seen it used in this way?
Peter LeFanu Lumsdaine has put all doubts to rest in this new MO thread. Sigh of relief.
Great! I am still quite interested in the construction I suggested, though. For example, we could replace by , and from there probably even . What on earth are such objects?!
By the way, the following related question seems to be open: Can every object be embedded into a flabby abelian group object? Phrased in set language, can any set be embedded into a flabby abelian group?
For the purposes of this question, a set is flabby if and only if for any subset such that , there exists an element such that . (The name originates from sheaf theory: A sheaf is flabby if and only if, from the point of view of the internal language of the sheaf topos, it’s a flabby set.)
Over at MO, Peter reminded us that any set can be embedded into an abelian group; and it’s also true that any set can be embedded into a flabby set (for instance powersets are flabby). But it seems to be open whether there is an intuitionistic proof that any set can be embedded into an abelian group whose underlying set is flabby. (This holds in all Grothendieck toposes, assuming the axiom of choice in the metatheory, but not much more seems to be known.)
A quick, naïve question, Ingo. In the internal language, statements in the Zariski topoi translate into set theoretic ones. Now, could one try to externalise this back to Set, i.e. could one obtain some kind of algebraic geometry by carrying out externally in Set the constructions one does internally in the usual Zariski topoi?
I suppose that this is too naïve, but I thought I’d ask anyway!
My reason for asking comes from ruminating upon . Many people have tried to build up an algebraic geometry from a deeper algebraic category, but one could try a deeper topos instead. For some aspects of the analogies, seems a reasonable place to look. However, an algebraic geometry of the kind I am wondering about would be kind of orthogonal approach, because one would I think be dropping multiplicativity, not additivity! But this is not a ridiculous idea, it seems to me: the difference between and is after all that we take a free abelian group rather than a free commutative ring.
The fact that the affine line becomes a field internally also seems to roughly fit the picture.
Richard, that’s certainly an intriguing idea which should be properly explored! I haven’t thought much about it.
However, naively, I think that one of the following is true:
(1) Set is not up to the job. (2) Usual classical metatheories are not up to the job. (3) One has to change algebraic geometry quite a bit in order to make sense in Set. Carrying out synthetic algebraic geometry in Set is not the right way to do it.
Here’s why: Several of the notions in synthetic algebraic geometry (which is what you get when you recast algebraic geometry in set-theoretic terms by switching into the big Zariski topos of a base scheme) crucially depend on the fact that the law of excluded middle is not available lest they get trivialized. However, in Set, it is (assuming a classical metalogic).
For instance, a central notion in synthetic algebraic geometry is that of synthetic quasicoherence. An -module is synthetically quasicoherent if and only if the canonical map is bijective for any finitely presented -algebra . This notion is central because, for instance, we use it do define open immersions and thus synthetic schemes in terms of it. Also all known ring-theoretic properties of the affine line follow from the statement that the affine line is synthetically quasicoherent as a module over itself.
However, if the law of excluded middle is available, the only ring which is synthetically quasicoherent over itself is the zero ring.
Thanks for the very interesting reply! It would be truly fascinating if one could get something interesting using a constructive but not a non-constructive meta-theory!
Let us suppose that we do have a constructive meta-theory. Would you have a suggestion for how to get started to see if we obtain something interesting? Don’t worry about , anything would be fine. Can we give an example of a scheme, for instance?
In such a context we could at least start to carry out standard algebraic geometry. (I’m not quite sure whether that’s what you had in mind.)
Fix a local ring which is synthetically quasicoherent over itself. We can then define all sorts of interesting schemes, for instance:
We can also give definitions of general notions: affine scheme, open immersion, scheme: see for instance Definition 19.48 in my notes.
Hi Ingo, haven’t been following, so this will be a dumb question: Why do you insist on displaying dualized -modules in your list above?
By the way, to properly typeset text in math mode, you may enclose it like so:
\text{text in math mode}
or, usually, better
\, \text{text in math mode} \,
in order to get the expected spacing.
Sorry, I didn’t notice your question earlier, Urs. (Do nForum notifications work for you? They don’t seem to for me, at the moment.)
I wanted to write these examples as an algebraic geometer would, by utilizing the spectrum. In the context of a fixed base ring , it makes some sense to define the spectrum of an -algebra as the set of -algebra homomorphisms . For instance, as displayed above. An innocent bystander might of course wonder: Wait. I can see that if is a field, this definition yields some of the prime ideals of (the preimages of the zero ideal). But what about the remaining prime ideals, and what about the case that might not be a field?
These worries are justified; but they are taken care of by the internal language, in view of the following fact: Let be a scheme. Let be an -algebra. Then the expression “” of the internal language of the big Zariski topos of denotes the functor of points of the relative spectrum . (Here is the canonical ring in the big Zariski topos, the functor of points of the affine line over ; and by “” I actually mean the mirror image of in the big Zariski topos.)
Coming from a cohomology background, you might further wonder: Doesn’t the process of passing from an -algebra to lose information? For instance .
This is where synthetic quasicoherence of plays a role. It ensures that can be reconstructed from as (set of maps). More precisely, the canonical map is a bijection.
Does this answer your question?
Thanks for the tip regarding spacing. I’ll edit my post in a second.
1 to 18 of 18