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.
Inspired by a discussion with Martin Escardo, I created taboo.
stub for syntomic cohomology
a stub entry — for the moment just to make links work at nondeterministic computation and at complexity class
Unstub the page with a basic but original blurb. Compare and contrast my article list of complexity classes on esowiki, which has a very different audience.
In looking for texts that would address the question “What is computation?” and arrive at an answer vaguely akin to path lifting/transport, I found (and have now added pointer to) this text:
which gets pretty close, in particular in and around their Figure 1.
added pointer to this recent preprint:
I have made some trivial edits to the wording, hoping to make it flow more nicely.
By the way, this entry is linking (at least now that I adjusted the plural redirect) to recursive function. This is only natural, but – unfortunately – our entry recursive function is empty (and always has been)!
Much of the material needed there is at partial recursive function. We should either put redirects or (better) add a little bit of content to recursive function.
while bringing some more structure into the section-outline at comma category I noticed the following old discussion there, which hereby I am moving from there to here:
[begin forwarded discussion]
+–{.query} It's a very natural notation, as it generalises the notation (or as is now more common) for a hom-set. But personally, I like (or if you want to differentiate from a cocomma category, but that seems an unlikely confusion), as it is a category of arrows from to . —Toby Bartels
Mike: Perhaps. I never write for a hom-set, only or where is the category involved, and this is also the common practice in nearly all mathematics I have read. I have seen for an internal-hom object in a closed monoidal category, and for a hom-set in a homotopy category, but not for a hom-set in an arbitrary category.
I would be okay with calling the comma category (or more generally the comma object) or if you are considering it as a discrete fibration from to . But if you are considering it as a category in its own right, I think that such notation is confusing. I don’t mind the arrow notations, but I prefer as less visually distracting, and evidently a generalization of the common notation for a slice category.
Toby: Well, I never stick ‘’ in there unless necessary to avoid ambiguity. I agree that the slice-generalising notation is also good. I'll use it too, but I edited the text to not denigrate the hom-set generalising notation so much.
Mike: The main reason I don’t like unadorned for either comma objects or hom-sets is that it’s already such an overloaded notation. My first thought when I see in a category is that we have and and we’re talking about the pair — surely also a natural generalization of the very well-established notation for ordered pairs.
Toby: The notation for a double comma object makes me like even more!
Mike: I’d rather avoid using in the name of an object; talking about projections looks a good deal more confusing to me than .
Toby: I can handle that, but after thinking about it more, I've realised that the arrow doesn't really work. If , then ought to be the set of transformations between them. (Or , but you can't keep that decoration up.)
Mike: Let me summarize this discussion so far, and try to get some other people into it. So far the only argument I have heard in favor of the notation is that it generalizes a notation for hom-sets. In my experience that notation for hom-sets is rare-to-nonexistent, nor do I like it as a notation for hom-sets: for one thing it doesn’t indicate the category in question, and for another it looks like an ordered pair. The notation for a comma category also looks like an ordered pair, which it isn’t. I also don’t think that a comma category is very much like a hom-set; it happens to be a hom-set when the domains of and are the point, but in general it seems to me that a more natural notion of hom-set between functors is a set of natural transformations. It’s really the fibers of the comma category, considered as a fibration from to , that are hom-sets. Finally, I don’t think the notation scales well to double comma objects; we could write but it is now even less like a hom-set.
Urs: to be frank, I used it without thinking much about it. Which of the other two is your favorite? By the way, Kashiwara-Schapira use . Maybe ? Lengthy, but at least unambiguous. Or maybe ?
Zoran Skoda: or are the only two standard notations nowdays, I think the original which was done for typographical reasons in archaic period is abandonded by the LaTeX era. is more popular among practical mathematicians, and special cases, like when ) and among category experts…other possibilities for notation should be avoided I think.
Urs: sounds good. I’ll try to stick to then.
Mike: There are many category theorists who write , including (in my experience) most Australians. I prefer myself, although I occasionally write if I’m talking to someone who I worry might be confused by .
Urs: recently in a talk when an over-category appeared as somebody in the audience asked: “What’s that quotient?”. But already looks different. And of course the proper even more so.
Anyway, that just to say: i like , find it less cumbersome than and apologize for having written so often.
Toby: I find more self explanatory, but is cool. was reasonable, but we now have better options.
=–
Query from Stephen on 2-pullback.
At comma object, Eduardo Pareja-Tobes put a query box which does not seem to have been ‘answered’. This was some time ago it seems.
removing query box from page
+– {: .query} Mike Shulman: Is there a formal statement in some formal system along the lines of “a non-extensional choice operator does not imply AC”?
Toby: I don't know about a formal statement, but I can give you an example.
Recall: In Per Martin-Löf's Intuitionistic Type Theory (and many other systems along similar lines), the basic notion axiomatised is not really that of a set (even though it might be called ’set’) but instead a preset (or ’type’). Often one hears that the axiom of choice does hold in these systems, which doesn't imply classical logic due to a lack of quotient (pre)sets. However, if we define a set to be a preset equipped with an equivalence predicate, then the axiom of choice fails (although we have COSHEP if presets come with an identity predicate).
A lot of these systems (including Martin-Löf's) use ’propositions as types’, in which is represented as , which comes equipped with an operation . That is not going to get us our choice operator, but since a choice operator is constructively questionable anyway, then let's throw in excluded middle. This is known to not imply choice, but we do have, for every preset , an element of , that is of . It's not literally true that is of type , of course, but that would be unreasonable in a structural theory; what we do have is a fixed such that, if is inhabited, then for some (necessarily unique) of type (where is the natural inclusion ), which I think should be considered good enough. This is for presets (types), but every set has a type of elements, so that gets us our operator.
How is this nonextensional? We do have if (which is a meaningful statement to Martin-Löf, albeit not a proposition exactly), but if and are given as subsets of some , then we may well have as subsets of without in the sense of identity of their underlying (pre)sets. In particular, if is a surjection and and are the preimages of elements and of , then will not imply that , and the proof of the axiom of choice does not go through. It will go through if and are identical, that is if in the underlying preset of , so again we do get choice for presets (again), but not for sets.
I'm not certain that a nonextensional global choice operator won't imply excluded middle in some other way, but I don't see how it would. You'd want to do something with the idea that always exists but belongs to if and only if is inhabited, but I don't see how to parse it (just by assuming that it exists) to decide the question.
Mike Shulman: That’s a very nice explanation/example, and it did help me to understand better what’s going on; thanks! (Did you mean to say “excluded middle” and not “AC” in your final paragraph?) What I would really like, though, is a statement like “the addition of a nonextensional global choice operator to ____ set theory is conservative” (i.e. doesn’t enable the proving of any new theorems that doen’t refer explicitly to the choice operator). Of course I am coming from this comment, wondering whether what you suggested really is a way to get a choice operator without implying the axiom of choice.
Toby: Yeah, I really did mean to say ’excluded middle’; remembering that comment, I assume that the real question is whether the thing is OK for a constructivist. I just argued , and I know the result , so I conclude ; but I don't know for certain. I certainly don't have conservative over , nor with any other theory (other than those that already model , obviously).
Mike Shulman: Where should I look for a proof that doesn’t imply AC?
Toby: I'm not sure, it's part of my folk knowledge now. Probably Michael J. Beeson's Foundations of Constructive Mathematics is the best bet. I'll try to get a look in there myself next week; I can see that it's not exactly obvious, and perhaps my memory is wrong now that I think about it.
Mike Shulman: I’m trying to prove the sort of statement I want over at SEAR+?.
Toby: No, I can't get anything at all out of Beeson (or other references) about full AC (for types equipped with equivalence relations) in .
Harry Gindi: I have references for this discussion that should settle the issue at hand:
Bell, J. L., 1993a. ’Hilbert’s epsilon-operator and classical logic’, Journal of Philosophical Logic, 22:1-18
Bell, J. L., 1993b. ’Hilbert’s epsilon operator in intuitionistic type theories’, Mathematical Logic Quarterly 39:323-337
Meyer Viol, W., 1995a. ’A proof-theoretic treatment of assignments’, Bulletin of the IGPL, 3:223-243
Toby: Thanks, Harry! Now I just have to find these journals at the library. =–
Anonymous
some bare minimum at cut rule
Change 1: Original page describes the fan theorem as requiring the bar to be decidable, claims that the “classical” fan theorem contradicts Brouwer’s continuity principle. The latter claim is not true; I corrected the error. I have stated the result as two separate theorems: the decidable fan theorem, about decidable bars, and the fan theorem, about bars in general.
Change 2: Slightly more information is provided about the relationship between the Fan Theorem and Bar Induction. Eventually, we should make a page about the latter.
Change 3: the section on equivalents to the fan theorem has been fixed somewhat. The section originally asserted that all of the statements provided were equivalent to the decidable fan theorem; in fact, some are equivalent to the decidable fan theorem and some to the full fan theorem.
created a minimum at function monad (aka “reader monad”, “environment monad”)
I have removed the bulk of the Idea section that I had written, starting way back when the entry was created in 2013.
I kept the other material that Mike (Shulman) had written.
I see now that mine was really besides the point.
Now that I finally understand this topic more deeply, maybe I find time to write a better explanation of what’s really going on.
When I was about to create it for flat connection I notice that we already did have Riemann-Hilbert correspondence. So now I have cross-linked it with flat connection, flat infinity-connection, local system, Riemann-Hilbert problem and the latter with Hilbert’s problems
I tried to implement the connection between D-modules and quasicoherent sheaves a bit more
added to D-module the alternative definition in terms of quasicoherent sheaves of the deRham space
added to deRham space accordingly a pointer to D-modules (also fixed wrong notation in the formulas there)
added to quasicoherent sheaf at the very bottom a pointer to D-modules.
This needs improving. Notably good references should be given.
I am starting something at six operations.
(Do we already have an nLab page on this? I seemed to remember something, but can’t find it.)
Added two propositions about the general case of monoids and comonoids in a closed monoidal categories. It looks that it could work in such a general context and thus be used in models of linear logic or in differential categories, so that’s exciting. I’ll try to prove them.
in analogy to what I just did at classical mechanics, I have now added some basic but central content to quantum mechanics:
Quantum mechanical systems
States and observables
Spaces of states
Flows and time evolution
Still incomplete and rough. But I have to quit now.
Wikipedia has a nice article on quantum operations.
The nLab also had a page quantum operations and channels (cache bug?), but I’ve renamed this to simply quantum operation since a quantum channel seems to be nothing but a quantum operation when viewed from the perspective of quantum information theory. Eventually, this page might need some disambiguation since there may be several uses of the term, but for now I think it is “ok”.
I think this page can be cleaned up. I started, but don’t think I will be able to finish.
In particular, there is some background material that might be better on separate pages. I’ll continue trying to clean things up, but family might be calling soon and I’ll need to run quickly whatever state it is in.
I also made the simple statement
In quantum mechanics, a quantum operation is a morphism in the category of density matrices
at the beginning of the Idea section motivated by O’Loan’s comment
A quantum channel is a mapping which sends density matrices to density matrices.
This seems innocent enough, but someone might check the statement. For one, I’ve never seen a category of density matrices, but the idea seems obvious enough. Maybe a word on density matrix would be good.
I started a bare minimum at quantum probability (redirecting noncommutative probability space etc.)
Some entries have long been secretly referencing such an entry, and I have cross-linked accordingly, for instance from von Neumann algebra and quantum computing.
I had the feeling somewhere we already had a detailed account of probability theory dually in terms of von NNeumann algebras, but if we do I didn’t find it(?)
a stub for the moment, to go alongside noise and quantum error correction
now creating this entry.
The technical material under “Details” (here) is copied over from what I had written at reader monad – Examples – quantum reader monad. (There may still be room left to adjust the wording in order to reflect that this material moved to a new entry.)
To this I have now added an Idea-section (here) which highlights the relation to (equivalence with) Bob Coecke’s “classical structures” (which term I made redirect to here now)
