The Lorentz action on the electric and magnetic fields.

The Lorentz group acts on a pair of a electric and magnetic field. The map toElectricMagneticField is equivariant, which turns a field strength into a pair of electric and magnetic fieldd, is equivariant with respect to this action.

TODO

This file currently only contains semiformal results, which

instance Electromagnetism.lorentzAction : MulAction (↑(LorentzGroup 3)) (ElectricField × MagneticField)

The Lorentz action on the electric and magnetic fields.

Equations

• Electromagnetism.lorentzAction = sorry

theorem Electromagnetism.toElectricMagneticField_equivariant (d : ℕ) (g : ↑(LorentzGroup 3)) (E : ElectricField) (B : MagneticField) (x : SpaceTime) : ↑(FieldStrength.toElectricMagneticField.symm (SMul.smul g (E, B))) x = ((realLorentzTensor.F.obj (IndexNotation.OverColor.mk ![realLorentzTensor.Color.up, realLorentzTensor.Color.up])).ρ g) (↑(FieldStrength.toElectricMagneticField.symm (E, B)) x)

The equivalence toElectricMagneticField is equivariant with respect to the group action.