The Magnetic Field

i. Overview

In 3-spatial dimensions from the electromagnetic potential we can define the magnetic field \vec B as (∇ × (A.vectorPotential t)) x. In this module we define this magnetic field from the electromagnetic potential.

In general dimensions we define the magnetic field matrix from the spatial components of the field strength matrix. This is an antisymmetric matrix.

ii. Key results

• ElectromagneticPotential.magneticField : The magnetic field from the electromagnetic potential in 3 spatial dimensions.
• ElectromagneticPotential.magneticFieldMatrix : The magnetic field matrix from the electromagnetic potential in general spatial dimensions.
• ElectromagneticPotential.time_deriv_magneticFieldMatrix : The time derivative of the magnetic field matrix in terms of the vector potential. (Aka Faraday's law).

iii. Table of contents

• A. The magnetic field
  • A.1. Relation between the magnetic field and the field strength matrix
  • A.2. Divergence of the magnetic field
• B. The field strength matrix in terms of the electric and magnetic fields
• C. Magnetic field matrix
  • C.1. Antisymmetry of the magnetic field matrix
  • C.2. Magnetic field in terms of the magnetic field matrix
  • C.3. Magnetic field matrix in terms of vector potentials
  • C.4. Smoothness of the magnetic field matrix
  • C.5. Differentiablity of the magnetic field matrix
  • C.6. Spatial derivative of the magnetic field matrix
  • C.7. Temporal derivative of the magnetic field matrix
  • C.8. curl of the magnetic field matrix

iv. References

A. The magnetic field

noncomputable def Electromagnetism.ElectromagneticPotential.magneticField (c : SpeedOfLight := 1) (A : ElectromagneticPotential) : MagneticField

The magnetic field from the electromagnetic potential.

Equations

• Electromagnetism.ElectromagneticPotential.magneticField c A t x = Space.curl (Electromagnetism.ElectromagneticPotential.vectorPotential c A t) x

theorem Electromagnetism.ElectromagneticPotential.magneticField_eq {c : SpeedOfLight} (A : ElectromagneticPotential) : magneticField c A = fun (t : Time) (x : Space) => Space.curl (vectorPotential c A t) x

A.1. Relation between the magnetic field and the field strength matrix

theorem Electromagnetism.ElectromagneticPotential.magneticField_fst_eq_fieldStrengthMatrix {c : SpeedOfLight} (A : ElectromagneticPotential) (t : Time) (x : Space) (hA : Differentiable ℝ A) : magneticField c A t x 0 = -(A.fieldStrengthMatrix ((SpaceTime.toTimeAndSpace c).symm (t, x))) (Sum.inr 1, Sum.inr 2)

theorem Electromagnetism.ElectromagneticPotential.magneticField_snd_eq_fieldStrengthMatrix {c : SpeedOfLight} (A : ElectromagneticPotential) (t : Time) (x : Space) (hA : Differentiable ℝ A) : magneticField c A t x 1 = (A.fieldStrengthMatrix ((SpaceTime.toTimeAndSpace c).symm (t, x))) (Sum.inr 0, Sum.inr 2)

theorem Electromagnetism.ElectromagneticPotential.magneticField_thd_eq_fieldStrengthMatrix {c : SpeedOfLight} (A : ElectromagneticPotential) (t : Time) (x : Space) (hA : Differentiable ℝ A) : magneticField c A t x 2 = -(A.fieldStrengthMatrix ((SpaceTime.toTimeAndSpace c).symm (t, x))) (Sum.inr 0, Sum.inr 1)

A.2. Divergence of the magnetic field

theorem Electromagnetism.ElectromagneticPotential.magneticField_div_eq_zero {c : SpeedOfLight} (A : ElectromagneticPotential) (hA : ContDiff ℝ 2 A) (t : Time) : Space.div (magneticField c A t) = 0

B. The field strength matrix in terms of the electric and magnetic fields

theorem Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic {c : SpeedOfLight} (A : ElectromagneticPotential) (t : Time) (x : Space) (hA : Differentiable ℝ A) (μ ν : Fin 1 ⊕ Fin 3) : (A.fieldStrengthMatrix ((SpaceTime.toTimeAndSpace c).symm (t, x))) (μ, ν) = match μ, ν with | Sum.inl 0, Sum.inl 0 => 0 | Sum.inl 0, Sum.inr i => -electricField c A t x i / c.val | Sum.inr i, Sum.inl 0 => electricField c A t x i / c.val | Sum.inr i, Sum.inr j => match i, j with | 0, 0 => 0 | 0, 1 => -magneticField c A t x 2 | 0, 2 => magneticField c A t x 1 | 1, 0 => magneticField c A t x 2 | 1, 1 => 0 | 1, 2 => -magneticField c A t x 0 | 2, 0 => -magneticField c A t x 1 | 2, 1 => magneticField c A t x 0 | 2, 2 => 0

theorem Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_eq_electric_magnetic_of_spaceTime (c : SpeedOfLight) (A : ElectromagneticPotential) (x : SpaceTime) (hA : Differentiable ℝ A) (μ ν : Fin 1 ⊕ Fin 3) : have tx := (SpaceTime.toTimeAndSpace c) x; (A.fieldStrengthMatrix x) (μ, ν) = match μ, ν with | Sum.inl 0, Sum.inl 0 => 0 | Sum.inl 0, Sum.inr i => -electricField c A tx.1 tx.2 i / c.val | Sum.inr i, Sum.inl 0 => electricField c A tx.1 tx.2 i / c.val | Sum.inr i, Sum.inr j => match i, j with | 0, 0 => 0 | 0, 1 => -magneticField c A tx.1 tx.2 2 | 0, 2 => magneticField c A tx.1 tx.2 1 | 1, 0 => magneticField c A tx.1 tx.2 2 | 1, 1 => 0 | 1, 2 => -magneticField c A tx.1 tx.2 0 | 2, 0 => -magneticField c A tx.1 tx.2 1 | 2, 1 => magneticField c A tx.1 tx.2 0 | 2, 2 => 0

C. Magnetic field matrix

noncomputable def Electromagnetism.ElectromagneticPotential.magneticFieldMatrix {d : ℕ} (c : SpeedOfLight := 1) (A : ElectromagneticPotential d) : Time → Space d → Fin d × Fin d → ℝ

The matrix corresponding to the magnetic field in general dimensions. In 3 space-dimensions this reduces to a vector.

Equations

• Electromagnetism.ElectromagneticPotential.magneticFieldMatrix c A = (SpaceTime.timeSlice c) fun (x : SpaceTime d) (ij : Fin d × Fin d) => (A.fieldStrengthMatrix x) (Sum.inr ij.1, Sum.inr ij.2)

theorem Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_eq {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) : magneticFieldMatrix c A = fun (t : Time) (x : Space d) (ij : Fin d × Fin d) => (A.fieldStrengthMatrix ((SpaceTime.toTimeAndSpace c).symm (t, x))) (Sum.inr ij.1, Sum.inr ij.2)

theorem Electromagnetism.ElectromagneticPotential.fieldStrengthMatrix_inr_inr_eq_magneticFieldMatrix {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) (x : SpaceTime d) (i j : Fin d) : (A.fieldStrengthMatrix x) (Sum.inr i, Sum.inr j) = magneticFieldMatrix c A ((SpaceTime.time c) x) (SpaceTime.space x) (i, j)

C.1. Antisymmetry of the magnetic field matrix

theorem Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_antisymm {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) (t : Time) (x : Space d) (i j : Fin d) : magneticFieldMatrix c A t x (i, j) = -magneticFieldMatrix c A t x (j, i)

@[simp]

theorem Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_diag_eq_zero {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) (t : Time) (x : Space d) (i : Fin d) : magneticFieldMatrix c A t x (i, i) = 0

C.2. Magnetic field in terms of the magnetic field matrix

theorem Electromagnetism.ElectromagneticPotential.magneticField_eq_magneticFieldMatrix {c : SpeedOfLight} (A : ElectromagneticPotential) (hA : Differentiable ℝ A) : magneticField c A = fun (t : Time) (x : Space) (i : Fin 3) => match i with | 0 => -magneticFieldMatrix c A t x (1, 2) | 1 => magneticFieldMatrix c A t x (0, 2) | 2 => -magneticFieldMatrix c A t x (0, 1)

theorem Electromagnetism.ElectromagneticPotential.magneticField_curl_eq_magneticFieldMatrix {x : Space} {i : Fin 3} {c : SpeedOfLight} (A : ElectromagneticPotential) (hA : ContDiff ℝ 2 A) (t : Time) : Space.curl (magneticField c A t) x i = ∑ j : Fin 3, Space.deriv j (fun (x : Space) => magneticFieldMatrix c A t x (j, i)) x

C.3. Magnetic field matrix in terms of vector potentials

theorem Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_eq_vectorPotential {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) (hA : Differentiable ℝ A) (t : Time) (x : Space d) (i j : Fin d) : magneticFieldMatrix c A t x (i, j) = Space.deriv j (fun (x : Space d) => vectorPotential c A t x i) x - Space.deriv i (fun (x : Space d) => vectorPotential c A t x j) x

C.4. Smoothness of the magnetic field matrix

theorem Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_contDiff {d : ℕ} {n : WithTop ℕ∞} {c : SpeedOfLight} (A : ElectromagneticPotential d) (hA : ContDiff ℝ (n + 1) A) (ij : Fin d × Fin d) : ContDiff ℝ n ↿fun (t : Time) (x : Space d) => magneticFieldMatrix c A t x ij

theorem Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_space_contDiff {d : ℕ} {n : WithTop ℕ∞} {c : SpeedOfLight} (A : ElectromagneticPotential d) (hA : ContDiff ℝ (n + 1) A) (t : Time) (ij : Fin d × Fin d) : ContDiff ℝ n fun (x : Space d) => magneticFieldMatrix c A t x ij

theorem Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_time_contDiff {d : ℕ} {n : WithTop ℕ∞} {c : SpeedOfLight} (A : ElectromagneticPotential d) (hA : ContDiff ℝ (n + 1) A) (x : Space d) (ij : Fin d × Fin d) : ContDiff ℝ n fun (t : Time) => magneticFieldMatrix c A t x ij

C.5. Differentiablity of the magnetic field matrix

theorem Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) (hA : ContDiff ℝ 2 A) (ij : Fin d × Fin d) : Differentiable ℝ ↿fun (t : Time) (x : Space d) => magneticFieldMatrix c A t x ij

