I take issue with the article on Linear Logic in the nLab. It says:

(In this way, linear logic has a perfect de Morgan duality.) The logical rules for negation can then be proved.

While this is true for *Classical* Linear Logic, for Intuitionistic Linear Logic things are very different and I feel that this whole 'dark side of the moon' is being thrown away for no good reason. There is no reason to decide that Classical Logic is better than Intuitionistic Logic and there is not reason to decide that Classical Linear Logic is better than Intuitionistic Linear Logic. the article should have a discussion of both realms. How do I go about adding this discussion, please?

thanks

Valeria ]]>

I just came across why (infinity,1)-categories?. Since the bulk of it was written 10 years ago, it could probably use some updating.

]]>Maksym Sokhatskyi announces that he is offering payment of

$$400/month$to anyone doing the job of adding to the $n$Lab, upon request, exposition and explanation of various basic mathematical topics, as needed by a community of type theorists looking into formalization of mathematics.

Concretely, there is demand for adding exposition/explanation to relevant $n$Lab pages of more basics of differential geometry formulated in terms of differential forms and de Rham calculus, than can currently be found on the $n$Lab.

See his

$\phantom{AAAA}$**Sponsorship call for submissions**

and be sure to email him at `maxim@synrc.com`

for details of the arrangement.

$\phantom{A}$

(This has grown out of a discussion where somebody else had complained about some $n$Lab page not providing useful examples, and me suggesting that you can’t complain about the the scope of work that is made available by volunteers unless and until you are paying for it.)

]]>Often when I am browsing the nlab my mouse will however over a sidebar and it will appear suddenly, this changes the positioning in the text. I know that clicking on it will keep it open but it can be a bit annoying especially when your mouse moves quicker than you intend. Its not exactly obvious that clicking on it will keep it open either. I propose something like a [Show] button, like the ones on wikipedia. That way we can expand the side bar when we want to clearly, I am not so sure what the utility of the mouse hover is.

]]>It seems like there’s some confusion in the definition section of the 2-limit page – it asserts the existence of a pseudonatural equivalence $K(X,L)\simeq Cat^\mathcal{C}(J,K(X,F-)),$ but these are hom-categories and not 2-categories themselves so pseudonatural transformations aren’t defined on them. The two obvious routes I see to rectify this are to require the equivalence on the full $2$-categories instead of the hom-categories, or to promote the hom-categories to discrete $2$-categories, but I’m not sure which (or if either) is implicitly intended. Any clarification is greatly appreciated.

]]>At the very least the pages all curently feel circular when trying to learn what exactly a 2-functor is, with [[pseudofunctor]] the only page really providing any accessible definitions (but they are very nice and explicit).

I have the various definitions and diagrams latexed up in my own notes (using xypic syntax) and would copy-paste them in and rewrite/merge the pages myself (assuming there are no objections) but I'm not sure which levers to pull on the nLab to merge/delete pages, or if a lowly browser like me even has such powers. ]]>

What is the most up-to-date and elegant way of writing tables on the nLab? I’m thinking of something similar to the one appearing at periodic table. Shall I just copy from the way it is done there?

]]>Hello. I would like to create a page about valuations, the concept in measure theory, which is distinct from valuations in ring theory. Is there an nlab-equivalent of Wikipedia’s disambiguation pages? Or what is the practice here, in case two concepts have the same name?

Thanks.

]]>Question : Let $P(M,G)$ be a principal $G$ bundle. How does connection on $P(M,G)$ defines a functor $\text{Hol}: \mathcal{P}_1(M)\rightarrow BG$ (here $BG$ is the Lie groupoid whose morphism set is $G$ whose object set is $\{*\}$).

I have seen in some places that, giving a connection on $P(M,G)$ is giving a map $P_1(M)\rightarrow G$.

Here $P_1(M)$ are special collection of special types of paths. This is the morphism set of what is called the path groupoid of $M$, usually denoted by $\mathcal{P}_1(M)$ whose objects are elements of $M$.

Once this is done, seeing the Lie group $G$ as a Lie groupoid $BG$ (I know this is a bad notation but let me use this for this time) whose set of objects is singleton and set of morphisms is $G$. This would then give a functor $\mathcal{P}_1(M)\rightarrow BG$. They say giving a connection means giving a functor $\mathcal{P}_1(M)\rightarrow BG$ with some good conditions.

