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. from this we can define the field strength tensor, the kinetic energy, and the electric and magnetic fields.

ii. Key results #

ElectromagneticPotential: is the type of electromagnetic potentials.
ElectromagneticPotential.deriv: the derivative tensor ∂_μ A^ν.
ElectromagneticPotential.toFieldStrength: the field strength tensor F_μ^ν.
ElectromagneticPotential.scalarPotential: the scalar potential φ.
ElectromagneticPotential.vectorPotential: the vector potential A_i.
ElectromagneticPotential.electricField: the electric field E.
ElectromagneticPotential.magneticField: the magnetic field B.

iii. Table of contents #

A. The electromagnetic potential
- A.1. The action on the space-time derivatives
- A.2. Differentiability
- A.3. Varitational adjoint derivative of component
- A.4. Variational adjoint derivative of derivatives of the potential
B. The derivative tensor of the electricomagnetic potential
- B.1. Equivariance of the derivative tensor
- B.2. The elements of the derivative tensor in terms of the basis
C. The field strength tensor
- C.1. Basic equalitites
- C.2. Elements of the field strength tensor in terms of basis
- C.3. The field strength matrix
  - C.3.1. Differentiability of the field strength matrix
- C.4. The antisymmetry of the field strength tensor
- C.5. Equivariance of the field strength tensor
E. The electric and magnetic fields
- E.1. The scalar potential
- E.2. The vector potential
- E.3. The electric field
  - E.3.1. Relation between the electric field and the field strength matrix
  - E.3.2. Differentiability of the electric field
- E.4. The magnetic field
  - E.4.1. Relation between the magnetic field and the field strength matrix
- E.5. Field strength matrix in terms of the electric and magnetic fields

iv. References #

https://quantummechanics.ucsd.edu/ph130a/130_notes/node452.html

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.

source

@[reducible, inline]

noncomputable abbrev Electromagnetism.ElectromagneticPotential :

Type

The electricomagnetic potential is a tensor A^μ.

Equations

Electromagnetism.ElectromagneticPotential = (SpaceTime → Lorentz.Vector)

Instances For

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 tenosr. ∂_ ρ A (Λ⁻¹ • x) κ.

source

theorem Electromagnetism.ElectromagneticPotential.spaceTime_deriv_action_eq_sum {x : SpaceTime} {μ ν : Fin 1 ⊕ Fin 3} (Λ : ↑(LorentzGroup 3)) (A : ElectromagneticPotential) (hA : Differentiable ℝ A) :

SpaceTime.deriv μ (fun (x : SpaceTime) => Λ • A (Λ⁻¹ • x)) x ν = ∑ κ : Fin 1 ⊕ Fin 3, ∑ ρ : Fin 1 ⊕ Fin 3, ↑Λ ν κ * ↑Λ⁻¹ ρ μ * SpaceTime.deriv ρ A (Λ⁻¹ • x) κ

A.2. Differentiability #

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

source

theorem Electromagnetism.ElectromagneticPotential.differentiable_component (A : ElectromagneticPotential) (hA : Differentiable ℝ A) (μ : Fin 1 ⊕ Fin 3) :

Differentiable ℝ fun (x : SpaceTime) => A x μ

A.3. Varitational 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.

source

noncomputable def Electromagnetism.ElectromagneticPotential.instInnerProductSpaceRealSpaceTimeOfNatNat :

InnerProductSpace ℝ SpaceTime

A local instance of the inner product structure on SpaceTime.

Equations

Electromagnetism.ElectromagneticPotential.instInnerProductSpaceRealSpaceTimeOfNatNat = SpaceTime.innerProductSpace 3

Instances For

source

theorem Electromagnetism.ElectromagneticPotential.hasVarAdjDerivAt_component (μ : Fin 1 ⊕ Fin 3) (A : SpaceTime → Lorentz.Vector) (hA : ContDiff ℝ (↑⊤) A) :

