feat: Basic field strength equalities

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

Physlib/Electromagnetism/Kinematics/FieldStrength.lean

@@ -29,13 +29,15 @@ 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. 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
@@ -59,28 +61,42 @@ 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
 
+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
 
-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
   (permT id (PermCond.auto) {(η d | μ μ' ⊗ A.deriv x | μ' ν) + - (η d | ν ν' ⊗ A.deriv x | ν' μ)}ᵀ)
 
 /-!
 
-### 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 practice,
+we don't expect them to be used explicitly. They are useful for proving some
+of the API within this module.
 
 -/
 
@@ -111,6 +127,15 @@ 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 toTensor_toFieldStrength {d} (A : ElectromagneticPotential d) (x : SpaceTime d) :
     Tensorial.toTensor (toFieldStrength A x) =
     (permT id (PermCond.auto) {(η d | μ μ' ⊗ A.deriv x | μ' ν)}ᵀ)
@@ -120,10 +145,155 @@ lemma toTensor_toFieldStrength {d} (A : ElectromagneticPotential d) (x : SpaceTi
 
 /-!
 
-### A.2. Elements of the field strength tensor in terms of basis
+### 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.
+
+-/
+
+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} :
+    A.toFieldStrength = fun x => ∑ μ, ∑ ν, toField {A.toFieldStrength x| [μ] [ν]}ᵀ •
+      Vector.basis μ ⊗ₜ[ℝ] 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]
+
+/-- 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 μ)) •
+      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
+
+/-- 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 μ) •
+      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
+
+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. 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]
+
+/-- 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 = ∑ μ, ∑ ν,
+      (∑ κ, ∑ ρ, Λ.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
+
+-/
+
+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 =
@@ -207,7 +377,7 @@ lemma toFieldStrength_basis_repr_apply_eq_single {d} {μν : (Fin 1 ⊕ Fin d) 
 
 /-!
 
-### A.3. 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.
@@ -246,7 +416,7 @@ lemma toFieldStrength_eq_fieldStrengthMatrix {d} (A : ElectromagneticPotential d
 
 /-!
 
-#### A.3.1. Differentiability of the field strength matrix
+#### A.5.1. Differentiability of the field strength matrix
 
 -/
 
@@ -333,7 +503,7 @@ lemma fieldStrengthMatrix_smooth {d} {A : ElectromagneticPotential d}
 
 /-!
 
-### A.4. 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.
 
@@ -369,22 +539,10 @@ lemma fieldStrengthMatrix_diag_eq_zero {d} (A : ElectromagneticPotential d) (x :
 
 /-!
 
-### 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.
+### 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)
@@ -424,7 +582,7 @@ lemma fieldStrengthMatrix_equivariant {d} (A : ElectromagneticPotential d)
 
 /-!
 
-### A.6. 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.
 

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

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

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