At natural deduction it says

natural deduction with computation rules gives a formulation of computation. See computational trinitarianism for discussion of this unification of concepts.

But I don’t see anything at these links to help explain the role of the C in FIEC (formation-introduction-elimination-computation). Philosophers call the satisfaction of computation rules ’harmony’, and there’s some reflection on why this is desirable, and of course arguments against.

There should presumably be perspectives on this from the three corners of the trinity of trinitarianism. What can we say from the perspectives of computing and of category theory?

]]>As many of you know, the nLab is currently hosted on a server at CMU, financed by a grant for HoTT there. I am not sure how long there is to go on that grant, but I am not sure it is longer than a couple of years. I would suggest that it might be a good idea try to begin applying for some further grants fairly soon. How shall we go about this?

I am also a little bit worried about whether there are any backups of the nLab or nForum currently if the server at CMU is hit by lightning. To safeguard years of work, we need some good safety net in place. One option, if we have the money, is to use cloud storage, e.g. Amazon’s. Their set up is such that it is basically impossible that the data could be lost. It is pay per use, and a priori quite cheap, but if we host the actual database there, since it is up 24/7, costs might not be completely trivial. We could perhaps use the cloud only for backup, say once a day, and maybe use an S3 bucket rather than a database, which would be a lot cheaper, but still not completely negligible.

Another option is to try to initiate some kind of ’goodwill system’ amongst a collection of universities across the world to call our server once a day, say, to get backups of the data. We could have a minimal web application hosted at CMU which monitors these, so we know they are taking place.

]]>I see this appeared:

- Ulrik Buchholtz, Floris van Doorn, Egbert Rijke,
*Higher Groups in Homotopy Type Theory*, (arXiv:1802.04315)

Maybe there’s more at infinity-action to consider.

]]>Here is another stub: Albert algebra.

It would be nice to get a reference to clear up the number of (real) Albert algebras. John Baez's octonion paper, among other literature (including our Jordan algebra), takes it for granted that there is only one (which is true, over the complex numbers, but people are usually working over the real numbers). But John himself points out on a Wikipedia talk page that there are two (and that's what I followed).

]]>started something at *splitting principle*

(wanted to do more, but need to interrupt now)

]]>We had a paragraph on split ocotnions buried in the entry *composition algebra*.

In order to be able to link to it, I have given that paragraph its own entry, now *split octonions*. But this deserves to be expanded of course.

I am running into the following simple question and am wondering if there is anything useful to be said.

Let

$\mathcal{A} \in dgcAlg_\mathbb{Q}$be a differential graded-commutative algebra in characteristic zero, whose underlying graded algebra is free graded-commutative on some graded vector space $V$:

$\mathcal{A} = (Sym(V), d) \,.$Consider an odd-graded element

$c \in \mathcal{A}_{odd} \,,$and write $(c)$ for the ideal it generates.

In this situation I’d like to determine whether it is true that

there is an inclusion $\mathcal{A}/(c) \hookrightarrow \mathcal{A}$;

for every element $\omega \in \mathcal{A}$ there is a decomposition

$\omega = \omega_0 + c \omega_1$for

*unique*$\omega_0, \omega_1 \in \mathcal{A}/(c) \hookrightarrow \mathcal{A}$.

For example if $c \neq 0 \in V_{odd} \hookrightarrow \mathcal{A}_{odd} \hookrightarrow \mathcal{A}$ is a generator, then these conditions are trivially true.

On the other extreme, if $c$ is the product of an odd number $\gt 1$ of odd generators, then it is not true. For example if $c = c_1 c_2 c_3$, with $c_1, c_2, c_3 \in V_{odd} \hookrightarrow \mathcal{A}_{odd}$, then for instance $c (1 + c_1) = c (1 + c_2) = c$ and so the coefficient $\omega_1$ is not unique.

Is there anything useful that one can say in general?

]]>I have tweaked the Idea-section at *naturalness*, and I added a pointer to the first decent discussion that I have seen: Clarke 17

Ben Webster created *symplectic duality*.

See his message at the $n$Café here.

]]>created stub for *N=2 D=4 super Yang-Mills theory*…

