refactor(Tensors): rename Tensor.toField to Tensor.toScalar

Physlib/Electromagnetism/Dynamics/Hamiltonian.lean

@@ -129,7 +129,7 @@ lemma canonicalMomentum_eq_gradient_kineticTerm {d}
 lemma canonicalMomentum_eq {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d)
     (hA : ContDiff ℝ 2 A) (J : LorentzCurrentDensity d) :
     A.canonicalMomentum 𝓕 J = fun x => fun μ =>
-      (1/𝓕.μ₀) * η μ μ • toField {A.toFieldStrength x | [μ] [Sum.inl 0]}ᵀ := by
+      (1/𝓕.μ₀) * η μ μ • toScalar {A.toFieldStrength x | [μ] [Sum.inl 0]}ᵀ := by
   rw [canonicalMomentum_eq_gradient_kineticTerm A hA J]
   funext x
   apply ext_inner_right (𝕜 := ℝ)

Physlib/Electromagnetism/Dynamics/IsExtrema.lean

@@ -90,7 +90,7 @@ lemma isExtrema_iff_toFieldStrength_eval {𝓕 : FreeSpace}
     (A : ElectromagneticPotential d)
     (hA : ContDiff ℝ ∞ A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ ∞ J) :
     IsExtrema 𝓕 A J ↔
-    ∀ x, ∀ ν, ∑ μ, ∂_ μ (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) x =
+    ∀ x, ∀ ν, ∑ μ, ∂_ μ (fun x => toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ) x =
       𝓕.μ₀ * J x ν := by
   rw [isExtrema_iff_gradLagrangian, gradLagrangian_eq_sum_toFieldStrength_eval A hA J hJ,
     funext_iff]

Physlib/Electromagnetism/Dynamics/KineticTerm.lean

@@ -87,7 +87,7 @@ Lorentz invariant.
 noncomputable def kineticTerm {d} (𝓕 : FreeSpace) (A : ElectromagneticPotential d) :
     SpaceTime d → ℝ := fun x =>
   - 1/(4 * 𝓕.μ₀) * {η' d | μ μ' ⊗ η' d | ν ν' ⊗
-    A.toFieldStrength x | μ ν ⊗ A.toFieldStrength x | μ' ν'}ᵀ.toField
+    A.toFieldStrength x | μ ν ⊗ A.toFieldStrength x | μ' ν'}ᵀ.toScalar
 
 /-!
 
