The Lorentz action on the electric and magnetic fields

i. Overview

We find the transformations of the electric and magnetic fields under a Lorentz boost in the x direction.

ii. Key results

• electricField_apply_x_boost : The transformation of the electric field under a boost in the x direction.
• magneticField_apply_x_boost : The transformation of the magnetic field under a boost in the x direction.

iii. Table of contents

• A. Boost of the electric field
• B. Boost of the magnetic field

iv. References

See e.g.

• https://en.wikipedia.org/wiki/Classical_electromagnetism_and_special_relativity

A. Boost of the electric field

The electric field E in a frame F following a boost in the x direction with speed β with |β| < 1 compared to a frame F' at a point x := (t, x, y, z) is related to the electric E' and magnetic fields B' in F' at the point x' := (γ (t + β x), γ (x + β t), y, z) (corresponding to the same space-time point) by:

• E_x x = E'_x x',
• E_y x = γ (E'_y x' - β B_z x'),
• E_z x = γ (E'_z x' + β B_y x').

theorem Electromagnetism.ElectromagneticPotential.electricField_apply_x_boost (β : ℝ) (hβ : |β| < 1) (A : ElectromagneticPotential) (hA : Differentiable ℝ A) (t : Time) (x : Space) : have Λ := LorentzGroup.boost 0 β hβ; have t' := { val := LorentzGroup.γ β * (t.val + β * x 0) }; have x' := fun (x_1 : Fin 3) => match x_1 with | 0 => LorentzGroup.γ β * (x 0 + β * t.val) | 1 => x 1 | 2 => x 2; electricField (fun (x : SpaceTime) => Λ • A (Λ⁻¹ • x)) t x = fun (x : Fin 3) => match x with | 0 => A.electricField t' x' 0 | 1 => LorentzGroup.γ β * (A.electricField t' x' 1 - β * A.magneticField t' x' 2) | 2 => LorentzGroup.γ β * (A.electricField t' x' 2 + β * A.magneticField t' x' 1)

B. Boost of the magnetic field

The magnetic field B in a frame F following a boost in the x direction with speed β with |β| < 1 compared to a frame F' at a point x := (t, x, y, z) is related to the electric E' and magnetic fields B' in F' at the point x' := (γ (t + β x), γ (x + β t), y, z) (corresponding to the same space-time point) by:

• B_x x = B'_x x',
• B_y x = γ (B'_y x' + β E_z x'),
• B_z x = γ (B'_z x' - β E_y x').

theorem Electromagnetism.ElectromagneticPotential.magneticField_apply_x_boost (β : ℝ) (hβ : |β| < 1) (A : ElectromagneticPotential) (hA : Differentiable ℝ A) (t : Time) (x : Space) : have Λ := LorentzGroup.boost 0 β hβ; have t' := { val := LorentzGroup.γ β * (t.val + β * x 0) }; have x' := fun (x_1 : Fin 3) => match x_1 with | 0 => LorentzGroup.γ β * (x 0 + β * t.val) | 1 => x 1 | 2 => x 2; magneticField (fun (x : SpaceTime) => Λ • A (Λ⁻¹ • x)) t x = fun (x : Fin 3) => match x with | 0 => A.magneticField t' x' 0 | 1 => LorentzGroup.γ β * (A.magneticField t' x' 1 + β * A.electricField t' x' 2) | 2 => LorentzGroup.γ β * (A.magneticField t' x' 2 - β * A.electricField t' x' 1)