From e6180584e2655d186036a9b52dd06dcf39a88e22 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 1 May 2026 07:51:37 +0100
Subject: [PATCH 1/9] feat: Basic field strength equalities

---
 .../Kinematics/FieldStrength.lean             | 65 ++++++++++++++++++-
 .../Relativity/Tensors/RealTensor/Basic.lean  |  9 ++-
 Physlib/Relativity/Tensors/Tensorial.lean     | 31 +++++++++
 3 files changed, 103 insertions(+), 2 deletions(-)

diff --git a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
index 6de8c6624..56b3b9b52 100644
--- a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
+++ b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
@@ -59,7 +59,9 @@ open TensorSpecies
 open Tensor
 open SpaceTime
 open TensorProduct
-open minkowskiMatrix
+open minkowskiMatrix Tensorial
+open Lorentz
+
 attribute [-simp] Fintype.sum_sum_type
 attribute [-simp] Nat.succ_eq_add_one
 
@@ -111,6 +113,67 @@ lemma toFieldStrength_eq_add {d} (A : ElectromagneticPotential d) (x : SpaceTime
   · rw [permT_permT]
     rfl
 
+lemma toFieldStrength_eq_sub_tensorDeriv {d} {A : ElectromagneticPotential d}
+    (hA : Differentiable ℝ A) (x : SpaceTime d) :
+    toFieldStrength A x =
+    Tensorial.toTensor.symm (permT id PermCond.auto {η d | μ μ' ⊗ tensorDeriv A x | μ' ν}ᵀ)
+    - Tensorial.toTensor.symm (permT ![1, 0] PermCond.auto
+    {η d | μ μ' ⊗ tensorDeriv A x | μ' ν}ᵀ) := by
+  simp only [toFieldStrength_eq_tensorDeriv hA, map_add, map_neg, sub_eq_add_neg, permT_permT]
+  rfl
+
+lemma toFieldStrength_eq_sum_basis_eval {d} {A : ElectromagneticPotential d} :
+    A.toFieldStrength = fun x => ∑ μ, ∑ ν, toField {A.toFieldStrength x| [μ] [ν]}ᵀ •
+      Lorentz.Vector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν := by
+  ext x
+  /- This is a fairly general proof, so we can generalize our tensor. -/
+  generalize (A.toFieldStrength x) = t
+  apply (Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr.injective
+  ext ⟨μ, ν⟩
+  simp only [map_sum, map_smul, Finsupp.coe_finset_sum, Finsupp.coe_smul, Finset.sum_apply,
+    Pi.smul_apply, Basis.tensorProduct_repr_tmul_apply, Basis.repr_self, Finsupp.single_apply,
+    smul_eq_mul, mul_ite, mul_one, mul_zero, Finset.sum_ite_irrel, Finset.sum_ite_eq',
+    Finset.mem_univ, ↓reduceIte, Finset.sum_const_zero]
+  obtain ⟨t, rfl⟩ := toTensor.symm.surjective t
+  induction' t using Tensor.induction_on_basis with b a t h t1 t2 h1 h2
+  · simp only [LinearEquiv.apply_symm_apply, basis_apply, evalT_pure, Pure.evalP, map_smul,
+      toField_pure, smul_eq_mul, mul_one, Pure.evalPCoeff]
+    change _ = _ * ((realLorentzTensor d).basis (Color.up)).repr
+      ((realLorentzTensor d).basis (Color.up) (b 1)) ν
+    /- Transforming the basis -/
+    let e := ComponentIdx.prod.trans ((Vector.indexEquiv (d := d)).prodCongr Vector.indexEquiv)
+    simp only [prod_basis_of_map_reindex Vector.basis_eq_map_tensor_basis
+        Vector.basis_eq_map_tensor_basis, Basis.repr_reindex, Basis.map_repr,
+      LinearEquiv.symm_symm, LinearEquiv.trans_apply, LinearEquiv.apply_symm_apply,
+      Finsupp.mapDomain_equiv_apply, basis_repr_pure, Pure.component_basisVector, Fin.isValue,
+      Pure.basisVector, Basis.repr_self, Finsupp.single_apply, mul_ite, mul_one, mul_zero]
+    grind [show e b = (b 0,  b 1) from rfl]
+  · simp only [map_zero, Finsupp.coe_zero, Pi.zero_apply]
+  · simp only [map_smul, h, smul_eq_mul, Finsupp.coe_smul, Pi.smul_apply]
+  · simp only [map_add, h1, h2, Finsupp.coe_add, Pi.add_apply]
+
+lemma toFieldStrength_eq_sum_basis {d} {A : ElectromagneticPotential d}
+    (hA : Differentiable ℝ A) (x : SpaceTime d) :
+    A.toFieldStrength x =  ∑ μ, ∑ ν, (∑ κ, (η μ κ *  ∂_ κ A x ν - η ν κ * ∂_ κ A x μ)) •
+      Lorentz.Vector.basis μ ⊗ₜ Lorentz.Vector.basis ν := by
+  apply (Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr.injective
+  ext ⟨μ, ν⟩
+  simp only [map_sum, map_smul, Finsupp.coe_finset_sum, Finsupp.coe_smul,
+    Finset.sum_apply, Pi.smul_apply, Basis.tensorProduct_repr_tmul_apply, Basis.repr_self,
+    Finsupp.single_apply, smul_eq_mul, mul_ite, mul_one, mul_zero, Finset.sum_ite_irrel,
+    Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte, Finset.sum_const_zero]
+  simp only [prod_basis_of_map_reindex Vector.basis_eq_map_tensor_basis
+        Vector.basis_eq_map_tensor_basis,
+    toFieldStrength_eq_sub_tensorDeriv hA, self_toTensor_apply, ← deriv_eq_tensorDeriv _ hA,
+    map_sub, Basis.repr_reindex, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
+    LinearEquiv.apply_symm_apply, Finsupp.coe_sub, Pi.sub_apply, Finsupp.mapDomain_equiv_apply,
+    permT_basis_repr_symm_apply, Function.comp_apply, contrT_basis_repr_apply_eq_fin,
+    prodT_basis_repr_apply, contrMetric_repr_apply_eq_minkowskiMatrix,
+    prod_tensor_basis_eq_map_reindex CoVector.basis_eq_map_tensor_basis
+        Vector.basis_eq_map_tensor_basis,
+    LinearEquiv.symm_apply_apply, Equiv.symm_symm, deriv_basis_repr_apply, Finset.sum_sub_distrib]
+  rfl
+
 lemma toTensor_toFieldStrength {d} (A : ElectromagneticPotential d) (x : SpaceTime d) :
     Tensorial.toTensor (toFieldStrength A x) =
     (permT id (PermCond.auto) {(η d | μ μ' ⊗ A.deriv x | μ' ν)}ᵀ)
diff --git a/Physlib/Relativity/Tensors/RealTensor/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Basic.lean
index a800d12c2..24ad73aad 100644
--- a/Physlib/Relativity/Tensors/RealTensor/Basic.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/Basic.lean
@@ -122,11 +122,18 @@ These re-express fields of `realLorentzTensor d` in terms of `Lorentz` data.
 
 -/
 
+
+
 @[simp]
+lemma basisIdxCongr_eq_refl {d : ℕ} {c1 c2 : realLorentzTensor.Color} (h : c1 = c2) :
+    TensorSpecies.basisIdxCongr (basisIdx := fun _ => Fin 1 ⊕ Fin d) h = Equiv.refl _ := by
+  rfl
+
+
 lemma basisIdxCongr_apply {d : ℕ} {c1 c2 : realLorentzTensor.Color} (h : c1 = c2)
     (i : Fin 1 ⊕ Fin d) :
     TensorSpecies.basisIdxCongr (basisIdx := fun _ => Fin 1 ⊕ Fin d) h i = i := by
-  rfl
+  simp
 
 lemma basis_eq_contrBasis {d : ℕ} :
     (realLorentzTensor d).basis Color.up = Lorentz.contrBasis (d := d) := rfl
diff --git a/Physlib/Relativity/Tensors/Tensorial.lean b/Physlib/Relativity/Tensors/Tensorial.lean
index e643ef0a3..14b517cbd 100644
--- a/Physlib/Relativity/Tensors/Tensorial.lean
+++ b/Physlib/Relativity/Tensors/Tensorial.lean
@@ -287,6 +287,37 @@ lemma basis_map_prod {n2 : ℕ} {c2 : Fin n2 → C} {M₂ : Type}
   simp only [LinearEquiv.apply_symm_apply]
   rfl
 
+open Tensor in
+lemma prod_basis_of_map_reindex {n2 : ℕ} {c2 : Fin n2 → C} {M₂ : Type}
+    [Tensorial S c M] [AddCommMonoid M₂] [Module k M₂]
+    [Tensorial S c2 M₂] {ι ι2 : Type}  {b : Module.Basis ι k M} {b2 : Module.Basis ι2 k M₂}
+    {e : Tensor.ComponentIdx c ≃ ι} {e2 : Tensor.ComponentIdx c2 ≃ ι2}
+    (h : b = ((Tensor.basis (S := S) c).map toTensor.symm).reindex e)
+    (h2 : b2 = ((Tensor.basis (S := S) c2).map  toTensor.symm).reindex e2) :
+    b.tensorProduct b2 = ((Tensor.basis (S := S) (Fin.append c c2)).map
+    (toTensor (S := S) (M := M ⊗[k] M₂)).symm).reindex
+    (ComponentIdx.prod.trans (e.prodCongr e2)) := by
+  ext ⟨i, j⟩
+  simp_rw [Tensorial.basis_map_prod, Module.Basis.tensorProduct_apply]
+  simp [h, h2]
+
+open Tensor in
+lemma prod_tensor_basis_eq_map_reindex {n2 : ℕ} {c2 : Fin n2 → C} {M₂ : Type}
+    [Tensorial S c M] [AddCommMonoid M₂] [Module k M₂]
+    [Tensorial S c2 M₂] {ι ι2 : Type}  {b : Module.Basis ι k M} {b2 : Module.Basis ι2 k M₂}
+    {e : Tensor.ComponentIdx c ≃ ι} {e2 : Tensor.ComponentIdx c2 ≃ ι2}
+    (h : b = ((Tensor.basis (S := S) c).map toTensor.symm).reindex e)
+    (h2 : b2 = ((Tensor.basis (S := S) c2).map  toTensor.symm).reindex e2) :
+    Tensor.basis (S := S) (Fin.append c c2) =
+    ((b.tensorProduct b2).map (toTensor (S := S) (M := M ⊗[k] M₂))).reindex
+    (ComponentIdx.prod.trans (e.prodCongr e2)).symm := by
+  rw [Tensor.basis_prod_eq]
+  ext r
+  simp
+  obtain ⟨⟨i, j⟩, rfl⟩ := ComponentIdx.prod.symm.surjective r
+  simp [h, h2, tensorEquivProd, toTensor_tprod]
+
+
 /-!
 
 ## E. Continuous properties

From 1e5dd5fa37b4da4cb82d7727f8eb61f79880f8db Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 1 May 2026 08:57:58 +0100
Subject: [PATCH 2/9] feat: toFieldStrength_eq_sum_basis_single

---
 .../Kinematics/FieldStrength.lean             | 85 ++++++++++++++-----
 1 file changed, 65 insertions(+), 20 deletions(-)

diff --git a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
index 56b3b9b52..41f5f45f5 100644
--- a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
+++ b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
@@ -29,13 +29,14 @@ We define a tensor version and a matrix version and prover various properties of
 ## 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
+  - A.1. Tensor equalities
+  - A.2. Vector equalities
+  - A.3. Elements of the field strength tensor in terms of basis
+  - A.4. The field strength matrix
+    - A.4.1. Differentiability of the field strength matrix
+  - A.5. The antisymmetry of the field strength tensor
+  - A.6. Equivariance of the field strength tensor
+  - A.7. 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
@@ -65,6 +66,13 @@ open Lorentz
 attribute [-simp] Fintype.sum_sum_type
 attribute [-simp] Nat.succ_eq_add_one
 
+TODO "Currently the API for the field strength tensor has the definition
+  of `fieldStrengthMatrix`. This is now unneeded, and should be replaced with
+  `toField {A.toFieldStrength x| [μ] [ν]}ᵀ` and suitble API around that.
+  To undertake this TODO, it is likely easier to start building the API
+  around `toField {A.toFieldStrength x| [μ] [ν]}ᵀ` and then remove `fieldStrengthMatrix`
+  once the API is in place."
+
 /-!
 
 ## A. The field strength tensor
@@ -82,7 +90,12 @@ noncomputable def toFieldStrength {d} (A : ElectromagneticPotential d) :
 
 /-!
 
-### A.1. Basic equalities
+### A.1. Tensor equalities
+
+These equalities for the field strength tensor are in
+terms of tensor expressions and index notation. In pratice,
+we don't expect them to be used explicitly. They are useful for proving some
+of the API within this module.
 
 -/
 
@@ -122,6 +135,25 @@ lemma toFieldStrength_eq_sub_tensorDeriv {d} {A : ElectromagneticPotential d}
   simp only [toFieldStrength_eq_tensorDeriv hA, map_add, map_neg, sub_eq_add_neg, permT_permT]
   rfl
 
+lemma toTensor_toFieldStrength {d} (A : ElectromagneticPotential d) (x : SpaceTime d) :
+    Tensorial.toTensor (toFieldStrength A x) =
+    (permT id (PermCond.auto) {(η d | μ μ' ⊗ A.deriv x | μ' ν)}ᵀ)
+    - (permT ![1, 0] (PermCond.auto) {(η d | μ μ' ⊗ A.deriv x | μ' ν)}ᵀ) := by
+  rw [toFieldStrength_eq_add]
+  simp
+
+/-!
+
+### A.2. Vector equalities
+
+These equalities for the field strength tensor are in terms of vector basis.
+They match some of the familiar forms one might expect to see the field strength
+tensor in.
+
+-/
+
+/-- The statement that `F = F^{μν} eᵤ ⊗ eᵥ` written explicitly, with
+  the components extracted via `toField`. -/
 lemma toFieldStrength_eq_sum_basis_eval {d} {A : ElectromagneticPotential d} :
     A.toFieldStrength = fun x => ∑ μ, ∑ ν, toField {A.toFieldStrength x| [μ] [ν]}ᵀ •
       Lorentz.Vector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν := by
@@ -174,16 +206,29 @@ lemma toFieldStrength_eq_sum_basis {d} {A : ElectromagneticPotential d}
     LinearEquiv.symm_apply_apply, Equiv.symm_symm, deriv_basis_repr_apply, Finset.sum_sub_distrib]
   rfl
 
-lemma toTensor_toFieldStrength {d} (A : ElectromagneticPotential d) (x : SpaceTime d) :
-    Tensorial.toTensor (toFieldStrength A x) =
-    (permT id (PermCond.auto) {(η d | μ μ' ⊗ A.deriv x | μ' ν)}ᵀ)
-    - (permT ![1, 0] (PermCond.auto) {(η d | μ μ' ⊗ A.deriv x | μ' ν)}ᵀ) := by
-  rw [toFieldStrength_eq_add]
-  simp
+lemma toFieldStrength_eq_sum_basis_single {d} {A : ElectromagneticPotential d}
+    (hA : Differentiable ℝ A) (x : SpaceTime d) :
+    A.toFieldStrength x = ∑ μ, ∑ ν, (η μ μ * ∂_ μ A x ν - η ν ν * ∂_ ν A x μ) •
+      Lorentz.Vector.basis μ ⊗ₜ Lorentz.Vector.basis ν := by
+  rw [toFieldStrength_eq_sum_basis hA x]
+  apply (Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr.injective
+  ext ⟨μ, ν⟩
+  simp [Basis.tensorProduct_repr_tmul_apply, Finsupp.single_apply]
+  rw [Finset.sum_eq_single μ, Finset.sum_eq_single ν]
+  · intro b _ hb
+    rw [minkowskiMatrix.off_diag_zero]
+    simp only [zero_mul]
+    exact id (Ne.symm hb)
+  · simp
+  · intro b _ hb
+    rw [minkowskiMatrix.off_diag_zero]
+    simp only [zero_mul]
+    exact id (Ne.symm hb)
+  · simp
 
 /-!
 
-### A.2. Elements of the field strength tensor in terms of basis
+### A.3. Elements of the field strength tensor in terms of basis
 
 -/
 
@@ -270,7 +315,7 @@ lemma toFieldStrength_basis_repr_apply_eq_single {d} {μν : (Fin 1 ⊕ Fin d) 
 
 /-!
 
-### A.3. The field strength matrix
+### A.4. The field strength matrix
 
 We define the field strength matrix to be the matrix representation of the field strength tensor
 in the standard basis.
@@ -309,7 +354,7 @@ lemma toFieldStrength_eq_fieldStrengthMatrix {d} (A : ElectromagneticPotential d
 
 /-!
 
-#### A.3.1. Differentiability of the field strength matrix
+#### A.4.1. Differentiability of the field strength matrix
 
 -/
 
@@ -396,7 +441,7 @@ lemma fieldStrengthMatrix_smooth {d} {A : ElectromagneticPotential d}
 
 /-!
 
-### A.4. The antisymmetry of the field strength tensor
+### A.5. The antisymmetry of the field strength tensor
 
 We show that the field strength tensor is antisymmetric.
 
@@ -432,7 +477,7 @@ lemma fieldStrengthMatrix_diag_eq_zero {d} (A : ElectromagneticPotential d) (x :
 
 /-!
 
-### A.5. Equivariance of the field strength tensor
+### A.6. 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
@@ -487,7 +532,7 @@ lemma fieldStrengthMatrix_equivariant {d} (A : ElectromagneticPotential d)
 
 /-!
 
-### A.6. Linearity of the field strength tensor
+### A.7. Linearity of the field strength tensor
 
 We show that the field strength tensor is linear in the potential.
 

From 6772286df99e3f195e851628d5fffe7dbdff64d7 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 1 May 2026 09:07:01 +0100
Subject: [PATCH 3/9] docs: Add documentation

---
 Physlib/Electromagnetism/Kinematics/EMPotential.lean   |  5 +++++
 Physlib/Electromagnetism/Kinematics/FieldStrength.lean | 10 +++++++++-
 2 files changed, 14 insertions(+), 1 deletion(-)

diff --git a/Physlib/Electromagnetism/Kinematics/EMPotential.lean b/Physlib/Electromagnetism/Kinematics/EMPotential.lean
index d4712a648..00be80a7d 100644
--- a/Physlib/Electromagnetism/Kinematics/EMPotential.lean
+++ b/Physlib/Electromagnetism/Kinematics/EMPotential.lean
@@ -139,6 +139,8 @@ noncomputable instance {d} : MulAction (LorentzGroup d) (ElectromagneticPotentia
     ext i
     simp [action_val, one_smul]
 
+TODO "Lift the action on `ElectromagneticPotential d` to a `DistribMulAction`."
+
 /-!
 
 ### A.3. Differentiability
@@ -163,6 +165,9 @@ lemma differentiable_action {d} (Λ : LorentzGroup d) (A : ElectromagneticPotent
     · exact hA
     · exact ContinuousLinearMap.differentiable (Lorentz.Vector.actionCLM Λ⁻¹)
 
+TODO "Add results related to the differentiability of the
+  derivative of the Electromagnetic potential."
+
 /-!
 
 ### A.4. The action on the space-time derivatives
diff --git a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
index 41f5f45f5..95ea9b08e 100644
--- a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
+++ b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
@@ -184,9 +184,12 @@ lemma toFieldStrength_eq_sum_basis_eval {d} {A : ElectromagneticPotential d} :
   · simp only [map_smul, h, smul_eq_mul, Finsupp.coe_smul, Pi.smul_apply]
   · simp only [map_add, h1, h2, Finsupp.coe_add, Pi.add_apply]
 
+
+/-- The statement that `F = F^{μν} eᵤ ⊗ eᵥ` written explicitly, with
+  the components given by `∑ κ, (η μ κ * ∂_ κ A x ν - η ν κ * ∂_ κ A x μ)`. -/
 lemma toFieldStrength_eq_sum_basis {d} {A : ElectromagneticPotential d}
     (hA : Differentiable ℝ A) (x : SpaceTime d) :
-    A.toFieldStrength x =  ∑ μ, ∑ ν, (∑ κ, (η μ κ *  ∂_ κ A x ν - η ν κ * ∂_ κ A x μ)) •
+    A.toFieldStrength x = ∑ μ, ∑ ν, (∑ κ, (η μ κ *  ∂_ κ A x ν - η ν κ * ∂_ κ A x μ)) •
       Lorentz.Vector.basis μ ⊗ₜ Lorentz.Vector.basis ν := by
   apply (Lorentz.Vector.basis.tensorProduct Lorentz.Vector.basis).repr.injective
   ext ⟨μ, ν⟩
@@ -206,6 +209,8 @@ lemma toFieldStrength_eq_sum_basis {d} {A : ElectromagneticPotential d}
     LinearEquiv.symm_apply_apply, Equiv.symm_symm, deriv_basis_repr_apply, Finset.sum_sub_distrib]
   rfl
 
+/-- The statement that `F = F^{μν} eᵤ ⊗ eᵥ` written explicitly, with
+  with the components given by `(η μ μ * ∂_ μ A x ν - η ν ν * ∂_ ν A x μ)`. -/
 lemma toFieldStrength_eq_sum_basis_single {d} {A : ElectromagneticPotential d}
     (hA : Differentiable ℝ A) (x : SpaceTime d) :
     A.toFieldStrength x = ∑ μ, ∑ ν, (η μ μ * ∂_ μ A x ν - η ν ν * ∂_ ν A x μ) •
@@ -226,6 +231,9 @@ lemma toFieldStrength_eq_sum_basis_single {d} {A : ElectromagneticPotential d}
     exact id (Ne.symm hb)
   · simp
 
+TODO "Add a section in this file on the evaluation of the field strength tensor's indices.
+  I.e. equalitites related to `toField {A.toFieldStrength x| [μ] [ν]}ᵀ`."
+
 /-!
 
 ### A.3. Elements of the field strength tensor in terms of basis

From 2b953567215f6d977bc19bca4747c9834c2d647f Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 1 May 2026 09:07:33 +0100
Subject: [PATCH 4/9] lint: spelling

---
 Physlib/Electromagnetism/Kinematics/FieldStrength.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
index 95ea9b08e..40a6b77ee 100644
--- a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
+++ b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
@@ -93,7 +93,7 @@ noncomputable def toFieldStrength {d} (A : ElectromagneticPotential d) :
 ### A.1. Tensor equalities
 
 These equalities for the field strength tensor are in
-terms of tensor expressions and index notation. In pratice,
+terms of tensor expressions and index notation. In practice,
 we don't expect them to be used explicitly. They are useful for proving some
 of the API within this module.
 

From 4c1268b4ec4ecd1d055deb5ccd5d0b31df0eb324 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 1 May 2026 09:09:17 +0100
Subject: [PATCH 5/9] refactor: Add TODO item.

---
 Physlib/Electromagnetism/Kinematics/FieldStrength.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
index 40a6b77ee..5f2e86cc5 100644
--- a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
+++ b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
@@ -240,6 +240,11 @@ TODO "Add a section in this file on the evaluation of the field strength tensor'
 
 -/
 
+TODO "For the electromagnetic field strength, we have lots of lemmas related
+  to the components of the field strength tensor in terms of the basis. For example,
+  `toTensor_toFieldStrength_basis_repr`, these should be removed. They are used
+  downstream, so there use there should be refactored."
+
 lemma toTensor_toFieldStrength_basis_repr {d} (A : ElectromagneticPotential d) (x : SpaceTime d)
     (b : ComponentIdx (S := realLorentzTensor d) (Fin.append ![Color.up] ![Color.up])) :
     (Tensor.basis _).repr (Tensorial.toTensor (toFieldStrength A x)) b =

From d26f0b8c4cf063a753625734d24acdf96a842be9 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 1 May 2026 15:57:29 +0100
Subject: [PATCH 6/9] feat: Group actions on the Field strength.

---
 .../Kinematics/FieldStrength.lean             | 79 +++++++++++++------
 1 file changed, 53 insertions(+), 26 deletions(-)

diff --git a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
index 5f2e86cc5..5b13710e2 100644
--- a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
+++ b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
@@ -31,12 +31,13 @@ We define a tensor version and a matrix version and prover various properties of
 - A. The field strength tensor
   - A.1. Tensor equalities
   - A.2. Vector equalities
-  - A.3. Elements of the field strength tensor in terms of basis
-  - A.4. The field strength matrix
-    - A.4.1. Differentiability of the field strength matrix
-  - A.5. The antisymmetry of the field strength tensor
-  - A.6. Equivariance of the field strength tensor
-  - A.7. Linearity of the field strength tensor
+  - A.3. The group action acting on the field strength tensor
+  - A.4. Elements of the field strength tensor in terms of basis
+  - A.5. The field strength matrix
+    - A.5.1. Differentiability of the field strength matrix
+  - A.6. The antisymmetry of the field strength tensor
+  - A.7. Equivariance of the field strength matrix
+  - A.8. 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
@@ -156,7 +157,7 @@ tensor in.
   the components extracted via `toField`. -/
 lemma toFieldStrength_eq_sum_basis_eval {d} {A : ElectromagneticPotential d} :
     A.toFieldStrength = fun x => ∑ μ, ∑ ν, toField {A.toFieldStrength x| [μ] [ν]}ᵀ •
-      Lorentz.Vector.basis μ ⊗ₜ[ℝ] Lorentz.Vector.basis ν := by
+      Vector.basis μ ⊗ₜ[ℝ] Vector.basis ν := by
   ext x
   /- This is a fairly general proof, so we can generalize our tensor. -/
   generalize (A.toFieldStrength x) = t
@@ -184,7 +185,6 @@ lemma toFieldStrength_eq_sum_basis_eval {d} {A : ElectromagneticPotential d} :
   · simp only [map_smul, h, smul_eq_mul, Finsupp.coe_smul, Pi.smul_apply]
   · simp only [map_add, h1, h2, Finsupp.coe_add, Pi.add_apply]
 
-
 /-- The statement that `F = F^{μν} eᵤ ⊗ eᵥ` written explicitly, with
   the components given by `∑ κ, (η μ κ * ∂_ κ A x ν - η ν κ * ∂_ κ A x μ)`. -/
 lemma toFieldStrength_eq_sum_basis {d} {A : ElectromagneticPotential d}
@@ -236,7 +236,46 @@ TODO "Add a section in this file on the evaluation of the field strength tensor'
 
 /-!
 
-### A.3. Elements of the field strength tensor in terms of basis
+## A.3. The group action acting on 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.
+
+-/
+
+set_option backward.isDefEq.respectTransparency false in
+lemma toFieldStrength_equivariant {d} (A : ElectromagneticPotential d) (Λ : LorentzGroup d)
+    (hf : Differentiable ℝ A) (x : SpaceTime d) :
+    (Λ • A).toFieldStrength x = Λ • A.toFieldStrength (Λ⁻¹ • x) := by
+  rw [toFieldStrength, deriv_equivariant A Λ hf, ← actionT_contrMetric Λ, toFieldStrength]
+  simp only [Tensorial.toTensor_smul, prodT_equivariant, contrT_equivariant, map_neg,
+    permT_equivariant, map_add, ← Tensorial.smul_toTensor_symm, smul_add, smul_neg]
+
+lemma toFieldStrength_action_eq_sum {d} (A : ElectromagneticPotential d) (Λ : LorentzGroup d)
+    (hf : Differentiable ℝ A) (x : SpaceTime d) :
+    (Λ • A).toFieldStrength x = ∑ μ, ∑ ν,
+      (∑ κ, ∑ ρ, Λ.1 μ κ * Λ.1 ν ρ * toField {A.toFieldStrength (Λ⁻¹ • x) | [κ] [ρ]}ᵀ) •
+      Vector.basis μ ⊗ₜ[ℝ] Vector.basis ν := by
+  conv_lhs => rw [toFieldStrength_equivariant A Λ hf x, toFieldStrength_eq_sum_basis_eval]
+  change Tensorial.smulLinearMap _ _ = _
+  simp only [Nat.reduceSucc, Nat.reduceAdd, Fin.isValue, Fin.succAbove_zero, map_sum, map_smul]
+  simp [smulLinearMap, smul_prod, Vector.smul_basis, tmul_sum, sum_tmul,
+    Finset.smul_sum, tmul_smul, smul_tmul, smul_smul]
+  conv_lhs => enter [2, μ, 2, ν]; rw [Finset.sum_comm]
+  conv_lhs => enter [2, μ]; rw [Finset.sum_comm]
+  rw [Finset.sum_comm]
+  refine Finset.sum_congr rfl (fun ν _ => ?_)
+  conv_lhs => enter [2, μ]; rw [Finset.sum_comm]
+  rw [Finset.sum_comm]
+  refine Finset.sum_congr rfl (fun μ _ => ?_)
+  simp [← Finset.sum_smul]
+  congr 1
+  exact Finset.sum_congr rfl (fun κ _ => Finset.sum_congr rfl (fun κ _ => by ring))
+
+/-!
+
+### A.4. Elements of the field strength tensor in terms of basis
 
 -/
 
@@ -328,7 +367,7 @@ lemma toFieldStrength_basis_repr_apply_eq_single {d} {μν : (Fin 1 ⊕ Fin d) 
 
 /-!
 
-### A.4. The field strength matrix
+### A.5. The field strength matrix
 
 We define the field strength matrix to be the matrix representation of the field strength tensor
 in the standard basis.
@@ -367,7 +406,7 @@ lemma toFieldStrength_eq_fieldStrengthMatrix {d} (A : ElectromagneticPotential d
 
 /-!
 
-#### A.4.1. Differentiability of the field strength matrix
+#### A.5.1. Differentiability of the field strength matrix
 
 -/
 
@@ -454,7 +493,7 @@ lemma fieldStrengthMatrix_smooth {d} {A : ElectromagneticPotential d}
 
 /-!
 
-### A.5. The antisymmetry of the field strength tensor
+### A.6. The antisymmetry of the field strength tensor
 
 We show that the field strength tensor is antisymmetric.
 
@@ -490,22 +529,10 @@ lemma fieldStrengthMatrix_diag_eq_zero {d} (A : ElectromagneticPotential d) (x :
 
 /-!
 
-### A.6. 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.
+### A.7. Equivariance of the field strength matrix
 
 -/
 
-set_option backward.isDefEq.respectTransparency false in
-lemma toFieldStrength_equivariant {d} (A : ElectromagneticPotential d) (Λ : LorentzGroup d)
-    (hf : Differentiable ℝ A) (x : SpaceTime d) :
-    toFieldStrength (Λ • A) x = Λ • toFieldStrength A (Λ⁻¹ • x) := by
-  rw [toFieldStrength, deriv_equivariant A Λ hf, ← actionT_contrMetric Λ, toFieldStrength]
-  simp only [Tensorial.toTensor_smul, prodT_equivariant, contrT_equivariant, map_neg,
-    permT_equivariant, map_add, ← Tensorial.smul_toTensor_symm, smul_add, smul_neg]
-
 set_option backward.isDefEq.respectTransparency false in
 lemma fieldStrengthMatrix_equivariant {d} (A : ElectromagneticPotential d)
     (Λ : LorentzGroup d) (hf : Differentiable ℝ A) (x : SpaceTime d)
@@ -545,7 +572,7 @@ lemma fieldStrengthMatrix_equivariant {d} (A : ElectromagneticPotential d)
 
 /-!
 
-### A.7. Linearity of the field strength tensor
+### A.8. Linearity of the field strength tensor
 
 We show that the field strength tensor is linear in the potential.
 

From ccddb735a5c5dd5431522ee2efc804ac86d51768 Mon Sep 17 00:00:00 2001
From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 1 May 2026 15:59:11 +0100
Subject: [PATCH 7/9] docs: Add lemma documentation

---
 Physlib/Electromagnetism/Kinematics/FieldStrength.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
index 5b13710e2..a1f2b299d 100644
--- a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
+++ b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
@@ -252,6 +252,10 @@ lemma toFieldStrength_equivariant {d} (A : ElectromagneticPotential d) (Λ : Lor
   simp only [Tensorial.toTensor_smul, prodT_equivariant, contrT_equivariant, map_neg,
     permT_equivariant, map_add, ← Tensorial.smul_toTensor_symm, smul_add, smul_neg]
 
+/-- This lemma expresses the component form of the transformed field strength
+tensor: when a Lorentz transformation Λ acts on the potential A, the resulting field strength
+tensor's components are given by the standard tensor transformation rule involving the Lorentz
+matrix elements Λ^μ_κ and Λ^ν_ρ applied to the original field components. -/
 lemma toFieldStrength_action_eq_sum {d} (A : ElectromagneticPotential d) (Λ : LorentzGroup d)
     (hf : Differentiable ℝ A) (x : SpaceTime d) :
     (Λ • A).toFieldStrength x = ∑ μ, ∑ ν,

From 605fa4f4fecc7904bc1522bde6457ed63fd0c811 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 4 May 2026 15:19:06 +0100
Subject: [PATCH 8/9] refactor: Fix notation

---
 Physlib/Electromagnetism/Kinematics/FieldStrength.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
index a1f2b299d..115a5c35e 100644
--- a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
+++ b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
@@ -78,12 +78,12 @@ TODO "Currently the API for the field strength tensor has the definition
 
 ## A. The field strength tensor
 
-We define the field strength tensor `F_μ^ν` in terms of the derivative of the
+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.
 
 -/
-/-- The field strength from an electromagnetic potential, as a tensor `F_μ^ν`. -/
+/-- The field strength from an electromagnetic potential, as a tensor `F^{μν}`. -/
 noncomputable def toFieldStrength {d} (A : ElectromagneticPotential d) :
     SpaceTime d → Lorentz.Vector d ⊗[ℝ] Lorentz.Vector d := fun x =>
   Tensorial.toTensor.symm

From adae0e01783efa111b7496e6ec51387d9aacd824 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 4 May 2026 15:23:44 +0100
Subject: [PATCH 9/9] refactor: TODO items

---
 Physlib/Electromagnetism/Kinematics/FieldStrength.lean | 6 ++++++
 Physlib/Relativity/Tensors/Basic.lean                  | 4 ++++
 2 files changed, 10 insertions(+)

diff --git a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
index 115a5c35e..c552cf4f9 100644
--- a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
+++ b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean
@@ -153,6 +153,12 @@ tensor in.
 
 -/
 
+TODO "Generalize the proof of `toFieldStrength_eq_sum_basis_eval` so that any tensor
+  can easily be written as the sum of its components times the basis.
+  The likely location for this is in the `Tensorial` module.
+  The TODO item with tag: 8285454220008908699 is likely a prerequisite to this."
+
+
 /-- The statement that `F = F^{μν} eᵤ ⊗ eᵥ` written explicitly, with
   the components extracted via `toField`. -/
 lemma toFieldStrength_eq_sum_basis_eval {d} {A : ElectromagneticPotential d} :
diff --git a/Physlib/Relativity/Tensors/Basic.lean b/Physlib/Relativity/Tensors/Basic.lean
index 19b26c738..904132717 100644
--- a/Physlib/Relativity/Tensors/Basic.lean
+++ b/Physlib/Relativity/Tensors/Basic.lean
@@ -54,6 +54,10 @@ def ComponentIdx.cast {n m : ℕ} {c : Fin n → C} {cm : Fin m → C}
     ComponentIdx (S := S) cm := fun j =>
       basisIdxCongr (by simp [hc]) (b (Fin.cast h.symm j))
 
+TODO "Define the equivalence between `ComponentIdx ![c]` and `basisIdx c`.
+  Replace Lorentz.Vector.indexEquiv and Lorentz.CoVector.indexEquiv with this more
+  general definition."
+
 /-!
 
 ## Pure tensors