1. Physlib
  2. Relativity
  3. Tensors
  4. RealTensor
  5. Vector
  6. Pre
  7. Modules
Imports
/- Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.Relativity.PauliMatrices.SelfAdjoint public import Mathlib.RepresentationTheory.Basic public import Physlib.Relativity.LorentzGroup.Basic public import Mathlib.Analysis.InnerProductSpace.PiL2

Modules associated with Real Lorentz vectors

We define the modules underlying real Lorentz vectors.

These definitions are preludes to the definitions of Lorentz.contr and Lorentz.co.

@[expose] public section

The module for contravariant (up-index) real Lorentz vectors.

The underlying value as a vector Fin 1 ⊕ Fin d → ℝ.

structure ContrMod (d : ℕ) where val : Fin 1 ⊕ Fin d → ℝ
@[ext] lemma ext {ψ ψ' : ContrMod d} (h : ψ.val = ψ'.val) : ψ = ψ' := d:ℕψ:ContrMod dψ':ContrMod dh:ψ.val = ψ'.val⊢ ψ = ψ' d:ℕψ':ContrMod dval✝:Fin 1 ⊕ Fin d → ℝh:{ val := val✝ }.val = ψ'.val⊢ { val := val✝ } = ψ' d:ℕval✝¹:Fin 1 ⊕ Fin d → ℝval✝:Fin 1 ⊕ Fin d → ℝh:{ val := val✝¹ }.val = { val := val✝ }.val⊢ { val := val✝¹ } = { val := val✝ } d:ℕval✝:Fin 1 ⊕ Fin d → ℝ⊢ { val := val✝ } = { val := { val := val✝ }.val } All goals completed! 🐙

The equivalence between ContrℝModule and Fin 1 ⊕ Fin d → ℂ.

def toFin1dℝFun : ContrMod d ≃ (Fin 1 ⊕ Fin d → ℝ) where toFun v := v.val invFun f := ⟨f⟩ left_inv _ := rfl right_inv _ := rfl

The instance of AddCommGroup on ContrℝModule defined via its equivalence with Fin 1 ⊕ Fin d → ℝ.

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 ℝ (ContrMod d) := Equiv.module ℝ toFin1dℝFun
@[simp] lemma val_add (ψ ψ' : ContrMod d) : (ψ + ψ').val = ψ.val + ψ'.val := rfl@[simp] lemma val_smul (r : ℝ) (ψ : ContrMod d) : (r • ψ).val = r • ψ.val := rfl

