Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Physlib.Electromagnetism.Distributional.Basic
public import Physlib.Relativity.Tensors.RealTensor.Metrics.Basic
public import Mathlib.Algebra.Order.Archimedean.Real.HomThe Field Strength Tensor
i. Overview
In this module we define the field strength tensor in terms of the electromagnetic potential.
ii. Key results
DistElectromagneticPotential.fieldStrength : The field strength for
electromagnetic potentials which are distributions.
iii. Table of contents
A. Field strength for distributions
A.1. Auxiliary definition of field strength for distributions, with no linearity
A.2. The definition of the field strength
A.3. Field strength written in terms of a basis
A.4. Equivariance of the field strength for distributions
iv. References
@[expose] public sectionA. Field strength for distributions
attribute [-simp] Fintype.sum_sum_typeattribute [-simp] Nat.succ_eq_add_oneA.1. Auxiliary definition of field strength for distributions, with no linearity
d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ -Tensorial.toTensor.symm
((permT (![1, 0] ∘ id) ⋯)
((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (Tensorial.toTensor ((distTensorDeriv A) ε))))) =
-Tensorial.toTensor.symm
((permT ![1, 0] ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (Tensorial.toTensor ((distTensorDeriv A) ε)))))
All goals completed! 🐙d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ Tensorial.toTensor
(Tensorial.toTensor.symm
((permT id ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (Tensorial.toTensor ((distTensorDeriv A) ε))))) -
Tensorial.toTensor.symm
((permT ![1, 0] ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (Tensorial.toTensor ((distTensorDeriv A) ε)))))) =
(permT id ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (Tensorial.toTensor ((distTensorDeriv A) ε)))) -
(permT ![1, 0] ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (Tensorial.toTensor ((distTensorDeriv A) ε))))
All goals completed! 🐙All goals completed! 🐙d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b:ComponentIdx (Fin.append ![Color.up] ![Color.up])hb:(Vector.basis.reindex Vector.indexEquiv.symm).tensorProduct (Vector.basis.reindex Vector.indexEquiv.symm) =
(Vector.basis.tensorProduct Vector.basis).reindex (Vector.indexEquiv.symm.prodCongr Vector.indexEquiv.symm)⊢ ((Vector.basis.tensorProduct Vector.basis).repr (A.fieldStrengthAux ε))
((Vector.indexEquiv.symm.prodCongr Vector.indexEquiv.symm).symm (ComponentIdx.prod b)) =
((Vector.basis.tensorProduct Vector.basis).repr (A.fieldStrengthAux ε)) (b 0, b 1)
All goals completed! 🐙All goals completed! 🐙d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b:Fin 1 ⊕ Fin da✝:b ∈ Finset.univhb:b ≠ μν.1⊢ 0 * ((distDeriv b) A) ε μν.2 = 0d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b:Fin 1 ⊕ Fin da✝:b ∈ Finset.univhb:b ≠ μν.1⊢ μν.1 ≠ b
d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)b:Fin 1 ⊕ Fin da✝:b ∈ Finset.univhb:b ≠ μν.1⊢ μν.1 ≠ b
All goals completed! 🐙
d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ μν.1 ∉ Finset.univ → η μν.1 μν.1 * ((distDeriv μν.1) A) ε μν.2 = 0 All goals completed! 🐙All goals completed! 🐙A.2. The definition of the field strength
lemma fieldStrength_eq_fieldStrengthAux {d} (A : DistElectromagneticPotential d)
(ε : 𝓢(SpaceTime d, ℝ)) :
A.fieldStrength ε = A.fieldStrengthAux ε := d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ (fieldStrength A) ε = A.fieldStrengthAux ε All goals completed! 🐙A.3. Field strength written in terms of a basis
d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ({ toFun := fun A => { toFun := fun ε => A.fieldStrengthAux ε, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ },
map_add' := ⋯, map_smul' := ⋯ }
A)
ε =
∑ μ, ∑ ν, (η μ μ * ((distDeriv μ) A) ε ν - η ν ν * ((distDeriv ν) A) ε μ) • Vector.basis μ ⊗ₜ[ℝ] Vector.basis ν
All goals completed! 🐙d:ℕμν:(Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)A:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)⊢ ((Vector.basis.tensorProduct Vector.basis).repr
(({ toFun := fun A => { toFun := fun ε => A.fieldStrengthAux ε, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ },
map_add' := ⋯, map_smul' := ⋯ }
A)
ε))
μν =
η μν.1 μν.1 * ((distDeriv μν.1) A) ε μν.2 - η μν.2 μν.2 * ((distDeriv μν.2) A) ε μν.1
All goals completed! 🐙d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin d⊢ η (μ, μ).1 (μ, μ).1 * ((distDeriv (μ, μ).1) A) ε (μ, μ).2 - η (μ, μ).2 (μ, μ).2 * ((distDeriv (μ, μ).2) A) ε (μ, μ).1 =
0
All goals completed! 🐙d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ ((Vector.basis.tensorProduct Vector.basis).repr
(-(fieldStrength A) ((SchwartzMap.evalCLM ℝ (SpaceTime d) ℝ (Vector.basis ν)) ((fderivCLM ℝ (SpaceTime d) ℝ) ε))))
(μ, μ) =
0
All goals completed! 🐙d:ℕA:DistElectromagneticPotential dε:𝓢(SpaceTime d, ℝ)μ:Fin 1 ⊕ Fin dν:Fin 1 ⊕ Fin d⊢ η (μ, ν).1 (μ, ν).1 * ((distDeriv (μ, ν).1) A) ε (μ, ν).2 - η (μ, ν).2 (μ, ν).2 * ((distDeriv (μ, ν).2) A) ε (μ, ν).1 =
-(η (ν, μ).1 (ν, μ).1 * ((distDeriv (ν, μ).1) A) ε (ν, μ).2 -
η (ν, μ).2 (ν, μ).2 * ((distDeriv (ν, μ).2) A) ε (ν, μ).1)
All goals completed! 🐙A.4. Equivariance of the field strength for distributions
d:ℕA:DistElectromagneticPotential dΛ:↑(LorentzGroup d)ε:𝓢(SpaceTime d, ℝ)ε':𝓢(SpaceTime d, ℝ)⊢ Tensorial.toTensor.symm
((permT id ⋯)
((contrT 2 1 2 ⋯) ((prodT (Λ • contrMetric d)) (Tensorial.toTensor (Λ • (distTensorDeriv A) ε'))))) -
Tensorial.toTensor.symm
((permT ![1, 0] ⋯)
((contrT 2 1 2 ⋯) ((prodT (Λ • contrMetric d)) (Tensorial.toTensor (Λ • (distTensorDeriv A) ε'))))) =
Λ •
(Tensorial.toTensor.symm
((permT id ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (Tensorial.toTensor ((distTensorDeriv A) ε'))))) -
Tensorial.toTensor.symm
((permT ![1, 0] ⋯) ((contrT 2 1 2 ⋯) ((prodT (contrMetric d)) (Tensorial.toTensor ((distTensorDeriv A) ε'))))))
All goals completed! 🐙