Then, to make sense of $2$-connections, they just have to consider $\mathcal{P}_2(M)\rightarrow \text{some category}$.

This is the set up.

I do not understand (I could not search it better) how giving a connection on $P(M,G)$ gives a map $\text{Hol}:P_1(M)\rightarrow G$. For each path $\gamma$ in $M$ they are associating an element of $G$ and calling it to be the holonomy of that path $\gamma$. They say it is given by integrating forms on paths.

All I know is, a connection on $P(M,G)$ is a $\mathfrak{g}$ valued $1$-form on $P$ with some extra conditions.

Suppose I have a path $\gamma$ on $M$, how do I associate an element of $G$? Is it $\int_{\gamma}\omega$? How to make sense of this? It is not clear how I should see this as $\omega$ is a form on $P$ and $\gamma$ is a path on $M$.

To make sense of this, there are two possible ways I can think of.

- I have to pull back the path $\gamma$ which is on $M$ to a path on $P$. So that both the differential form and path are in same space.
- I have to push forward $\omega$ to a (collection of) form(s) on $M$. So that both the differential form and path are in same space.

Given a path $\gamma:[0,1]\rightarrow M$ with $\gamma(0)=x$, fix a point $u\in \pi^{-1}(x)$. Then, connection gives a unique path $\widetilde{\gamma}$ in $P$ whose starting point is $u$ such that projection of $\widetilde{\gamma}$ along $\pi$ is $\gamma$. The problem here is that we have to fix a point $u$. Only then we can get a curve. It can happen that for any two points on $\pi^{-1}(x)$ may give same result but I am not sure if that is true. I mean, let $\widetilde{\gamma}_u,\widetilde{\gamma}_v$ be lifts of $\gamma$ fixing $u\in \pi^{-1}(x)$ and $v\in \pi^{-1}(x)$ respectively. Does it then happen that $\int_{\widetilde{\gamma}_u}\omega=\int_{\widetilde{\gamma}_v}\omega$?

Even if this is the case, **what does it mean to say integrating a $\mathfrak{g}$ valued $1$-form on a path?** How is it defined? I guess it should give an element $A$ of $\mathfrak{g}$ (just like integrating a $\mathbb{R}$ valued $1$-form along a path gives an element of $\mathbb{R}$). Do we then see image of $A$ under $\text{exp}:\mathfrak{g}\rightarrow G$ to get an element of $G$? We can declare this to be $\int_{\gamma}\omega$.

**Is this how we associate an element of $G$ to a path $\gamma$ in $M$??**

Otherwise, given $\omega$ on $P$, using trivialization, we can get an open cover $\{U_i\}$ of $M$ and get forms $\mathfrak{g}$ valued $1$-forms $\omega_i$ on $U_i$ with some compatibility on intersections.

We can consider $\gamma_i:[0,1]\bigcap \gamma^{-1}(U_i)\rightarrow U_i$. These $\gamma_i$ are paths on $U_i$ and $\omega_i$ are $1$-forms on $U_i$. So, $\int_{U_i}\gamma_i$ makes sense. This gives a collection of elements $\{A_i\}$ of $\mathfrak{g}$ and may be all these comes from a single element $A\in \mathfrak{g}$ and seeing its image under $\text{exp}:\mathfrak{g}\rightarrow G$ gives an element in $G$. We can then declare it to be $\int_{\gamma}\omega$.

**Is this how we associate an element of $G$ to a path $\gamma$ in $M$??**

Any comments are welcome.

I could not find a place where this is discussed in detail. So, asking here.

]]>I came across this whilst browsing, I think it is in need of some formatting. I do not have time right now so I am dropping it here for you to see. Checkout equivariant sheaf

]]>I seem to notice the all pages tab loading much faster. Was something changed?

]]>I want to add something to the page https://ncatlab.org/nlab/show/Chern-Weil+homomorphism

I want to give an out line of how Kobayashi and Nomizu (page 293, volume 2) describes Weil homomorphism.

Is that OK to do so?

]]>It seems to me that the definition \Omega-groups [[Omega-group]] in the n-lab page is not correct, since in the original definition given by Higgins in

P. J. Higgins, "Groups with multiple operators", Proceedings of the London Mathematical Society, 1956

there is no request for the additional operations to distribute over the group operation. The actual definition given in the n-lab is closest to the notion of categories of interest, in the sense of G. Orzech.

In fact, both those notions are of interest and perhaps both of them should be dealt with in the n-lab.