The linear equivalence between ContrℝModule and (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ℝ (ψ : ContrMod d) := toFin1dℝEquiv ψ
lemma toFin1dℝ_eq_val (ψ : ContrMod d) : ψ.toFin1dℝ = ψ.val := d:ℕψ:ContrMod d⊢ ψ.toFin1dℝ = ψ.val All goals completed! 🐙

The standard basis.

The standard basis of ContrℝModule indexed by Fin 1 ⊕ Fin d.

def stdBasis : Basis (Fin 1 ⊕ Fin d) ℝ (ContrMod d) := Basis.ofEquivFun toFin1dℝEquiv
d:ℕμ:Fin 1 ⊕ Fin d⊢ Pi.single μ 1 μ = 1 All goals completed! 🐙@[simp] lemma stdBasis_apply_same (μ : Fin 1 ⊕ Fin d) : (stdBasis μ).val μ = 1 := stdBasis_toFin1dℝEquiv_apply_same μd:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dh:μ ≠ ν⊢ Pi.single μ 1 ν = 0 All goals completed! 🐙@[simp] lemma stdBasis_inl_apply_inr (i : Fin d) : (stdBasis (Sum.inl 0)).val (Sum.inr i) = 0 := d:ℕi:Fin d⊢ (stdBasis (Sum.inl 0)).val (Sum.inr i) = 0 d:ℕi:Fin d⊢ Sum.inl 0 ≠ Sum.inr i All goals completed! 🐙lemma stdBasis_apply (μ ν : Fin 1 ⊕ Fin d) : (stdBasis μ).val ν = if μ = ν then 1 else 0 := d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (stdBasis μ).val ν = if μ = ν then 1 else 0 d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (toFin1dℝEquiv.symm (Pi.single μ 1)).val ν = if μ = ν then 1 else 0 d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ Pi.single μ 1 ν = if μ = ν then 1 else 0 d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (if ν = μ then 1 else 0) = if μ = ν then 1 else 0 d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (ν = μ) = (μ = ν) All goals completed! 🐙

Decomposition of a contravariant Lorentz vector into the standard basis.

d:ℕv:ContrMod dμ:Fin 1 ⊕ Fin db:Fin 1 ⊕ Fin da✝:b ∈ Finset.univhbμ:b ≠ μ⊢ toFin1dℝEquiv v b • 0 = 0 All goals completed! 🐙

mulVec

Multiplication of a matrix with a vector in ContrMod.

abbrev mulVec (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) : ContrMod d := Matrix.toLinAlgEquiv stdBasis M v

Multiplication of a matrix with a vector in ContrMod.

scoped[Lorentz] infixr:73 " *ᵥ " => ContrMod.mulVec
@[simp] lemma mulVec_toFin1dℝ (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) : (M *ᵥ v).toFin1dℝ = M *ᵥ v.toFin1dℝ := d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝv:ContrMod d⊢ (M *ᵥ v).toFin1dℝ = M *ᵥ v.toFin1dℝ All goals completed! 🐙@[simp] lemma mulVec_val (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) : (M *ᵥ v).val = M *ᵥ v.val := d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝv:ContrMod d⊢ (M *ᵥ v).val = M *ᵥ v.val All goals completed! 🐙lemma mulVec_sub (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v w : ContrMod d) : M *ᵥ (v - w) = M *ᵥ v - M *ᵥ w := d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝv:ContrMod dw:ContrMod d⊢ M *ᵥ (v - w) = M *ᵥ v - M *ᵥ w All goals completed! 🐙lemma sub_mulVec (M N : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) : (M - N) *ᵥ v = M *ᵥ v - N *ᵥ v := d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝN:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝv:ContrMod d⊢ (M - N) *ᵥ v = M *ᵥ v - N *ᵥ v All goals completed! 🐙lemma mulVec_add (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v w : ContrMod d) : M *ᵥ (v + w) = M *ᵥ v + M *ᵥ w := d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝv:ContrMod dw:ContrMod d⊢ M *ᵥ (v + w) = M *ᵥ v + M *ᵥ w All goals completed! 🐙@[simp] lemma one_mulVec (v : ContrMod d) : (1 : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) *ᵥ v = v := d:ℕv:ContrMod d⊢ 1 *ᵥ v = v All goals completed! 🐙lemma mulVec_mulVec (M N : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : ContrMod d) : M *ᵥ (N *ᵥ v) = (M * N) *ᵥ v := d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝN:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝv:ContrMod d⊢ M *ᵥ N *ᵥ v = (M * N) *ᵥ v All goals completed! 🐙

The norm

(Not the Minkowski norm, but the norm of a vector in ContrℝModule d.)

A NormedAddCommGroup structure on ContrMod. This is not an instance, as we don't want it to be applied always.

@[reducible] def norm : NormedAddCommGroup (ContrMod d) where norm v := ‖v.val‖₊ dist_self x := Pi.normedAddCommGroup.dist_self x.val dist_triangle x y z := Pi.normedAddCommGroup.dist_triangle x.val y.val z.val dist_comm x y := Pi.normedAddCommGroup.dist_comm x.val y.val eq_of_dist_eq_zero {x y} := fun h => ext (MetricSpace.eq_of_dist_eq_zero h) dist_eq x y := Pi.normedAddCommGroup.dist_eq x.val y.val

The underlying space part of a ContrMod formed by removing the first element. A better name for this might be tail.

def toSpace (v : ContrMod d) : EuclideanSpace ℝ (Fin d) := WithLp.toLp 2 (v.val ∘ Sum.inr)

The representation.

The representation of the Lorentz group acting on ContrℝModule d.

def rep : Representation ℝ (LorentzGroup d) (ContrMod d) where toFun g := Matrix.toLinAlgEquiv stdBasis g map_one' := EmbeddingLike.map_eq_one_iff.mpr rfl map_mul' x y := d:ℕx:↑(LorentzGroup d)y:↑(LorentzGroup d)⊢ (toLinAlgEquiv stdBasis) ↑(x * y) = (toLinAlgEquiv stdBasis) ↑x * (toLinAlgEquiv stdBasis) ↑y All goals completed! 🐙
lemma rep_apply_toFin1dℝ (g : LorentzGroup d) (ψ : ContrMod d) : (rep g ψ).toFin1dℝ = g.1 *ᵥ ψ.toFin1dℝ := d:ℕg:↑(LorentzGroup d)ψ:ContrMod d⊢ ((rep g) ψ).toFin1dℝ = ↑g *ᵥ ψ.toFin1dℝ All goals completed! 🐙

To Self-Adjoint Matrix

The linear equivalence between the vector-space ContrMod 3 and self-adjoint 2×2-complex matrices.

def toSelfAdjoint : ContrMod 3 ≃ₗ[ℝ] selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ) := toFin1dℝEquiv ≪≫ₗ (Finsupp.linearEquivFunOnFinite ℝ ℝ (Fin 1 ⊕ Fin 3)).symm ≪≫ₗ PauliMatrix.pauliBasis'.repr.symm
x:ContrMod 3⊢ ↑(x.toFin1dℝ (Sum.inl 0) • ⟨PauliMatrix.pauliMatrix (Sum.inl 0), ⋯⟩ - x.toFin1dℝ (Sum.inr 0) • ⟨PauliMatrix.pauliMatrix (Sum.inr 0), ⋯⟩ - x.toFin1dℝ (Sum.inr 1) • ⟨PauliMatrix.pauliMatrix (Sum.inr 1), ⋯⟩ - x.toFin1dℝ (Sum.inr 2) • ⟨PauliMatrix.pauliMatrix (Sum.inr 2), ⋯⟩) = x.toFin1dℝ (Sum.inl 0) • PauliMatrix.pauliMatrix (Sum.inl 0) - x.toFin1dℝ (Sum.inr 0) • PauliMatrix.pauliMatrix (Sum.inr 0) - x.toFin1dℝ (Sum.inr 1) • PauliMatrix.pauliMatrix (Sum.inr 1) - x.toFin1dℝ (Sum.inr 2) • PauliMatrix.pauliMatrix (Sum.inr 2) All goals completed! 🐙i:Fin 1 ⊕ Fin 3⊢ (stdBasis i).toFin1dℝ (Sum.inl 0) • ⟨PauliMatrix.pauliMatrix (Sum.inl 0), ⋯⟩ - (stdBasis i).toFin1dℝ (Sum.inr 0) • ⟨PauliMatrix.pauliMatrix (Sum.inr 0), ⋯⟩ - (stdBasis i).toFin1dℝ (Sum.inr 1) • ⟨PauliMatrix.pauliMatrix (Sum.inr 1), ⋯⟩ - (stdBasis i).toFin1dℝ (Sum.inr 2) • ⟨PauliMatrix.pauliMatrix (Sum.inr 2), ⋯⟩ = PauliMatrix.pauliBasis' i match i with i:Fin 1 ⊕ Fin 3⊢ (stdBasis (Sum.inl 0)).toFin1dℝ (Sum.inl 0) • ⟨PauliMatrix.pauliMatrix (Sum.inl 0), ⋯⟩ - (stdBasis (Sum.inl 0)).toFin1dℝ (Sum.inr 0) • ⟨PauliMatrix.pauliMatrix (Sum.inr 0), ⋯⟩ - (stdBasis (Sum.inl 0)).toFin1dℝ (Sum.inr 1) • ⟨PauliMatrix.pauliMatrix (Sum.inr 1), ⋯⟩ - (stdBasis (Sum.inl 0)).toFin1dℝ (Sum.inr 2) • ⟨PauliMatrix.pauliMatrix (Sum.inr 2), ⋯⟩ = PauliMatrix.pauliBasis' (Sum.inl 0) All goals completed! 🐙 i:Fin 1 ⊕ Fin 3⊢ (stdBasis (Sum.inr 0)).toFin1dℝ (Sum.inl 0) • ⟨PauliMatrix.pauliMatrix (Sum.inl 0), ⋯⟩ - (stdBasis (Sum.inr 0)).toFin1dℝ (Sum.inr 0) • ⟨PauliMatrix.pauliMatrix (Sum.inr 0), ⋯⟩ - (stdBasis (Sum.inr 0)).toFin1dℝ (Sum.inr 1) • ⟨PauliMatrix.pauliMatrix (Sum.inr 1), ⋯⟩ - (stdBasis (Sum.inr 0)).toFin1dℝ (Sum.inr 2) • ⟨PauliMatrix.pauliMatrix (Sum.inr 2), ⋯⟩ = PauliMatrix.pauliBasis' (Sum.inr 0) i:Fin 1 ⊕ Fin 3⊢ -⟨PauliMatrix.pauliMatrix (Sum.inr 0), ⋯⟩ = ⟨-PauliMatrix.pauliMatrix (Sum.inr 0), PauliMatrix.pauliSelfAdjoint'._proof_3⟩ All goals completed! 🐙 i:Fin 1 ⊕ Fin 3⊢ (stdBasis (Sum.inr 1)).toFin1dℝ (Sum.inl 0) • ⟨PauliMatrix.pauliMatrix (Sum.inl 0), ⋯⟩ - (stdBasis (Sum.inr 1)).toFin1dℝ (Sum.inr 0) • ⟨PauliMatrix.pauliMatrix (Sum.inr 0), ⋯⟩ - (stdBasis (Sum.inr 1)).toFin1dℝ (Sum.inr 1) • ⟨PauliMatrix.pauliMatrix (Sum.inr 1), ⋯⟩ - (stdBasis (Sum.inr 1)).toFin1dℝ (Sum.inr 2) • ⟨PauliMatrix.pauliMatrix (Sum.inr 2), ⋯⟩ = PauliMatrix.pauliBasis' (Sum.inr 1) i:Fin 1 ⊕ Fin 3⊢ -⟨PauliMatrix.pauliMatrix (Sum.inr 1), ⋯⟩ = ⟨-PauliMatrix.pauliMatrix (Sum.inr 1), PauliMatrix.pauliSelfAdjoint'._proof_4⟩ All goals completed! 🐙 i:Fin 1 ⊕ Fin 3⊢ (stdBasis (Sum.inr 2)).toFin1dℝ (Sum.inl 0) • ⟨PauliMatrix.pauliMatrix (Sum.inl 0), ⋯⟩ - (stdBasis (Sum.inr 2)).toFin1dℝ (Sum.inr 0) • ⟨PauliMatrix.pauliMatrix (Sum.inr 0), ⋯⟩ - (stdBasis (Sum.inr 2)).toFin1dℝ (Sum.inr 1) • ⟨PauliMatrix.pauliMatrix (Sum.inr 1), ⋯⟩ - (stdBasis (Sum.inr 2)).toFin1dℝ (Sum.inr 2) • ⟨PauliMatrix.pauliMatrix (Sum.inr 2), ⋯⟩ = PauliMatrix.pauliBasis' (Sum.inr 2) i:Fin 1 ⊕ Fin 3⊢ -⟨PauliMatrix.pauliMatrix (Sum.inr 2), ⋯⟩ = ⟨-PauliMatrix.pauliMatrix (Sum.inr 2), PauliMatrix.pauliSelfAdjoint'._proof_5⟩ All goals completed! 🐙All goals completed! 🐙