@@ -105,7 +105,7 @@ lemma kineticTerm_equivariant {d} {𝓕 : FreeSpace} (A : ElectromagneticPotenti
   conv_lhs =>
     enter [2]
     rw [toFieldStrength_equivariant A Λ hf, Tensorial.toTensor_smul, ← actionT_coMetric Λ]
-    simp only [prodT_equivariant, contrT_equivariant, toField_equivariant]
+    simp only [prodT_equivariant, contrT_equivariant, toScalar_equivariant]
 
 /-!
 
@@ -116,9 +116,9 @@ lemma kineticTerm_equivariant {d} {𝓕 : FreeSpace} (A : ElectromagneticPotenti
 lemma kineticTerm_eq_sum {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (x : SpaceTime d) :
     A.kineticTerm 𝓕 x =
     - 1/(4 * 𝓕.μ₀) * ∑ μ, ∑ ν, ∑ μ', ∑ ν', η μ μ' * η ν ν' *
-      toField {A.toFieldStrength x | [μ] [ν]}ᵀ * toField {A.toFieldStrength x | [μ'] [ν']}ᵀ := by
+      toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ * toScalar {A.toFieldStrength x | [μ'] [ν']}ᵀ := by
   rw [kineticTerm]
-  rw [toField_eq_repr]
+  rw [toScalar_eq_repr]
   rw [contrT_basis_repr_apply_eq_fin]
   conv_lhs =>
     enter [2, 2, μ]
@@ -161,7 +161,7 @@ lemma kineticTerm_eq_sum {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d)
 
 lemma kineticTerm_eq_sum_sq {d} {𝓕 : FreeSpace}
     (A : ElectromagneticPotential d) (x : SpaceTime d) : A.kineticTerm 𝓕 x =
-    - 1/(4 * 𝓕.μ₀) * ∑ μ, ∑ ν, η μ μ * η ν ν * ‖toField {A.toFieldStrength x | [μ] [ν]}ᵀ‖ ^ 2 := by
+    - 1/(4 * 𝓕.μ₀) * ∑ μ, ∑ ν, η μ μ * η ν ν * ‖toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ‖ ^ 2 := by
   rw [kineticTerm_eq_sum]
   congr 1
   refine Finset.sum_congr rfl fun μ _ => Finset.sum_congr rfl fun ν _ => ?_
@@ -252,12 +252,12 @@ lemma kineticTerm_eq_electricMatrix_magneticFieldMatrix_time_space {𝓕 : FreeS
   rw [Finset.sum_add_distrib]
   simp only [Fin.isValue, Finset.sum_neg_distrib]
   have h1 : ∑ i, ∑ j, magneticFieldMatrix 𝓕.c A t x (i, j) ^ 2
-      = ∑ i, ∑ j, toField {A.toFieldStrength ((toTimeAndSpace 𝓕.c).symm (t, x)) |
+      = ∑ i, ∑ j, toScalar {A.toFieldStrength ((toTimeAndSpace 𝓕.c).symm (t, x)) |
         [Sum.inr i] [Sum.inr j]}ᵀ ^ 2 := by rfl
   rw [h1]
   ring_nf
   have h2 : ‖electricField 𝓕.c A t x‖ ^ 2 = 𝓕.c.val ^ 2 *
-      ∑ i, |toField {A.toFieldStrength ((toTimeAndSpace 𝓕.c).symm (t, x)) |
+      ∑ i, |toScalar {A.toFieldStrength ((toTimeAndSpace 𝓕.c).symm (t, x)) |
       [Sum.inl 0] [Sum.inr i]}ᵀ| ^ 2 := by
     rw [EuclideanSpace.norm_sq_eq]
     conv_lhs =>
@@ -311,7 +311,7 @@ lemma kineticTerm_contDiff {d} {n : WithTop ℕ∞} {𝓕 : FreeSpace} (A : Elec
     (hA : ContDiff ℝ (n + 1) A) :
     ContDiff ℝ n (A.kineticTerm 𝓕) := by
   rw [funext fun x => kineticTerm_eq_sum (𝓕 := 𝓕) A x]
-  have h (μ ν) : ContDiff ℝ n (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) :=
+  have h (μ ν) : ContDiff ℝ n (fun x => toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ) :=
     toFieldStrength_eval_contDiff hA
   fun_prop
 
@@ -502,7 +502,7 @@ components of the field strength tensor.
 lemma gradKineticTerm_eq_fieldStrength {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential d)
     (x : SpaceTime d) (ha : ContDiff ℝ ∞ A) :
     A.gradKineticTerm 𝓕 x = ∑ (ν : (Fin 1 ⊕ Fin d)), (1/𝓕.μ₀ * η ν ν) •
-    (∑ (μ : (Fin 1 ⊕ Fin d)), (∂_ μ (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) x))
+    (∑ (μ : (Fin 1 ⊕ Fin d)), (∂_ μ (fun x => toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ) x))
     • Lorentz.Vector.basis ν := by
   calc _
     _ = ∑ (ν : (Fin 1 ⊕ Fin d)), ∑ (μ : (Fin 1 ⊕ Fin d)),
@@ -518,7 +518,7 @@ lemma gradKineticTerm_eq_fieldStrength {d} {𝓕 : FreeSpace} (A : Electromagnet
         ring_nf
         simp
     _ = ∑ (ν : (Fin 1 ⊕ Fin d)), ∑ (μ : (Fin 1 ⊕ Fin d)),
-      ((1/𝓕.μ₀ * η ν ν) * (∂_ μ (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) x)) •
+      ((1/𝓕.μ₀ * η ν ν) * (∂_ μ (fun x => toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ) x)) •
           Lorentz.Vector.basis ν := by
         refine Finset.sum_congr rfl fun ν _ => Finset.sum_congr rfl fun μ _ => ?_
         congr 2
@@ -528,7 +528,7 @@ lemma gradKineticTerm_eq_fieldStrength {d} {𝓕 : FreeSpace} (A : Electromagnet
             fderiv_const_mul (by fun_prop), fderiv_const_mul (by fun_prop)]
         simp [SpaceTime.deriv_eq]
     _ = ∑ (ν : (Fin 1 ⊕ Fin d)), (1/𝓕.μ₀ * η ν ν) •
-        (∑ (μ : (Fin 1 ⊕ Fin d)), (∂_ μ (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) x))
+        (∑ (μ : (Fin 1 ⊕ Fin d)), (∂_ μ (fun x => toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ) x))
         • Lorentz.Vector.basis ν := by
         apply Finset.sum_congr rfl (fun ν _ => ?_)
         rw [← Finset.sum_smul, ← Finset.mul_sum, ← smul_smul]
@@ -622,7 +622,7 @@ lemma gradKineticTerm_smul {d} {𝓕 : FreeSpace} (A : ElectromagneticPotential
   apply Finset.sum_congr rfl (fun μ _ => ?_)
   conv_rhs =>
     rw [SpaceTime.deriv_eq]
-    change (c • fderiv ℝ (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) x)
+    change (c • fderiv ℝ (fun x => toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ) x)
       (Lorentz.Vector.basis μ)
     rw [← fderiv_const_smul
       (toFieldStrength_eval_differentiable <| hA.of_le (ENat.LEInfty.out)).differentiableAt,

Physlib/Electromagnetism/Dynamics/Lagrangian.lean

@@ -308,7 +308,7 @@ lemma lagrangian_hasVarGradientAt_gradLagrangian {𝓕 : FreeSpace}
 lemma gradLagrangian_eq_sum_toFieldStrength_eval {𝓕 : FreeSpace} (A : ElectromagneticPotential d)
     (hA : ContDiff ℝ ∞ A) (J : LorentzCurrentDensity d) (hJ : ContDiff ℝ ∞ J) :
     A.gradLagrangian 𝓕 J = fun x => ∑ ν,
-      (η ν ν • (1 / 𝓕.μ₀ * ∑ μ, ∂_ μ (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) x
+      (η ν ν • (1 / 𝓕.μ₀ * ∑ μ, ∂_ μ (fun x => toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ) x
       - J x ν) • Lorentz.Vector.basis ν) := by
   rw [gradLagrangian_eq_kineticTerm_sub A hA J hJ]
   funext x

Physlib/Electromagnetism/Kinematics/Boosts.lean

@@ -81,7 +81,7 @@ lemma electricField_apply_x_boost_zero {d : ℕ} {c : SpeedOfLight} (β : ℝ) (
     enter [2]
     rw [toFieldStrength_eval_antisymm]
   trans γ β ^ 2 * (1 - β ^ 2) *
-      toField {A.toFieldStrength
+      toScalar {A.toFieldStrength
       ((boost (d := d.succ) 0 β hβ)⁻¹ • (SpaceTime.toTimeAndSpace c).symm (t, x)) |
       [Sum.inl 0] [Sum.inr 0]}ᵀ
   · ring

Physlib/Electromagnetism/Kinematics/EMPotential.lean

@@ -601,15 +601,15 @@ open Tensorial
 /-- Evaluation of the tensor components of `∂_ μ A x ν`. -/
 lemma tensorDeriv_eval_eq {d} {A : ElectromagneticPotential d} (hA : Differentiable ℝ A)
     (x : SpaceTime d) (μ ν : Fin 1 ⊕ Fin d) :
-    toField {tensorDeriv A.val x | [μ] [ν]}ᵀ = ∂_ μ A x ν := by
+    toScalar {tensorDeriv A.val x | [μ] [ν]}ᵀ = ∂_ μ A x ν := by
   trans (Lorentz.CoVector.basis.tensorProduct Lorentz.Vector.basis).repr (deriv A x) (μ, ν); swap
   · simp [deriv, Basis.tensorProduct_repr_tmul_apply, Finsupp.single_apply]
   rw [deriv_eq_tensorDeriv _ hA]
   generalize (tensorDeriv A.val x) = t
   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]
+      toScalar_pure, smul_eq_mul, mul_one, Pure.evalPCoeff]
     change _ * (Lorentz.contrBasis d).repr (Lorentz.contrBasis d (b 1)) ν = _
     /- Transforming the basis -/
     let e : ComponentIdx (Fin.append ![Color.down] ![Color.up])

Physlib/Electromagnetism/Kinematics/ElectricField.lean

@@ -150,7 +150,7 @@ lemma electricField_eq_toFieldStrength_eval {c : SpeedOfLight}
     (A : ElectromagneticPotential d) (t : Time)
     (x : Space d) (i : Fin d) (hA : Differentiable ℝ A) :
     A.electricField c t x i = - c *
-    toField {A.toFieldStrength ((toTimeAndSpace c).symm (t, x)) | [Sum.inl 0] [Sum.inr i]}ᵀ := by
+    toScalar {A.toFieldStrength ((toTimeAndSpace c).symm (t, x)) | [Sum.inl 0] [Sum.inr i]}ᵀ := by
   rw [toFieldStrength_eval_apply_eq_single]
   simp only [Fin.isValue, inl_0_inl_0, one_mul, inr_i_inr_i, neg_mul, sub_neg_eq_add]
   rw [electricField]
@@ -189,15 +189,15 @@ lemma electricField_eq_toFieldStrength_eval {c : SpeedOfLight}
 lemma toFieldStrength_eval_inl_inr_eq_electricField {c : SpeedOfLight}
     (A : ElectromagneticPotential d)
     (x : SpaceTime d) (i : Fin d) (hA : Differentiable ℝ A) :
-    toField {A.toFieldStrength x | [Sum.inl 0] [Sum.inr i]}ᵀ =
+    toScalar {A.toFieldStrength x | [Sum.inl 0] [Sum.inr i]}ᵀ =
     - (1 /c) * A.electricField c (x.time c) x.space i := by
   rw [electricField_eq_toFieldStrength_eval A (x.time c) x.space i hA]
   simp
 
 lemma toFieldStrength_eval_inr_inl_eq_electricField {c : SpeedOfLight}
     (A : ElectromagneticPotential d)
     (x : SpaceTime d) (i : Fin d) (hA : Differentiable ℝ A) :
-    toField {A.toFieldStrength x | [Sum.inr i] [Sum.inl 0]}ᵀ =
+    toScalar {A.toFieldStrength x | [Sum.inr i] [Sum.inl 0]}ᵀ =
     (1 /c) * A.electricField c (x.time c) x.space i := by
   rw [toFieldStrength_eval_antisymm A x (Sum.inr i) (Sum.inl 0),
     toFieldStrength_eval_inl_inr_eq_electricField A x i hA]
@@ -308,7 +308,7 @@ open Space
 lemma time_deriv_electricField_eq_toFieldStrength_eval {d} {A : ElectromagneticPotential d}
     {c : SpeedOfLight} (hA : ContDiff ℝ 2 A) (t : Time) (x : Space d) (i : Fin d) :
     ∂ₜ (fun t => A.electricField c t x) t i =
-    - c ^ 2 * ∂_ (Sum.inl 0) (fun x => toField {A.toFieldStrength x | [Sum.inl 0] [Sum.inr i]}ᵀ)
+    - c ^ 2 * ∂_ (Sum.inl 0) (fun x => toScalar {A.toFieldStrength x | [Sum.inl 0] [Sum.inr i]}ᵀ)
     ((toTimeAndSpace c).symm (t, x)) := by
   rw [SpaceTime.deriv_sum_inl c]
   simp only [one_div, ContinuousLinearEquiv.apply_symm_apply, Fin.isValue, smul_eq_mul, neg_mul]
@@ -326,7 +326,7 @@ lemma time_deriv_electricField_eq_toFieldStrength_eval {d} {A : ElectromagneticP
 lemma div_electricField_eq_toFieldStrength_eval {d} {A : ElectromagneticPotential d}
     {c : SpeedOfLight} (hA : ContDiff ℝ 2 A) (t : Time) (x : Space d) :
     (∇ ⬝ A.electricField c t) x = c * ∑ (μ : (Fin 1 ⊕ Fin d)),
-      (∂_ μ (fun x => toField {A.toFieldStrength x | [μ] [Sum.inl 0]}ᵀ)
+      (∂_ μ (fun x => toScalar {A.toFieldStrength x | [μ] [Sum.inl 0]}ᵀ)
         ((toTimeAndSpace c).symm (t, x))) := by
   rw [Finset.mul_sum]
   simp only [Fin.isValue, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero,