Research proof index

Index evaluation of the field strength tensor agrees with the corresponding component of the field strength matrix. -/ lemma toFieldStrength_eval_eq_fieldStrengthMatrix {d} (A : ElectromagneticPotential d) (x : SpaceTime d) (μ ν : Fin 1 ⊕ Fin d) : toField {A.toFieldStrength x | [μ] [ν]}ᵀ = A.fieldStrengthMatrix x (μ, ν) := by rw [toFieldStrength_eval_eq_b...

The field strength of the bare-gradient potential B^μ := ∂_μ χ for χ(x) = x⁰·xⁱ is nonzero (follows from fieldStrengthMatrix_bareGradient_inl_inr).

The statement that F = F^{μν} eᵤ ⊗ eᵥ written explicitly, with the components given by ∑ κ, (η μ κ * ∂_ κ A x ν - η ν κ * ∂_ κ A x μ).

The statement that F = F^{μν} eᵤ ⊗ eᵥ written explicitly, with with the components given by (η μ μ * ∂_ μ A x ν - η ν ν * ∂_ ν A x μ).

Evaluating both tensor indices of the field strength gives the coefficient in the standard tensor-product basis.

A pure-gauge potential has vanishing field strength.