I was going to edit the page, but I preferred to share this comment before doing it.

Best,

Beppe. ]]>

Suppose C is a category, with a given multiplicatively closed set of morphisms S ⊆ C. The role of the denominator conditions on S is rather similar to the role of a Quillen model structure on C, for which S is the set of weak equivalences. However, the precise relationship between these concepts is not clear to me.

This question is included in the book

Derived Categories

3rd prepubllication version: https://arxiv.org/abs/1610.09640 v3

In more detail: in Example 6.2.29 in the book I discuss the derived category of commutative DG rings. The main innovation is that there is a congruence on the category of comm DG rings by the quasi-homotopy relation. The passage from the corresponding homotopy category to the derived category is a right Ore localization. (There is a similar story for NC DG rings, but another homotopy is used to formulate quasi-homotopies.) The question above is Remark 6.2.30 there.

This issue is also touched upon in my paper

The Squaring Operation for Commutative DG Rings

https://www.math.bgu.ac.il/~amyekut/publications/squaring-DG/squaring-DG.html

and in the lecture notes

The Derived Category of Sheaves of Commutative DG Rings

https://www.math.bgu.ac.il/~amyekut/lectures/shvs-dgrings/abstract.html

If participants of the forum have some ideas on this matter, I would like to hear them, and maybe also mention them in my book.

Amnon Yekutieli ]]>

I don’t know what’s up, but the page “Join of Simplicial Sets” seems to have been blanked by an anonymous user.

https://ncatlab.org/nlab/show/join+of+simplicial+sets

]]>The HoTT book establishes a way to “informally” discuss HoTT. This is not entirely obvious to outsiders that this is a well defined notion. I would like to create an article, where I can point readers if they are feeling unsure about the informal language. I will probably call it something like “informal HoTT”.

I am unaware of any literature arguing that this is a good idea (apart from the HoTT book).

This came up whilst looking at the article functor (homotopytypetheory), I think Urs had added the formal definition. Now I would argue that this is completely pointless because the informal language can be “converted” directly into the formal notion. Not to mention that this whole philosophy is completely irrelevent to someone looking up the definition of a functor in HoTT.

I would like to hear your opinions on how we might go about this.

]]>I added a table to homotopy groups of spheres (homotopytypetheory) a while ago. Looking back it is looking very bleak. Is there a way I can add some colour to break it up a little?

]]>For some reason, I checked just now that the first revision to the nLab was made on the 28th of November 2008. So this date may serve as the 10th birthday of the nLab, if people wish to mark it in some way!

I am not quite sure when the first edit with significant mathematical content was made. The page classifying topos was one of the earliest created, but there was not any serious content on it for a while.

]]>I have added the page Rezk completion (homotopytypetheory) which gives us a lot of links to fill. I will pretty much try and add all of chapter 9 to the wiki but I welcome any help. Note that there is an (indexing) page Category theory in HoTT (homotopytypetheory) so make sure to add it there.

]]>It’s come up time and time again that HoTT Wiki and nlab should be more linked or less linked. I have created this post to finally settle the issue.

I personally propose that HoTT wiki stands on its own, and can also link to the nlab. But it shouldn’t rely on the nlab to explain things. I believe the (not explicitly mentioned) point of HoTT Wiki is to be an accumulation of mathematics in HoTT and essentially a proof of concept. It has the potential to have a much wider reach than the HoTT book can (for obvious reasons) and I forsee it being a useful tool for researchers in HoTT as reference and knowledge.

This doesn’t come without issues however: nlab has a vast amount of content on HoTT and this would cause a lot of duplication. Especially in the future when newer articles are added to HoTT wiki and not to nlab. But part of this issue is because HoTT wiki is in its infancy, thus nlab cannot really rely on linking to it.

Another point I want to make is that HoTT wiki shouldn’t necesserily be about the npov. But rather doing mathematics with oo-groupoids. There is of course a lot of potential for HoTT to interact with the npov and I think that should really be the subject of nlab HoTT rather than the HoTT wiki.

Of course these are all my opinions and I would love to hear some ayes and neys on this subject. And for this post to serve as a future reference for those confused about this topic.

]]>This page would essentially survey results about algebraic topology in HoTT and homotopy groups calculated in HoTT.

I imagine an algebraic topologist who is interesting in doing homotopy theory, would find this page very useful with all known and used constructions etc.

Is anyone else in favour of this change? ]]>