… for the moment mainly such as to be able to make *Coulomb branch* and *Higgs branch* redirect to it, which are needed at *symplectic duality*

Over in another thread, David Roberts asks for explanation of a bunch of terms in QFT (here).

In reaction I have started a minimum of explanation for one more item in the list: *hidden sector*.

Over in another thread, David Roberts asks for explanation of a bunch of terms in QFT (here).

Here I started a minimum of explanation for one item in the list: *protection from quantum corrections*.

Over at structure sheaf I saw this uncompleted sentence: “In particular for $\mathbf{H}_{th}$ an”

What is the rest of that supposed to be?

]]>started a minimum for *integral Steenrod square*

at Bockstein homomorphism in the examples-section where it says

$\mathbf{B}^n U(1) \simeq \mathbf{B}^{n+1}\mathbb{Z}$I have added the parenthetical remark

(which is true in ambient contexts such as $ETop\infty Grpd$ or $Smooth \infty Grpd$)

Just to safe the reader from a common trap. Because it is not true in $Top \simeq \infty Grpd$. The problem is that in all traditional literature the crucial distinction between $Top$ and $ETop \infty Grpd$ (or similar) is often appealed to implicitly, but rarely explicitly. In $Top \simeq \infty Grpd$ we have instead $\mathbf{B}^n U(1) \simeq K(U(1), n)$.

]]>started something basic at *Steenrod square*

I added to walking structure a 2-categorical theorem that implies that usually “the underlying X of the walking X is the initial X”. This fact seems like it should be well-known, but I don’t offhand know a reference for it, can anyone give a pointer?

]]>if you have been looking at the logs you will have seen me work on this for a few days already, so I should say what I am doing:

I am working on creating an entry *twisted smooth cohomology in string theory* . This is supposed to eventually serve as the set of notes for my lectures at the *ESI Program K-Theory and Quantum Fields* in the next weeks.

This should probably sit on my personal web, and I can move it there eventually. But for the moment I am developing it as an $n$Lab entry because that saves me from prefixing every single wiki-link with

```
nLab:
```

]]>
**Theorem:**

Let $K$ be a complex with $r$ combinatorial components. Then $H_{0}(K)$ is isomorphic to the direct sum of (not $r$ but) $2r$ copies of the group $Z$ of integers.

**Proof for one component:**

As 0-cycles are synonymous with 0-chains, they have $\alpha_{0}$ many dimensions-of-freedom for sure. How many the 0-boundaries of our component have? Since the incidence matrix is a $\alpha_{0}$ by $\alpha_{1}$ matrix (see my previous posting with ‘homology’ tag), they have at least $\alpha_{1} - \alpha_{0}$ many for sure. And 1 more for the rank deficiency! The proof follows from this arithmetic.

]]>I want to record a certain lemma on the nlab that is rarely made explicit (slight variation here: https://arxiv.org/abs/1112.0094).

The theorem is that if you have a profunctor $R$ from $C$ to $D$ and it is representable as a functor $F : C \to D$ then the action of $F$ on morphisms is uniquely determined by $R$ and the representation isomorphism.

This explains the initially strange feature of type theoretic connectives, which have semantics as functors but we never actually define their action on morphisms because we can derive the action from the introduction and elimination rules.

My question is should this get a page on the nlab, called I guess “Representability determines Functoriality” or something like that? Or should I try to find some existing page?

And a meta-question is should I err on the side of just making a page with whatever name I feel like or come to discuss the name here on the nforum? Is it easy to change names of pages after the fact?

]]>added a few lines and original references to *supersymmetry breaking*.

Took a stab at a general formulation of Poisson summation formula, although the class of functions to which it is supposed to apply wasn’t nailed down (yet).

(Some of the ingredients of Tate’s thesis are currently on my mind.)

]]>I have spent some minutes starting to put some actual expository content into the Idea-section on *higher gauge theory*. Needs to be much expanded, still, but that’s it for the moment.

A *lot* of new visitors have trouble entering math on the forum. It ought to be easy to add some more descriptive help text to the formatting options below the post. Could it say something like

To use (La)TeX mathematics in your post, make sure “Markdown+Itex” is selected and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted; see here for a list.

?

]]>