Topology

The type ContrMod d carries an instance of a topological group, induced by it's equivalence to Fin 1 ⊕ Fin d → ℝ.

instance : TopologicalSpace (ContrMod d) := TopologicalSpace.induced ContrMod.toFin1dℝEquiv (Pi.topologicalSpace)
lemma toFin1dℝEquiv_isInducing : IsInducing (@ContrMod.toFin1dℝEquiv d) := d:ℕ⊢ IsInducing ⇑toFin1dℝEquiv All goals completed! 🐙lemma toFin1dℝEquiv_symm_isInducing : IsInducing ((@ContrMod.toFin1dℝEquiv d).symm) := d:ℕ⊢ IsInducing ⇑toFin1dℝEquiv.symm d:ℕx:ContrMod d ≃ₜ (Fin 1 ⊕ Fin d → ℝ) := toFin1dℝEquiv.toEquiv.toHomeomorphOfIsInducing ⋯⊢ IsInducing ⇑toFin1dℝEquiv.symm All goals completed! 🐙

The module for covariant (up-index) complex Lorentz vectors.

The underlying value as a vector Fin 1 ⊕ Fin d → ℝ.

structure CoMod (d : ℕ) where val : Fin 1 ⊕ Fin d → ℝ
@[ext] lemma ext {ψ ψ' : CoMod d} (h : ψ.val = ψ'.val) : ψ = ψ' := d:ℕψ:CoMod dψ':CoMod dh:ψ.val = ψ'.val⊢ ψ = ψ' d:ℕψ':CoMod dval✝:Fin 1 ⊕ Fin d → ℝh:{ val := val✝ }.val = ψ'.val⊢ { val := val✝ } = ψ' d:ℕval✝¹:Fin 1 ⊕ Fin d → ℝval✝:Fin 1 ⊕ Fin d → ℝh:{ val := val✝¹ }.val = { val := val✝ }.val⊢ { val := val✝¹ } = { val := val✝ } d:ℕval✝:Fin 1 ⊕ Fin d → ℝ⊢ { val := val✝ } = { val := { val := val✝ }.val } All goals completed! 🐙

