added pointer to:

- Fosco Loregian,
*Cohesion in Rome*, talk notes, Dec. 2019 (pdf)

Fixed error in “left adjoints preserve monomorphisms”

najliel

]]>Fixed error in “left adjoints preserve monomorphisms”

najliel

]]>Changed Sierpinksi to Sierpinski

Anonymous

]]>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*.

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.

Okay, thanks for the feedback, glad it worked. (And thanks for spotting the typo, have fixed that now!)

Right, so for the $\mathbb{D}$, I am still unsure. We certainly have the statement that, on FormalSmoothSet, $\Im$ is given by localization at the class of all

$X \times \mathbb{D}_V \longrightarrow X$where not only $X$ ranges, but also $\mathbb{D}_V$. It would feel gratifying if we could just use a single $\mathbb{D}_V$ here, such as $\mathbb{D}^1 \coloneqq Spec(\mathbb{R}[\epsilon]/(\epsilon^2))$, but maybe we cannot.

I am thinking now that we may say at least that

$\Im \lt L_{\mathbb{D}^1}$and that this already serves to axiomatically capture the fact that $\Im$ 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 $\bigcirc$ which is localization at an object $\mathbb{A}$ would be

$\bigcirc\!\!\!\!\!\!\!\mathbb{A} \,.$Too whimsical?

Of course it works less well with superscripts, such as $\bigcirc\!\!\!\!\!\!\!\mathbb{R}^{0\vert 1}$…

]]>Yes, Urs, that helps a lot. Let’s see if I understand. Being local reducing to just checking the $p_1 : R^n\times R^1 \to R^n$ makes sense because the $R^n$ are the objects of the site so everything is modelled on them. Then the inductive argument is just that being local at $R^0\times R_1 \to R^0$ means all morphisms from $R^1$ are constant and so by induction all morphisms from $R^n$ are constant because they must be constant in each component, which makes it local for $R^n \times R^1 \to R^n$.

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 $D^n$ for some $D$.

I think there is one typo which is in (6) it says $p_1 : R^n\times R^1 \to R^1$ but should say $R^n\times R^1 \to R^n$

]]>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 $\mathbb{R}^1$-localization.

This may or may not cover what you were asking for. Let me know.

The argument for the $\infty$-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 $\mathbb{R}^{0\vert 1}$-localization, in turn, is directly analogous. But I’ll spell that out, too, now, for completeness of exposition. [edit: now here]

]]>Re #79

We had had vaguely related discussion elsewhere…

It looks like that was (at least in part) at Super-spectra, generalized cohomology, etc..

]]>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 $\im$ 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.

]]>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 $[[\mathbb{D}^1(1), X],\mathbb{R}] \simeq C^\infty(T X)$

but for the super-infinitesimal 1-disc we have $[[\mathbb{R}^{0\vert 1}, X],\mathbb{R}] \simeq \Omega^\bullet(X)$,

where on the right the differential forms $\Omega^\bullet(X)$ appear as the polynomials of those functions on $T X$ which are fixed on first order infinitesimals (fiberwise linear functions).

]]>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 $\Im$-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 $\Im$ we get a concept of infinitesimal neighbourhood (of unspecified order) and using $\rightrightarrows$ we get a concept of sub-neighbourhood inside that. In the model by $SuperFormalSmoothSet$ 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.

]]>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/$\infty$-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?

]]>Sorry, what do you mean by “intended reference”? I am not sure what you are asking.

]]>Re #72 and $\Im$, infinitesimal shape, there’s a whole tower of orders of infinitesimal

$ʃ \lt \Im = \Im_{(\infty)} \lt \cdots \lt \Im_{(3)} \lt \Im_{(2)} \lt \Im_{(1)} \lt id.$

There’s also something like a $\Im_{germ}$, 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?

]]>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 $X$ restricts to that of the model space for all $x \colon \flat X$. But Felix considered it for $x \colon X$. 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 $x \colon \flat X$. 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…

]]>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 $\sharp$ and $\flat$ 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 $\Re$) have to be added “type theoretically” because they are coreflectors like $\flat$ and so how to add them is still unclear, though this will hopefully be figured out by LSR soon.

]]>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

