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).
DistElectromagneticPotential.fieldStrength : The field strength for electromagnetic potentials which are distributions.

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
B. Field strength for distributions
- B.1. Auxiliary definition of field strength for distributions, with no linearity
- B.2. The definition of the field strength
- B.3. Field strength written in terms of a basis
- B.4. Equivariance of the field strength for distributions

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.

source

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

Instances For

A.1. Basic equalities #

source

theorem Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_add {d : ℕ} (A : ElectromagneticPotential d) (x : SpaceTime d) :

source

theorem Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength {d : ℕ} (A : ElectromagneticPotential d) (x : SpaceTime d) :

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

source

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)))

source

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)

source

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.

source

@[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

Instances For

source

theorem Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq {d : ℕ} (A : ElectromagneticPotential d) (x : SpaceTime d) :

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

source

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 ν

source

theorem Electromagnetism.ElectromagneticPotential.toFieldStrength_eq_fieldStrengthMatrix {d : ℕ} (A : ElectromagneticPotential d) :

A.toFieldStrength = fun (x : SpaceTime d) => ∑ μ : Fin 1 ⊕ Fin d, ∑ ν : Fin 1 ⊕ Fin d, (A.fieldStrengthMatrix x) (μ, ν) • Lorentz.Vector.basis μ ⊗ₜ[ℝ ] Lorentz.Vector.basis ν

A.3.1. Differentiability of the field strength matrix #

source

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) μν

source

theorem Electromagnetism.ElectromagneticPotential.toFieldStrength_differentiable {d : ℕ} {A : ElectromagneticPotential d} (hA : ContDiff ℝ 2 A) :

Differentiable ℝ A.toFieldStrength

source

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))) μν

source

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))) μν

source

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) μν

source

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.

source

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))

source

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

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

source

@[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.

source

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)

source

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.

source

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

source

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

source

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

(c • A).toFieldStrength x = c • A.toFieldStrength x

source

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

(c • A).fieldStrengthMatrix x = c • A.fieldStrengthMatrix x

B. Field strength for distributions #

B.1. Auxiliary definition of field strength for distributions, with no linearity #

source

noncomputable def Electromagnetism.DistElectromagneticPotential.fieldStrengthAux {d : ℕ} (A : DistElectromagneticPotential d) (ε : SchwartzMap (SpaceTime d) ℝ) :

TensorProduct ℝ (Lorentz.Vector d) (Lorentz.Vector d)

An auxiliary definition for the field strength of an electromagnetic potential based on a distribution. On Schwartz maps this has the same value as the field strength tensor, but no linearity or continuous properties built in.

Equations

Instances For

source