The Field Strength Tensor

i. Overview

In this module we define the field strength tensor in terms of the electromagnetic potential.

We define a tensor version and a matrix version and prover various properties of these.

ii. Key results

• toFieldStrength : The field strength tensor from an electromagnetic potential.
• fieldStrengthMatrix : The field strength matrix from an electromagnetic potential (matrix representation of the field strength tensor in the standard basis).

iii. Table of contents

• A. The field strength tensor
  • A.1. Basic equalities
  • A.2. Elements of the field strength tensor in terms of basis
  • A.3. The field strength matrix
    • A.3.1. Differentiability of the field strength matrix
  • A.4. The antisymmetry of the field strength tensor
  • A.5. Equivariance of the field strength tensor
  • A.6. Linearity of the field strength tensor

iv. References

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

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

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

Equations

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

A.1. Basic equalities

theorem Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add {d : ℕ} (A : ElectromagneticPotential d) (x : SpaceTime d) : A.toFieldStrength x = TensorSpecies.Tensorial.toTensor.symm ((TensorSpecies.Tensor.permT id ⋯) ((TensorSpecies.Tensor.contrT 2 1 2 ⋯) ((TensorSpecies.Tensor.prodT (TensorSpecies.Tensorial.toTensor (realLorentzTensor.contrMetric d))) (TensorSpecies.Tensorial.toTensor (A.deriv x))))) - TensorSpecies.Tensorial.toTensor.symm ((TensorSpecies.Tensor.permT ![1, 0] ⋯) ((TensorSpecies.Tensor.contrT 2 1 2 ⋯) ((TensorSpecies.Tensor.prodT (TensorSpecies.Tensorial.toTensor (realLorentzTensor.contrMetric d))) (TensorSpecies.Tensorial.toTensor (A.deriv x)))))

theorem Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength {d : ℕ} (A : ElectromagneticPotential d) (x : SpaceTime d) : TensorSpecies.Tensorial.toTensor (A.toFieldStrength x) = (TensorSpecies.Tensor.permT id ⋯) ((TensorSpecies.Tensor.contrT 2 1 2 ⋯) ((TensorSpecies.Tensor.prodT (TensorSpecies.Tensorial.toTensor (realLorentzTensor.contrMetric d))) (TensorSpecies.Tensorial.toTensor (A.deriv x)))) - (TensorSpecies.Tensor.permT ![1, 0] ⋯) ((TensorSpecies.Tensor.contrT 2 1 2 ⋯) ((TensorSpecies.Tensor.prodT (TensorSpecies.Tensorial.toTensor (realLorentzTensor.contrMetric d))) (TensorSpecies.Tensorial.toTensor (A.deriv x))))

A.2. Elements of the field strength tensor in terms of basis

theorem Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength_basis_repr {d : ℕ} (A : ElectromagneticPotential d) (x : SpaceTime d) (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 d, (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)))

theorem Electromagnetism.ElectromagneticPotential.toFieldStrength_tensor_basis_eq_basis {d : ℕ} (A : ElectromagneticPotential d) (x : SpaceTime d) (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 = ((Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr (A.toFieldStrength x)) (finSumFinEquiv.symm (b 0), finSumFinEquiv.symm (b 1))

theorem Electromagnetism.ElectromagneticPotential.toFieldStrength_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.toFieldStrength x)) μν = ∑ κ : Fin 1 ⊕ Fin d, (minkowskiMatrix μν.1 κ * SpaceTime.deriv κ A x μν.2 - minkowskiMatrix μν.2 κ * SpaceTime.deriv κ A x μν.1)

theorem Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply_eq_single {d : ℕ} {μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)} (A : ElectromagneticPotential d) (x : SpaceTime d) : ((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

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

@[reducible, inline]

noncomputable abbrev Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix {d : ℕ} (A : ElectromagneticPotential d) (x : SpaceTime d) : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d) →₀ ℝ

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)

