The Electromagnetic Potential

i. Overview

The electromagnetic potential A^μ is the fundamental objects in electromagnetism. Mathematically it is related to a connection on a U(1)-bundle.

We define the electromagnetic potential as a function from spacetime to contravariant Lorentz vectors.

ii. Key results

• ElectromagneticPotential: is the type of electromagnetic potentials.
• ElectromagneticPotential.deriv: the derivative tensor ∂_μ A^ν.

iii. Table of contents

• A. The electromagnetic potential
  • A.1. The action on the space-time derivatives
  • A.2. Differentiability
  • A.3. Variational adjoint derivative of component
  • A.4. Variational adjoint derivative of derivatives of the potential
• B. The derivative tensor of the electromagnetic potential
  • B.1. Equivariance of the derivative tensor
  • B.2. The elements of the derivative tensor in terms of the basis

iv. References

• https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html
• https://ph.qmul.ac.uk/sites/default/files/EMT10new.pdf

A. The electromagnetic potential

We define the electromagnetic potential as a function from spacetime to contravariant Lorentz vectors, and prove some simple results about it.

@[reducible, inline]

noncomputable abbrev Electromagnetism.ElectromagneticPotential (d : ℕ := 3) : Type

The electromagnetic potential is a tensor A^μ.

Equations

• Electromagnetism.ElectromagneticPotential d = (SpaceTime d → Lorentz.Vector d)

A.1. The action on the space-time derivatives

Given a ElectromagneticPotential A^μ, we can consider its derivative ∂_μ A^ν. Under a Lorentz transformation Λ, this transforms as ∂_ μ (fun x => Λ • A (Λ⁻¹ • x)), we write an expression for this in terms of the tensor. ∂_ ρ A (Λ⁻¹ • x) κ.

theorem Electromagnetism.ElectromagneticPotential.spaceTime_deriv_action_eq_sum {d : ℕ} {μ ν : Fin 1 ⊕ Fin d} {x : SpaceTime d} (Λ : ↑(LorentzGroup d)) (A : ElectromagneticPotential d) (hA : Differentiable ℝ A) : SpaceTime.deriv μ (fun (x : SpaceTime d) => Λ • A (Λ⁻¹ • x)) x ν = ∑ κ : Fin 1 ⊕ Fin d, ∑ ρ : Fin 1 ⊕ Fin d, ↑Λ ν κ * ↑Λ⁻¹ ρ μ * SpaceTime.deriv ρ A (Λ⁻¹ • x) κ

A.2. Differentiability

We show that the components of field strength tensor are differentiable if the potential is.

theorem Electromagnetism.ElectromagneticPotential.differentiable_component {d : ℕ} (A : ElectromagneticPotential d) (hA : Differentiable ℝ A) (μ : Fin 1 ⊕ Fin d) : Differentiable ℝ fun (x : SpaceTime d) => A x μ

A.3. Variational adjoint derivative of component

We find the variational adjoint derivative of the components of the potential. This will be used to find e.g. the variational derivative of the kinetic term, and derive the equations of motion.

theorem Electromagnetism.ElectromagneticPotential.hasVarAdjDerivAt_component {d : ℕ} (μ : Fin 1 ⊕ Fin d) (A : SpaceTime d → Lorentz.Vector d) (hA : ContDiff ℝ (↑⊤) A) : HasVarAdjDerivAt (fun (A' : SpaceTime d → Lorentz.Vector d) (x : SpaceTime d) => A' x μ) (fun (A' : SpaceTime d → ℝ) (x : SpaceTime d) => A' x • Lorentz.Vector.basis μ) A

A.4. Variational adjoint derivative of derivatives of the potential

We find the variational adjoint derivative of the derivatives of the components of the potential. This will again be used to find the variational derivative of the kinetic term, and derive the equations of motion (Maxwell's equations).

theorem Electromagnetism.ElectromagneticPotential.deriv_hasVarAdjDerivAt {d : ℕ} (μ ν : Fin 1 ⊕ Fin d) (A : SpaceTime d → Lorentz.Vector d) (hA : ContDiff ℝ (↑⊤) A) : HasVarAdjDerivAt (fun (A : SpaceTime d → Lorentz.Vector d) (x : SpaceTime d) => SpaceTime.deriv μ A x ν) (fun (ψ : SpaceTime d → ℝ) (x : SpaceTime d) => -(fderiv ℝ ψ x) (Lorentz.Vector.basis μ) • Lorentz.Vector.basis ν) A

B. The derivative tensor of the electromagnetic potential

We define the derivative as a tensor in Lorentz.CoVector ⊗[ℝ] Lorentz.Vector for the electromagnetic potential A^μ. We then prove that this tensor transforms correctly under Lorentz transformations.

noncomputable def Electromagnetism.ElectromagneticPotential.deriv {d : ℕ} (A : ElectromagneticPotential d) : SpaceTime d → TensorProduct ℝ (Lorentz.CoVector d) (Lorentz.Vector d)

The derivative of the electric potential, ∂_μ A^ν.

Equations

• A.deriv x = ∑ μ : Fin 1 ⊕ Fin d, ∑ ν : Fin 1 ⊕ Fin d, SpaceTime.deriv μ A x ν • Lorentz.CoVector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν

B.1. Equivariance of the derivative tensor

We show that the derivative tensor is equivariant under the action of the Lorentz group. That is, ∂_μ (fun x => Λ • A (Λ⁻¹ • x)) = Λ • (∂_μ A (Λ⁻¹ • x)), or in words: applying the Lorentz transformation to the potential and then taking the derivative is the same as taking the derivative and then applying the Lorentz transformation to the resulting tensor.

theorem Electromagnetism.ElectromagneticPotential.deriv_equivariant {d : ℕ} {x : SpaceTime d} (A : ElectromagneticPotential d) (Λ : ↑(LorentzGroup d)) (hf : Differentiable ℝ A) : deriv (fun (x : SpaceTime d) => Λ • A (Λ⁻¹ • x)) x = Λ • A.deriv (Λ⁻¹ • x)

B.2. The elements of the derivative tensor in terms of the basis

We show that in the standard basis, the elements of the derivative tensor are just equal to ∂_ μ A x ν.

@[simp]

theorem Electromagnetism.ElectromagneticPotential.deriv_basis_repr_apply {d : ℕ} {μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)} (A : ElectromagneticPotential d) (x : SpaceTime d) : ((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.deriv x)) μν = SpaceTime.deriv μν.1 A x μν.2

theorem Electromagnetism.ElectromagneticPotential.toTensor_deriv_basis_repr_apply {d : ℕ} (A : ElectromagneticPotential d) (x : SpaceTime d) (b : TensorSpecies.Tensor.ComponentIdx (Fin.append ![realLorentzTensor.Color.down] ![realLorentzTensor.Color.up])) : ((TensorSpecies.Tensor.basis (Fin.append ![realLorentzTensor.Color.down] ![realLorentzTensor.Color.up])).repr (TensorSpecies.Tensorial.toTensor (A.deriv x))) b = SpaceTime.deriv (finSumFinEquiv.symm (b 0)) A x (finSumFinEquiv.symm (b 1))