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.
created cohesive topos.
wrote an Idea-section that is meant to explain why the concept is very natural, trying to provide some of the chat that one cannot find in the terse (but beautiful in its own way) article by Lawvere
spelled out the definition in some detail, here, too, trying to fill in things that Lawvere is glossing over, making it all very explicit;
started an Examples-section:
copied over the discussion that is a connected topos. checking the remaining axioms for cohesive topos are easy, but i have not typed that yet
included a little discussion of how diffeological spaces fit in, following our conversation in another thread
started an analogous section for , but just a stub so far
but added in a section that goes rgrough the various items in Lawvere’s definition and discusses their meaning in a cohesive oo-topos
Impressive…
I am very much impressed by what Lawvere is doing here. You can see that his article is a direct continuation of his thoughts that led to SDG and those expressed in his “Categorical dynamics”-lecture:
he is really at heart a physicists, in the following sense: he is deeply interested in the mathematical model building of reality. (See his intro where he talks about the “weatherman’s topos”!) He is searching for those structures in abstract category theory that do reflect the world. He is asking: What is a space in which physics can take place? Concretely: What is the abstract context in which one can talk about continuum dynamics? I gather even though he is an extraordinary mind, he did not push beyond continuum mechanics, otherwise he would also be asking: What is the abstract context in which quantum field theory takes place?
Now, because he is working so close to the fundamental root of everything, of course there is quite a distance from his “very fundamental physics” to the “fundamental physics” that most people will recognize as such. Which conversely leads to this interesting effect that you can see him try to find a dictionary between category theory and ontological concepts in philosophy. What is the precise abstract definition of space, quantity, quality etc? He gives definitions for all this. And I think the right ones (Though I still need to understand his definion of “quality”. I mean I follow the specific definition, but I do not see yet what it means .) Then he continues further towards the more tangible world, defining extensive and intensive quantities, as if writing a book on thermodynamics. And indeed, in his article on cohesion he uses all these analogies with heating and cooling! While one probably has to be careful with how to say these things in the (ignorant) public, but I think it is absolutely admirable how here a pure category theorists is actively working on unravelling the very foundations of reality. I was hoping for many years that more category theorists would see the immense applicability of the theory to theory-modelling in physics. As Lurie says rightly: “Category theory is not theory for its own sake, but for the sake of other theory.” And fundamental theoretical physics is all about scanning the space of theories for those that fit reality (as opposed to the physics that most theoretical physicists do, which is scanning the phenomena of one fixed theory.)
We can see that Lawvere is pushing in this direction, I think. Which is why I wanted to emphasize what his axioms for a cohesive topos are like if we generalize them to cohesive oo-topos . Because then out of the very same set of axioms springs a structure that all by itself gets even closer to being a model for physical reality: this is the point I kept emphasizing here and there: that just the assumption that we have an oo-connected oo-topos, and hence also just the assumption that we have a cohesive oo-topos (which implies the former) gives rise to a refinement of the intrinsic cohomology of the oo-topos (which is always there) to intrisic differential cohomology. In a better world I would walk over to Lawvere and try to tell him that that’s what models real-world physics fundamentally: a bare topos or oo-topos with its notion of cohomology is a context for kinematics (just the configurations, no forces, no dynamics) while differential cohomology encodes the forces and the dynamics. (In case this statement is raising eyebrows with anyone: let me know and we can discuss this in detail, look at examples, etc. This is an important story).
For instance the differential equations in a synthetic smooth topos that Lawvere considered around “Categorical dynamics” can be really understood without intervention “by hand” as coming from differential cocycles in the corresponding oo-topos. This is really what the theory of (derived) D-modules etc. is about. But even though it all flows by itself out of a general abstract source of concepts, unwinding it is a long story. I wish there were more people like Lawvere around, with his perspective on the general abstract basis of everything and at the same time with the overview over modern derived oo-topos theory and the understanding that the richer structure people are seeing in these is Lawvere’s observation that reality springs out of topos theory taken to full blossoming: reality springs out of oo-topos-theory.
This is beautifully written, Urs. I think you ought to contact Lawvere with your appreciation. He is likely to reply and have further enlightening things to add.
I agree with Todd and Zoran. This is very nice stuff.
The four adjoints of a cohesive topos and the structure they give rise to reminds me of the five monoidal structures on the category of Schur functors. (Not that there is any relation, just the rich and constrained structure is amazing to see)
You can see that his article is a direct continuation of his thoughts that led to SDG and those expressed in his “Categorical dynamics”-lecture
Is this available online somewhere? My google skills are notoriously bad.
I had a brief look, but it’s in an Aarhus report, which isn’t likely to be digitised in the usual channels. Maybe someone could get a scan? Also, it might be polite to ask Lawvere if it could be publicly distributed.
Unless I am misled, one of the conditions in the definition is redundant: the right adjoint in a local geometric morphism is always fully faithful (see C3.6.1 in the Elephant). As I noted at the other thread, being local is in general (i.e. for ) more than just the existence of , full faithfulness of being one of the equivalent versions of the extra condition, but connectedness of is another equivalent version which was already assumed earlier in the definition. So I removed that condition from the definition and made it a remark instead.
Todd,
thanks, I’ll think about that. Maybe I should first polish and streamline the entry on cohesive topos a bit more and put in the things I was thinking about (see below). Then I could ask him for advise about that.
Mike,
thanks, right, you said this before. Thanks for improving this.
Eric,
if memory serves the “Categorical dynamics”-text is not available online, but these lecture notes are which appear to cover a similar ground.
Everyobody,
not sure if I have enough time today, but my plan is to do the following
state a precise definition of cohesive oo-topos. The adjunction part is clear, but we need to think about how to interpret the clause that mentions monomorphisms. As we discussed elsewhere, the only really sane definition of mono in the oo-context is “regular mono”, the -limit over a cosimplicial diagram. I think with that definition what I say next will give the examples of cohesive oo-toposes that one wants to see.
take the various propositions and proofs that I filled into the Examples-section yesterday and streamline them as follows:
one should be able to give a simple definition of a “cohesive site” such that the category of oo-sheaves over it is a cohesive oo-topos. It should go something like this:
A cohesive site is
a concrete site;
with products;
such that the Cech-nerves of any covering family is degreewise a coproduct of representable;
(in view of the following condition this is the abstract way of saying that covers are “good covers”)
such that the simplicial sets (degreewise send every representable to the point) is a contractible Kan complex and such that (degreewise replace every representable by its set of points (using that the site is assumed to be concrete)) is equivalent to
(the first is saying that the objects in the site are “contractible” as seen by its topology, the seond is just the oo-version of the conditon on a concrete site, saying that the topology is compatible with the notion of concreteness)
I think that is
sufficient for showing that oo-sheaves on this site form an cohesive oo-topos
a set of conditions fulfilled by the kinds of sites we are interested in in the practice of modelling gros toposes.
But I will need to write this out now. I already mention it here in case anyone feels like offering help as I go along.
Okay, I spent some time with the entry:
created a subsection Sites of cohesion with essentially the above definition and the beginning of a list of examples;
worked through the propositions and proofs at oo-Topos over a site of cohesion,checking item-by-item that the oo-sheaf topos over a site of cohesion is cohesive.
I am running out of time now. My argument that the oo-morphisms are -regular monos was written a bit hastily. Right now I think it is correct, but I should go over it in more leisure later.
Also I haven’t yet typed the proof that commutes with powering by Kan complexes, but I think that’s obvious from the other discussion. I’ll type it up later.
This is certainly a form of metaphysics, in the best possible sense, working on the constitutive mathematical language in which physical theories must be expressed. Could #3 not go on the Cafe at some point? That might pull in some great mathematicians :).
By the way, without understanding things nearly enough (if only I didn’t have to spend time reading people’s ethics theses), am I hearing hints of what you said above in Sullivan’s Algebra, Topology and Algebraic Topology of 3D Ideal Fluids?
Could #3 not go on the Cafe at some point?
I am thinking about that. Need to run now to a colloquium dinner, after that I try to polish the discussion at cohesive topos a bit more, then I try to post something.
am I hearing hints of what you said above in Sullivan’s
Please give me a page number, I am too busy to read the whole article.
I have added the remaining propositions and proofs to cohesive topos.
Except for one: I noticed that checking is maybe not that easy after all. To start with I might have to think more about how the cartesian closure on -stacks is modeled in terms of simplicial presheaves. And once I have that, I need to probably start with a fibrant model for , then form in simplicial presheaves and then pass to a cofibrant resolution of that to be able to form the derived . Maybe it’s too late at night now for me, but at the moment I don’t really see anymore why I thought that would be easy to analyse.
- such that the Cech-nerves of any covering family is degreewise representable;
are you sure about this? Even for Cart this isn’t true, but degreewise a coproduct of representables.
That’s what I mean. Typo.
I fixed this in the above comment. But you are not supposed to be scrutinizing that comment. You are supposed to be looking at the entry cohesive topos instead.
I have now posted something over to the blog: here.
Next I am trying to get a better feeling for Lawvere’s extensive quality and intensive quality . By def 4 it ought to be true that the terminal geometric morphism itself counts as in intentive quality.
Let me look at that in the -context. Then there is the following dictionary between Lawvere’s imagery and the identifications in -connected -toposes that I have been talking about:
let
What Lawvere calls the rarefied substance of is the map that I write from flat objects to objects (the forgetful functor from flat principal -bundles to the underlying -bundles).
What Lawvere calls the condensed substance of is the map that I write – the inclusion of as the constant paths into its path -groupoid.
What Lawvere calls the cooling map, the composite is the topologists’s inclusion .
It looks to me that for what he wants to say in section IV the -topos-perspective is really mandatory: he is trying to characterize infinitesimal objects now using the properties of a cohesive topos. Unless I am misunderstanding, his discussion there remains inconclusive: we hear “it seems clear that…”, and “weak infinitesimal nature…” and “surprisingly often…” .
But I think the situation is clear: in the -topos the map is – geometric realization. The objects in the kernel of are therefore cohesive structures whose underlying topologial space is the point. These are the infinitesimal objects. For instance take the infinity-Lie algebroids as discussed there, under they map to the realization of their space of objects.
So the “canonical intensive quality” that Lawvere speaks about, the full sub--topos on those objects for which (the “cooling map”) is an equivalence contains precisely those cohesive -groupoids which are “discrete up to an infinitesimal thickening”. For instance disjoint unitions of -algebras etc.
Notice that over at function algebras on infinity-stacks we are making this precise by finding full subcategories of objects in the kernel of and seeing that these are indeed -Lie algebroids.
the only really sane definition of mono in the oo-context is “regular mono”
Why is that? What’s wrong with monomorphism in an (infinity,1)-category? (Regular monos might be the right thing to take here—I don’t have any intuition for that, since in a 1-topos all monics are regular. But it seems to me that non-regular monos have some role to play in (∞,1)-topoi.
As I mentioned at the cafe, I created cohesive site to talk about the 1-categorical version. I still like the idea of moving the definition of “(∞,1)-cohesive sites” and proof that they give cohesive (∞,1)-topoi to a page like (infinity,1)-cohesive site – then the pages cohesive topos and cohesive (infinity,1)-topos can be more about the behavior of the topoi themselves.
okay, I started splitting things off: created
and tried to move the material appropriately. There is more to be done, but I have to quit now.
following the latest Café-discussion and so that the nLab definitions are not secretly inconsistent with Lawvere’s terminology but clear on where they differ, if they differ, I have
added two more paragraphs to the end of the Idea-section of cohesive topos, explaining the idea of the additional two axioms;
edited the definition such that all three groups of axioms have their own name:
cohesive topos
cohesive pieces have points
pieces of products are products of pieces
I changed “pieces of products are products of pieces” to “pieces of powers are powers of pieces” since that axiom is actually only about powers of a single space, not products of arbitrary families. (Have you figured out yet what property of a site ensures that property of a topos?)
I also reworded your reference to “the generic object of a cohesive topos” which confused me for a bit since it sounded like a reference to the generic model in a classifying topos.
Right, thanks.
No, I haven’t thought about that axiom any more. I need some motivation for this axiom before I have energy to think about it.
In Lawvere’s article, the “continuity”-axiom is invoked only once, in “Theorem 1” on page 4.
But right below that he remarks that with a little bit of homotopy theory, one could drop the continuity axiom after all!
The theorem 1 itself seems to be getting at something interesting: I suppose the “” is a typo for and we are to keep in mind the case where and are topological spaces, so that is homotopy-classes of continuous maps . So I guess we are to think of this as an indicating relations of cohesive toposes to localization theory. But as far as I follow what’s meant to be going on, I’d think that cohesive -toposes would do the trick in a better way. But maybe I am missing something.
I started an Examples-section simplicial sets. But really need to call it quits now.
I realize that I do not fully follow Lawvere’s proof of his theorem 2 when it comes to this bit
it follows that this subcategory is closed under arbitrary subobjects and arbitrary products and is hence by completeness epi-reflective;
I understand closure under subobjects. Not sure why it is closed under non-finite products. And not sure how to get the reflector from this.
Can anyone help me?
Can you translate the proof out of the language of “intensive quantities” and “quality types” into a statement about categories and functors?
Okay, I have now written down the statement and Lawvere’s proof in ordnary terms at cohesive topos – Properties.
I inserted markers
(....details....)
at all points where one should make the reasoning more explicit. Some of them I can fill myself. But some of them I am not sure about.
This here should be a way to see that is a reflective subcategory:
by definition it is the full subcategory on objects such that is an iso
that’s equivalent to saying that for all we have that is an iso.
that should be equivalent to saying that for all we have that is an iso
that would mean that is the category of -local objects for .
That implies that is reflective hence that is coreflective.
Oh, I only now see Mike’s latest reply over at the Cafe.
there should be a discussion of the following natural :
Question: for a cohesive topos, what is the condition (if any) on an object so that the slice is itself is cohesive?
It is easy to see that being connected helps (): that makes be connected.
Intuitively one expects that should imply that is local, but I am not yet sure (that ought to be easy to see, though).
Then what else? Intuitively I would expect that somehow needs to be “maximally non-concrete”. But not sure.
Then what else?
I think being a tiny object is sufficient for to be local (easy proof now at local topos). So if is both connected as well as tiny (or contractible and tiny in the -case), then satisfies all the conditions of a cohesive topos except that possibly may fail to preserve binary products (and nothing said yet about the extra axioms “pieces have points”).
I am trying to see if slicing cohesive -toposes over suitable objects can be used as an alternative route to derived geometry: if we start with a 1-localic cohesive -topos such as , then the slice over an -truncated object will be -localic. We know that for the corresponding derived geometry (-sheaves over the -site of simplicial smooth rings^op) it should be -localic. So possibly there is a slice over an un-truncated object that achieves this.
Possibly one could consider obects to slice over such as the -stack of all simplicial -rings (i.e. ) or the like. I don’t know, this is just to indicate what kind of idea I am after here.
added to the Definition-section of cohesive topos the remark that the dual of “pieces have points” is equivalently “discrete objects are concrete” (!)
For emphasis, I have expanded the above remark to the statement that precisely if a cohesive topos satisfies that extra axiom “pieces have points” then also its sub-quasitopos of concrete objects is cohesive.
have added material to the Properties-section at cohesive topos.
in Adjoint quadruples I state some properties of the quadruple of adjoints in the definition of a cohesive topos.
I spell out the proof that is epi for all precisely if is mono for all a bit more explicitly than Peter Johnstone does. This is a curious kind of exercise. It feels like doing th most trivial of computation, but without the right formalism. I guess it’s all a tautology with a suitable strng diagram calculus, but that this lives in 4d or something, where visualization breaks down.
Already a few days back I had added one further subsection Relations between the axioms, summarizing Johnstone’s observations.
I’m thinking that a lot of these properties/structures would be great in settings more general than topoi. For example, in pretopoi or quasitopoi (I know this is mentioned in the article), or even lextensive cartesian closed categories or similar. Certainly we can ask for the four adjoints, for ’pieces have points’ and ’pieces of powers are powers of pieces’ in much more general setting.
Similarly, for categories of simplicial objects in one of the above ’generalised cohesive categories’, there should be a generalisation of a cohesive (oo,1)-topos.
Yes, lots of things still to be done. In Axiomatic cohesion more general categories than toposes are envisioned. The restriction of the concept to toposes in the Lab entry is due to me. I find the point of view that the ambient context is a topos with possibly some non-topos subcategories of interest to be useful. But that should not stop anyone from going in other directions.
I have started a new section at cohesive topos, titled Internal modal logic. This is induced from discussion with Mike on the HoTT blog here, but still a bit experimental.
Do you have any sense that this will make any contact with what a philosopher understands by modal logic? There was discussion of a kind of modality in a category here.
In the course of brushing-up the references at allegory I came to Bob Walters’ blog and from there to his Como Category Theory Archive and there I found a link to a pdf with notes on that Como 2008 lecture by Lawvere on cohesive toposes, of which so far I only new a video of the first 10 minutes existed.
So I added links to these pdf notes to cohesive topos and to Cohesive Toposes – Combinatorial and Infinitesimal Cases .
(However, looking over these notes there is nothing much in there which is not also in Axiomatic Cohesion. While bornological spaces make an appearance, they are not put into a cohesive topos.)
Why does Lawvere see bornological spaces as so important? He often speaks of them?
I see here I mentioned that
Lawvere speaks in ’Volterra’s Functionals and Covariant Cohesion’ of bornology involving a notion of covariant cohesiveness.
I don’t know. In general I find that the collection of examples or non-examples that he gives for cohesion in his writings is not the one I would find most immediate for the presentation of the topic.
So what’s the conclusion on Lawvere’s axiom (b) (in [Axiomatic cohesion]), that “pieces of powers are powers of pieces”?
My view is that it should be dropped, because it is false for reflexive graphs (and hence, simplicial sets). Consider the following reflexive graph :
Obviously, is connected. But is not: there is no (finite) path connecting to . In some sense this is because is not fibrant; as soon as we can compose and invert paths, this ceases to be a problem.
Hm, good point.
Generally, I never arrived at a definite “conclusion” about these extra axioms, but after an initial interest I came to generally ignore them, and have not felt a loss since. But maybe there is something here which I have been missing.
Not to change the subject, but … Urs, I’m writting up something that talks a bit about -cohesion. I’m wondering what the right way is to reference your work on this. Is there a paper or preprint I can point to, or should I just refer to an nlab page? And if so, is there some accepted way to give references to nlab pages?
Hi Charles, thanks, interesting. I’d be most interested in seeing what you have to say!
I’d be grateful if you could give a citation like this:
Eventually I should post a version of this to the arXiv, but somehow that plan keeps getting postponed. The main definitions of cohesion however do appear scattered in various of my other articles. I’ll list a few, just for completeness, and since I am aware that I did a terrible job with publishing the theory as such (namely I didn’t, instead I published a bunch of articles with applications to QFT and string theory only).
The first time that the axioms appear in print, though without being very much amplified on (coauthor pressure ;-) is in
and then with full amplification in
Also the axioms and a quick survey on how they induce differential cohomology is in section 2.3 of
Thanks, Urs. I have nothing too fancy to say about the topic. Just some examples: global equivariant homotopy theory has cohesion all over the place, it turns out.
Which new nLab entries are needed then? Do these deserve separate entries?
There’s a book length treatment of the latter by Schwede, Global homotopy theory.
Mike mentioned Anna Marie Bohmann’s work on glabal equivariant homotopy theory here as a special case of enriched indexed categories.
Do these deserve separate entries? * global equivariant homotopy theory * global homotopy theory
I think, David, you answer your own question! Even if they are stubs for the moment, so I created them! … just as stubs global homotopy theory and global equivariant homotopy theory
But looking closer, what’s global about ’global homotopy theory’, if it’s not about being globally equivariant?
This book introduces a context for global homotopy theory. Here ’global’ refers to simultaneous and compatible actions of compact Lie groups. It has been noticed since beginnings of equivariant homotopy theory that certain theories naturally exist not just for a particular group, but in a uniform way for all groups in a specific class. (Schwede)
In fact, you are right in a deeper way, David. The objects seem to be presheaves of spaces or simplicial sets on some category. Generally with simplicial presheaves, the global model structures are those with weak equivalences defined objectwise whilst either the fibrations or cofibrations are similarly defined. To get the local model category structure you localise at a cover or hypercover, I think. Here in Schwede’s work the process is similar but the terminology is more or less reversed! (I may be wrong on this as I have not absorbed what he says yet.)
Continuing #51, I wonder if enriched indexed categories more generally support modalities.
@Tim, David is right, “global homotopy theory” is a shorthand (I think an unfortunate shorthand) for “global equivariant stable homotopy theory”. In particular a “global equivalence” or better “global equivariant equivalence” in this context is not an equivalence in a global model structure on simplicial presheaves, but is crucially a type of weak equivalence defining a localization in the usual sense.
I have taken the liberty of renaming the entries that you created to make this terminology explicit, then I have edited a bit. But let’s have dicussion of global equivariant stable homotopy theory in its own thread.
My day today is severely broken now anyway, so I can just as well stop pretending that I will do what I badly need to do and instead edit around a bit on the nLab.
So at cohesive topos I have now finally given the points-to-pieces transform its own dedicated section.
I have added cross-links to the differential cohomology diagram which involves the points-to-pieces transform in its bottom part.
I mentioned this before. it feels like it might be a hint of something to be uncovered. But I am not sure yet.
added to cohesive topos – Definition – Further axioms the statement of the Aufhebungsaxiom
Also added the comment that this is in some way dual to the condition that the shape of the terminal object is terminal.
Is anything known about inductive types in cohesive toposes? In particular, about the inductive types within the discrete objects? I guess this will be in part III of the elephant.
In http://arxiv.org/abs/1509.07584 I showed that some inductive types, like , are automatically discrete. I didn’t try to consider the general case.
I have filled in comprehensive details for cohesive toposes from cohesive sites (this section) and the example of smooth sets (this section)
(Previously there had just been placeholder-pointers for this material.)
I am developing this material in parallel as lecture notes in the chapter geometry of physics – smooth sets. Accordingly, this material is not meant to be optimized for being fancy, but for being instructive and explanatory. In this vein the discussion sticks to the perspective of the Cech groupoid for all matters of descent, in a way that is meant to ease the generalization to infinity-cohesive toposes over infinity-cohesive sites.
have been working (this section) on spelling out in full detail the points-to-pieces transform in its two incarnations (in the cohesive topos and in the base topos), their relation, and the equivalence of “pieces have points” to “discrete objects are concrete”.
Am mostly done, only remains to spell out the proof of Johnstone’s lemma 2.1 in detail. But I need to get dinner now.
Due to the additions there is now some redundancy with other paragraphs in the entry. Will clear them out.
now awake again. Of course the triangle itself commutes just by zig-zag, but we still ne to invert its morphisms in order to deduce the desired equation. Now fixed.
Finally I am close to writing an entry on “super differential cohesive toposes”, the third stage after “cohesive toposes” and “differentially cohesive toposes”.
I had long had the thought that more elegant terminology would be on the right of the following table
long name | short name |
---|---|
cohesive topos | cohesive topos |
differentially cohesive topos | elastic topos |
super-differentially cohesive topos | solid topos |
How much of an uproar would this terminology cause, if any?
The idea of the terminology is the following:
Where a cohesive topos allows, of course, to speak of geometry where all we know is that points cohere in a geometric way (“differential topology”)…
…in a differentially cohesive topos we know how to enhance this to form manifolds with G-structures, hence Riemannian metrics, hence Laplace operators, hence geometry with “elasticity” (as in hearing the shape of a drum)…
…and finally in a super-differential cohesive topos we know how to further enhance this to a something which in applications to physics is responsible for solidity of matter, whence “solid geometry”.
What I’d like to know is if any regular here would be very unhappy if I started an entry “solid topos”. The definition would roughly be: a topos equipped with adjoint modalities of the following arrangement:
To the originator of a concept comes the honour of naming it, I should think, so long as there aren’t good scientific reasons against their choice.
We’re typically imagining here a particular model of super formal smooth infinity-groupoids. Then there’s a super version of complex analytic ∞-groupoid. What other cases could be imagined? Is it possible that the rationale for ’solid’ only works in special cases?
Is it possible that the rationale for ’solid’ only works in special cases?
It is my hope that axioms for solid toposes with some extra nicety assumption could single out supergeometric models, or at least narrow in on supergeometry enough so that the result captures what is really essential about supergeometry.
This is a little vague, as I don’t fully understand it yet. Which is why I want to start developing more notes on it, that might help develop the thoughts.
My motivating observation here is the following:
The key aspect of superalgebraic infinitesimals is really that they know about first order infinitesimals among all higher order infinitesimals. Hence about tangent spaces inside jet spaces.
Namely the odd-graded subspace of any supercommutative superalebra consists entirely of first-order infinitesimals, and, conversely, this actually chjaracterizes supercommutativity:
If, in any associative algebra, and are first order infinitesimals (square to zero) then the condition that also any linear combination is still first order infinitesimal is equivalently the supercommutativity
Formally dually, this has to do with the fact that super-dimension of super Cartesian spaces adds under Cartesian product
while that of bosonic formal disks does not: Writing for the order-k infinitesimal disk in , we have
In terms of abstract modalities, this is related to the following:
In SuperFormalSmoothSets, we have,
the shape modality is given by localization at just (hence at all morphisms )
the “rheonomic modality” is also given by localization at just one object this way, the superpoint
in contrast to the infinitesimal shape modality, which requires localizing at all finite-order infinitesimal disks.
So I am thinking about the axiom that in a diagram for solid toposes, we require that shape and rheonomy are given by localization at single objects, respectively, which we then synthetically regard as the real line and the superpoint, respectively.
Not sure yet.
Then I am hoping that we can axiomatize first-order neighbourhoods inside formal neighbourhoods this way. This should be those subobjects of
hence, dually, those sup-objects of
which “contain the last factor”.
Not sure yet how to say this formally. I am trying to say here that the odd part of is lineary identified with that even part of which is spanned by the single generator of that last factor.
Ah, maybe I just want to consider
Hm, since I want to say “odd”, and I have a modality “even” , clearly I need its “determinate negation”, hence the fiber of its unit map
Then
is a bosonic first order infinitesimal disk, as desired! Unfortunately it is of some weird dimension .
Hi, Urs a bit of an aside but your comment
In SuperFormalSmoothSets, we have,
the shape modality is given by localization at just (hence at all morphisms )
the “rheonomic modality” is also given by localization at just one object this way, the superpoint
in contrast to the infinitesimal shape modality, which requires localizing at all finite-order infinitesimal disks.
is a very nice summary that answers some questions that I/we had when we were trying to add the elastic cohesion modalities. I wonder is there anywhere on the nlab that records it in such a nice way?
(The question I had was that in the mean-time before LSR is extended to dependent type theory if we could develop a sort of middle ground type theory in a similar fashion to Mike’s Real Cohesive HoTT where we define the coreduction modality as localization at all infinitesimal disks, defined perhaps by modifying SDG axioms. Then we would have one fewer modality to have to add to the judgmental structure of the type theory.)
Hi Max,
right, I will try to include a clear discussion of this in the lecture notes that I am writing this week.
But the first two statements are not meant to be deep, as they concern just the model I have in mind. Its site consists, by definition, of super formal Cartesian spaces of the form
for all and all finite dimensional nilpotent maximal ideals in a real algebra .
Since as well as , it is fairly immediate that the sheaves on this site that are local with respect to and/or are precisely the sheaves constant in these factors, and with standard arguments we have that the inclusion of the full subcategories on these has a left adjoint, and that establishes the localization.
The third point is more subtle, and I may have said it wrong above: While, as before, it is fairly immediate that it is sufficient to localize at all the for the respective local objects to form the reflective subcategory inclusion for infinitesimal shape, I don’t know if this is necessary.
One might hope that it would be sufficient to localize at just a single infinitesimal disk, namely
Is this localization still equivalent to localization at all the ? Currently I don’t really know. This would be important to sort out.
But let me ask you: Either way, how would that help you to construct infinitesimal shape, instead of axiomatizing it? It sounds like you are thinking about assuming the Kock-Lawvere axiom scheme. That should of course allow to construct infinitesimal shape, but then its the KL-axiom scheme that needs to be postulated, no?! Which seems much heavier than just axiomatizing infinitsimal shape right away?
Ok, I’ll try to clarify as best I can, but this is all pretty half-baked and I haven’t seriously worked on this in a while.
First, there is a question of whether we add in the modality by type theoretic introduction and elimination rules or by postulating various axioms inside another type theory. This is the difference between the modality being part of the “doctrine” or the “theory” in the terminology Mike Shulman has been using lately. How to add in infinitesimal shape or even the ordinary shape type via type theoretic rules is currently unkown, but would likely require adding additional modal contexts to Cohesive HoTT that correspond to their inclusion as subcategories/subfibrations. However we’re not sure how the structure of type dependency interacts with this: which modal types can depend on which others? LSR are working on solving this problem in a great generality.
So in the mean time what can be done? We can instead axiomatize the modality somehow. Here you are right that adding Kock-Lawvere axioms is not the easiest way to do this. We could instead just suppose that there is a modality internally, and this is essentially what Felix did in his thesis work on doing some elastic cohesion syntactically.
But we could also go further and try to axiomatize more elements of our intended model, in the same way that Real Cohesive HoTT does. It seemed to me like the Kock-Lawvere axioms would be an appropriate way to do that and we could get something close to an “extension” of Real Cohesion, though not exactly because we have to axiomatize the Reals as well because constructing the reals internally by Dedekind cuts produces a coreduced type. I’m not sure what the benefits of this would be for doing SDG, but it seemed like the hybrid approach in Real Cohesion had some benefits by using and to give statements of the “sharp” and “crisp” versions of the Brouwer Fixed Point theorem. Maybe a hybrid type KL Cohesion type theory would give us a nice formulation of some results in SDG but who knows. Finally, anything you do with a purely axiomatic modality would give you a theorem here as well.
Either way, the other two modalities ( and ) have to be added “type theoretically” because they are coreflectors like and so how to add them is still unclear, though this will hopefully be figured out by LSR soon.
Thanks, but please say again why imposing the KL-scheme would be better than imposing the modalities directly? That seems upside-down to me, but maybe I am missing something.
With Felix and Vincent I am finally starting to look into the semantic side of the formalization of G-structures again (I was distracted from this by over two years now, it seems). This made me realize a little subtlety that needs attention: When I formalized torsion-free G-structures in dcct (v2), I considered the condition that the G-structure on restricts to that of the model space for all . But Felix considered it for . This should not make a difference for ordinary manifolds, since these are concrete objects. But it could make a difference for supermanifolds, since they are not. I need to think about this, but I suspect we really do need the version with . Maybe that’ll be a good test case for modalities at different “layers” of the progressing interplaying with each other. But it will take me some time to get back to speed with this…
Re #72 and , infinitesimal shape, there’s a whole tower of orders of infinitesimal
There’s also something like a , as we discussed elsewhere:
Something completely different happens when we apply de Rham space formalism to contracting ∞-nilpotent neighbourhoods. Instead of quotients by actions of formal neighbourhoods of diagonals we get quotients by actions of germs of diagonals… Since in differential geometry there are many more orders of vanishing than just the finite ones, the infinitesimal theory we get here is much richer.
Are you able to single one of this out as the intended reference?
Sorry, what do you mean by “intended reference”? I am not sure what you are asking.
I was continuing the discussion from #67, #68 and #72. There’s always a balance when defining a concept which is to include a key example as to how restrictive to be. You evidently want the definition of ’solid topos’ to include super formal smooth sets/-groupoids with shape and rheonomy modalities as those localisations. But regarding infinitesimal shape, does the definition as is stands peg down which size of infinitesimal neighbourhood is being quotiented?
The narrowing-in on the models needs more thinking and experimenting.
But I seem to have abandoned the approach of asking for a hierarchy of -modalities, in favor of what looks more elegant to me: Use the supergeometric modalities to pick out the first-order infinitesimal neighbourhoods inside the formal disks.
So using we get a concept of infinitesimal neighbourhood (of unspecified order) and using we get a concept of sub-neighbourhood inside that. In the model by this is the first-order neighbourhood inside the formal neighbourhood. To axiomatize this, we could require that the comparison map is a proper subobject inclusion. Maybe we’ll come up with nicer way to say this.
These things need more exploration now. I have let them rest for maybe two years. But I might have a chance now to pick them up again.
We had had vaguely related discussion elsehwhere, about how supergeometry is all about knowing of first-order infinitesimals, as follows:
For the bosonic infinitesimal 1-disk we have that
but for the super-infinitesimal 1-disc we have ,
where on the right the differential forms appear as the polynomials of those functions on which are fixed on first order infinitesimals (fiberwise linear functions).
Re: 74
I think for the most part just axiomatizing the modalities would be easier since you’ve already done the work of figuring out what axioms they should satisfy.
Honestly, I’m not familiar enough with this stuff to predict what the benefits of taking the KL axioms as primitive and defining as localization would be. At the very least it would just give us a nicer type theory for SDG then just adding KL axioms to type theory without adding modalities.
Re #79
We had had vaguely related discussion elsewhere…
It looks like that was (at least in part) at Super-spectra, generalized cohomology, etc..
Hi Max,
re your request in #71
I wonder is there anywhere on the nlab that records it in such a nice way?
I have now written out in the lecture notes here, in full elementary detail, the proof that “shape” on the cohesive topos SmoothSet is given by -localization.
This may or may not cover what you were asking for. Let me know.
The argument for the -topos invokes the projective local model structure and observes that everything is (co-)fibrant enough that we immediately reduce to this 0-truncated argument.
The argument for -localization, in turn, is directly analogous. But I’ll spell that out, too, now, for completeness of exposition. [edit: now here]
Yes, Urs, that helps a lot. Let’s see if I understand. Being local reducing to just checking the makes sense because the are the objects of the site so everything is modelled on them. Then the inductive argument is just that being local at means all morphisms from are constant and so by induction all morphisms from are constant because they must be constant in each component, which makes it local for .
Then by what you said in 72, the reason this proof doesn’t carry immediately over to the elastic case is that the formal disks aren’t just for some .
I think there is one typo which is in (6) it says but should say
Okay, thanks for the feedback, glad it worked. (And thanks for spotting the typo, have fixed that now!)
Right, so for the , I am still unsure. We certainly have the statement that, on FormalSmoothSet, is given by localization at the class of all
where not only ranges, but also . It would feel gratifying if we could just use a single here, such as , but maybe we cannot.
I am thinking now that we may say at least that
and that this already serves to axiomatically capture the fact that knows about infinitesimals of arbitrary order. This may be all that matters, maybe.
By the way, I was wondering if good notation for a modality which is localization at an object would be
Too whimsical?
Of course it works less well with superscripts, such as …
Re #79, you expressed your hesitancy about relying on these facts back here:
…what is certainly true is that as we progress from cohesion – where non-closed differential forms only appear via a choice of Hodge filtration of the de Rham coefficient objects – to solid cohesion, then it is possible to require that the previously chosen Hodge filtrations are compatible with the concept of differential forms as seen by the supergeometry, hence it is possible to sharpen the axioms and leave less to human choice, more to the gods. However, making the connection formal seems not to be particularly elegant, as it involves going to function algebras etc. That’s why I am hesitant of phrasing it as an additional axiom.
Hi Max,
further re your request in #71, I have now written out the proof also for the homotopy-theoretic version of the statement:
now here at homotopy localization.
1 to 90 of 90