Lorentz group actions related to SpaceTime

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

iv. References

A. Lorentz group action on Schwartz functions

A.1. The definition of the action

def SpaceTime.schwartzAction {d : ℕ} : ↑(LorentzGroup d) →* SchwartzMap (SpaceTime d) ℝ →L[ℝ] SchwartzMap (SpaceTime d) ℝ

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

Equations

• SpaceTime.schwartzAction = { toFun := fun (Λ : ↑(LorentzGroup d)) => SchwartzMap.compCLM ℝ ⋯ ⋯, map_one' := ⋯, map_mul' := ⋯ }

A.2. Basic properties of the action

theorem SpaceTime.schwartzAction_mul_apply {d : ℕ} (Λ₁ Λ₂ : ↑(LorentzGroup d)) (η : SchwartzMap (SpaceTime d) ℝ) : (schwartzAction Λ₂) ((schwartzAction Λ₁) η) = (schwartzAction (Λ₂ * Λ₁)) η

theorem SpaceTime.schwartzAction_apply {d : ℕ} (Λ : ↑(LorentzGroup d)) (η : SchwartzMap (SpaceTime d) ℝ) (x : SpaceTime d) : ((schwartzAction Λ) η) x = η (Λ⁻¹ • x)

A.3. Injectivity of the action

theorem SpaceTime.schwartzAction_injective {d : ℕ} (Λ : ↑(LorentzGroup d)) : Function.Injective ⇑(schwartzAction Λ)

A.4. Surjectivity of the action

theorem SpaceTime.schwartzAction_surjective {d : ℕ} (Λ : ↑(LorentzGroup d)) : Function.Surjective ⇑(schwartzAction Λ)

B. Lorentz group action on distributions

B.1. The SMul instance

instance SpaceTime.instSMulElemMatrixSumFinOfNatNatRealLorentzGroupDistribution {n d : ℕ} {c : Fin n → realLorentzTensor.Color} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] [(realLorentzTensor d).Tensorial c M] [T2Space M] : SMul (↑(LorentzGroup d)) ((SpaceTime d)→d[ℝ] M)

Equations

• One or more equations did not get rendered due to their size.

theorem SpaceTime.lorentzGroup_smul_dist_apply {n d : ℕ} {c : Fin n → realLorentzTensor.Color} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] [(realLorentzTensor d).Tensorial c M] [T2Space M] (Λ : ↑(LorentzGroup d)) (f : (SpaceTime d)→d[ℝ] M) (η : SchwartzMap (SpaceTime d) ℝ) : (Λ • f) η = Λ • f ((schwartzAction Λ⁻¹) η)

B.2. The DistribMulAction instance

instance SpaceTime.instDistribMulActionElemMatrixSumFinOfNatNatRealLorentzGroupDistribution {n d : ℕ} {c : Fin n → realLorentzTensor.Color} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] [(realLorentzTensor d).Tensorial c M] [T2Space M] : DistribMulAction (↑(LorentzGroup d)) ((SpaceTime d)→d[ℝ] M)

Equations

• One or more equations did not get rendered due to their size.

B.3. The SMulCommClass instance

instance SpaceTime.instSMulCommClassRealElemMatrixSumFinOfNatNatLorentzGroupDistribution {n d : ℕ} {c : Fin n → realLorentzTensor.Color} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] [(realLorentzTensor d).Tensorial c M] [T2Space M] : SMulCommClass ℝ (↑(LorentzGroup d)) ((SpaceTime d)→d[ℝ] M)