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.
The page constant morphism says
As with Set, any morphism which factors through a terminal object is constant but although this is an “if and only if” in Set it need not be in a general category.
I think the two are equivalent in any category with a terminal object, as explained here. That is, a morphism is constant if and only if the natural transformation factors through the terminal object in the presheaf category, so that if the latter is representable then so is the factorization of .
Have I missed something? If not I’ll edit the page.
The original statement dates back to me and therefore is almost certainly me “playing safe”. Toby, Mike, and Urs all at least read the page and didn’t see fit to correct it, but they may have assumed that I knew what I was talking about (dangerous assumption here!).
I’ve only looked at it for a minute, but what FInn says looks right.
(I have also done my standard editorial thing to the entry now… ;-)
didn’t see fit to correct it
Wait, I don’t think there is anything outright wrong in the entry. The entry seems to say that not in every category does a constant morphism factor through a terminal object.
What Finn observes is that if a terminal object exists, then every constant morphism factors through it. But a terminal object may not exist.
OK, thanks, that all mirrors what I suspected. I’ve edited the page now.
Do we have an example of a constant morphism in a category without terminal object?
Isn’t it true that the category of fields doesn’t have a terminal object? I saw this proved somewhere but I forget how. Then any constant morphism at 0 will be an example.
Edit: no, that can’t be right, because if there was a field morphism with constant value 0 that would make 0=1 in the codomain.
Wait a minute, I don’t agree with the change. I think the identity morphism of any subterminal object is a constant morphism, but not every subterminal object admits a global section.
That sounds plausible, but it seems to mean that the two aren’t equivalent even in Set, right?
Yes, that’s right! The identity map of the empty set is constant according to this definition, but it doesn’t factor through the terminal object.
That makes me less sure that this is the right definition of “constant morphism”.
Well, that’s a bit of a bugger. I wonder if there’s a way to characterise the objects for which the equivalence fails; maybe it holds for morphisms out of non-subterminals or something. But it’s too late here to start thinking about it now.
I think the equivalence holds for any morphism whose domain admits a global section. Proof: if is constant as defined on the page, and admits a global section , then and are two morphisms , hence , so factors through the terminal object . The converse is obvious.
I think non-subterminals isn’t strong enough; if is subterminal, nonterminal, and nonempty, then the fold map is constant, but doesn’t factor through the terminal object. Similarly for the fold into one summand , and is not generally subterminal.
I think the equivalence holds for any morphism whose domain admits a global section. Proof:
With that clause Finn’s previous argument is patched: the argument secretly assumed that the hom-spaces are inhabited in the first place.
So it seems that with his argument the assumption can be relaxed to: assume is inhabited for all .
Thanks, everyone. I’ve edited the page constant morphism accordingly.
I don’t quite see how the two definitions can be equivalent in the absence of a terminal object, since in that case the “factors through the terminal object” definition doesn’t even make sense. And of course in the presence of a terminal object, Hom(K,X) being inhabited for all K is equivalent to X admitting a global section.
I’ve clarified the phrasing a little.
The empty map is constant in that it doesn’t vary, but it has no constant value. They’re different things, like the different senses of connected.
I’ve put in a version of the strict definition that needs no terminal object.
Nice, thanks Toby! That helps clarify. It really is just like the question of whether the empty set is connected.
Somehow Toby’s edit restored the bit that Mike complained about in #15, so I’ve rewritten it again.
I thought that at first too, but actually, Toby also changed the second definition so that that bit becomes true in a category without a terminal object. So I reverted your edit. (-:
Oh, right, I didn’t see that bit.
In case anyone is interested, essentially the same issue discussed earlier in this thread has come up recently on the homotopy type theory mailing list. In that context there are at least three proposed definitions of “constant function” :
If is an hset, then (1) and (2) are equivalent, but even then both are weaker than (3) (e.g. when ); in this case we recover the dichotomy discussed at constant morphism. But when is not an hset, then (1) and (2) can also differ, e.g. there are models with satisfying (1) where is a merely-inhabited set (i.e. its -truncation is contractible) and is a 1-type with no global points, so there are no functions .
For that reason, I’m inclined not to consider (1) as a notion of “constant function”, but I’m curious to hear other opinions.
It looks to me that (1) is deficient because it comes from the truncation of a hypercover, no? At least, here is how I think about it in the 1-topos case: (1) says that factors through the coequaliser of the two projections , which is precisely the image of .
Yes, I entirely agree with you. Unfortunately, I haven’t managed to convince Martin Escardo of that yet. Care to help?
I tried reading through the preceding discussion but I’m afraid I can’t really follow…
Sorry. It is a bit all over the place.
I don't understand this bit:
is a 1-type with no global points
I read this as
is a groupoid with no objects
which doesn't work.
But possibly I am mixing internal and external language. Is the resolution that you working in a non-well-pointed model of HoTT?
In any case, I can follow the main argument, as I can distinguish (1) and (2) in a non-well-pointed topos, or in the category of locales, or in other places where non-empty things may have no global points.
Yes, the phrase “global point” is only really meaningful at the meta-level. In type theory the appropriate statement is that there is no closed term of type Y, which is a meta-statement about the type theory, and distinct from the internal assertion “Y is not inhabited”.
Prompted by this MO question I looked back at the page constant morphism, and I don’t think the terminal-object-free version of Definition 2 is correct. If, as suggested by Sridhar and Qiaochu, we define a morphism to be constant if its image under the Yoneda embedding factors through the terminal presheaf, then I think we would get something like “we can choose for each object a morphism such that for any we have and moreover for any we have ”. In other words, for each object there is a specified morphism , chosen naturally in , such that if any morphism factors through then is the unique one that does. This includes, for instance, the map in (which factors through the terminal object), whereas the definition as stated does not.
It seems to me we can say more simply that is constant, in the sense corresponding to factoring through even if no terminal object is actually around, just in case “we can choose for each object a morphism such that for any we have and moreover we have ”.
I think you’re right. I’ll fix the page when I get a moment, unless someone else has done it first.
Fixed.
1 to 35 of 35