Real Lorentz vectors

We define real Lorentz vectors in as representations of the Lorentz group.

def Lorentz.Contr (d : ℕ) : Rep ℝ ↑(LorentzGroup d)

The representation of LorentzGroup d on real vectors corresponding to contravariant Lorentz vectors. In index notation these have an up index ψⁱ.

Equations

• Lorentz.Contr d = Rep.of Lorentz.ContrMod.rep

instance Lorentz.instTopologicalSpaceCarrierRealVModuleCatElemMatrixSumFinOfNatNatLorentzGroupContr {d : ℕ} : TopologicalSpace ↑(Contr d).V

The representation of contravariant Lorentz vectors forms a topological space, induced by its equivalence to Fin 1 ⊕ Fin d → ℝ.

Equations

• Lorentz.instTopologicalSpaceCarrierRealVModuleCatElemMatrixSumFinOfNatNatLorentzGroupContr = TopologicalSpace.induced (⇑Lorentz.ContrMod.toFin1dℝEquiv) Pi.topologicalSpace

theorem Lorentz.continuous_contr {d : ℕ} {T : Type} [TopologicalSpace T] (f : T → ↑(Contr d).V) (h : Continuous fun (i : T) => ContrMod.toFin1dℝ (f i)) : Continuous f

theorem Lorentz.contr_continuous {d : ℕ} {T : Type} [TopologicalSpace T] (f : ↑(Contr d).V → T) (h : Continuous (f ∘ ⇑ContrMod.toFin1dℝEquiv.symm)) : Continuous f

def Lorentz.Co (d : ℕ) : Rep ℝ ↑(LorentzGroup d)

The representation of LorentzGroup d on real vectors corresponding to covariant Lorentz vectors. In index notation these have an up index ψⁱ.

Equations

• Lorentz.Co d = Rep.of Lorentz.CoMod.rep

Isomorphism between contravariant and covariant Lorentz vectors

def Lorentz.Contr.toCo (d : ℕ) : Contr d ⟶ Co d

The morphism of representations from Contr d to Co d defined by multiplication with the metric.

Equations

• One or more equations did not get rendered due to their size.

def Lorentz.Co.toContr (d : ℕ) : Co d ⟶ Contr d

The morphism of representations from Co d to Contr d defined by multiplication with the metric.

Equations

• One or more equations did not get rendered due to their size.

def Lorentz.contrIsoCo (d : ℕ) : Contr d ≅ Co d

The isomorphism between Contr d and Co d induced by multiplication with the Minkowski metric.

Equations

• Lorentz.contrIsoCo d = { hom := Lorentz.Contr.toCo d, inv := Lorentz.Co.toContr d, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Other properties

theorem Lorentz.Contr.ρ_stdBasis (μ : Fin 1 ⊕ Fin 3) (Λ : ↑(LorentzGroup 3)) : ((Contr 3).ρ Λ) (ContrMod.stdBasis μ) = ∑ j : Fin 1 ⊕ Fin 3, ↑Λ j μ • ContrMod.stdBasis j