I’ve been hearing a bit about Noether’s second theorem, and its interpretation in GR. Is it sufficiently different from her first theorem to warrant a new page?

I know Urs has written on the second theorem here.

I believe there is some question of what it says in GR, i.e., how to understand energy-momentum conservation.

]]>http://www.logic.at/staff/bruno/Papers/2010-PhysicsAndProofTheory-PC.pdf

It includes an example of energy conservation as a cut:

'To solve problems of physics, certain invariants (such as energy) are frequently

used. This is so because solving problems by using a derived principle (such

as the principle of energy conservation) is usually easier than solving them by

using the most basic physical laws or axioms. This section intends to exemplify

how problem solution can generally be seen from a proof-theoretic perspective

in which the use of derived principles corresponds to an implicit use of the cut

rule.' ]]>

Thanks for fixing it! I was a bit unsure where to switch the sign, whether in Proposition 1 or in Theorem 1, since also the presymplectic structure in Definition 1 depends on it, but I guess that can also be defined with either sign, and so it wouldn’t really matter. Now it’s consistent in any case.

]]>Oh, now I see. You are right. Of course I can have any sign I want where $d\Theta$ is introduced, but then I need to carry it along properly, which I didn’t. Fixed now here. Sorry for causing you this trouble. Thanks for insisting.

]]>Hi Urs, thanks for checking this. I wonder whether we might have different sign conventions somewhere… Let’s see. Here’s my calculation, starting from the Lagrangian $L = \mathcal{L}(q^a,\dot{q}^a)dt$, I find the vertical derivative and Euler-Lagrange-Equations:

$\delta L = \left(\frac{\partial\mathcal{L}}{\partial q^a}\theta^a + \frac{\partial\mathcal{L}}{\partial\dot{q}^a}\dot{\theta}^a\right) \wedge dt\,, \quad E(L) = \left(\frac{\partial\mathcal{L}}{\partial q^a} - D_t\frac{\partial\mathcal{L}}{\partial\dot{q}^a}\right)\theta^a \wedge dt\,.$Here I wrote $\theta^a$ and $\dot{\theta}^a$ for the basic contact one-forms and $D_t$ for the total derivative. Now the next line is where the minus comes into the game, from reordering the wedge product $\theta^a \wedge dt$, since $d(f\theta^a) = D_t f\,dt \wedge \theta^a + f\,dt \wedge \dot{\theta}^a$:

$d\Theta = \delta L - E(L) = \left(\frac{\partial\mathcal{L}}{\partial\dot{q}^a}\dot{\theta}^a + D_t\frac{\partial\mathcal{L}}{\partial\dot{q}^a}\theta^a\right) \wedge dt = - d\left(\frac{\partial\mathcal{L}}{\partial\dot{q}^a}\theta^a\right)\,.$Finally, with the vector field $v = \sum_{\lambda = 0}^{\infty}q^a_{(\lambda+1)}\bar{\partial}_a^{\lambda}$, which has $\iota_v\theta^a = \dot{q}^a$, I get

$\iota_v\Theta = -\frac{\partial\mathcal{L}}{\partial\dot{q}^a}\dot{q}^a\,.$By the way, you can also find this sign inconsistency if you look at the proof of Noether’s theorem at the end of this section. There you conclude that $\delta L + d\Theta = E(L)$, but on top of the section you have $\delta L = E(L) + d\Theta$. I checked the proof (in particular the part $-d\iota_v\Theta = \iota_v d\Theta$) and came to the same result, i.e., Theorem 1 and its proof are consistent among each other, but Proposition 1 is not.

]]>mhohmann, I have now fixed in the entry the issue with $\theta$ appearing in lower case where it was introduced instead in upper case notation, thanks again.

(for bystanders: we are talking about the paragraphs in the entry starting here)

Regarding the sign:

a sign in the definition of $\Theta$ should not matter (we could have any non-zero prefactor in the definition of $\Theta$ without changing anything but the normalization of $\Theta$) so I wouldn’t think that this solves the isse that you ran into.

I am rather wondering why you have the minus sign in

$\iota_v\Theta = -\frac{\partial\mathcal{L}}{\partial\dot{q}^a}\dot{q}^a$

(in #27). I don’t seem to get that.

]]>That may happen that there is a sign error. I’ll try to check tomorrow when I have the leisure. Thanks for the alert.

]]>I wonder whether there is a sign mistake in the Lagrangian version derivation (and maybe a confusion between $\theta$ and $\Theta$?) - or whether my derivation is wrong. I tried to show the energy conservation from a simple Lagrangian $L = \mathcal{L}(q^a,\dot{q}^a)dt$. The vector field describing time translation should be $v = \sum_{\lambda = 0}^{\infty}q^a_{(\lambda+1)}\bar{\partial}_a^{\lambda}$. Now taking $\Theta$ from $d\Theta = \delta L - E(L)$ I get

