Do you happen have a more precise source for this than Francis’ note? It remains a little unclear what kind of “fibering” he is referring to, and what exactly the space $Map(M,N)$ is.

]]>Added mention of the fibration of $Imm^f(M,N)$ over $Map(M, N)$, where the fiber over $f$ is $Hom^{inj}_{Vect_M}(T M, f^{\ast}T N)$.

$Imm^f(M,N)$ is often studied as better behaved than $Imm(M,N)$.

]]>Added a subsection on the relation to formal immersions.

]]>made the definition a more detailed proposition (now here)

]]>Now is there any possibility of proving this with differential cohesive HoTT?

Sounds like a major research program. For comparison, the problems that I started to make a list of (here) are meant to be essentially “formalization ready”: We have a formal classical proof, or at least a detailed sketch of one. It’ still a bit of work from there to a computer checked proof, but at least there is a clear strategy.

Here you seem to be asking pretty generic questions, in comparison. Any questions relating to the actual smooth $n$-spheres will first need to solve the problem of narrowing in the synthetic language on the “standard model”, modeled on standard smooth manifolds.

As I had tried to say elsewhere, maybe one way to approach this is to impose the following axioms to differential cohesion:

ask shape to be homotopy localization at a homogeneous type $\mathbb{A}^1$ (as in Def. 4.8 in Felix’s arXiv:1806.05966)

ask for an identification $\flat(\mathbb{A}^1) \simeq \mathbb{R}^1_{Cauchy}$

require that composed with the counit $\mathbb{R}^{1}_{Cauchy} \simeq \flat(\mathbb{A}) \to A$ this respects homogeneous type structure.

Intuitively it seems that this should make $\mathbb{A}^n$-manifolds (Def. 7.1), hence in particular $n$-spheres, behave much like actual smooth $n$-manifolds, maybe enough so to prove some classical theorem.

]]>There is a constructive eversion via the Roseman moves of 2-knot theory. Scott Carter has more than one book discussing it, it is a beautiful topic. But I would be astonished if HoTT can express it.

I would love a proof assistant for knot theory, and would even try to write one, but I have no idea even in theory how to formulate a good syntactics that captures both local moves and less local considerations. Somehow the fact that diagrammatic knot theory lives in the plane, and the geometric manipulations that are possible in the plane, seem essential, and I have no idea how to capture this 2D aspect syntactically.

]]>Thanks for explaining!

Once the cache is there, they load quite quickly.

But that’s just what didn’t used to work: For long pages even the caching process was timing out, never producing a cached version. Anyway, it’s great that it works now.

There are a couple of slight gaps for the moment:

That’s okay. Better a little inconvenience for the author, than a fatal inconvenience for the readers.

Soon, probably tomorrow, I can fill these gaps and generate the rendered content for all pages.

Thank you so much!!

]]>I added mention of the result that the 2-sphere can be everted in 3-space.

Now is there any possibility of proving this with differential cohesive HoTT? A proof would give us a recipe for an eversion.

]]>This was my usual mistake when deleting a page manually, deleting in one table in the database and not another. Fixed. If I remember, I will put something in place to avoid getting a 500 in these cases.

]]>I tried on Firefox. It worked. I tried on Chrome i got the 500 nessage so I returned to Firefox… and got the 500 message. Finally I tried on Safari… 500.

]]>Latest Revisions is currntly giving me a “500 Internal Server Error” with both Firefox and Chrome.

]]>Actually around this time I was driving my family home through Østerdalen, so unfortunately cannot take any credit for this! The only thing I may have contributed to was that I tested the loading time for these pages a couple of days ago, which will have generated the cache for the pages. Once the cache is there, they load quite quickly.

However, your message spurred me to try to do something! I think I may have come up with something which works in the short term for speeding up page rendering, without requiring massive changes to the codebase. Take a look at Sandbox now. It should load quite quickly (minus MathJax), regardless of which browser you are on, and regardless whether a cache already exists. Whereas if you load geometry of physics – perturbative quantum field theory, it will take a couple of minutes if the cache does not exist.

What I have done is to tweak what happens when a page is edited or created, so that the rendered content is saved in a directory on the nLab server. The rendered content was in fact already generated as part of saving a page edit or creation, it just was not stored. When the page is loaded, there is now a check whether the rendered content exists, and if it does, this will just be loaded in verbatim.

There are a couple of slight gaps for the moment: if you make a link on a page A for a page B that does not yet exist, and then create the page B, the link on page A will not be updated until you make an edit (any edit); and similarly for imports (if you import page B to page A and make a change to page B, it will not be reflected in page A until you make an edit (any edit) to page A. Also for now there is no way to manually ask for the rendered content to be generated, one has to wait until a page is edited. Soon, probably tomorrow, I can fill these gaps and generate the rendered content for all pages. After that, I’ll push to github.

In summary, for now you will not see the benefit of the new rendering unless a page has been edited after now (or a few minutes ago).

The saving of page edits still takes a long time, because I am still using the old page renderer. I will get to re-writing it eventually, and actually filling in the gaps above will help contribute to that, but for now I was looking just to make some improvement without major changes to fundamental parts of the codebase.

]]>added mentioning of Gelfand duality as an example (here)

]]>added pointer to Porst-Tholen 91, section 4-c for Gelfand duality as the center of an adjunction between general (compactly generated Hausdorff) topological spaces and general (topological) complex algebras

]]>brief category:people entry for hyperlinking references at *topological algebra* and *Gelfand duality*

added pointer to Negropontis 71. I suppose, historically, that’s the origin of category-theoretic discussion of Gelfand duality?

]]>added pointer to Johnstone 82 and added remark that this discusses Gelfand duality with *real*-valued function algebras.

I am looking for a reference that makes explicit first the general adjunction between topological spaces and (star-)algebras, and then obtains Gelfand duality as the fixed point equivalence of this adjunction. I see lots of chat about this perspective, but what’s a citable reference that spells it out?

]]>I think Richard is in the process of fixing the huge rendering time issue! (e.g. try this or this)

That’s magnificent!

]]>replaced various occurences of “map” by more specific terms (bundle morphism, smooth function, continuous function)

Added plural redirect.

]]>I just realized that long ago I had already written out a proof that Aufhebung $\overset{\rightsquigarrow}{\Im X} \simeq \Im X$ implies that

$\overset{\rightsquigarrow}{\eta^{\Im}_X} \;\simeq\; \eta^{\Im}_{\overset{\rightsquigarrow}{X}}$Now reproduced here.

]]>Made a start here.

]]>Re #1, how does the concept of ’formal immersion’ fit in? This is

A formal immersion $F$ from $M$ to $N$ is an injective bundle map $T M \to T N$.

It seems to be easier to handle than the plain immersions, though in some case collections of each are weakly homotopy equivalent.

]]>That is bizarre! I can only think there is some javascript running on each key press, which seems bizarre. I’ll look into it when I get the chance.

]]>Tweaked the dashboard entry at Technical TODO list (nlabmeta).

]]>