1. Physlib
  2. SpaceAndTime
  3. SpaceTime
  4. LorentzAction
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.SpaceAndTime.SpaceTime.Basic public import Physlib.Mathematics.Distribution.Basic

i. Overview

We already have a Lorentz group action on SpaceTime d, in this module we define the induced action on Schwartz functions and distributions.

ii. Key results

    schwartzAction : Defines the action of the Lorentz group on Schwartz functions.

    An instance of DistribMulAction for the Lorentz group acting on distributions.

iii. Table of contents

    A. Lorentz group action on Schwartz functions

      A.1. The definition of the action

      A.2. Basic properties of the action

      A.3. Injectivity of the action

      A.4. Surjectivity of the action

    B. Lorentz group action on distributions

      B.1. The SMul instance

      B.2. The DistribMulAction instance

      B.3. The SMulCommClass instance

      B.4. Action as a linear map

iv. References

@[expose] public sectionattribute [-simp] Fintype.sum_sum_type

A. Lorentz group action on Schwartz functions

A.1. The definition of the action

The Lorentz group action on Schwartz functions taking the Lorentz group to continuous linear maps.

d:ℕΛ₁:↑(LorentzGroup d)Λ₂:↑(LorentzGroup d)η:𝓢(SpaceTime d, ℝ)x:SpaceTime d⊢ η (Λ₂⁻¹ • Λ₁⁻¹ • x) = ((compCLM ℝ ⋯ ⋯ * compCLM ℝ ⋯ ⋯) η) x All goals completed! 🐙

A.2. Basic properties of the action

lemma schwartzAction_mul_apply {d} (Λ₁ Λ₂ : LorentzGroup d) (η : 𝓢(SpaceTime d, ℝ)) : schwartzAction Λ₂ (schwartzAction (Λ₁) η) = schwartzAction (Λ₂ * Λ₁) η := d:ℕΛ₁:↑(LorentzGroup d)Λ₂:↑(LorentzGroup d)η:𝓢(SpaceTime d, ℝ)⊢ (schwartzAction Λ₂) ((schwartzAction Λ₁) η) = (schwartzAction (Λ₂ * Λ₁)) η All goals completed! 🐙lemma schwartzAction_apply {d} (Λ : LorentzGroup d) (η : 𝓢(SpaceTime d, ℝ)) (x : SpaceTime d) : (schwartzAction Λ η) x = η (Λ⁻¹ • x) := rfl

A.3. Injectivity of the action

All goals completed! 🐙

A.4. Surjectivity of the action

d:ℕΛ:↑(LorentzGroup d)η:𝓢(SpaceTime d, ℝ)⊢ (schwartzAction (Λ * Λ⁻¹)) η = η All goals completed! 🐙

B. Lorentz group action on distributions

B.1. The SMul instance

instance : SMul (LorentzGroup d) ((SpaceTime d) →d[ℝ] M) where smul Λ f := (Tensorial.actionCLM (realLorentzTensor d) Λ) ∘L f ∘L (schwartzAction Λ⁻¹)lemma lorentzGroup_smul_dist_apply (Λ : LorentzGroup d) (f : (SpaceTime d) →d[ℝ] M) (η : 𝓢(SpaceTime d, ℝ)) : (Λ • f) η = Λ • (f (schwartzAction Λ⁻¹ η)) := rfl

B.2. The DistribMulAction instance

set_option synthInstance.maxHeartbeats 40000n:ℕd:ℕc:Fin n → realLorentzTensor.ColorM:Typeinst✝³:NormedAddCommGroup Minst✝²:NormedSpace ℝ Minst✝¹:(realLorentzTensor d).Tensorial c Minst✝:T2Space MΛ:↑(LorentzGroup d)f1:(SpaceTime d)→d[ℝ] Mf2:(SpaceTime d)→d[ℝ] Mη:𝓢(SpaceTime d, ℝ)⊢ Λ • (f1 + f2) ((schwartzAction Λ⁻¹) η) = (Λ • f1 + Λ • f2) η All goals completed! 🐙

B.3. The SMulCommClass instance

All goals completed! 🐙

B.4. Action as a linear map

The Lorentz action on distributions as a linear map.

All goals completed! 🐙