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.
1 to 91 of 91
Warning: What follows is just trivia. But since we had related discussion here before, maybe I am excused to waste time with this.
Way back, we (maybe mostly Mike and me) had agreed on symbols for the three modalities of cohesion – – and seemed to have been happy with ever since.
Moreover, in the last months I have been stabilizing myself on writing and for the reduction modality and the infinitesimal flat modality of differential cohesion. The choice of works really well, I think, both with the “re” in “reduction” as well as with the intuitive meaning that the reduced types are what is real about a formal geometry. This suggests to use for one of the other two. It doesn’t really seem to work for the infinitesimal shape, but using it for infinitesimal flat seems okay.
In any case, that leaves the infinitesimal shape modality in need of a good symbol.
Originally (and still on several Lab pages) I had denoted it , alluding to the fact that it produces “infinitesimal path -groupoids”. I still think that’s a great way to think about it, but since finite shape has come to be called and also since now the other two differential modalities don’t carry an -subscript anymore, it feels a bit anachronistic now.
Better would be one single nice symbol for infinitesimal shape. Which one?
One idea I have is this: the modal types of infinitesimal shape in the slice over are precisely the (formally) étale types over . Maybe there is a nice 1-symbol reflection of “étale”.
And there is, of sorts: a ligature of the two letters “et” is what became “&”. Aren’t there also some other versions of a ligature of “et” somewhere in the common TeX collection of symbols?
Unrelated to your ét idea, but what about δ? It has connotations of infinitesimal variation (as in, variational calculus).
On https://en.wikipedia.org/wiki/Ampersand are mentioned some related Unicode ligatures like 🙰 and 🙲.
David, I’ll think about that. However the risk is that it looks like a differentiation operation, which is not really what infinitesimal shape is.
Mike, thanks. Unfortunately, all of these appear as boxes on my system, and hence probably on many other people’s system. Actually I like the look of “&” here, which (at least on my system) comes out as in this picture. I like this because it is most easily recognized as coming from “Et”.
In LaTeX, I see that
\it \&
comes out as a very curly symbol that still has some resemablance wit “Et”.
Huh, that’s funny; they look fine to me. Maybe I have better Unicode fonts installed than the average person? I would have expected European computers in general to be more Unicode-aware than American ones. Can you see 🙵?
The LaTeX \textit{\&} looks nice too; I guess it is to be attributed to the Computer Modern fonts. (WP says “The Computer Modern fonts replace it with an “E.T.” symbol in the cmti#(text italic) fonts, so it can be entered as {\it\&} in running text when using the default (Computer Modern) fonts.”) But we need to have something to use on the lab (and forum, and blogs, etc.) too.
This European computer saw all three as boxes.
Thanks, Mike. Yes, I know that I could install font packages that would make all this display. But after I did this twice on two computers once, I ran out of energy on the third, and on my handheld it didn’t work anyway. (The EU is notorious for standardizing cucumber curvature radii, but it’s much more shy when it comes to enforcing useful standards ;-)
But this italic ampersand is maybe good. To try it out, I have implemented it at infinitesimal shape modality. Does that look like a sustainable choice of symbols?
Well, I’m wary of using an ordinary ampersand (which is I guess all we have available in iTeX) as a unary operator; it looks pretty weird to me.
Okay, thanks for giving feedback. That’s what I was looking for. I’ll sleep over it. Further alternative suggestions are very welcome, too.
It’s frustrating because I do like the idea of an ampersand-like symbol, and the other funny Unicode symbols look perfect to me. (-:
Hm. I just googled around and downloaded and installed something. Still doesn’t work. Would have to google around more and install more, I suppose.
On the other hand, even if it displayed on your and on my system, we don’t want to be typing unicode numbers all the time. Already the shape modality is a pain in this respect.
What we’d need is a simple macro functionality on the nLab. Such that we could declare something like “\et” and specify that on systems with fonts available it should display as character #49541229464549 and otherwise as &
I can’t see the characters in #3 either, but they should be the ones labelled 1F670 and 1F672 on the second page of this pdf. These “ornamental dingbats” were apparently added to the Unicode standard in June 2014, which is probably why many of us can’t see them.
A simple global macro functionality would be awesome! Can we put in a request?
Global macros wouldn’t be too difficult to implement, I think, but I am not sure how to achieve the behaviour Urs mentioned in #11 (showing different characters based on browser support). That would have to be done client-side, while iTeX is compiled server-side. But I’ll think about it.
Global macros would already be quite excellent!
But, so what does a client have to do (to install) to see those ampersands?
I wish I knew!
Mike, what operating system are you using?
Ubuntu Linux
And RHEL, at work.
Strange. I’ve tried it on a machine running Linux Mint, which is closely related to Ubuntu. It might not be an operating system issue after all. But I have no idea what’s going on.
Another possibility might be the “Tironian et”:
http://www.fileformat.info/info/unicode/char/204a/index.htm
https://en.wikipedia.org/wiki/Tironian_notes#Support_on_computers
Unfortunately, it probably looks too much like a number .
@Mike: Good thing the number 7 hardly makes it into any articles on the nLab.
Good thing the number 7 hardly makes it into any articles on the nLab.
The number 7 is a key player in entries such as 7-sphere, quaternionic Hopf fibration, octonionic Hopf fibration, H-space, Hopf invariant one problem, G2-manifold, M-theory on G2-manifolds, etc.
Then there are D7-branes playing a pivotal role in the M/F-theory story, see the F-branes – table.
In many other articles the number 7 appears in lists labeled by low lying integers, such as homotopy groups of spheres, spin group, orthogonal group, Whitehead tower, etc.
Perhaps someone ought to write seven trees in one.
The Tironian et doesn’t look that much like a 7 to my eyes. It looks closer to (but still quite distinct). Meanwhile, those Gothic letters always seem to confound me (the first looks like an ; the second might be an , or might be a – I never seem to remember these things).
According to wikipedia,
Some applications … substitute the Tironian et with the box-drawing character U+2510 ┐, as it displays widely.
The Gothic letters are \Re and \Im, which were named I guess because some people use them for Real and Imaginary parts of a complex number. So the second is an (Urs is using it to stand for “infinitesimal”), but I agree that it’s often hard to identify Gothic letters.
What do you think, Urs, does ⁊ look too much like ? It may depend somewhat on the fonts people’s browsers are using.
What do you think, Urs, does ⁊ look too much like ?
I’d be happy with the look of it in itself, but of course only the most erudite of readers will feel reminded of “étale” when seeing “⁊” – a connection which I had hoped an Et-ligature would help to make.
I don’t know. Might it make sense to just wait… until the unicode characters that you suggested in #3 are more widely supported?
Or let’s come back to #4: The curious thing is that here on the nForum – but not on the nLab – the plain ampersand from my keyboard comes out just right (on my system at least), namely as the Trebuchet ampersand. If this works here, should it not somehow be possible to make this work more generally?
Testing an idea:
hmm, doesn’t really work. I was thinking you might be able to make a home-made ligature using an upright capital E and t, but I can’t get the forum to recognise \mathrm.
Of course I’m half-kidding about Gothic letters in mathematics, which have been around forever (and of course I can always, and did in fact, check up on the ones Mike explained in #25). More seriously, I will ask: what word beginning with R does the stand for, in Urs’s context? (And less seriously but truthfully: I did for the longest time think that the Gothic A was a U, and the Gothic P was a B.)
what word beginning with R does the stand for, in Urs’s context?
Reduction, in the traditional sense of reduced scheme. It is the symbol for the reduction modality.
I thought was a pretty good symbol for this, because besides alliterating the technical term of “reduction”, its pronounciation as “real part” harmonizes with the nature of reduced spaces: an infinitesimal thickening of a space is an etheral halo around its reduced part, invisible for any map into it out of a reduced space.
When writing a paper, of course, we should be fine as long as whoever is compiling the TeX file has the appropriate fonts installed.
In poking around regarding what the appropriate font might be, I now have a guess as to why the nice ligatures work for me and no one else: I have the Symbola font installed. Would anyone else care to try installing it and see whether that makes 🙰 display for you?
With that font installed, we can then get the character in a LaTeX document as well, as long as we compile with xelatex:
\documentclass{amsart}
\usepackage{fontspec}
\newcommand{\et}{\text{\fontspec{Symbola} ?}}
\begin{document}
\[ \Re \dashv \Im \dashv \et \]
\end{document}
with the appropriate UTF-8 character inserted after the fontspec command – the nforum software doesn’t seem able to handle that actual character. Unfortunately, arXiv and journals probably don’t have Symbola installed or support xetex.
Re #4, even if we could get that to work for everyone reliably, I would still prefer not to use any kind of ampersand as a unary operator.
We could, of course, just make it with an image file…
I installed Symbola on OS X 10.10.5 as per #30 and I can get the fancy ligature Mike’s been using.
I’m confused. #1 of this thread suggests using & or a version of it for infinitesimal shape, because its modal morphisms are the etale ones. But on various nLab pages it seems that I now see being used for the infinitesimal shape and & for the infinitesimal flat. Was there a switch at some point? What does & have to do with infinitesimal flat?
(In general I’m lacking in intuition for infinitesimal flat; what for instance does it do when applied to a reduced object like ?)
Hi Mike,
that’s true, at some point I switched to using for infinitesimal shape. I have to admit that I forget when this happened, but it’s now all over the place.
The rationale for writing some form of ampersand for infinitesimal flat came from this observation, showing that is formally étale for every .
On the poisitive side, my system finally shows me the unicode characters that you suggested in #3. I like them, especially the second one there.
Regarding intuition for infinitesimal flat, I am going entirely by the adjunction with infinitesimal shape, and the good intuition that I have for that (infinitesimal path infinity-groupoid).
I don’t have an explicit description for infinitesimal flat of reduced objects. Indeed I haven’t used infinitesimal flat much at all beyond the fact that its existence implies that infinitesimal shape preserves colimits.
If it’s ’just’ the infinitesimal version of , why can’t we use out intuitions from the latter? After all, from shape, one can see how infinitesimal shape goes.
Is it that passage to the infinitesimal version has lost flat’s right adjoint, so we’re thrown back on viewing infinitesimal flat through its relation to the left adjoint, hence just as some modification of coefficients necessary to make sense of the effect of infinitesimal shape?
Is there an intuitive reason why flat has a right adjoint, but infinitesimal flat doesn’t?
If it’s ’just’ the infinitesimal version of , why can’t we use out intuitions from the latter?
Yes, that’s what works for me. But for the plain flat modality one may develop two kinds of intuitions, and only one seems to generalize: On the one hand is the moduli space for finite flat parallel transport with coefficients in . On the other hand is the locally constant object on the underlying object of with its cohesion forgotten.
The former intuition generalizes: “infinitesimal flat X” is the moduli object for infinitesimal parallel transport with coefficients in .
That’s what i was referring to when saying we get the intuition on infinitesimal flat from its adjunction to infinitesimal shape.
and only one seems to generalize
My hunch was to link that to infinitesimal flat’s lack of right adjoint.
Is it easy to see how as
the locally constant object on the underlying object of with its cohesion forgotten
preserves colimits, where infinitesimal flat fails?
[Similarly, I remember looking but not finding an intuitive way to see why infinitesimal shape gets a left adjoint, when shape doesn’t have one.]
I don’t really buy the intuition of as an infinitesimal version of shape. The cohesive builds new equalities from continuous paths; in particular, it creates new higher -groupoid structure where there wasn’t any before. But doesn’t do that — it’s left exact, so it preserves -types for all . It makes more sense to me to think of as forgetting the existing infinitesimal directions entirely and then stipulating that the only infinitesimal directions are constant, dual to how forgets the existing infinitesimal directions and then stipulates that there are exactly the “canonical” ones induced from the smooth structure.
Formally, it’s the adjunction that’s analogous to , so in that sense is more like than it is like . Both and forget the cohesion and then add it back in universally; similarly, both and forget the infinitesimal directions and then add them back in universally.
I don’t really buy the intuition of as an infinitesimal version of shape.
While it’s true that some aspects of are crucially different from , this intuition is justified from crystals: Just like maps out of are modeled by parallel transport along finite paths, so maps out of a “de Rham stack “ are modeled by parallel transport along infintesimal paths (“crystalline cohomology”). For a quick reference see item (3) on p. 2 of Lurie’s note .
The reason that does not change the tuncation degree is because the infinitesmal paths are “too short” to wind around cycles.
Isn’t it the case that the modalities will reveal different similarities depending what you look for? Down that vertical central axis of the staggered version there are three localisations for kinds of dimension: .
Yes, that’s a good way to think about it. Where is shorthand for localization at all the infinitesimally thickened points.
I suppose maybe that’s helpful if you already know about crystals, but to me it just sounds more confusing.
There’s David Speyer’s introductory Three ways of looking at a local system: the infinitesimal perspective and his follow-up The infinitesimal site.
Let me rephrase that in a more productive way. If I don’t already know what crystals are, can I use my existing intuition that simply “declares the only infinitesimal directions to be constant” to understand crystaline cohomology?
(By the way, for anyone who doesn’t know, one of the groups at the HoTT MRC next month will be working on differential cohesive HoTT. The goal is basically to do for differential cohesion what BFP RCoHoTT did for continuous cohesion. Maybe this will result in my finally understanding differential cohesion!)
declares the only infinitesimal directions to be constant” to understand crystaline cohomology?
I’d think so. The key is to make that declaration propositionally, i.e. to impose the constancy not by saying that a step in an infinitesimal direction is equal to a constant step, but to say that there is a “path” connecting the two.
That’s what is described on that page in the note by Lurie that I pointed to.
(I believe (but never checked) that because these infintiesimal paths are so short that there is no further information in them besides their endpoints, hence because these infinitesimal paths are all straight edges that one imagines that all these infinitesimal meighbour points with all these straight paths connecting them look like a “crystal”.)
Anyway, just as cohomology with local coefficients is equivalently the cohomology of the shape of , hence of the infinity-groupoid of finite paths in , so crystalline cohomology is equivalently the cohomology of this groupoid of infinitesimal paths in .
By the way, for anyone who doesn’t know, one of the groups at the HoTT MRC next month will be working on differential cohesive HoTT. The goal is basically to do for differential cohesion what BFP RCoHoTT did for continuous cohesion. Maybe this will result in my finally understanding differential cohesion!
Felix Wellen had recently told me about this. I am (positively) surprised. There is no indication of this activity on the MRC page.
The public MRC announcement page isn’t going to change; the project assignments and so on are being done internally between the organizers and the participants.
I think I do now see that my intuition for needs some modification. I usually think about local toposes mainly in terms of cohesive and similar models, where a good intuition comes from thinking about concrete objects, where is monic. But it seems that it is more rare for to be monic. In particular, Felix just mentioned to the MRC group the interpretation of its kernel-pair as the relation “ is infinitesimally close to ”, whose equivalence classes are tangent spaces.
On the other hand, this example also makes me wary of the “shape” analogy for a different reason, namely that , unlike , is not usually going to be surjective either. (In particular, since is lex, but infinitesimally close points are not generally equal.) It doesn’t seem right to think of as “quotienting out infinitesimal paths” if can be inhabited even when is empty.
Here’s a suggestion for a related but perhaps better intuition. A good general intuition for in cohesion is “discontinuously ”, i.e. an element of that is not required to depend continuously on the context, and inherits only (co)trivial cohesion from . Similarly, could we say that means “infinitesimally ”, meaning an element of that is defined “up to infinitesimal variation in the context” and moreover ignores all infinitesimal differences in ? For instance, in the context of , we may not be able to inhabit , but if and are infinitesimally close then we can “almost” do so, and hence we can inhabit . And the second clause is similar to quotienting out infinitesimal paths, but perhaps makes it more clear that we shouldn’t expect to get any higher homotopy thereby.
namely that , unlike , is not usually going to be surjective
That’s right, in fact there is established terminology for this: If is surjective then is called formally smooth.
All objects are formally smooth in the differential geometric models such as formal smooth infinity-groupoids, but it is not generally the case in algebraic geometry. There one needs Noetherian-ness.
Here’s a suggestion for a related but perhaps better intuition. […] could we say that means “infinitesimally ”, meaning an element of that is defined “up to infinitesimal variation in the context” and moreover ignores all infinitesimal differences in ?
Sounds good to me!
That sounds like Curry’s idea that is an internalisation into a stricter system of what is true in a more relaxed (stronger) system. Neel Krishnaswami seemed to be reinventing that here.
I give (here) a simple analogous case in which all dogs have an (individual) owner, where that a dog is a ’possible’ pug means there is a co-owned dog which is a pug.
All objects are formally smooth in the differential geometric models
I was wondering about that. I don’t have any intuition for “global” objects (in the empty context) that aren’t formally smooth, but I guess that makes sense since I don’t have much intuition for algebraic geometry. But the example of shows that even in differential geometry this can fail in nonempty contexts, right?
From C^\infty-Differentiable Spaces
A differentiable space is formally smooth if and only if each has an open neighbourhood which is isomorphic to the Whitney subspace of a closed subset of some . (p. 124)
Now, given a closed subset of , the Whitney subspace is the differentiable subspace of defined by the Whitney ideal of all differentiable functions on whose Taylor expansion at any point is null.
@Mike,
this can fail in nonempty contexts, right?
That sounds right. I haven’t thought about this is non-empty contexts much.
@David,
the statement I am referring to, that is epi in the differential geometric model, is prop. 2.18 in arXiv:1701.06238.
I thought we were trying to think up non-formally smooth spaces in a differential geometric context. Doesn’t what I quoted suggest what would be need there for formal smoothness to fail?
we were trying to think up non-formally smooth spaces in a differential geometric context.
Oh, okay. So then first you need to specify a model of differential cohesion inside which to find such examples. Do you want a model still to be a topos?
Re #46,
The goal is basically to do for differential cohesion what BFP RCoHoTT did for continuous cohesion.
Since choosing an accessible, prominent target theorem, the BFP, was an important feature of that work, what might you choose as a target in the differential case?
Not sure; maybe Urs has some suggestions? The first step is to set up the type theory; depending on how difficult that is, it might take a lot of the week.
Felix Wellen is in the group, so he may be able to help us with goals to aim for too.
As you will know, Felix Wellen’s thesis will be the solution to the first of the list of formalization probems that I had advertized in Some thoughts on the future of modal homotopy type theory. The others listed there concern other modalities.
To my mind, the central application where everything about cohesion and differential cohesion in -toposes comes together is the theory of “infinitesimally integrable definite globalizations of differential cocycles” in section 5.3.13 of dcct (v2).
This is about fixing a differential cocycle on a cohesive group and then, given a “-manifold” (étale -stack modeled on ), ask for the obstructions to having a differential cocycle on all of which suitably restricts on the infinitesimal neighbourhood of each point to the given cocycle on , restricted to the infinitesimal neighbourhood of the neutral element.
This is the homotopy theoretic version of what Bryant calls definite forms, controlling for instance the theory of -manifolds.
Theorem 5.3.129 in dcct (v2) states that an obstruction to the existence of such globalizations is the existence of integrable -structure on the -manifold (the way Felix discusses at the end of his thesis) for the “quantomorphism” group of the given differential cocycles, namely the differential concretification of its automorphism -group.
I think this is an absolutely central statement to higher differential geometry, though its consequences need to be fleshed out further.
It’s remarkable how all the modalities interact here: shape and flat control the existence of the differential cocycle in the first place, sharp controls the differential concretification of its automorphism group and infinitesimal shape governs the concepts of -manifolds, definite globalizations and torsion-free -stuctures.
On the other hand, this theorem takes a fair bit of prerequisite definitions and lemmas. This will be a bit of work to formalize. But the effort would certainly be worth it.
Thanks!
sharp controls the differential concretification of its automorphism group
Is this the of or of ? I am currently rather confused about how these are related to each other, if at all.
You are right, something needs to be adjusted here. For the construction to come out as intended, it needs to be the sharp on . Otherwise the result is of the intended result.
I need to look into this.
Incidentally, my formula for the differential concretification using the operator also contained a mistake, in that it did not actually produce the claimed object in the model. This was thankfully pointed out to me by Alexander Schenkel and Marco Benini. We fixed the formula for the 1-truncated case in arXiv:1704.01378, and I fixed it for the general case in the Lab’s Sandbox (of all places). But then I got overwhelmed with other duties. I need to get back to this and eventually produce a coherent writeup.
What is the correct definition? I don’t see any ’s in prominence on the Sandbox.
Thanks. Is some of the notation confused there? Are the “conn” subscripts the same as the Conn boldface?
Oh, no, wait, I see, it is something else, some chain complex. Can that be defined synthetically?
Right, so the boldface is used for the moduli stacks of connections, while the -subscript on denotes the classifying stacks. So is to denote the concretification of .
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.
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?
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.
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?
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.
How does that formula apply generally? It uses the Deligne complex.
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 equipped with a filtration , thought of as degreewise forgetting connection data (a “Hodge filtration”). Given this, then the concretification of on a geometrically contractible type is defined starting with
and
and then inductively
.
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.)
Right, let me recall:
If we do have the “first oder infinitesimal interval” in hand, then there is the usual SDG Yoga: define microlinear spaces , then say what it means for a map to be fiberwise linear. These fiberwise linear maps then are the differential 1-forms on . 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” to is not all that useful: does not modulate differential 1-forms, only a sub-object of it does, which takes work to carve out.)
If however we pass to the super-geometric version of , the superpoint , then this problem goes away: For every then the full type of functions is, externally, the full de Rham complex of differential forms on (regarded as a super-space by its canonical -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 on .
Re #75: okay, great, thanks. That pullback is just the fiberwise , 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.
That pullback is just the fiberwise
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 the types and behave like those of closed and co-closed -valued differential forms, respectively ) then there are these two options:
axiomatize 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 such that the “rheonomy modality” is -localization and then obtain the full de Rham complex in one go as
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” and .
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.
Are either (1) or (2) an instance of or (when restricted to closed or co-closed forms)? I mean, I presume so in the model, but is it provable synthetically that they are?
Sorry, but what do and mean here?
For a comonadic modality
(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.
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.
what do and 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 the types and have the interpretation of the (co-)closed -valued differential forms is discussed in some detail at differential cohomology diagram. Unfortunately, there I write instead and for these (co-)fibers.
Since we don’t have an official definition for monads, can we just imitate def 0.13:
The negative of a comonadic moment is what remains after taking away the piece of pure -quality, hence is the cofiber (nlab) of the counit map:
So how about this?
The negative of a monadic moment is what results from quotienting out the pure -quality, hence 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.
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 negative of a monadic moment is the fiber (nlab) of the unit map…
Maybe we could say “co-quotient” for the fiber.
Ok, have put something in as Definition 0.17.
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.
Thanks for the alert. That’s really interesting.
1 to 91 of 91