HasVarAdjDerivAt (fun (A' : SpaceTime → Lorentz.Vector) (x : SpaceTime) => A' x μ) (fun (A' : SpaceTime → ℝ) (x : SpaceTime) => 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).

source

theorem Electromagnetism.ElectromagneticPotential.deriv_hasVarAdjDerivAt (μ ν : Fin 1 ⊕ Fin 3) (A : SpaceTime → Lorentz.Vector) (hA : ContDiff ℝ (↑⊤) A) :

HasVarAdjDerivAt (fun (A : SpaceTime → Lorentz.Vector) (x : SpaceTime) => SpaceTime.deriv μ A x ν) (fun (ψ : SpaceTime → ℝ) (x : SpaceTime) => -(fderiv ℝ ψ x) (Lorentz.Vector.basis μ) • Lorentz.Vector.basis ν) A

B. The derivative tensor of the electricomagnetic 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.

source

noncomputable def Electromagnetism.ElectromagneticPotential.deriv (A : ElectromagneticPotential) :

SpaceTime → TensorProduct ℝ Lorentz.CoVector Lorentz.Vector

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

Equations

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

Instances For

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.

source

theorem Electromagnetism.ElectromagneticPotential.deriv_equivariant {x : SpaceTime} (A : ElectromagneticPotential) (Λ : ↑(LorentzGroup 3)) (hf : Differentiable ℝ A) :

deriv (fun (x : SpaceTime) => Λ • 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 ν.

source

@[simp]

theorem Electromagnetism.ElectromagneticPotential.deriv_basis_repr_apply {μν : (Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)} (A : ElectromagneticPotential) (x : SpaceTime) :

((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.deriv x)) μν = SpaceTime.deriv μν.1 A x μν.2

C. The field strength tensor #

We define the field strength tensor F_μ^ν in terms of the derivative of the electromagnetic potential A^μ. We then prove that this tensor transforms correctly under Lorentz transformations.

source

noncomputable def Electromagnetism.ElectromagneticPotential.toFieldStrength (A : ElectromagneticPotential) :

SpaceTime → TensorProduct ℝ Lorentz.Vector Lorentz.Vector

The field strength from an electromagnetic potential, as a tensor F_μ^ν.

Equations

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

Instances For

C.1. Basic equalitites #

C.2. Elements of the field strength tensor in terms of basis #

source

theorem Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength_basis_repr (A : ElectromagneticPotential) (x : SpaceTime) (b : TensorSpecies.Tensor.ComponentIdx (Fin.append ![realLorentzTensor.Color.up ] ![realLorentzTensor.Color.up ])) :

((TensorSpecies.Tensor.basis (Fin.append ![realLorentzTensor.Color.up ] ![realLorentzTensor.Color.up ])).repr (TensorSpecies.Tensorial.toTensor (A.toFieldStrength x))) b = ∑ κ : Fin 1 ⊕ Fin 3, (minkowskiMatrix (finSumFinEquiv.symm (b 0)) κ * SpaceTime.deriv κ A x (finSumFinEquiv.symm (b 1)) - minkowskiMatrix (finSumFinEquiv.symm (b 1)) κ * SpaceTime.deriv κ A x (finSumFinEquiv.symm (b 0)))

source

theorem Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply {μν : (Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)} (A : ElectromagneticPotential) (x : SpaceTime) :

((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) μν = ∑ κ : Fin 1 ⊕ Fin 3, (minkowskiMatrix μν.1 κ * SpaceTime.deriv κ A x μν.2 - minkowskiMatrix μν.2 κ * SpaceTime.deriv κ A x μν.1)

source

theorem Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply_eq_single {μν : (Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)} (A : ElectromagneticPotential) (x : SpaceTime) :

((Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) μν = minkowskiMatrix μν.1 μν.1 * SpaceTime.deriv μν.1 A x μν.2 - minkowskiMatrix μν.2 μν.2 * SpaceTime.deriv μν.2 A x μν.1

C.3. The field strength matrix #

We define the field strength matrix to be the matrix representation of the field strength tensor in the standard basis.

This is currently not used as much as it could be.

source

@[reducible, inline]

noncomputable abbrev Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix (A : ElectromagneticPotential) (x : SpaceTime) :

(Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3) →₀ ℝ

The matrix corresponding to the field strength in the standard basis.

Equations

A.fieldStrengthMatrix x = (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)

Instances For

source

theorem Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_tensor_basis_repr (A : ElectromagneticPotential) (x : SpaceTime) (μ ν : Fin 1 ⊕ Fin 3) :

(A.fieldStrengthMatrix x) (μ, ν) = ((TensorSpecies.Tensor.basis (Fin.append ![realLorentzTensor.Color.up ] ![realLorentzTensor.Color.up ])).repr (TensorSpecies.Tensorial.toTensor (A.toFieldStrength x))) fun (x : Fin (Nat.succ 0 + Nat.succ 0)) => match x with | 0 => finSumFinEquiv μ | 1 => finSumFinEquiv ν

C.3.1. Differentiability of the field strength matrix #

source

theorem Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable {A : ElectromagneticPotential} {μν : (Fin 1 ⊕ Fin 3) × (Fin 1 ⊕ Fin 3)} (hA : ContDiff ℝ 2 A) :

Differentiable ℝ fun (x : SpaceTime) => (A.fieldStrengthMatrix x) μν

C.4. The antisymmetry of the field strength tensor #

We show that the field strength tensor is antisymmetric.

source

theorem Electromagnetism.ElectromagneticPotential.toFieldStrength_antisymmetric (A : ElectromagneticPotential) (x : SpaceTime) :

TensorSpecies.Tensorial.toTensor (A.toFieldStrength x) = (TensorSpecies.Tensor.permT ![1, 0] ⋯) (-TensorSpecies.Tensorial.toTensor (A.toFieldStrength x))

source

theorem Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_antisymm (A : ElectromagneticPotential) (x : SpaceTime) (μ ν : Fin 1 ⊕ Fin 3) :

(A.fieldStrengthMatrix x) (μ, ν) = -(A.fieldStrengthMatrix x) (ν, μ)

source

@[simp]

theorem Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_diag_eq_zero (A : ElectromagneticPotential) (x : SpaceTime) (μ : Fin 1 ⊕ Fin 3) :

(A.fieldStrengthMatrix x) (μ, μ) = 0

C.5. Equivariance of the field strength tensor #

We show that the field strength tensor is equivariant under the action of the Lorentz group. That is transforming the potential and then taking the field strength is the same as taking the field strength and then transforming the resulting tensor.

source

theorem Electromagnetism.ElectromagneticPotential.toFieldStrength_equivariant (A : ElectromagneticPotential) (Λ : ↑(LorentzGroup 3)) (hf : Differentiable ℝ A) (x : SpaceTime) :

toFieldStrength (fun (x : SpaceTime) => Λ • A (Λ⁻¹ • x)) x = Λ • A.toFieldStrength (Λ⁻¹ • x)

source

theorem Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_equivariant (A : ElectromagneticPotential) (Λ : ↑(LorentzGroup 3)) (hf : Differentiable ℝ A) (x : SpaceTime) (μ ν : Fin 1 ⊕ Fin 3) :

(fieldStrengthMatrix (fun (x : SpaceTime) => Λ • A (Λ⁻¹ • x)) x) (μ, ν) = ∑ κ : Fin 1 ⊕ Fin 3, ∑ ρ : Fin 1 ⊕ Fin 3, ↑Λ μ κ * ↑Λ ν ρ * (A.fieldStrengthMatrix (Λ⁻¹ • x)) (κ, ρ)

E. The electric and magnetic fields #

We now define the scalar and vector potentials, and the electric and magnetic fields in terms of the electromagnetic potential. This breaks the manifest Lorentz covariance.

source

noncomputable def Electromagnetism.ElectromagneticPotential.scalarPotential (A : ElectromagneticPotential) :

Time → Space → ℝ

The scalar potential from the electromagnetic potential.

Equations