Imports
/-
Copyright (c) 2026 Rob Sneiderman. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rob Sneiderman
-/
module
public import Mathlib.RepresentationTheory.Continuous.Basic
public import Physlib.SpaceAndTime.TimeAndSpace.EuclideanGroup.Action
The Euclidean group action on Schwartz maps over TimeAndSpace
i. Overview
In this file we define the pullback action of the Euclidean group on Schwartz maps over
TimeAndSpace d. The action is
g • η = fun tx => η (g⁻¹ • tx).
ii. Key results
TimeAndSpace.schwartzEuclideanAction : The Euclidean group action on Schwartz maps as a
continuous representation (ContRepresentation).
TimeAndSpace.instMulActionSchwartzMap : The induced MulAction instance on Schwartz maps.
TimeAndSpace.smul_schwartzMap_apply : Pointwise formula for the action.
iii. Table of contents
A. The pullback action on Schwartz maps
iv. References
@[expose] public sectionA. The pullback action on Schwartz maps
Pointwise formula for the monoid-homomorphism form of the Schwartz-map pullback action.
@[simp]
lemma schwartzEuclideanAction_apply {d : ℕ} (g : EuclideanGroup d) (η : 𝓢(TimeAndSpace d, F))
(tx : TimeAndSpace d) :
(schwartzEuclideanAction g η) tx = η (g⁻¹ • tx) := rfl
Pointwise formula for the MulAction instance on Schwartz maps.
@[simp]
lemma smul_schwartzMap_apply {d : ℕ} (g : EuclideanGroup d) (η : 𝓢(TimeAndSpace d, F))
(tx : TimeAndSpace d) :
(g • η) tx = η (g⁻¹ • tx) := rfl
Applying g and then h to a Schwartz map is the pullback action of h * g.
All goals completed! 🐙Each Euclidean-group pullback action on Schwartz maps is injective.
lemma schwartzEuclideanAction_injective {d : ℕ} (g : EuclideanGroup d) :
Function.Injective (schwartzEuclideanAction (F := F) g) := F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕg:EuclideanGroup d⊢ Function.Injective ⇑(schwartzEuclideanAction g)
F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕg:EuclideanGroup dη1:𝓢(TimeAndSpace d, F)η2:𝓢(TimeAndSpace d, F)hη:(schwartzEuclideanAction g) η1 = (schwartzEuclideanAction g) η2⊢ η1 = η2
F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕg:EuclideanGroup dη1:𝓢(TimeAndSpace d, F)η2:𝓢(TimeAndSpace d, F)hη:(schwartzEuclideanAction g) η1 = (schwartzEuclideanAction g) η2tx:TimeAndSpace d⊢ η1 tx = η2 tx
F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕg:EuclideanGroup dη1:𝓢(TimeAndSpace d, F)η2:𝓢(TimeAndSpace d, F)hη:(schwartzEuclideanAction g) η1 = (schwartzEuclideanAction g) η2tx:TimeAndSpace dhtx:((schwartzEuclideanAction g) η1) (g • tx) = ((schwartzEuclideanAction g) η2) (g • tx)⊢ η1 tx = η2 tx
All goals completed! 🐙Each Euclidean-group pullback action on Schwartz maps is surjective.
lemma schwartzEuclideanAction_surjective {d : ℕ} (g : EuclideanGroup d) :
Function.Surjective (schwartzEuclideanAction (F := F) g) := F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕg:EuclideanGroup d⊢ Function.Surjective ⇑(schwartzEuclideanAction g)
F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕg:EuclideanGroup dη:𝓢(TimeAndSpace d, F)⊢ ∃ a, (schwartzEuclideanAction g) a = η
F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕg:EuclideanGroup dη:𝓢(TimeAndSpace d, F)⊢ (schwartzEuclideanAction g) ((schwartzEuclideanAction g⁻¹) η) = η
F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕg:EuclideanGroup dη:𝓢(TimeAndSpace d, F)tx:TimeAndSpace d⊢ ((schwartzEuclideanAction g) ((schwartzEuclideanAction g⁻¹) η)) tx = η tx
All goals completed! 🐙