Lorentz group

Stream: PhysLean

[Jeremy Lindsay]

Currently, Lorentz group results in PhysLean are defined for arbitrary dimension. I'm wondering if, instead of just showing that the restricted Lorentz group $SO^+(1, 3)$ is the identity component of the Lorentz group $O(1, 3)$, I should prove the more general result: according to

• https://en.wikipedia.org/wiki/Indefinite_orthogonal_group#Topology and
• https://en.wikipedia.org/wiki/Lorentz_group#Generalization_to_higher_dimensions,
  the identity component of $O(p, q)$ is $SO^+(p, q)$.

Thoughts?

[Joseph Tooby-Smith]

I think this seems like a good idea! I think the proof given in Proposition 2.10 of:

https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf

might work generally (related to the 'generalized boosts' already in PhysLean) and also has the advantage of other useful little results to physics. More generally, I found it difficult to find any other proof of this statement when I looked a while ago, even for the $(1,3)$ case.

[Jeremy Lindsay]

A different proof sketch, for reference: https://math.stackexchange.com/questions/5057218/where-can-i-find-a-proof-that-the-indefinite-orthogonal-group-op-q-has-four

[Joseph Tooby-Smith]

(sorry started typing this before your comment).

If you end up going down this road I suggested, I think the first step would be to do this TODO item:

• TODO (6VZKU): file PhysLean.Relativity.Lorentz.Group.Boosts.Generalized

which should be relatively easy, since the proper part is done, and the orthochronous part should follow similarly.

[Jeremy Lindsay]

I may have found two errors in https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf, The Lorentz Group by Guillem Cobos. (Looks like the link is broken, so here is a copy: The Lorentz Group (Cobos).pdf.) Near the bottom of page 19 it is written:

Directly from the general expression of $\phi_{uv}$ we check

$$(\phi_{uv})_{11} = (e_1, \phi_{uv}(e_1)) = 1 + u_1 v_1 + (u_1^2 - 1) v_1^2 + (v_1^2 - 1) u_1^2 > 0 .$$

The map $\phi_{uv} : \mathbb R^4 \to \mathbb R^4$ is the "generalised boost" defined here in PhysLean:

$$\phi_{uv}(x) \coloneqq x + 2 (x, u) v - \frac{(x, u + v)}{1 + (u, v)} (u + v) ,$$

where $u, v$ are any fixed elements of $P := \{ u \in \mathbb R^4 \mid u_1 > 0, \, (u, u) = 1 \}$. However, my calculation gives

$$(\phi_{uv})_{11} = 1 + 2 u_1 v_1 - \frac{(u_1 + v_1)^2}{1 + (u, v)} ,$$

which Lean agrees with. These two expressions are not equivalent: take $u = v = (1, 0, 0, 0)$, which yields

$$(\phi_{uv})_{11} = 1 + 1 + 0 + 0 = 2$$

in the paper's expression, and

$$(\phi_{uv})_{11}= 1 + 2 - \frac{4}{2} = 1$$

in mine. The paper also says

We have used the fact that $u, v \in P$ when taking into account $u_1, v_1 \geq 1$.

But as far as I can tell, we can only conclude $u_1, v_1 > 0$.

---

Not sure if I've missed something or if the orthochronous property of (the matrix representation of) $\phi_{uv}$ requires a different proof. I spent a bit of time trying to prove this but the inequalities are nasty. Will pick up tomorrow :moon:

[Joseph Tooby-Smith]

The fact that $1 \leq u_1, v_1$ corresponds to:

https://physlean.com/docs/PhysLean/Relativity/Tensors/RealTensor/Vector/Pre/NormOne.html#Lorentz.Contr.NormOne.FuturePointing.mem_iff_inl_one_le_inl

[Joseph Tooby-Smith]

I agree with your expression for $(\phi_{uv})_{11}$, but can't think of a proof that it is positive.

[Joseph Tooby-Smith]

An alternative way to show this would be:

