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.
I have expanded logical functor by some stuff taken from the Elephant.
In the course of this I have created stubs for cartesian morphism, evaluation map and touched power object.
I have also done some editorial edits to topos (adding subsections and lead-ins)
As far as cartesian morphism there are two different universal properties in the literature, which are equivalent for Grothendieck fibered categories but not in general. In what Urs calls the “traditional definition” (but is in fact a later one) one has for every , for every , for every such that … there exist a unique da da da. This way it is spelled in Vistoli’s lectures. This is in fact the strongly cartesian property, stronger than one in Gabriel-Grothendieck SGA I.6. The usual, Grothendieck, or weak property takes for the identity, and the unique lift is of the identity at . Then a Grothendieck fibered category is the one which has cartesian lifts for all morphisms below and all targets, and cartesian morphisms are closed under composition. With the strong cartesian property one does not need to require the closedness under composition. Now a theorem says that in a Grothendieck fibered category, a morphism is strongly cartesian iff it is cartesian.
As far as evaluation map, I am not sure how much is the tension between evaluation map and evaluation morphism. I mean evaluation morphism is usually a thing in categorical setup like here; the same with coevaluation. When saying evaluation map it reminds me of the evaluation maps in analysis, with coherent states, on which I worked using this name, in noncommutative geometry and so on. For example, having a point of on a space, there is an associated evaluation map such that . This appears in the treatments of Gel’fand-Naimark theorem. Now, it is not only terminology, I think it is in fact useful to treat evaluations of that kind and categorical together. Why I think so. Well, the Gel’fand-Neimark is a reconstruction theorem. It uses evaluation functional at some point. Tannakian reconstruction uses Yoneda (at more than one point) which is also about evaluations, I mean taking into an object, this is an evaluation with values in sets, rather than in complex numbers as it is with Gel’fand-Naimark. In fact I think that every reconstruction theorem I know uses some sort of evaluation maps or evaluation functors and duality based on them.
Sorry, I had meant to say that I created cartesian functor. I did not touch cartesian morphism today!
It does not matter who and when has done what, the discussion items above stay under consideration :)
As far as cartesian functor, I will change it immediately. This definition is a very special case of the codomain fibration. Cartesian functor in general is the one which sends cartesian morphisms into cartesian morphisms.
Now the definition section is
A strong monoidal functor between cartesian categories is called a cartesian functor. More generally, a functor between Grothendieck’s fibered categories is cartesian if it sends cartesian morphisms into cartesian morphisms. The first definition then follows in the case of the codomain fibration for cartesian categories (with a choice of cartesian lifts to make them also monoidal categories).
I see various kinds of monoidal functors listed, but not strict monoidal functor. Strong is up to iso, strict is on the nose.
Urs, 3: By the way, in 2 I added a paragraph about evaluation maps possibly after you wrote 3. I do not know if you noticed it.
Thanks for the addtion to cartesian functor.
concerning:
the discussion items above stay under consideration
you often post comments like this here. I never quite know what to do with it. Why don’t you just add these remarks to the entries?
Concerning “evaluation map”: do you want to rename the entry to “evaluation morphism”? Fine with me!
you often post comments like this here. I never quite know what to do with it. Why don’t you just add these remarks to the entries?
I do not write into entries unless I have time and references to be fairly safe that I am not writing nonsense, or writing something what is against the opinion of the rest of the contributors. If I am just reacting on new posts in latest changes that by default means that I am not working on this right now, but just quickly read the news (I wish somebody would complementary react to those entries I really work on, usually my own latest changes reports get no feedback; like when I worked on D-geometry entries). Sometimes I do sacrifice my plan, and skip my ordinary work upon noticing I can improve things rather quickly and then switch to that task, but most often I do not change the whole schedule for that day, finding all the literature and so on to write a sensible something on what I find controversial, what somebody else now intensively works on (and hence will quicker incorporate input partly from me, in a way consistent with his grand plan) and where I just happen to know that there is another aspect, or that something is not quite correct and so on. I do not think that these remarks are good enough for the entries, nor checked upon the evidence. They could have entered entries as queries but there is now a dislike in nCommunity to add the queries.
Renaming evaluation map to evaluation morphism might be in the right direction, but I am not sure, I think we should eventually think on the comparison of various evaluation maps in mathematics and see if there is a possibility for a unique n-Perspective. I gave just some remarks which may help finding such.
Addition to 8 (Urs’s question what to do with my mathematical remarks is still puzzling me):
We are all routinely telling our mathematical opinions and questions on the things people currently work on (and which are not of our own concern now) and do some additions when we feel able to (and there are some minimal criteria for the latter!). The raw material from a distant memory scattered in bits and pieces is hardly good enough to enter it into nLab right away, but confident people (not me!) may be free to do more in this vain. If somebody else is on top of those entries one can make the use of these bits and pieces, or somebody can spot them later.
I am always happy when I get similar bits and pieces of feedback on entries I currently work on. The higher category theory is a new subject to me and I had far more education in very classical fashion and areas, including very classical approaches to physics (mainly predating string theory and supersymmetry) and algebra; ideally this could be quite complementary to typical contributions of super-modern n-people like Mike and Urs.
I never quite know what to do with it.
Urs, why would you do “it” ? There are many people and long future when some useful information in nForum can get used by somebody. Thus the things are left and open for consideration. You started using the phrase “just for the record” so what is worse in the phrase “under consideration” that I got labelled for using it (I think for the first time, anyway) ?
Hey Zoran,
sorry for causing this trouble. Of course we want to discuss stuff and I enjoy every single comment. But often you post definite-sounding statements that sound like they deserve to be in the corresponding nLab entry and then I just wonder why you don’t just include them there.
Maybe my statements sometimes sound far more definite as statements than I really feel about them…better take them more casually, as it is usually the case in my feeling. :) Edit: however I can do something about the cartesian morphism now.
I added to logical functor the statements and sketch-proofs of A2.3.8 and A2.4.8.
Can you say what the -version will be?
That’s an interesting question that I’m currently puzzling over; it’s not immediately obvious how to “preserve” the non-unique object classifiers. My best guess is that it’s a locally cartesian closed functor preserving finite limits and colimits (which implies that it preserves object classifiers) such that any morphism in is classified by the -image of some object classifier in . This implies that preserves the subobject classifier, so it’s at least as strong as the 1-categorical notion; it also includes all pullback functors.
However, there are some interesting divergences. For instance, I believe that a left adjoint of any logical -functor is automatically conservative, and hence identifies the adjunction with a pullback. In other words, the -version of an atomic geometric morphism is simply a local homeomorphism. There is some sense to this: for instance, the classical example of an atomic topos is for a group , which is not a slice 1-topos of ; but the corresponding -topos is the slice . Perhaps there is a tower of intermediate notions of -atomicity. But I haven’t completely wrapped my head around it yet.
I also don’t see how to prove that a logical -functor has a left adjoint iff it has a right adjoint. That worries me a little, although I might come to terms with it as just an accident of -impredicativity. Probably the opposite of an elementary -topos is not monadic over it either.
On the other hand, for interpreting type theory, we want the syntactic category of type theory to be the initial object in an -category of elementary -toposes with a specified tower of universes that are preserved (up to equivalence) by the functors. So there may be room for more than one notion of “logical functor”.
Re 14, Mike what do you have in mind when you say that F preserving (limits and? ) colimits implies that it preserves object classifiers ?
Being locally cartesian closed and preserving finite limits and colimits. That implies that it preserve the univalence axiom, and by an “object classifier” there I just meant a univalent morphism , i.e. such that pullback of is an embedding of into the core of the slice over .
1 to 16 of 16