The equivalence between CoℝModule and Fin 1 ⊕ Fin d → ℝ.

def toFin1dℝFun : CoMod d ≃ (Fin 1 ⊕ Fin d → ℝ) where toFun v := v.val invFun f := ⟨f⟩ left_inv _ := rfl right_inv _ := rfl

The instance of AddCommGroup on CoℝModule defined via its equivalence with Fin 1 ⊕ Fin d → ℝ.

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 ℝ (CoMod d) := Equiv.module ℝ toFin1dℝFun

The linear equivalence between CoℝModule and (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ℝ (ψ : CoMod d) := toFin1dℝEquiv ψ

The standard basis.

The standard basis of CoℝModule indexed by Fin 1 ⊕ Fin d.

def stdBasis : Basis (Fin 1 ⊕ Fin d) ℝ (CoMod d) := Basis.ofEquivFun toFin1dℝEquiv
d:ℕμ:Fin 1 ⊕ Fin d⊢ Pi.single μ 1 μ = 1 All goals completed! 🐙@[simp] lemma stdBasis_apply_same (μ : Fin 1 ⊕ Fin d) : (stdBasis μ).val μ = 1 := stdBasis_toFin1dℝEquiv_apply_same μd:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin dh:μ ≠ ν⊢ Pi.single μ 1 ν = 0 All goals completed! 🐙lemma stdBasis_apply (μ ν : Fin 1 ⊕ Fin d) : (stdBasis μ).val ν = if μ = ν then 1 else 0 := d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (stdBasis μ).val ν = if μ = ν then 1 else 0 d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (toFin1dℝEquiv.symm (Pi.single μ 1)).val ν = if μ = ν then 1 else 0 d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ Pi.single μ 1 ν = if μ = ν then 1 else 0 d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (if ν = μ then 1 else 0) = if μ = ν then 1 else 0 d:ℕμ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ (ν = μ) = (μ = ν) All goals completed! 🐙

Decomposition of a covariant Lorentz vector into the standard basis.

d:ℕv:CoMod dμ:Fin 1 ⊕ Fin db:Fin 1 ⊕ Fin da✝:b ∈ Finset.univhbμ:b ≠ μ⊢ toFin1dℝEquiv v b • 0 = 0 All goals completed! 🐙

mulVec

Multiplication of a matrix with a vector in CoMod.

abbrev mulVec (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : CoMod d) : CoMod d := Matrix.toLinAlgEquiv stdBasis M v

Multiplication of a matrix with a vector in CoMod.

scoped[Lorentz] infixr:73 " *ᵥ " => CoMod.mulVec
@[simp] lemma mulVec_toFin1dℝ (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : CoMod d) : (M *ᵥ v).toFin1dℝ = M *ᵥ v.toFin1dℝ := d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝv:CoMod d⊢ (M *ᵥ v).toFin1dℝ = M *ᵥ v.toFin1dℝ All goals completed! 🐙@[simp] lemma mulVec_val (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v : CoMod d) : (M *ᵥ v).val = M *ᵥ v.val := d:ℕM:Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝv:CoMod d⊢ (M *ᵥ v).val = M *ᵥ v.val All goals completed! 🐙

The representation

The representation of the Lorentz group acting on CoℝModule d.

def rep : Representation ℝ (LorentzGroup d) (CoMod d) where toFun g := Matrix.toLinAlgEquiv stdBasis (LorentzGroup.transpose g⁻¹) map_one' := d:ℕ⊢ (toLinAlgEquiv stdBasis) ↑(LorentzGroup.transpose 1⁻¹) = 1 All goals completed! 🐙 map_mul' x y := d:ℕx:↑(LorentzGroup d)y:↑(LorentzGroup d)⊢ (toLinAlgEquiv stdBasis) ↑(LorentzGroup.transpose (x * y)⁻¹) = (toLinAlgEquiv stdBasis) ↑(LorentzGroup.transpose x⁻¹) * (toLinAlgEquiv stdBasis) ↑(LorentzGroup.transpose y⁻¹) All goals completed! 🐙