In the page dependent sum type, the presented “term introduction rule” seems not really dependent, since the typing derivation of the second element is not aware of the first. I would expect $\frac{\vdash t:A\quad \vdash u:B[t/x]}{\vdash (t,u):\Sigma(x:A).B}$ which corresponds to what is presented in the text on positive and negative versions.

]]>At Gabriel-Ulmer duality we had a case of two links next to each other rendering without a gap, the first two in

I added a space with $\backslash :$, but this is rather wide. Maybe other browsers already see a gap.

Here on the nForum I do see the gap.

]]>This page is entirely blank at the moment. It would probably be better to simply redirect “inclusion functor” to “subcategory” and delete this page. I’ve added the redirect to “subcategory”, but the redirect doesn’t take effect while the original page still exists.

]]>In the crazy world of British academia we need to give evidence that work in our departments is having “impact” on the world, outside our subject and preferably outside academia. As you may imagine, it’s not always so easy to show rapid and significant impact in philosophy, since we tend to work on the time scale of centuries. I was wondering then if I could make a case that the nLab has made a difference. I know Urs was looking out for endorsements, and even has one pinned on his Twitter account.

What kind of evidence do we have for its impact? Could we gather it some place? We could put out a request on Twitter.

]]>On the nLab there are several links to a (nonexistent) page monoid object which are then redirected to monoid, while I think they should be redirected to monoid in a monoidal category, since we are talking about *internal* monoids. How can this be done systematically?

I’ve started a table on Google sheets of Grothendieck topologies on Sch. You should be able to add comments. This is by no means complete but I started with arXiv:1407.5782 and this comparison graph.

There are definitely a lot more coloumns to add but this is a start.

Eventually I would like to turn this into a table on the nlab, but it is easier to collect data on sheets for now.

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

]]>