theorem Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable_space {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) (hA : ContDiff ℝ 2 A) (t : Time) (ij : Fin d × Fin d) : Differentiable ℝ fun (x : Space d) => magneticFieldMatrix c A t x ij

theorem Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_differentiable_time {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) (hA : ContDiff ℝ 2 A) (x : Space d) (ij : Fin d × Fin d) : Differentiable ℝ fun (t : Time) => magneticFieldMatrix c A t x ij

C.6. Spatial derivative of the magnetic field matrix

theorem Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_space_deriv_eq {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) (hA : ContDiff ℝ 2 A) (t : Time) (x : Space d) (i j k : Fin d) : Space.deriv k (fun (x : Space d) => magneticFieldMatrix c A t x (i, j)) x = Space.deriv i (fun (x : Space d) => magneticFieldMatrix c A t x (k, j)) x - Space.deriv j (fun (x : Space d) => magneticFieldMatrix c A t x (k, i)) x

C.7. Temporal derivative of the magnetic field matrix

theorem Electromagnetism.ElectromagneticPotential.time_deriv_magneticFieldMatrix {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) (hA : ContDiff ℝ 2 A) (t : Time) (x : Space d) (i j : Fin d) : Time.deriv (fun (x_1 : Time) => magneticFieldMatrix c A x_1 x (i, j)) t = Space.deriv i (fun (x : Space d) => electricField c A t x j) x - Space.deriv j (fun (x : Space d) => electricField c A t x i) x

