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

refactor: Renaming

Browse source
This commit is contained in:
jstoobysmith 2024-11-08 07:11:57 +00:00
parent 87865a00b7
commit 87aae0f879
2 changed files with 27 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean/SpaceTime/LorentzVector/Real/Basic.lean
View file

@ -30,11 +30,11 @@ namespace Lorentz
/-- The representation of `LorentzGroup d` on real vectors corresponding to contravariant
Lorentz vectors. In index notation these have an up index `ψⁱ`. -/
def Contr (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of ContrℝModule.rep
def Contr (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of ContrMod.rep
/-- The representation of `LorentzGroup d` on real vectors corresponding to covariant
Lorentz vectors. In index notation these have an up index `ψⁱ`. -/
def Co (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of CoℝModule.rep
def Co (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of CoMod.rep
end Lorentz
end

50
HepLean/SpaceTime/LorentzVector/Real/Modules.lean
View file

@ -26,16 +26,16 @@ open MatrixGroups
open Complex
/-- The module for contravariant (up-index) real Lorentz vectors. -/
structure ContrℝModule (d : ℕ) where
structure ContrMod (d : ℕ) where
/-- The underlying value as a vector `Fin 1 ⊕ Fin d → ℝ`. -/
val : Fin 1 ⊕ Fin d → ℝ
namespace ContrℝModule
namespace ContrMod
variable {d : ℕ}
/-- The equivalence between `ContrℝModule` and `Fin 1 ⊕ Fin d → ℂ`. -/
def toFin1dℝFun : ContrℝModule d ≃ (Fin 1 ⊕ Fin d → ℝ) where
def toFin1dℝFun : ContrMod d ≃ (Fin 1 ⊕ Fin d → ℝ) where
toFun v := v.val
invFun f := ⟨f⟩
left_inv _ := rfl
@ -43,62 +43,62 @@ def toFin1dℝFun : ContrℝModule d ≃ (Fin 1 ⊕ Fin d → ℝ) where
/-- The instance of `AddCommMonoid` on `ContrℝModule` defined via its equivalence
with `Fin 1 ⊕ Fin d → ℝ`. -/
instance : AddCommMonoid (ContrℝModule d) := Equiv.addCommMonoid toFin1dℝFun
instance : AddCommMonoid (ContrMod d) := Equiv.addCommMonoid toFin1dℝFun
/-- The instance of `AddCommGroup` on `ContrℝModule` defined via its equivalence
with `Fin 1 ⊕ Fin d → ℝ`. -/
instance : AddCommGroup (ContrℝModule d) := Equiv.addCommGroup toFin1dℝFun
instance : AddCommGroup (ContrMod d) := Equiv.addCommGroup toFin1dℝFun
/-- The instance of `Module` on `ContrℝModule` defined via its equivalence
with `Fin 1 ⊕ Fin d → ℝ`. -/
instance : Module ℝ (ContrℝModule d) := Equiv.module ℝ toFin1dℝFun
instance : Module ℝ (ContrMod d) := Equiv.module ℝ toFin1dℝFun
@[ext]
lemma ext (ψ ψ' : ContrℝModule d) (h : ψ.val = ψ'.val) : ψ = ψ' := by
lemma ext (ψ ψ' : ContrMod d) (h : ψ.val = ψ'.val) : ψ = ψ' := by
cases ψ
cases ψ'
subst h
rfl
@[simp]
lemma val_add (ψ ψ' : ContrℝModule d) : (ψ + ψ').val = ψ.val + ψ'.val := rfl
lemma val_add (ψ ψ' : ContrMod d) : (ψ + ψ').val = ψ.val + ψ'.val := rfl
@[simp]
lemma val_smul (r : ℝ) (ψ : ContrℝModule d) : (r • ψ).val = r • ψ.val := rfl
lemma val_smul (r : ℝ) (ψ : ContrMod d) : (r • ψ).val = r • ψ.val := rfl
/-- The linear equivalence between `ContrℝModule` and `(Fin 1 ⊕ Fin d → ℝ)`. -/
@[simps!]
def toFin1dℝEquiv : ContrℝModule d ≃ₗ[ℝ] (Fin 1 ⊕ Fin d → ℝ) :=
def toFin1dℝEquiv : ContrMod d ≃ₗ[ℝ] (Fin 1 ⊕ Fin d → ℝ) :=
Equiv.linearEquiv ℝ toFin1dℝFun
/-- The underlying element of `Fin 1 ⊕ Fin d → ℝ` of a element in `ContrℝModule` defined
through the linear equivalence `toFin1dℝEquiv`. -/
abbrev toFin1dℝ (ψ : ContrℝModule d) := toFin1dℝEquiv ψ
abbrev toFin1dℝ (ψ : ContrMod d) := toFin1dℝEquiv ψ
/-- The standard basis of `ContrℝModule` indexed by `Fin 1 ⊕ Fin d`. -/
@[simps!]
def stdBasis : Basis (Fin 1 ⊕ Fin d) ℝ (ContrℝModule d) := Basis.ofEquivFun toFin1dℝEquiv
def stdBasis : Basis (Fin 1 ⊕ Fin d) ℝ (ContrMod d) := Basis.ofEquivFun toFin1dℝEquiv
/-- The representation of the Lorentz group acting on `ContrℝModule d`. -/
def rep : Representation ℝ (LorentzGroup d) (ContrℝModule d) where
def rep : Representation ℝ (LorentzGroup d) (ContrMod d) where
toFun g := Matrix.toLinAlgEquiv stdBasis g
map_one' := (MulEquivClass.map_eq_one_iff (Matrix.toLinAlgEquiv stdBasis)).mpr rfl
map_mul' x y := by
simp only [lorentzGroupIsGroup_mul_coe, _root_.map_mul]
end ContrℝModule
end ContrMod
/-- The module for covariant (up-index) complex Lorentz vectors. -/
structure CoℝModule (d : ℕ) where
structure CoMod (d : ℕ) where
/-- The underlying value as a vector `Fin 1 ⊕ Fin d → ℝ`. -/
val : Fin 1 ⊕ Fin d → ℝ
namespace CoℝModule
namespace CoMod
variable {d : ℕ}
/-- The equivalence between `CoℝModule` and `Fin 1 ⊕ Fin d → ℝ`. -/
def toFin1dℝFun : CoℝModule d ≃ (Fin 1 ⊕ Fin d → ℝ) where
def toFin1dℝFun : CoMod d ≃ (Fin 1 ⊕ Fin d → ℝ) where
toFun v := v.val
invFun f := ⟨f⟩
left_inv _ := rfl
@ -106,31 +106,31 @@ def toFin1dℝFun : CoℝModule d ≃ (Fin 1 ⊕ Fin d → ℝ) where
/-- The instance of `AddCommMonoid` on `CoℂModule` defined via its equivalence
with `Fin 1 ⊕ Fin d → ℝ`. -/
instance : AddCommMonoid (CoℝModule d) := Equiv.addCommMonoid toFin1dℝFun
instance : AddCommMonoid (CoMod d) := Equiv.addCommMonoid toFin1dℝFun
/-- The instance of `AddCommGroup` on `CoℝModule` defined via its equivalence
with `Fin 1 ⊕ Fin d → ℝ`. -/
instance : AddCommGroup (CoℝModule d) := Equiv.addCommGroup toFin1dℝFun
instance : AddCommGroup (CoMod d) := Equiv.addCommGroup toFin1dℝFun
/-- The instance of `Module` on `CoℝModule` defined via its equivalence
with `Fin 1 ⊕ Fin d → ℝ`. -/
instance : Module ℝ (CoℝModule d) := Equiv.module ℝ toFin1dℝFun
instance : Module ℝ (CoMod d) := Equiv.module ℝ toFin1dℝFun
/-- The linear equivalence between `CoℝModule` and `(Fin 1 ⊕ Fin d → ℝ)`. -/
@[simps!]
def toFin1dℝEquiv : CoℝModule d ≃ₗ[ℝ] (Fin 1 ⊕ Fin d → ℝ) :=
def toFin1dℝEquiv : CoMod d ≃ₗ[ℝ] (Fin 1 ⊕ Fin d → ℝ) :=
Equiv.linearEquiv ℝ toFin1dℝFun
/-- The underlying element of `Fin 1 ⊕ Fin d → ℝ` of a element in `CoℝModule` defined
through the linear equivalence `toFin1dℝEquiv`. -/
abbrev toFin1dℝ (ψ : CoℝModule d) := toFin1dℝEquiv ψ
abbrev toFin1dℝ (ψ : CoMod d) := toFin1dℝEquiv ψ
/-- The standard basis of `CoℝModule` indexed by `Fin 1 ⊕ Fin d`. -/
@[simps!]
def stdBasis : Basis (Fin 1 ⊕ Fin d) ℝ (CoℝModule d) := Basis.ofEquivFun toFin1dℝEquiv
def stdBasis : Basis (Fin 1 ⊕ Fin d) ℝ (CoMod d) := Basis.ofEquivFun toFin1dℝEquiv
/-- The representation of the Lorentz group acting on `CoℝModule d`. -/
def rep : Representation ℝ (LorentzGroup d) (CoℝModule d) where
def rep : Representation ℝ (LorentzGroup d) (CoMod d) where
toFun g := Matrix.toLinAlgEquiv stdBasis (LorentzGroup.transpose g⁻¹)
map_one' := by
simp only [inv_one, LorentzGroup.transpose_one, lorentzGroupIsGroup_one_coe, _root_.map_one]
@ -138,7 +138,7 @@ def rep : Representation ℝ (LorentzGroup d) (CoℝModule d) where
simp only [_root_.mul_inv_rev, lorentzGroupIsGroup_inv, LorentzGroup.transpose_mul,
lorentzGroupIsGroup_mul_coe, _root_.map_mul]
end CoℝModule
end CoMod
end
end Lorentz