Thanks for the alert. That’s really interesting.

]]>Re #79 and the superalgebra approach to the de Rham complex, I see that Buium uses this approach in arithmetic differential geometry. If you can see page 33 of his book, he points out that there is no de Rham calculus available, but he can then use the Lie superalgebra formalism.

]]>Ok, have put something in as Definition 0.17.

]]>Maybe we could say “co-quotient” for the fiber.

]]>Ok, so what could we have to parallel the comonadic “is what remains after taking away the piece of..” ? Or just drop it and have

]]>The

negativeof a monadic moment $\bigcirc$ is the fiber (nlab) of the unit map…

Yes. Maybe not “quotienting out” for the fiber. On the other hand if we do this on stable types, then the fiber of a morphism is of course also the cofiber of a shifted morphism.

]]>Since we don’t have an official definition for monads, can we just imitate def 0.13:

The

$\overline{\Box}(X) \coloneqq cofib(\Box X \to X) \,.$negativeof a comonadic moment $\Box$ is what remains after taking away the piece of pure $\Box$-quality, hence is the cofiber (nlab) of the counit map:

So how about this?

]]>The

$\overline{\bigcirc}(X) \coloneqq fib(X \to \bigcirc X) \,.$negativeof a monadic moment $\bigcirc$ is what results from quotienting out the pure $\bigcirc$-quality, hence is the fiber (nlab) of the unit map:

what do $\overline{\flat}E$ and $\overline{ʃ} E$ mean here?

Sorry, my bad. Yes, as David says, I am using this sometimes to denote the homotopy (co-)fiber of the (co-)unit of the given (co-)monad. (Def. 2.7 in arXiv:1402.7041 or def. 0.13 here).

And the statement which I was referring to, that for a stable cohesive type $E$ the types $\overline{\flat}E$ and $\overline{ʃ} E$ have the interpretation of the (co-)closed $E$-valued differential forms is discussed in some detail at *differential cohomology diagram*. Unfortunately, there I write instead ${\flat}_{dR} E$ and ${ʃ}_{dR} E$ for these (co-)fibers.

is it provable synthetically that they are?

I haven’t tried. That would certainly be a worthwhile question to look into.

The key step in the proof would presumeably not be so much concerned with the nature of the differential forms as such, but with the interalization of the Dold-Kan corespondence: One will need way to turn a chain complex of stable types into a stable type and show that this construction behaves properly.

Once this is established the remainder should be immediate.

]]>For a comonadic modality

$\overline{\Box} X \coloneqq cofib(\Box X \to X).$(See Definition 2.2.14 of dcct.)

For a monadic one, it’s the fiber of the unit, though I’m not sure this is made explicit anywhere. It appears in the differential cohomology diagram in Proposition 2.2.17 at the same point in dcct.

Notation is certainly not consistent across nLab.

]]>Sorry, but what do $\overline{\flat}E$ and $\overline{ʃ} E$ mean here?

]]>Are either (1) or (2) an instance of $\overline{\flat}E$ or $\overline{ʃ} E$ (when restricted to closed or co-closed forms)? I mean, I presume so in the model, but is it provable synthetically that they are?

]]>That pullback is just the fiberwise $\sharp$

Ah, right. So that’s some improvement already! I bet you’ll see many more improvements. I wish I had time to further think about this stuff with you right now.

I don’t think we’ll try solid cohesion yet.

I understand, this was in reaction to David’s suggestion.

The punchline is just that if you do want to see explicit differential forms in a synthetic treatment (as opposed to just knowing that for every stable type $E$ the types $\overline{\flat}E$ and $\overline{ʃ} E$ behave like those of closed and co-closed $E$-valued differential forms, respectively ) then there are these two options:

axiomatize $D^1$ via a Kock-Lawvere axiom scheme and proceed in the established fashion – this works but is not elegant,

pass to solid cohesion, require that there is an object $\mathbb{R}^{0 \vert 1}$ such that the “rheonomy modality” $Rh$ is $\mathbb{R}^{0\vert 1}$-localization and then obtain the full de Rham complex in one go as

$\Omega^\bullet(-) \;\coloneqq\; \mathbb{R}^{ \left( (-)^{\mathbb{R}^{0\vert 1}} \right)}$

I am not saying that you should do (either of) this. On the contrary, I have been advocating all along the perspective that it is not urgent to consider a synthetic axiomatization of exactly the standard differential forms if we already have the “general differential forms” $\overline{\flat} E$ and $\overline{ʃ} E$.