$\sigma_v = \mathcal{L}\,, \quad \iota_v\Theta = -\frac{\partial\mathcal{L}}{\partial\dot{q}^a}\dot{q}^a\,, \quad \sigma_v - \iota_v\Theta = \mathcal{L} + \frac{\partial\mathcal{L}}{\partial\dot{q}^a}\dot{q}^a$Well, you see the problem - the Hamiltonian should have a relative $-$ between these terms. I think $\Theta$ right in the top should be defined with the opposite sign. Oh, and it should probably be $\Theta$ instead of $\theta$ in the statement of the Noether theorem?

]]>Looking through the article, I see that the parametric type theory is used to prove (as a “free theorem”) that a given (“Lagrangian”) function has a given invariance. But it seems to me now that neither Noether’s theorem, nor conservation laws nor conserved quantities are claimed to be derived by means of any type theory. Instead, it seems that once the invariance of a function is established via parametricity, there is an appeal to the standard textbook discussion of Noether’s theorem to claim that “now a conservation law follows”. But this step itself is not being formalized in the text.

That’s at least my impression from reading the text. If anyone here has further insight, please let me know.

Therefore I have changed in the entry “formalizes the Noether theorem” to something like “formalizes the invariance of a (Lagrangian) function”.

I took the liberty of adding to the list of References at *Noether theorem* the following lines:

]]>A formalization of Noether’s theorem in cohesive homotopy type theory is discussed in sections “2.7 Noether symmetries and equivariant structure” and “3.2 Local observables, conserved currents and higher Poisson bracket homotopy Lie algebras” of

- Urs Schreiber,
Classical field theory via Cohesive homotopy types (schreiber)(2013)

I had fixed and expanded in the entry:

]]>

- Robert Atkey,
From Parametricity to Conservation Laws, via Noether’s Theorem, talk atPrinciples of Programming Languages (POPL) 2014(pdf article, web slides, pdf slides)

pdf link does not work

]]>I have added to the References at *Noether theorem* the following

]]>A formalization of (aspects of) the Noether theorem in parametric dependent type theory is discussed in

- Robert Atkey,
From Parametricity to Conservation Laws, via Noether’s Theorem, talk atPrinciples of Programming Languages (POPL) 2014(web, pdf slides

Thanks for the pointer. Such as not to keep this a secret, I have added it here.

]]>arXiv:math/0312219 Title: A formalism for the renormalization procedure Authors: Dmitry E. Tamarkin

has the first part of the work, the rest unfortunately never appeared in a form of a preprint. n particular derived symplectic reduction, and the study of nonlinear Poisson sigma model (and ist relations to topological A and B-model) are not treated in the first part. Chrestomaty is a general variant of what is in this first preprint defined as “system”.

]]>I took from some lectures but not all, but it is not easy to find them. I thnk Goncharov took more careful notes.

]]>Hrestomaty (chrestomaty ?) is certain object in homotopical algebra in the language of pseudotensor categories (a version of color operads used by Beilinson-Drinfeld school) which in his published preprint is something like what he calls there system. But the symmetries like what is essentially $L_\infty$ kind of thing are another special case. Thus the physical system and the symmetries are objects belonging to the same general class of (c)hrestomaties.

He gave lectures on this in Paris in 2004 (series of about 6 sessions) with examples like derived Hamiltonian reduction, Noether theorems, quantization of nonlinear Poisson sigma model, and its reductions (which included topological A-model and topological B-model) etc. It was amazing project; he got Hopf algebras of renormalization as functions of the torsor of equivalences between different homotopical resolutions for example (probably Connes-Kreimer Hopf algebras are a special case, but he did not go into combinatorial details, though it was very likely). He also explained the role of Green functions in producing short exact sequences needed to obtain the homotopical resolutions by splicing. Goncharov was in the lectures and he suspected that he could do this over other fields (not only complex numbers). But Tamarkin was not happy with the progress of the project and abandoned it. There is a preprint on the free field theory case on the net (before he started using the terminology of hrestomaties), and the rest has never appeared as a preprint. I asked him later, he said he considered it too difficult project for himself and that he thinks that the approach by Costello is better. Still I feel pity some of his discoveries and examples never appeared in print. He also used lots of techniques from Beilinson-Drinfeld work in action what is quite nice.

]]>So, Tamarkin said that in his formalism of “hrestomaties” in BV, every conservation law gave some symmetry but not every symmetry came that way, so that it was not truly 1-1. Upside down because deriving conservation from a symmetry, i.e. producing the inverse did not exist in full generality which he allowed for the higher symmetries and conservation laws. Maybe an artifact of the theory, of course. Though the theory was based on quite nice homotopical resolutions, what looked canonical. I might have hand written notes somewhere.

]]>have added one more brief pargraph at the end of *Simple schematic idea* on the more general case where the symmetry leaves the Lagrangian invariant only up to an exact term.

@Jim: Okay, I have edded YKS’s book to the References

@Zoran: not sure I understand the thing about upside-down. The point of the theorem is that both are equivalent to each other, neither is more fundamental. Maybe in the usual Lagrangian formulation this is not 100% explicit, but in the Hamiltonian formulation it is fully manifest.

]]>added a paragraph with the *Simple schematic idea*.

Yes, maybe we should talk Noether charges etc.

Tamarkin was saying in his formalism for BV and higher geometry Noether theorem is kind of upside down. Not that symmetries are basic and then conservation laws from them, but the conservation laws are fundamental and the symmetries appear defined in some cases from those (maybe I was not precise).

For future redirects: under Noether’s theorem algebraic geometers mean Noether normalization theorem, quite fundamental in algebraic geometry and commutative algebra (e.g. the Hilbert Nullstellensatz being a corrolary).

]]>