mathematical tools for (axiomatic/algebraic) QFT

Stream: Natural sciences

[Yoh Tanimoto]

Hello! I just noticed this channel today and glad to see many people interested in Lean and physics.

I am working on mathematical quantum field theory (a.k.a. axiomatic/algebraic/constructive QFT). There are many quantum field theories that have been rigorously constructed and I would like to see them fomalised. However, many things are still missing in mathlib, so I am currently trying to add some basic tools to it, a bit randomly.

If anyone is interested in any of the following, we might able to organize!

• distribution theory (Fourier/Laplace transform, analytic continuation)
• unitary representations of groups
• spectral decomposition for (self-adjoint/normal) operators on a Hilbert space
• von Neumann algebras

[Joseph Tooby-Smith]

Hey! I used to work on functorial quantum field theories, which aren't too far in spirit from AQFTs.

In case you haven't seen this: I'm working on a project `HepLean' with the goal of trying to formalise high energy physics (very broadly defined) in Lean. If/when you get around to formalising parts of AQFTs, it would be great to have them included in this project (if not in Mathlib).

In any case, I'm certainly interested in unitary representations of groups (and Lie algebras), and potentially von Neumann algebras and things related (from a CFT perspective).

[Patrick Massot]

Yoh Tanimoto said:

If anyone is interested in any of the following, we might able to organize!

• distribution theory (Fourier/Laplace transform, analytic continuation)
• unitary representations of groups
• spectral decomposition for (self-adjoint/normal) operators on a Hilbert space
• von Neumann algebras

All those topics are more or less actively worked on already. Before starting anything serious in those direction you should make sure to post a message in the mathlib4 stream.

[Frédéric Dupuis]

Indeed, for example I have just PRed #14177 with a view towards getting started on von Neumann algebras.

[Yoh Tanimoto]

Hi Joseph! I saw your project, very nice!
Formalizing AQFT is still a bit far, we need more definitions to start with.
But you have already have Lorentz metric and Lorentz group!
I defined the Poincaré group here as a subgroup of the affine group, without thinking about PR'ing or so
https://github.com/yoh-tanimoto/mathlib4/blob/yoh/yoh/wightman/minkowski.lean
I was wondering which is the best definition. Maybe at some point one wants to classify the positive-energy representations, so it might be better to define it as the semidirect product of the translation group and the Lorentz group. Any thought?

[Yoh Tanimoto]

@Patrick Massot thanks, I know that there are some works going on, but I will keep in mind to post a message.

@Frédéric Dupuis Great that you PR'ed WOT! I also tried to define SOT but not really in a useful form. Are you going to do that and/or the double commutant theorem?

[Frédéric Dupuis]

Yes, that's the general direction I'd like to go in!

[Joseph Tooby-Smith]

@Yoh Tanimoto Nice! I like your notation for the metric.

C.f. the definition of the Poincare Group, one can always define an equivalence to the semidirect product of translations and the Lorentz Group. I think defining it as the group

{g : (R2 →ᵃ[ℝ] R2) | ∀ (x y : R2), ‖x-y‖M = ‖g x - g y‖M }

is a slightly better variation on what you have. Then invertibility becomes a theorem rather than a definition.

C.f. what is in HepLean about the Lorentz metric and group, it needs refactoring a bit, and generalising to any dimension d.

[Yoh Tanimoto]

thanks for your comment!
Why do you think it's better to define it as g : R2 →ᵃ[ℝ] R2? With g : R2 ≃ᵃ[ℝ] R2 you can benefit from theorems for AffineEquiv and LinearEquiv...

[Joseph Tooby-Smith]

When I first defined the Lorentz group I did it similar to what you did, as an element of `(Fin 4 → ℝ) ≃ₗ[ℝ] (Fin 4 → ℝ) preserving the metric. The problem was that every time I wanted to show M was part of the Lorentz group, it wasn't enough to show it preserved the metric, I also had to show it was invertible (which follows from it preserving the metric). It ended up being easier to make this manifest. (By defining it through R2 →ᵃ[ℝ] R2 you can also explicitly tell lean what the inverse is in terms of traces etc.)

You can still benefit from AffineEquiv, just define a map Poincare -> AffineEquiv.

[Yoh Tanimoto]

I see, if you want to treat concrete example.

maybe it is more practical to keep two definitions, one as `AffineEquiv" and proving that it is isomorphic to the usual semidirect product, where the latter is defined as you do? In this way, examples can be checked in the latter definition, while the former acts on the Minkowski space by definition.

[Joseph Tooby-Smith]

Even non-concrete examples like defining the homomorphism a group into it.

The latter will also act on Minkowski space by definition. And if you really wanted you could just define the way it acts on Minkowski space through the map Poincare -> AffineEquiv. I'm struggling to see the benefits one would get rom defining it through AffineEquiv.

[Yoh Tanimoto]

you could, but if every time you have to compose it with an isomorphism it's tedious.

if you consider the action of g : Poincare on the space of functions, then it is f (g⁻¹ x).