theorem Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_tensor_basis_repr {d : ℕ} (A : ElectromagneticPotential d) (x : SpaceTime d) (μ ν : Fin 1 ⊕ Fin d) : (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 ν

A.3.1. Differentiability of the field strength matrix

theorem Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable {d : ℕ} {A : ElectromagneticPotential d} {μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)} (hA : ContDiff ℝ 2 A) : Differentiable ℝ fun (x : SpaceTime d) => (A.fieldStrengthMatrix x) μν

theorem Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_space {d : ℕ} {A : ElectromagneticPotential d} {μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)} (hA : ContDiff ℝ 2 A) (t : Time) {c : SpeedOfLight} : Differentiable ℝ fun (x : Space d) => (A.fieldStrengthMatrix ((SpaceTime.toTimeAndSpace c).symm (t, x))) μν

theorem Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_differentiable_time {d : ℕ} {A : ElectromagneticPotential d} {μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)} (hA : ContDiff ℝ 2 A) (x : Space d) {c : SpeedOfLight} : Differentiable ℝ fun (t : Time) => (A.fieldStrengthMatrix ((SpaceTime.toTimeAndSpace c).symm (t, x))) μν

theorem Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_contDiff {d : ℕ} {n : WithTop ℕ∞} {A : ElectromagneticPotential d} {μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)} (hA : ContDiff ℝ (n + 1) A) : ContDiff ℝ n fun (x : SpaceTime d) => (A.fieldStrengthMatrix x) μν

theorem Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_smooth {d : ℕ} {A : ElectromagneticPotential d} (hA : ContDiff ℝ (↑⊤) A) (μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)) : ContDiff ℝ ↑⊤ fun (x : SpaceTime d) => (A.fieldStrengthMatrix x) μν

A.4. The antisymmetry of the field strength tensor

We show that the field strength tensor is antisymmetric.

theorem Electromagnetism.ElectromagneticPotential.toFieldStrength_antisymmetric {d : ℕ} (A : ElectromagneticPotential d) (x : SpaceTime d) : TensorSpecies.Tensorial.toTensor (A.toFieldStrength x) = (TensorSpecies.Tensor.permT ![1, 0] ⋯) (-TensorSpecies.Tensorial.toTensor (A.toFieldStrength x))

theorem Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_antisymm {d : ℕ} (A : ElectromagneticPotential d) (x : SpaceTime d) (μ ν : Fin 1 ⊕ Fin d) : (A.fieldStrengthMatrix x) (μ, ν) = -(A.fieldStrengthMatrix x) (ν, μ)

@[simp]

theorem Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_diag_eq_zero {d : ℕ} (A : ElectromagneticPotential d) (x : SpaceTime d) (μ : Fin 1 ⊕ Fin d) : (A.fieldStrengthMatrix x) (μ, μ) = 0

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

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

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

A.6. Linearity of the field strength tensor

We show that the field strength tensor is linear in the potential.

theorem Electromagnetism.ElectromagneticPotential.toFieldStrength_add {d : ℕ} (A1 A2 : ElectromagneticPotential d) (x : SpaceTime d) (hA1 : Differentiable ℝ A1) (hA2 : Differentiable ℝ A2) : (A1 + A2).toFieldStrength x = A1.toFieldStrength x + A2.toFieldStrength x

theorem Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_add {d : ℕ} (A1 A2 : ElectromagneticPotential d) (x : SpaceTime d) (hA1 : Differentiable ℝ A1) (hA2 : Differentiable ℝ A2) : (A1 + A2).fieldStrengthMatrix x = A1.fieldStrengthMatrix x + A2.fieldStrengthMatrix x

theorem Electromagnetism.ElectromagneticPotential.toFieldStrength_smul {d : ℕ} (c : ℝ) (A : ElectromagneticPotential d) (x : SpaceTime d) (hA : Differentiable ℝ A) : (c • A).toFieldStrength x = c • A.toFieldStrength x

theorem Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_smul {d : ℕ} (c : ℝ) (A : ElectromagneticPotential d) (x : SpaceTime d) (hA : Differentiable ℝ A) : (c • A).fieldStrengthMatrix x = c • A.fieldStrengthMatrix x