This is maybe analogous to the story of Euclid’s synthetic axioms: There it is not too urgent to impose the parallel postulate, even if classical experience seems to suggest otherwise. On the contrary, it is useful to first prove things in more generality and only consider the axiom later.

]]>Re #75: okay, great, thanks. That pullback is just the fiberwise $\sharp$, so it has a nice type-theoretic interpretation if we regard the filtration as a tower of dependent types.

Re #77: that’s neat, but it’s turning out to be hard enough to write down a type theory for differential cohesion, so I don’t think we’ll try solid cohesion yet.

]]>Right, let me recall:

If we do have the “first oder infinitesimal interval” $D^1 = \{x \in \mathbb{R}\vert x^2 = 0\} \subset \mathbb{R}$ in hand, then there is the usual SDG Yoga: define microlinear spaces $X$, then say what it means for a map $T X \coloneqq X^{D^1} \longrightarrow \mathbb{R}$ to be fiberwise linear. These fiberwise linear maps $T X \to \mathbb{R}$ then are the differential 1-forms on $X$. Then one defines the wedge products and with this finally higher degree forms.

This is not very elegant, though, first of all due to that requirement to restrict by hand to fiberwise linearity. (Which is also why the “amazing right adjoint” $(-)_{D^1}$ to $(-)^{D^1}$ is not all that useful: $\mathbb{R}_{D^1}$ does not modulate differential 1-forms, only a sub-object $\Omega^1 \subset \mathbb{R}_{D^1}$ of it does, which takes work to carve out.)

If however we pass to the super-geometric version of $D^1$, the superpoint $\mathbb{R}^{0\vert 1}$, then this problem goes away: For every $X$ then the full type of functions $X^{\mathbb{R}^{0\vert 1}} \longrightarrow \mathbb{R}$ is, externally, the full de Rham complex of differential forms on $X$ (regarded as a super-space by its canonical $\mathbb{Z}/2$-grading of even/odd-degree forms). It even automatically knows the de Rham differential: that is given by the canonical action of the odd component of $Aut(\mathbb{R}^{0\vert 1})$ on $X^{\mathbb{R}^{0\vert 1}} \to \mathbb{R}$.

]]>It sounds like this is heading close to some of the issues appearing in that inconclusive discussion we had on FTC. Perhaps there is something there for eager young differentially cohesive HoTT-ers in Snowbird to develop, such as that intriguing idea that the solid cohesion of the super-world might be used to characterise constructions at the differential (elastic) stage. (But perhaps the solid modalities are for a later date.)

]]>Sorry, Mike, if I am being unclear. I see that the note in the Sandbox was a bit terse.

The general formula needs as input a type $A$ equipped with a filtration $A = A_n \to A_{n-1} \to \cdots \to A_0$, thought of as degreewise forgetting connection data (a “Hodge filtration”). Given this, then the concretification of $A$ on a geometrically contractible type $\Sigma$ is defined starting with

$A \mathbf{Conn}_0(\Sigma) \coloneqq [\Sigma, A_0]$ and

and then inductively

$A \mathbf{Conn}_{k+1}(\Sigma) \coloneqq im_{n-k}\left( [\Sigma, A_{k+1}] \to \sharp [\Sigma, A_{k+1}] \underset{\sharp [\Sigma, A_k]}{\times} A \mathbf{Conn}_k(\Sigma)\right)$.

]]>How does that formula apply generally? It uses the Deligne complex.

]]>That formula which I had pointed you to above (now here) gives the right answer for ordinary differential cocycles. That’s the only case for which we know a priori what the answer should be. So then from there one would be inclined to turn this around and take that formula, which now applies generally, to be the definition of differential concretification.

]]>The theorem involves differential concretification, and you said in #64 that your formula for differential concretification was wrong. Is there a correct formula for differential concretification that works for arbitrary cocycles?

]]>The result I was pointing to expresses the obstruction to a definite globalization of any (differential) cocycle, it is not specific to cocycles in Deligne cohomology.

]]>Can you say more, then, about what you were suggesting in #61 as a goal for formalization? If one of the main inputs to the result can’t be defined synthetically, what exactly would you like to see done synthetically?

]]>Right, so the boldface $G\mathbf{Conn}(X)$ is used for the moduli stacks of connections, while the $conn$-subscript on $\mathbf{B}G_{conn}$ denotes the classifying stacks. So $G \mathbf{Conn}(X)$ is to denote the concretification of $[X, \mathbf{B}G_{conn}]$.

I don’t know that these Deligne chain complexes may be defined synthetically. The argument in the Sandbox is less ambitious: It just means to show that there is a construction formulated abstractly using just cohesion (that def 3.1) which in the standard model applied to these chain complexes yields the expected result.

]]>Oh, no, wait, I see, it is something else, some chain complex. Can that be defined synthetically?

]]>