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.
Maybe I am looking at the wrong places: is there somewhere a discussion of examples for classes of toposes that satisfy COSHEP?
What is known about which sites induce toposes that validate COSHEP?
In COSHEP, it is mentioned that all presheaf toposes satisfy this condition. It’s mentioned at realizability topos, and ought to be mentioned at COSHEP as well, that all realizability toposes satisfy it, and more generally toposes that arise via ex/lex completion satisfy it.
I don’t know (haven’t thought about) a good answer to the second question.
Nor have I.
Thanks for the replies.
I did see the presheaf-topos example, but somehow I counted that as “trivial”. Maybe that’s not the right attitude. But I was looking at Todd’s comments at projective object about having enough projectives if satisfies COSHEP and thought it would be nice to add some examples of classes of sites that we find to be nice contexts for homological algebra this way.
Nevertheless, I have now taken the liberty of formatting the entry COSHEP a little bit more, to make it easier to spot what is going on where.
I have also added a list of related entries.
One comment on the formatting: I am not a fan of Remark-sections. They are tedious to read as one never knows what to expect. I suggest that these paragraphs in the Remark-section be either turned into numbered remarks that go right after the axiom, in as far as they are really remarks on the axiom, or else they should be turned into numbered propositions to go into the Properties-section.
Sorry for keeping being a pain about such formatting. But maybe you can see where I am coming from. If you don’t object, I can do that rearranging.
Finally an actual technical remark: the statement that is now labeled Remark 2 seems to be wrong to me. An epimorphism out of a projective is not in general called a projective resolution, but it may generally be called a projective presentation. Do you actively disagree with that statement?
I don’t object to your rearranging, I don’t think, but I’d really have to see it to be sure. I’m not persuaded that all remarks fall under one of those two categories you mention, but I’ll certainly bear in mind what your preferences seem to be (even though I’m not bothered by remarks sections).
I agree with you about projective presentation. All instances of the word “resolution” after the first one seem to be unproblematic.
Okay, I have been editing COSHEP a bit more. Please have careful look at the new version of the Statement-section: since originally further below it said that the “the dual axiom is that there are enough injectives” I thought we should say somewhere explicitly that COSHEP is the statement that “there are enough projectives”.
So I made now the first version of the statement appear, then the definition of projective object be recalled, and then that reformulated be stated explicitly.
I am slightly worried that I am mixing up external with internal meaning here. But if I do, it means (apart from me being really tired now) that the entry does not help me enough, and so maybe then you could try to clarify that. Sorry.
If I may follow my heretic vein once more, let me ask:
What’s the “COS” to do in “COSHEP”?
It seems to add no information for a foundational axiom to say “categories of sets” and insead seems to be more of a distraction and also to violate common conventions. To compare: we don’t say “categories of sets have split epimorphisms”, but instead we speak simply of the “axiom of choice”.
Instead of “COSHEP” this should just be called the “axiom of enough projectives”. That would also get rid of this long acronym. These acronyms make simple ideas feel very opaque. They make a sceret science out of something which when said in plain words has a direct meaning also to people not immediately involved.
Just a suggestion.
The page is called ’presention axiom’…
So if I go and replace in the entry all occurences of “COSHEP” with “presentation axiom”, nobody will object? Because I would like to do that.
I’ve been pronouncing COSHEP as a two-syllable word in my head all this time. Was that wrong?
I am not worried about how one pronounces it. I just find it less than helpful with any pronounciation.
The assumption that “there are enough projectives” is an entirely standard one, familiar in large corners of mathematics. But if somebody in such a corner hears you talk about “COSHEP” (in whichever pronounciation) he won’t have a clue that you are talking about something basic that he teaches his kids over breakfast.
And I think even in itself the abbreviation “COSHEP” it is suboptimal: “EP”, that’s the essence. Why not call it “EP” if an abbreviation is desired? It’s as comprehensible or incomprehensible as “COSHEP” to the non-inititated. And “categories of sets have…” is not really something that one wants to put in the name of an axiom, I think. We don’t say “assume that categories of sets have excluded middle”. We just say: assume the axiom of excluded middle.
Can anyone see what I mean? Not that we should have a lengthy discussion about it. If you disagree, let’s just leave it at that. I won’t insist. I just thought I’d mention it.
I agree with you, Urs. I would never call the axiom COSHEP if I was talking about a general topos, only in some foundational specific contexts.
While I don’t see anything wrong with the name ’COSHEP’ myself, I’d be perfectly happy to get rid of it in the interests of not needlessly proliferating different names for the same thing. I do kind of feel like saying that a topos satisfies some foundational axiom should refer by default to the internal version, though.
I do kind of feel like saying that a topos satisfies some foundational axiom should refer by default to the internal version, though.
Let’s see, what is the internal statement?
I’d like to start writing something like
Now is and so forth.
But now I am unsure how to say . We talked about this recently in the context of the type-theoretic axiom of choice. So I guess I should say something like
= “if the (-1)-truncation of any with has a section”.
Or the like. I like to think that I can figure this out when thinking about it long enough. But maybe you could provide some hints.
Let’s see, what is the internal statement?
I thought Mike simply meant “every object is covered by an internally projective object.”
No objection if anyone wants to put in the type-theoretic elaborations, but I’d be dismayed if that very simple formulation got buried.
I’d also like to say that for the purpose of constructing projective resolutions, it’s the external notion that’s really being used. Of course the internal version implies the external if is (externally) projective. In the other direction, there is a correction to be made, as noted in another recent thread.
as noted in another recent thread.
Do you maybe have a minute to incorporate the upshot of that discussion into the entry presentation axiom? It would do the entry good, I think.
I put in some remarks in the topos section. But I haven’t tried to fix the examples that come after.
Thanks!
A propos of the first example in this section, please see my comment in the internally projective objects thread.
I meant the actual internalization of the presentation axiom, in the sense of type theory or stack semantics. That might be the same as “every object is covered by an internally projective object”, but not a priori. A straightforward interpretation in the stack semantics gives “for every , there exists an epi and an epi such that is internally projective in .”
I’d also like to say that for the purpose of constructing projective resolutions, it’s the external notion that’s really being used.
Well, yes, as long as you are constructing externally projective resolutions… (-:
I meant the actual internalization of the presentation axiom, in the sense of type theory or stack semantics. That might be the same as “every object is covered by an internally projective object”, but not a priori.
Right; thanks. David Roberts also mentioned this in another thread.
Well, yes, as long as you are constructing externally projective resolutions… (-:
That seemed to be the context for some comments exchanged between Urs and me, probably in connection with the course he’s teaching. But of course, you’re right.
Agree with David #12. I invented the term ‘COSHEP’ because I was thinking about foundations (and because I didn't know ‘presentation axiom’). One would not say that some random category ‘satisfies COSHEP’. (Although Mike's remarks about internal vs external are also important here.)
Urs #4 regarding Remark sections.
I don't understand. If you don't like Remark sections (and I don't either), then why create them? Just make the remark.
If you don’t like Remark sections (and I don’t either), then why create them?
I don’t create them. In this case Mike did.
I misunderstood! You created Remark environments, which I don't like either. But I agree with you about where to put the remarks.
You created Remark environments, which I don’t like either.
What is it you don’t like about them?
This may not be the place to go into it, but as I said in #23, I would just make the remark. Having definitions and theorems in environments helps one find and refer to them, but there is not much point to this with remarks, so the ‘Remark.’ (worse ‘Remark 1.’) is just clutter.
But one problem is that some environments (chiefly definitions) don't have anything to mark their ending, so you don't know where the definition stops and the surrounding text (which consists of remarks) starts. But I'd like to find a solution to mark the end of a definition better than beginning the next paragraph with ‘Remark.’.
I very much agree with Toby’s second paragraph of #27: the lack of a definitive ending to a definition is definitely an irritant.
Re his first paragraph: very often, I also find that too many separate environments (like remark environments) give text a cluttered or choppy look which is visually unattractive to me. On the other hand, having remarks to refer back to can be useful down the line, so I cannot say I am absolutely opposed to them.
(Sometimes it would be nice to get rid of numbering but keep the anchoring. For example, being able to anchor to something one wants to read as “Theorem (Hilbert)”, and not have it come out looking like “Theorem (Hilbert) 4”, which is goofy-looking, that would be nice. Maybe there’s a simple solution to that that I don’t know.)
When I’m writing a paper, I generally only add “remark” environments when the remark is one that I’ll want to refer to somewhere else in the paper, so that it’ll have a number that I can refer to. I generally apply the same principle on the nLab — which in particular means that I would never create an unnumbered remark.
Maybe there could be an end-of-theorem-statement and end-of-definition marker, kind of like the which ends a proof.
Finally, what I’ve done sometimes to give a label or attribution to a numbered theorem is
+--{: .num_theorem #Hilbert}
###### Theorem
**(Hilbert)**
Theorem text goes here
=--
I thought I remembered that for Instiki’s theorem-magic to work correctly, it’s actually important that the ###### header line contain only the appropriate word “Theorem” or “Definition” or etc. But maybe my memory is wrong.
one problem is that some environments (chiefly definitions) don’t have anything to mark their ending, so you don’t know where the definition stops and the surrounding text (which consists of remarks) starts. But I’d like to find a solution to mark the end of a definition better than beginning the next paragraph with ‘Remark.’.
I find, if I may say so, that you all tend to write in a style that would profit from having less “surrounding text”. Since we are not writing a collaborative novel here, every bit of “surrounding text” that does not carry an indication of what it’s going to do with the reader means extra work on the reader and possibly superfluous work on the reader’s part.
Keep in mind that readers of the Lab will scan entries for information, not print them out and read them first line to last at night in bed before going to sleep, anxiously expecting the whodunnit in the last line.
Sometimes I find paragraphs where without line break we see a definition, then a historical remark, then a theorem mentioned, then an aside and lastly the end of the definition. Whenever I can I take these paragraphs apart. If that gives the text a “choppy” appearance that’s okay, I think, beause the content was choppy before, but not visually recognizably so. Better have it be choppy and recognizably so. It’s math, not a novel.
Well, that’s my opinion. You will all disagree and we will never find agreement, so no need to further hash this out. I am just saying this in case it may ever so slightly nudge you in this direction next time you wonder about whether to create a Remark-environment or not.
@Mike #29: that sort of works, although “Hilbert” then becomes part of the italicized text, which I don’t want. I suppose it’s a minor issue.
Whenever I can I take these paragraphs apart. If that gives the text a “choppy” appearance that’s okay
Okay by you, perhaps. Perhaps not okay by the original author, who might wish to impart some narrative flow. Conveying points of view can be like telling a story (cf. David Corfield’s remarks on mathematics as narrative, e.g., here). Some people might come here partly to hear points of view explained in a graceful and human way. Consider how gifted writers like John Baez write mathematics.
Just as you wish to nudge us in a certain direction (towards the way you want to see entries written), I would like to nudge you in a direction of greater tolerance towards the different styles in which your nLab coworkers choose to express themselves. Caricaturing and belittling those efforts as “whodunnits” is rude, if I may say so.
It is possible for different kinds of “content” to be put together into a paragraph which flows nicely to read and makes sense. There is a style to writing mathematics that matters greatly in terms of readability; all the logical organization of content in the world will not make something readable if one doesn’t put any thought into how the words flow. Apparently this doesn’t matter to you, Urs, but I think it matters to a lot of people, regardless of whether we are looking up a reference to learn facts or reading a novel at bedtime. I can’t ask you to write in a style that is evidently foreign to you, but I would second Todd’s request that you respect others’ efforts to write things in a way that we and many others find easier to read.
I would like to have CSS such that
+-- {: .num_theorem #Hilbert}
###### Theorem (Hilbert)
Theorem text goes here
=--
will have the opening parenthesis recognised so that the theorem number will be put before it. This is probably not possible.
Keep in mind that readers of the Lab will scan entries for information, not print them out and read them first line to last at night in bed before going to sleep, anxiously expecting the whodunnit in the last line.
That is pretty much how I read them, when possible.
But I didn't mean to start an argument about Remark environments. I misunderstood what Urs wrote about Remark sections, which didn't seem to match his behaviour, so I got a little snarky about that. That was my fault for not reading carefully.
1 to 34 of 34