DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat: LorentzAction_on_isEmpty

Browse source
This commit is contained in:
jstoobysmith 2024-07-16 11:59:29 -04:00
parent 86e7ea6c0f
commit d385f72087
2 changed files with 15 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

9
HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
View file

@ -270,13 +270,8 @@ open Matrix
/-- The action of the Lorentz group on `ofReal v` is trivial. -/
@[simp]
lemma lorentzAction_ofReal (r : ℝ) : Λ • ofReal d r = ofReal d r := by
refine ext' rfl ?_
funext i
erw [lorentzAction_smul_coord]
simp only [Finset.univ_unique, Finset.univ_eq_empty, Finset.prod_empty, one_mul,
Finset.sum_singleton, IndexValue]
rfl
lemma lorentzAction_ofReal (r : ℝ) : Λ • ofReal d r = ofReal d r :=
lorentzAction_on_isEmpty Λ (ofReal d r)
/-- The action of the Lorentz group on `ofVecUp v` is by vector multiplication. -/
@[simp]

13
HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
View file

@ -139,4 +139,17 @@ instance lorentzAction : MulAction (LorentzGroup d) (RealLorentzTensor d X) wher
@[simps!]
instance : MulAction (LorentzGroup d) (Marked d X n) := lorentzAction
/-- The action on an empty Lorentz tensor is trivial. -/
lemma lorentzAction_on_isEmpty [IsEmpty X] (Λ : LorentzGroup d) (T : RealLorentzTensor d X) :
Λ • T = T := by
refine ext' rfl ?_
funext i
erw [lorentzAction_smul_coord]
simp only [Finset.univ_unique, Finset.univ_eq_empty, Finset.prod_empty, one_mul,
Finset.sum_singleton]
simp only [IndexValue, Unique.eq_default]
/-! TODO: Show that the Lorentz action commutes with multiplication. -/
/-! TODO: Show that the Lorentz action commutes with contraction. -/
/-! TODO: Show that the Lorentz action commutes with rising and lowering indices. -/
end RealLorentzTensor