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

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2024-07-17 15:15:44 -04:00
parent 5da7605301
commit 36752fa5c4
2 changed files with 13 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

17
HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
View file

@ -5,9 +5,9 @@ Authors: Joseph Tooby-Smith
-/
import Mathlib.Logic.Function.CompTypeclasses
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.Normed.Field.Basic
import Mathlib.CategoryTheory.Core
import Mathlib.CategoryTheory.Types
import Mathlib.Data.Fintype.BigOperators
import Mathlib.Logic.Equiv.Fin
import Mathlib.Tactic.FinCases
/-!
# Real Lorentz Tensors
@ -61,10 +61,9 @@ structure RealLorentzTensor (d : ℕ) (X : Type) where
coord : RealLorentzTensor.IndexValue d color → ℝ
namespace RealLorentzTensor
open Matrix CategoryTheory
open Matrix
universe u1
variable {d : ℕ} {X Y Z : Type}
variable (c : X → Colors)
variable {d : ℕ} {X Y Z : Type} (c : X → Colors)
/-!
@ -144,7 +143,7 @@ def indexValueIso (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors}
Equiv.piCongrLeft (fun y => RealLorentzTensor.ColorsIndex d (j y)) f
lemma indexValueIso_symm_apply' (d : ℕ) (f : X ≃ Y) {i : X → Colors} {j : Y → Colors}
(h : i = j ∘ f) (y : IndexValue d j) (x : X) :
(h : i = j ∘ f) (y : IndexValue d j) (x : X) :
(indexValueIso d f h).symm y x = (colorsIndexCast (congrFun h x)).symm (y (f x)) := by
rfl
@ -324,7 +323,7 @@ def UnmarkedIndexValue (T : Marked d X n) : Type :=
instance [Fintype X] [DecidableEq X] (T : Marked d X n) : Fintype T.UnmarkedIndexValue :=
Pi.fintype
instance [Fintype X] [DecidableEq X] (T : Marked d X n) : DecidableEq T.UnmarkedIndexValue :=
instance [Fintype X] (T : Marked d X n) : DecidableEq T.UnmarkedIndexValue :=
Fintype.decidablePiFintype
/-- The index values restricted to marked indices. -/
@ -334,7 +333,7 @@ def MarkedIndexValue (T : Marked d X n) : Type :=
instance [Fintype X] [DecidableEq X] (T : Marked d X n) : Fintype T.MarkedIndexValue :=
Pi.fintype
instance [Fintype X] [DecidableEq X] (T : Marked d X n) : DecidableEq T.MarkedIndexValue :=
instance [Fintype X] (T : Marked d X n) : DecidableEq T.MarkedIndexValue :=
Fintype.decidablePiFintype
lemma color_eq_elim (T : Marked d X n) :

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

@ -167,12 +167,13 @@ lemma toTensorRepMat_oneMarkedIndexValue_dual (T : Marked d X 1) (S : Marked d Y
(oneMarkedIndexValue x) := by
rw [toTensorRepMat_apply, toTensorRepMat_apply]
erw [Finset.prod_singleton, Finset.prod_singleton]
simp
simp only [Fin.zero_eta, Fin.isValue, lorentzGroupIsGroup_inv]
rw [colorMatrix_cast h, colorMatrix_dual_cast]
rw [Matrix.reindex_apply, Matrix.reindex_apply]
simp
simp only [Fin.isValue, lorentzGroupIsGroup_inv, minkowskiMetric.dual_dual, Subtype.coe_eta,
Equiv.symm_symm, Matrix.submatrix_apply]
rw [colorMatrix_transpose]
simp
simp only [Fin.isValue, Matrix.transpose_apply]
apply congrArg
simp only [Fin.isValue, oneMarkedIndexValue, colorsIndexDualCast, Equiv.coe_fn_symm_mk,
Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.coe_fn_mk, Equiv.apply_symm_apply,
@ -276,7 +277,7 @@ lemma lorentzAction_mapIso (f : X ≃ Y) (Λ : LorentzGroup d) (T : RealLorentzT
rw [mapIso_apply_coord]
rw [lorentzAction_smul_coord', lorentzAction_smul_coord']
let is : IndexValue d T.color ≃ IndexValue d ((mapIso d f) T).color :=
indexValueIso d f (by funext x ; simp)
indexValueIso d f (by funext x; simp)
rw [← Equiv.sum_comp is]
refine Finset.sum_congr rfl (fun j _ => ?_)
rw [mapIso_apply_coord]