lemma isOrthochronous_on_connected_components {Λ Λ' : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) :
    IsOrthochronous Λ ↔ IsOrthochronous Λ' := by
  sorry

lemma isOthochronous (u v : FuturePointing d) :
    IsOrthochronous (toLorentz u v) := by
  apply (isOrthochronous_on_connected_components (toLorentz_in_connected_component_1 u v)).mp
  simp [IsOrthochronous]

I think the proof of the first result is similar to isProper_on_connected_components, but using orthchroMap instead of det.

Though it would be nice if it was possible using the inequalities :(.

[Joseph Tooby-Smith]

(deleted: Nevermind - there was a mistake in what I wrote, sorry, will see if I can fix)

[Dominic Steinitz]

One day we will do this by principal bundles - my progress is glacially slow so don't hold your breath

[Joseph Tooby-Smith]

Here is my attempt number 2:

Lemma:

$$(\phi_{uv})_{11} = 1 + \frac{||u_1 \vec v - v_1 \vec u||^2}{1 + (u,v)}$$

where $\vec u$ is the space vector underlying $u$ etc.

Proof:

First note that

$$||u_1 \vec v - v_1 \vec u||^2 = u_1^2 || \vec v||^2 + v_1^2 || \vec u||^2 - 2 u_1 v_1 \vec u \cdot \vec v$$

Then using that $|| \vec v||^2 = v_1^2 -1$ and similar for $\vec u$ we get

$$||u_1 \vec v - v_1 \vec u||^2 = u_1^2 (v_1^2 -1) + v_1^2 (u_1^2 -1) - 2 u_1 v_1 \vec u \cdot \vec v \\ = 2 u_1 v_1 ( u_1 v_1 - \vec u \cdot \vec v) - u_1^2 - v_1^2 \\ = 2 u_1 v_1 (u,v) - u_1^2 -v_1^2 \\ = 2 u_1 v_1 (1 + (u, v)) - u_1^2 -v_1^2 - 2 u_1 v_1 \\ = 2 u_1 v_1 (1 + (u, v)) - (u_1 + v_1)^2$$

Thus

$$1 + \frac{||u_1 \vec v - v_1 \vec u||^2}{1 + (u,v)} \\ = 1 + \frac{2 u_1 v_1 (1 + (u, v)) - (u_1 + v_1)^2}{1 + (u,v)}\\ = 1 + 2 u_1 v_1 - \frac{(u_1+ v_1)^2}{1+ (u,v)} = (\phi_{uv})_{11}$$

q.e.d.

From this lemma it is clear that the second term is greater than zero, and thus

$$1 \leq (\phi_{uv})_{11}$$

which is stronger then the required condition, and what I would expect.

[Joseph Tooby-Smith]

Dominic Steinitz said:

One day we will do this by principal bundles - my progress is glacially slow so don't hold your breath

More generally I'm very excited about having principal bundles formalized, then one can start doing gauge field theory properly :)

[Jeremy Lindsay]

Joseph Tooby-Smith said:

Here is my attempt number 2:

Nice!!

[Jeremy Lindsay]

Quick update: apologies for the intermittent and slow progress—am currently swimming in full-time work + interviews + PhD apps. In case I am holding back this part of PhysLean, I would not be offended whatsoever if anyone wanted to take over my current PR!

[Joseph Tooby-Smith]

Hey, no worries at all! What I can do is clean up the PR a bit, and replace the results which contain a sorry with semiformal_results, and add a semiformal_result for my little lemma above. This should be relatively easy, and means what has been done in that PR is not lost or forgotten about.

[Joseph Tooby-Smith]

I've done the above here PR524. I can merge once the linters are finished.

[Joseph Tooby-Smith]

I managed to show here (in a larger PR631, which isn't yet merged due to linting) that there is a homeomorphism

LorentzGroup.restricted d ≃ₜ Lorentz.Velocity d × Matrix.specialOrthogonalGroup (Fin d) ℝ

In physics terms, the inverse map here says that every element of the restricted Lorentz group corresponds to a boost multiplied by a rotation.

This goes a long way to show that LorentzGroup.restricted d is connected, all that is left is to show that

import Mathlib

lemma _root_.Matrix.specialOrthogonalGroup_connectedSpace {d : ℕ} :
  ConnectedSpace (Matrix.specialOrthogonalGroup (Fin d) ℝ) := by sorry

which isn't in Mathlib yet :(.