$\mathbb{R}^n \times \mathbb{D}_V \times \mathbb{R}^{0\vert q}$for all $n,q \in \mathbb{N}$ and all finite dimensional nilpotent maximal ideals $V$ in a real algebra $\mathbb{R} \oplus V$.

Since $\mathbb{R}^n \simeq (\mathbb{R}^1)^n$ as well as $\mathbb{R}^{0\vert q} \simeq (\mathbb{R}^{0\vert 1})^q$, it is fairly immediate that the sheaves on this site that are local with respect to $\mathbb{R}^1$ and/or $\mathbb{R}^{0\vert 1}$ 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 $\mathbb{D}_V$ 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

$\mathbb{D}^1(1) \coloneqq Spec( \mathbb{R}[\epsilon]/(\epsilon^2) ) \,.$Is this localization still equivalent to localization at all the $\mathbb{D}_V$? 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?

]]>Hi, Urs a bit of an aside but your comment

In SuperFormalSmoothSets, we have,

the shape modality is given by localization at just $\mathbb{R}^1$ (hence at all morphisms $(\mathbb{R}^1)^n \to \ast$)

the “rheonomic modality” is

alsogiven by localization at just one object $\mathbb{R}^{0\vert 1}$ this way, the superpointin 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 $\Im$ 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.)

]]>Hm, since I want to say “odd”, and I have a modality “even” $= \rightrightarrows$, clearly I need its “determinate negation”, hence the fiber of its unit map

$\overline{\rightrightarrows} \coloneqq fib(\eta^{\rightrightarrows}) \,.$Then

$\overset{ \rightrightarrows }{\left( \overline{\rightrightarrows}(\mathbb{R}^{0\vert q}) \right) \times \mathbb{R}^{0\vert 1} } \;\simeq\; \mathbb{D}^{q!/2}(1)$is a bosonic first order infinitesimal disk, as desired! Unfortunately it is of some weird dimension $q!/2$.

]]>Ah, maybe I just want to consider

$FirstOrderInfin(-) \;\coloneqq\; \overset{\rightrightarrows}{[\mathbb{R}^{0\vert 1}, (-)]}$ ]]>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, $\theta_1$ and $\theta_2$ are first order infinitesimals (square to zero) then the condition that also any linear combination $c_1 \theta_1 + c_2 \theta_2$ is still first order infinitesimal is equivalently the supercommutativity

$\theta_1 \theta_2 + \theta_2 \theta_1 \;=\; 0$Formally dually, this has to do with the fact that super-dimension of super Cartesian spaces adds under Cartesian product

$\mathbb{R}^{0 \vert q} \times \mathbb{R}^{0 \vert q'} =\mathbb{R}^{0 \vert q + q'}$while that of bosonic formal disks does not: Writing $\mathbb{D}^n(k)$ for the order-k infinitesimal disk in $\mathbb{R}^n$, we have

$\mathbb{D}^n(k) \times \mathbb{D}^{n'}(k) \neq \mathbb{D}^{n+n'}(k)$In terms of abstract modalities, this is related to the following:

In SuperFormalSmoothSets, we have,

the shape modality is given by localization at just $\mathbb{R}^1$ (hence at all morphisms $(\mathbb{R}^1)^n \to \ast$)

the “rheonomic modality” is

*also*given by localization at just one object $\mathbb{R}^{0\vert 1}$ this way, the superpointin 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

$\overset{\rightrightarrows}{ \mathbb{R}^{0\vert q} \times \mathbb{R}^{0\vert 1} }$hence, dually, those sup-objects of

$\big( C^\infty( \mathbb{R}^{0\vert q}) \otimes C^\infty(\mathbb{R}^{0\vert 1} ) \big)_{even}$which “contain the last factor”.

Not sure yet how to say this formally. I am trying to say here that the odd part of $C^\infty( \mathbb{R}^{0\vert q})$ is lineary identified with that even part of $\left( C^\infty( \mathbb{R}^{0\vert q}) \otimes C^\infty(\mathbb{R}^{0\vert 1} ) \right)_{even}$ which is spanned by the single generator of that last factor.

]]>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?

]]>