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 6de8c6624..c552cf4f9 100644 --- a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean +++ b/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,20 +61,29 @@ 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 @@ -80,7 +91,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 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. 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 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