theorem Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_magneticFieldMatrix {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) (hA : ContDiff ℝ 3 A) (t : Time) (x : Space d) (i j : Fin d) : Time.deriv (Time.deriv fun (x_1 : Time) => magneticFieldMatrix c A x_1 x (i, j)) t = Space.deriv i (fun (x : Space d) => Time.deriv (fun (t : Time) => electricField c A t x) t j) x - Space.deriv j (fun (x : Space d) => Time.deriv (fun (t : Time) => electricField c A t x) t i) x

C.8. curl of the magnetic field matrix

theorem Electromagnetism.ElectromagneticPotential.curl_magneticFieldMatrix_eq_electricField_fieldStrengthMatrix {d : ℕ} {c : SpeedOfLight} (A : ElectromagneticPotential d) (hA : ContDiff ℝ 2 A) (t : Time) (x : Space d) (i : Fin d) : ∑ j : Fin d, Space.deriv j (fun (x : Space d) => magneticFieldMatrix c A t x (j, i)) x = 1 / c.val ^ 2 * Time.deriv (fun (t : Time) => electricField c A t x) t i + ∑ μ : Fin 1 ⊕ Fin d, SpaceTime.deriv μ (fun (x : SpaceTime d) => (A.fieldStrengthMatrix x) (μ, Sum.inr i)) ((SpaceTime.toTimeAndSpace c).symm (t, x))