From b458c758bcb1b97ee6226aad71619f34880f5b54 Mon Sep 17 00:00:00 2001 From: ZhiKai Pong Date: Tue, 22 Sep 2026 21:07:48 +0100 Subject: [PATCH] refactor(Tensors): rename Tensor.toField to Tensor.toScalar MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Rename the map from rank-zero tensors to the scalars `k`, `Tensor.toField`, to `Tensor.toScalar`, together with its lemmas (`toScalar_default`, `toScalar_injective`, `toScalar_pure`, `toScalar_permT`, `toScalar_basis_default`, `toScalar_basis`, `toScalar_eq_repr`, `toScalar_equivariant`, `eq_smul_toScalar`, `contrT_toScalar`, `Vector.toScalar_eval_eval_eq_tensorProduct_repr`, `toScalar_conjScalar`). The old name was easily confused with fields in the electromagnetism files, e.g. `toField {A.toFieldStrength x | [μ] [ν]}ᵀ`. Co-authored-by: Claude Opus 5.5 --- .../Dynamics/Hamiltonian.lean | 2 +- .../Electromagnetism/Dynamics/IsExtrema.lean | 2 +- .../Dynamics/KineticTerm.lean | 24 ++++----- .../Electromagnetism/Dynamics/Lagrangian.lean | 2 +- .../Electromagnetism/Kinematics/Boosts.lean | 2 +- .../Kinematics/EMPotential.lean | 4 +- .../Kinematics/ElectricField.lean | 10 ++-- .../Kinematics/FieldStrength.lean | 52 +++++++++--------- .../Kinematics/GaugeTransformation.lean | 6 +-- .../Kinematics/MagneticField.lean | 14 ++--- Physlib/Particles/SuperSymmetry/N1/Basic.lean | 12 ++--- Physlib/Relativity/Tensors/API-map.yaml | 6 +-- Physlib/Relativity/Tensors/Basic.lean | 54 +++++++++---------- Physlib/Relativity/Tensors/Evaluation.lean | 8 +-- .../Tensors/LeviCivita/Contractions.lean | 6 +-- Physlib/Relativity/Tensors/Product.lean | 4 +- .../Relativity/Tensors/RealTensor/Basic.lean | 6 +-- .../RealTensor/Vector/MinkowskiProduct.lean | 6 +-- .../Tensors/RealTensor/Vector/Tensorial.lean | 4 +- Physlib/Relativity/Tensors/Tensorial.lean | 4 +- 20 files changed, 114 insertions(+), 114 deletions(-) diff --git a/Physlib/Electromagnetism/Dynamics/Hamiltonian.lean b/Physlib/Electromagnetism/Dynamics/Hamiltonian.lean index b26dacd602..e7106ec5c9 100644 --- a/Physlib/Electromagnetism/Dynamics/Hamiltonian.lean +++ b/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 (𝕜 := ℝ) diff --git a/Physlib/Electromagnetism/Dynamics/IsExtrema.lean b/Physlib/Electromagnetism/Dynamics/IsExtrema.lean index 046a681fcd..27366589ae 100644 --- a/Physlib/Electromagnetism/Dynamics/IsExtrema.lean +++ b/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] diff --git a/Physlib/Electromagnetism/Dynamics/KineticTerm.lean b/Physlib/Electromagnetism/Dynamics/KineticTerm.lean index 5e4465c8e7..8950abfc9a 100644 --- a/Physlib/Electromagnetism/Dynamics/KineticTerm.lean +++ b/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, diff --git a/Physlib/Electromagnetism/Dynamics/Lagrangian.lean b/Physlib/Electromagnetism/Dynamics/Lagrangian.lean index 20cdf844b9..e9b5e3a803 100644 --- a/Physlib/Electromagnetism/Dynamics/Lagrangian.lean +++ b/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 diff --git a/Physlib/Electromagnetism/Kinematics/Boosts.lean b/Physlib/Electromagnetism/Kinematics/Boosts.lean index 14f42e21aa..82f5b53fdc 100644 --- a/Physlib/Electromagnetism/Kinematics/Boosts.lean +++ b/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 diff --git a/Physlib/Electromagnetism/Kinematics/EMPotential.lean b/Physlib/Electromagnetism/Kinematics/EMPotential.lean index 78e3f59b0a..2955ec6a4a 100644 --- a/Physlib/Electromagnetism/Kinematics/EMPotential.lean +++ b/Physlib/Electromagnetism/Kinematics/EMPotential.lean @@ -601,7 +601,7 @@ 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] @@ -609,7 +609,7 @@ lemma tensorDeriv_eval_eq {d} {A : ElectromagneticPotential d} (hA : Differentia 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]) diff --git a/Physlib/Electromagnetism/Kinematics/ElectricField.lean b/Physlib/Electromagnetism/Kinematics/ElectricField.lean index 3b039ba582..5b524cfb4c 100644 --- a/Physlib/Electromagnetism/Kinematics/ElectricField.lean +++ b/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,7 +189,7 @@ 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 @@ -197,7 +197,7 @@ lemma toFieldStrength_eval_inl_inr_eq_electricField {c : SpeedOfLight} 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, diff --git a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean index a55f126e8f..3bb6a84e62 100644 --- a/Physlib/Electromagnetism/Kinematics/FieldStrength.lean +++ b/Physlib/Electromagnetism/Kinematics/FieldStrength.lean @@ -17,7 +17,7 @@ public import Mathlib.Algebra.Order.Archimedean.Real.Hom In this module we define the field strength tensor in terms of the electromagnetic potential. We define the tensor and prove various properties of it. Its components are accessed -through index evaluation, `toField {A.toFieldStrength x | [μ] [ν]}ᵀ`. +through index evaluation, `toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ`. ## ii. Key results @@ -136,9 +136,9 @@ tensor in. -/ /-- The statement that `F = F^{μν} eᵤ ⊗ eᵥ` written explicitly, with - the components extracted via `toField`. -/ + the components extracted via `toScalar`. -/ lemma toFieldStrength_eq_sum_basis_eval {d} {A : ElectromagneticPotential d} : - A.toFieldStrength = fun x => ∑ μ, ∑ ν, toField {A.toFieldStrength x| [μ] [ν]}ᵀ • + A.toFieldStrength = fun x => ∑ μ, ∑ ν, toScalar {A.toFieldStrength x| [μ] [ν]}ᵀ • Vector.basis μ ⊗ₜ[ℝ] Vector.basis ν := by ext x exact prod_eq_sum_eval Vector.basis_eq_map_tensor_basis @@ -233,7 +233,7 @@ lemma contDiff_toFieldStrength {d} {n : WithTop ℕ∞} {A : ElectromagneticPote ### A.5. Components of the field strength tensor The components `F^{μν}` of the field strength tensor are accessed through index evaluation, -`toField {A.toFieldStrength x | [μ] [ν]}ᵀ`. This is the canonical way to refer to the +`toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ`. This is the canonical way to refer to the components of the field strength tensor, and is what should be used downstream. #### A.5.1. Index evaluation @@ -244,9 +244,9 @@ components of the field strength tensor, and is what should be used downstream. tensor basis. -/ lemma toFieldStrength_eval_eq_tensor_basis_repr {d} (A : ElectromagneticPotential d) (x : SpaceTime d) (μ ν : Fin 1 ⊕ Fin d) : - toField {A.toFieldStrength x | [μ] [ν]}ᵀ = + toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ = (Tensor.basis _).repr (Tensorial.toTensor (toFieldStrength A x)) (fun | 0 => μ | 1 => ν) := by - rw [Vector.toField_eval_eval_eq_tensorProduct_repr, Vector.tensor_basis_repr_toTensor_prod_apply] + rw [Vector.toScalar_eval_eval_eq_tensorProduct_repr, Vector.tensor_basis_repr_toTensor_prod_apply] /-- The coefficient of the field strength tensor in the tensor basis is given by index evaluation. -/ @@ -254,7 +254,7 @@ lemma toFieldStrength_tensor_basis_repr_eq_eval {d} (A : ElectromagneticPotentia (x : SpaceTime d) (b : ComponentIdx (S := realLorentzTensor d) (Fin.append ![Color.up] ![Color.up])) : (Tensor.basis _).repr (Tensorial.toTensor (toFieldStrength A x)) b = - toField {A.toFieldStrength x | [b 0] [b 1]}ᵀ := by + toScalar {A.toFieldStrength x | [b 0] [b 1]}ᵀ := by rw [toFieldStrength_eval_eq_tensor_basis_repr] congr 1 funext i @@ -264,7 +264,7 @@ lemma toFieldStrength_tensor_basis_repr_eq_eval {d} (A : ElectromagneticPotentia electromagnetic potential. -/ lemma toFieldStrength_eval_apply {d} (A : ElectromagneticPotential d) (x : SpaceTime d) (μ ν : Fin 1 ⊕ Fin d) : - toField {A.toFieldStrength x | [μ] [ν]}ᵀ = + toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ = ∑ κ, (η μ κ * ∂_ κ A x ν - η ν κ * ∂_ κ A x μ) := by rw [toFieldStrength_eval_eq_tensor_basis_repr, toTensor_toFieldStrength] simp only [map_sub, Finsupp.coe_sub, Pi.sub_apply, Tensor.permT_basis_repr_symm_apply, @@ -277,7 +277,7 @@ lemma toFieldStrength_eval_apply {d} (A : ElectromagneticPotential d) Minkowski metric. -/ lemma toFieldStrength_eval_apply_eq_single {d} (A : ElectromagneticPotential d) (x : SpaceTime d) (μ ν : Fin 1 ⊕ Fin d) : - toField {A.toFieldStrength x | [μ] [ν]}ᵀ = + toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ = η μ μ * ∂_ μ A x ν - η ν ν * ∂_ ν A x μ := by rw [toFieldStrength_eval_apply, Finset.sum_sub_distrib, Finset.sum_eq_single μ @@ -294,35 +294,35 @@ open ContDiff lemma toFieldStrength_eval_differentiable {d} {A : ElectromagneticPotential d} {μ ν : Fin 1 ⊕ Fin d} (hA : ContDiff ℝ 2 A) : - Differentiable ℝ (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) := by + Differentiable ℝ (fun x => toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ) := by simp only [toFieldStrength_eval_apply_eq_single] fun_prop lemma toFieldStrength_eval_differentiable_space {d} {A : ElectromagneticPotential d} {μ ν : Fin 1 ⊕ Fin d} (hA : ContDiff ℝ 2 A) (t : Time) {c : SpeedOfLight} : Differentiable ℝ (fun x => - toField {A.toFieldStrength ((toTimeAndSpace c).symm (t, x)) | [μ] [ν]}ᵀ) := by - change Differentiable ℝ ((fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) ∘ + toScalar {A.toFieldStrength ((toTimeAndSpace c).symm (t, x)) | [μ] [ν]}ᵀ) := by + change Differentiable ℝ ((fun x => toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ) ∘ fun x => (toTimeAndSpace c).symm (t, x)) exact (toFieldStrength_eval_differentiable hA).comp (by fun_prop) lemma toFieldStrength_eval_differentiable_time {d} {A : ElectromagneticPotential d} {μ ν : Fin 1 ⊕ Fin d} (hA : ContDiff ℝ 2 A) (x : Space d) {c : SpeedOfLight} : Differentiable ℝ (fun t => - toField {A.toFieldStrength ((toTimeAndSpace c).symm (t, x)) | [μ] [ν]}ᵀ) := by - change Differentiable ℝ ((fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) ∘ + toScalar {A.toFieldStrength ((toTimeAndSpace c).symm (t, x)) | [μ] [ν]}ᵀ) := by + change Differentiable ℝ ((fun x => toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ) ∘ fun t => (toTimeAndSpace c).symm (t, x)) exact (toFieldStrength_eval_differentiable hA).comp (by fun_prop) lemma toFieldStrength_eval_contDiff {d} {n : WithTop ℕ∞} {A : ElectromagneticPotential d} {μ ν : Fin 1 ⊕ Fin d} (hA : ContDiff ℝ (n + 1) A) : - ContDiff ℝ n (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) := by + ContDiff ℝ n (fun x => toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ) := by simp only [toFieldStrength_eval_apply_eq_single] fun_prop lemma toFieldStrength_eval_smooth {d} {A : ElectromagneticPotential d} (hA : ContDiff ℝ ∞ A) (μ ν : Fin 1 ⊕ Fin d) : - ContDiff ℝ ∞ (fun x => toField {A.toFieldStrength x | [μ] [ν]}ᵀ) := + ContDiff ℝ ∞ (fun x => toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ) := toFieldStrength_eval_contDiff (by simpa using hA) /-! @@ -335,13 +335,13 @@ We show that the field strength tensor is antisymmetric. lemma toFieldStrength_eval_antisymm {d} (A : ElectromagneticPotential d) (x : SpaceTime d) (μ ν : Fin 1 ⊕ Fin d) : - toField {A.toFieldStrength x | [μ] [ν]}ᵀ = - toField {A.toFieldStrength x | [ν] [μ]}ᵀ := by + toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ = - toScalar {A.toFieldStrength x | [ν] [μ]}ᵀ := by rw [toFieldStrength_eval_apply, toFieldStrength_eval_apply, ← Finset.sum_neg_distrib] exact Finset.sum_congr rfl fun κ _ => by simp lemma toFieldStrength_eval_diag_eq_zero {d} (A : ElectromagneticPotential d) (x : SpaceTime d) (μ : Fin 1 ⊕ Fin d) : - toField {A.toFieldStrength x | [μ] [μ]}ᵀ = 0 := by + toScalar {A.toFieldStrength x | [μ] [μ]}ᵀ = 0 := by rw [toFieldStrength_eval_apply_eq_single, sub_self] lemma toFieldStrength_antisymmetric {d} (A : ElectromagneticPotential d) (x : SpaceTime d) : @@ -362,9 +362,9 @@ lemma toFieldStrength_antisymmetric {d} (A : ElectromagneticPotential d) (x : Sp lemma toFieldStrength_eval_equivariant {d} (A : ElectromagneticPotential d) (Λ : LorentzGroup d) (hf : Differentiable ℝ A) (x : SpaceTime d) (μ ν : Fin 1 ⊕ Fin d) : - toField {(Λ • A).toFieldStrength x | [μ] [ν]}ᵀ = - ∑ κ, ∑ ρ, (Λ.1 μ κ * Λ.1 ν ρ) * toField {A.toFieldStrength (Λ⁻¹ • x) | [κ] [ρ]}ᵀ := by - simp only [Vector.toField_eval_eval_eq_tensorProduct_repr] + toScalar {(Λ • A).toFieldStrength x | [μ] [ν]}ᵀ = + ∑ κ, ∑ ρ, (Λ.1 μ κ * Λ.1 ν ρ) * toScalar {A.toFieldStrength (Λ⁻¹ • x) | [κ] [ρ]}ᵀ := by + simp only [Vector.toScalar_eval_eval_eq_tensorProduct_repr] rw [toFieldStrength_equivariant A Λ hf x] generalize A.toFieldStrength (Λ⁻¹ • x) = F induction F using TensorProduct.inductionOn with @@ -386,7 +386,7 @@ 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) | [κ] [ρ]}ᵀ) • + (∑ κ, ∑ ρ, Λ.1 μ κ * Λ.1 ν ρ * toScalar {A.toFieldStrength (Λ⁻¹ • x) | [κ] [ρ]}ᵀ) • Vector.basis μ ⊗ₜ[ℝ] Vector.basis ν := by rw [toFieldStrength_eq_sum_basis_eval] simp only [toFieldStrength_eval_equivariant A Λ hf x] @@ -402,8 +402,8 @@ We show that the field strength tensor is linear in the potential. lemma toFieldStrength_eval_add {d} (A1 A2 : ElectromagneticPotential d) (x : SpaceTime d) (hA1 : Differentiable ℝ A1) (hA2 : Differentiable ℝ A2) (μ ν : Fin 1 ⊕ Fin d) : - toField {(A1 + A2).toFieldStrength x | [μ] [ν]}ᵀ = - toField {A1.toFieldStrength x | [μ] [ν]}ᵀ + toField {A2.toFieldStrength x | [μ] [ν]}ᵀ := by + toScalar {(A1 + A2).toFieldStrength x | [μ] [ν]}ᵀ = + toScalar {A1.toFieldStrength x | [μ] [ν]}ᵀ + toScalar {A2.toFieldStrength x | [μ] [ν]}ᵀ := by simp only [toFieldStrength_eval_apply, ← Finset.sum_add_distrib] refine Finset.sum_congr rfl fun κ _ => ?_ simp only [SpaceTime.deriv_eq, add_val, fderiv_add hA1.differentiableAt hA2.differentiableAt, @@ -421,8 +421,8 @@ lemma toFieldStrength_add {d} (A1 A2 : ElectromagneticPotential d) lemma toFieldStrength_eval_smul {d} (c : ℝ) (A : ElectromagneticPotential d) (x : SpaceTime d) (hA : Differentiable ℝ A) (μ ν : Fin 1 ⊕ Fin d) : - toField {(c • A).toFieldStrength x | [μ] [ν]}ᵀ = - c * toField {A.toFieldStrength x | [μ] [ν]}ᵀ := by + toScalar {(c • A).toFieldStrength x | [μ] [ν]}ᵀ = + c * toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ := by simp only [toFieldStrength_eval_apply, Finset.mul_sum] refine Finset.sum_congr rfl fun κ _ => ?_ simp only [SpaceTime.deriv_eq, smul_val, fderiv_const_smul hA.differentiableAt, FunLike.coe_smul, diff --git a/Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean b/Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean index 07a6c5e162..aafc1e449a 100644 --- a/Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean +++ b/Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean @@ -267,8 +267,8 @@ lemma toFieldStrength_gaugeTransform {d} (A : ElectromagneticPotential d) lemma toFieldStrength_eval_gaugeTransform {d} (A : ElectromagneticPotential d) (χ : SpaceTime d → ℝ) (hA : Differentiable ℝ A) (hχ : ContDiff ℝ 2 χ) (x : SpaceTime d) (μ ν : Fin 1 ⊕ Fin d) : - toField {(gaugeTransform χ A).toFieldStrength x | [μ] [ν]}ᵀ = - toField {A.toFieldStrength x | [μ] [ν]}ᵀ := by + toScalar {(gaugeTransform χ A).toFieldStrength x | [μ] [ν]}ᵀ = + toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ := by rw [toFieldStrength_gaugeTransform A χ hA hχ] /-! @@ -343,7 +343,7 @@ lemma toFieldStrength_eval_bareGradient_inl_inr {d : ℕ} (i : Fin d) (x : SpaceTime d) : let χ : SpaceTime d → ℝ := fun y => y (Sum.inl 0) * y (Sum.inr i) let B : ElectromagneticPotential d := ⟨fun y μ => ∂_ μ χ y⟩ - toField {B.toFieldStrength x | [Sum.inl 0] [Sum.inr i]}ᵀ = 2 := by + toScalar {B.toFieldStrength x | [Sum.inl 0] [Sum.inr i]}ᵀ = 2 := by intro χ B have hχ : ContDiff ℝ 2 χ := by show ContDiff ℝ 2 (fun y : SpaceTime d => y (Sum.inl 0) * y (Sum.inr i)) diff --git a/Physlib/Electromagnetism/Kinematics/MagneticField.lean b/Physlib/Electromagnetism/Kinematics/MagneticField.lean index 3ffc4faa10..23cd64b711 100644 --- a/Physlib/Electromagnetism/Kinematics/MagneticField.lean +++ b/Physlib/Electromagnetism/Kinematics/MagneticField.lean @@ -92,7 +92,7 @@ lemma magneticField_eq {c : SpeedOfLight} (A : ElectromagneticPotential) : lemma magneticField_coord_eq_toFieldStrength_eval {i : Fin 3} {c : SpeedOfLight} (A : ElectromagneticPotential) (t : Time) (x : Space) (hA : Differentiable ℝ A) : - A.magneticField c t x i = - toField {A.toFieldStrength ((toTimeAndSpace c).symm (t, x)) | + A.magneticField c t x i = - toScalar {A.toFieldStrength ((toTimeAndSpace c).symm (t, x)) | [Sum.inr (i+1)] [Sum.inr (i+2)]}ᵀ := by rw [toFieldStrength_eval_apply_eq_single] simp only [Fin.isValue, inr_i_inr_i, neg_mul, one_mul, sub_neg_eq_add, neg_add_rev, neg_neg] @@ -168,7 +168,7 @@ lemma ofElectromagneticField_magneticField {c : SpeedOfLight} lemma toFieldStrength_eval_eq_electric_magnetic {c} (A : ElectromagneticPotential) (t : Time) (x : Space) (hA : Differentiable ℝ A) (μ ν : Fin 1 ⊕ Fin 3) : - toField {A.toFieldStrength ((toTimeAndSpace c).symm (t, x)) | [μ] [ν]}ᵀ = + toScalar {A.toFieldStrength ((toTimeAndSpace c).symm (t, x)) | [μ] [ν]}ᵀ = match μ, ν with | Sum.inl 0, Sum.inl 0 => 0 | Sum.inl 0, Sum.inr i => - A.electricField c t x i / c @@ -200,7 +200,7 @@ lemma toFieldStrength_eval_eq_electric_magnetic_of_spaceTime (c : SpeedOfLight) (A : ElectromagneticPotential) (x : SpaceTime) (hA : Differentiable ℝ A) (μ ν : Fin 1 ⊕ Fin 3) : let tx := SpaceTime.toTimeAndSpace c x - toField {A.toFieldStrength x | [μ] [ν]}ᵀ = + toScalar {A.toFieldStrength x | [μ] [ν]}ᵀ = match μ, ν with | Sum.inl 0, Sum.inl 0 => 0 | Sum.inl 0, Sum.inr i => - A.electricField c tx.1 tx.2 i / c @@ -231,17 +231,17 @@ lemma toFieldStrength_eval_eq_electric_magnetic_of_spaceTime (c : SpeedOfLight) In `3` space-dimensions this reduces to a vector. -/ noncomputable def magneticFieldMatrix (c : SpeedOfLight := 1) (A : ElectromagneticPotential d) : Time → Space d → (Fin d × Fin d) → ℝ := timeSlice c <| fun x ij => - toField {A.toFieldStrength x | [Sum.inr ij.1] [Sum.inr ij.2]}ᵀ + toScalar {A.toFieldStrength x | [Sum.inr ij.1] [Sum.inr ij.2]}ᵀ lemma magneticFieldMatrix_eq {c : SpeedOfLight} (A : ElectromagneticPotential d) : A.magneticFieldMatrix c = fun t x ij => - toField {A.toFieldStrength ((toTimeAndSpace c).symm (t, x)) | + toScalar {A.toFieldStrength ((toTimeAndSpace c).symm (t, x)) | [Sum.inr ij.1] [Sum.inr ij.2]}ᵀ := rfl lemma toFieldStrength_eval_inr_inr_eq_magneticFieldMatrix {c : SpeedOfLight} (A : ElectromagneticPotential d) (x : SpaceTime d) (i j : Fin d) : - toField {A.toFieldStrength x | [Sum.inr i] [Sum.inr j]}ᵀ = + toScalar {A.toFieldStrength x | [Sum.inr i] [Sum.inr j]}ᵀ = A.magneticFieldMatrix c (x.time c) x.space (i, j) := by simp [magneticFieldMatrix_eq] @@ -464,7 +464,7 @@ lemma curl_magneticFieldMatrix_eq_electricField_toFieldStrength_eval {d : ℕ} { (hA : ContDiff ℝ 2 A) (t : Time) (x : Space d) (i : Fin d) : ∑ j, Space.deriv j (A.magneticFieldMatrix c t · (j, i)) x = (1/c^2) * ∂ₜ (fun t => A.electricField c t x) t i + - (∑ (μ : (Fin 1 ⊕ Fin d)), (∂_ μ (fun x => toField {A.toFieldStrength x | [μ] [Sum.inr i]}ᵀ) + (∑ (μ : (Fin 1 ⊕ Fin d)), (∂_ μ (fun x => toScalar {A.toFieldStrength x | [μ] [Sum.inr i]}ᵀ) ((toTimeAndSpace c).symm (t, x)))) := by trans (1/c^2) * ∂ₜ (fun t => A.electricField c t x) t i + (- (1/c^2) * ∂ₜ (fun t => A.electricField c t x) t i + diff --git a/Physlib/Particles/SuperSymmetry/N1/Basic.lean b/Physlib/Particles/SuperSymmetry/N1/Basic.lean index 5a0a147d7e..7eba969850 100644 --- a/Physlib/Particles/SuperSymmetry/N1/Basic.lean +++ b/Physlib/Particles/SuperSymmetry/N1/Basic.lean @@ -412,12 +412,12 @@ def conjChiralCovector ((chiralTensor (ι := ι)).conjT t) set_option backward.isDefEq.respectTransparency false in -/-- For scalar tensors, `toField` of the normalized tensor conjugate is the complex conjugate of -`toField`. -/ -lemma toField_conjScalar (t : (chiralTensor (ι := ι)).Tensor ![]) : - (conjScalar t).toField = star t.toField := by - rw [conjScalar, toField_permT] - rw [toField_eq_repr, toField_eq_repr] +/-- For scalar tensors, `toScalar` of the normalized tensor conjugate is the complex conjugate of +`toScalar`. -/ +lemma toScalar_conjScalar (t : (chiralTensor (ι := ι)).Tensor ![]) : + (conjScalar t).toScalar = star t.toScalar := by + rw [conjScalar, toScalar_permT] + rw [toScalar_eq_repr, toScalar_eq_repr] change componentMap (S := (chiralTensor (ι := ι)).toTensorSpecies) ((chiralTensor (ι := ι)).bar ∘ ![]) ((chiralTensor (ι := ι)).conjT t) (fun j => Fin.elim0 j) = star ((basis (S := (chiralTensor (ι := ι)).toTensorSpecies) ![]).repr t (fun j => Fin.elim0 j)) diff --git a/Physlib/Relativity/Tensors/API-map.yaml b/Physlib/Relativity/Tensors/API-map.yaml index 67438323c8..a7907f3d65 100644 --- a/Physlib/Relativity/Tensors/API-map.yaml +++ b/Physlib/Relativity/Tensors/API-map.yaml @@ -38,10 +38,10 @@ Requirements: done: true location: "Physlib/Relativity/Tensors/TensorSpecies/Basic.lean (TensorSpecies, basisIdxCongr, τ_τ_apply, basis_congr, numIndices)" - - description: "The API contains the type `Tensor` of tensors with a given list of index colors, the type `Pure` of pure tensors, the type `ComponentIdx` of component labels, the passage between a tensor and its components, the component basis, and the identification of rank-zero tensors with the base field." + - description: "The API contains the type `Tensor` of tensors with a given list of index colors, the type `Pure` of pure tensors, the type `ComponentIdx` of component labels, the passage between a tensor and its components, the component basis, and the identification of rank-zero tensors with the scalars." done: true location: | - Physlib/Relativity/Tensors/Basic.lean (Tensor, Pure, Pure.toTensor, Pure.component, Pure.basisVector, Tensor.componentMap, ofComponents, basis, basis_repr_pure, toField); Physlib/Relativity/Tensors/ComponentIdx/Basic.lean (ComponentIdx, ComponentIdx.congr_right, ComponentIdx.cast); Physlib/Relativity/Tensors/ComponentIdx/Single.lean (ComponentIdx.single); Physlib/Relativity/Tensors/ComponentIdx/Product.lean (ComponentIdx.prod); Physlib/Relativity/Tensors/ComponentIdx/Contraction.lean (ComponentIdx.dropPair, ComponentIdx.DropPairSection, ComponentIdx.DropPairSection.ofFinEquiv, ComponentIdx.DropPairSection.ofFinEquiv_dropPair) + Physlib/Relativity/Tensors/Basic.lean (Tensor, Pure, Pure.toTensor, Pure.component, Pure.basisVector, Tensor.componentMap, ofComponents, basis, basis_repr_pure, toScalar); Physlib/Relativity/Tensors/ComponentIdx/Basic.lean (ComponentIdx, ComponentIdx.congr_right, ComponentIdx.cast); Physlib/Relativity/Tensors/ComponentIdx/Single.lean (ComponentIdx.single); Physlib/Relativity/Tensors/ComponentIdx/Product.lean (ComponentIdx.prod); Physlib/Relativity/Tensors/ComponentIdx/Contraction.lean (ComponentIdx.dropPair, ComponentIdx.DropPairSection, ComponentIdx.DropPairSection.ofFinEquiv, ComponentIdx.DropPairSection.ofFinEquiv_dropPair) - description: "The API contains the action of the symmetry group on pure tensors and on tensors, the permutation of indices along a color-preserving map, and the notion `IsReindexing` of such a map together with its closure under inverse, composition and the index maps used by products, evaluation and contraction." done: true @@ -83,7 +83,7 @@ Requirements: - description: "The API contains the tensor species `realLorentzTensor d` of real Lorentz tensors, with colors `up` and `down`, built from the contravariant and covariant modules, their representations of the Lorentz group, their bases, and the contraction, metric and unit maps; the metric tensors of the species are computed in the standard basis, and the pairwise tensor products of the contravariant and covariant modules are identified with square matrices." done: true location: | - Physlib/Relativity/Tensors/RealTensor/Basic.lean (realLorentzTensor, realLorentzTensor.Color, τ_up_eq_down, τ_down_eq_up, contrPCoeff_basis, contrT_eq_sum_evalT, contrT_toField); Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Modules.lean (ContrMod, CoMod, AddCommGroup (ContrMod d), Module ℝ (ContrMod d), AddCommGroup (CoMod d), Module ℝ (CoMod d), ContrMod.rep, CoMod.rep, ContrMod.stdBasis, CoMod.stdBasis); Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Basic.lean (contrBasis, coBasis, contrIsoCo); Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Contraction.lean (contrCoContract, coContrContract, contrContrContractField); Physlib/Relativity/Tensors/RealTensor/Metrics/Pre.lean (preContrMetric, preCoMetric); Physlib/Relativity/Tensors/RealTensor/Units/Pre.lean (preContrCoUnit, preCoContrUnit); Physlib/Relativity/Tensors/RealTensor/Metrics/Basic.lean (coMetric, contrMetric, actionT_coMetric, actionT_contrMetric, coMetric_repr_apply_eq_minkowskiMatrix, contrMetric_repr_apply_eq_minkowskiMatrix, metricTensor_repr_apply_eq_minkowskiMatrix, toDualMapAtIndex_basis_repr_apply, toDualMapAtIndex_basis_repr_apply_eq_mul); Physlib/Relativity/Tensors/RealTensor/Units/Basic.lean (unitTensor_repr_apply); Physlib/Relativity/Tensors/RealTensor/Matrix/Pre.lean (contrContrToMatrixRe, coCoToMatrixRe, contrCoToMatrixRe, coContrToMatrixRe) + Physlib/Relativity/Tensors/RealTensor/Basic.lean (realLorentzTensor, realLorentzTensor.Color, τ_up_eq_down, τ_down_eq_up, contrPCoeff_basis, contrT_eq_sum_evalT, contrT_toScalar); Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Modules.lean (ContrMod, CoMod, AddCommGroup (ContrMod d), Module ℝ (ContrMod d), AddCommGroup (CoMod d), Module ℝ (CoMod d), ContrMod.rep, CoMod.rep, ContrMod.stdBasis, CoMod.stdBasis); Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Basic.lean (contrBasis, coBasis, contrIsoCo); Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Contraction.lean (contrCoContract, coContrContract, contrContrContractField); Physlib/Relativity/Tensors/RealTensor/Metrics/Pre.lean (preContrMetric, preCoMetric); Physlib/Relativity/Tensors/RealTensor/Units/Pre.lean (preContrCoUnit, preCoContrUnit); Physlib/Relativity/Tensors/RealTensor/Metrics/Basic.lean (coMetric, contrMetric, actionT_coMetric, actionT_contrMetric, coMetric_repr_apply_eq_minkowskiMatrix, contrMetric_repr_apply_eq_minkowskiMatrix, metricTensor_repr_apply_eq_minkowskiMatrix, toDualMapAtIndex_basis_repr_apply, toDualMapAtIndex_basis_repr_apply_eq_mul); Physlib/Relativity/Tensors/RealTensor/Units/Basic.lean (unitTensor_repr_apply); Physlib/Relativity/Tensors/RealTensor/Matrix/Pre.lean (contrContrToMatrixRe, coCoToMatrixRe, contrCoToMatrixRe, coContrToMatrixRe) - description: "The API contains Lorentz vectors and covectors as functions on `Fin 1 ⊕ Fin d`, with their module, norm and inner-product structures, their charted-space structures, their standard bases, their representations of the Lorentz group, their tensorial instances and the invariant contraction between them, together with the coordinate maps and the time and spatial parts of a vector, and the model with corners under which vectors are treated as a manifold." done: true diff --git a/Physlib/Relativity/Tensors/Basic.lean b/Physlib/Relativity/Tensors/Basic.lean index 8a8aefb659..d09b71ed9c 100644 --- a/Physlib/Relativity/Tensors/Basic.lean +++ b/Physlib/Relativity/Tensors/Basic.lean @@ -40,7 +40,7 @@ This file realizes `Tensor S c` as a `PiTensorProduct`, relates pure tensors to their components, constructs the component basis, and supplies the inherited finite-dimensional and module-topology instances. It also defines the natural action of `G` on pure tensors and tensors, the associated permutation maps, and -the map from rank-zero tensors to the base field. +the map from rank-zero tensors to the scalars `k`. From this setup we get the usual index-notation operations in a uniform way: contraction, raising/lowering, and permutation of indices. @@ -642,63 +642,63 @@ lemma permT_injective {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C} (injective_iff_map_eq_zero' _).mpr (permT_eq_zero_iff h) /-! -## field +## Rank-zero tensors as scalars -/ -/-- The linear map between tensors with zero indices and the underlying field +/-- The linear map between tensors with zero indices and the underlying scalars `k`. -/ -noncomputable def toField {c : Fin 0 → C} : S.Tensor c →ₗ[k] k := +noncomputable def toScalar {c : Fin 0 → C} : S.Tensor c →ₗ[k] k := (PiTensorProduct.isEmptyEquiv (Fin 0)).toLinearMap -lemma toField_default {c : Fin 0 → C} : - toField (Pure.toTensor default : S.Tensor c) = 1 := by - simp [toField, Pure.toTensor] +lemma toScalar_default {c : Fin 0 → C} : + toScalar (Pure.toTensor default : S.Tensor c) = 1 := by + simp [toScalar, Pure.toTensor] -lemma toField_injective {c : Fin 0 → C} : - Function.Injective (toField : S.Tensor c → k) := +lemma toScalar_injective {c : Fin 0 → C} : + Function.Injective (toScalar : S.Tensor c → k) := (PiTensorProduct.isEmptyEquiv (Fin 0)).injective @[simp] -lemma toField_pure {c : Fin 0 → C} (p : Pure S c) : - toField (p.toTensor : S.Tensor c) = 1 := by - rw [Subsingleton.elim p default, toField_default] +lemma toScalar_pure {c : Fin 0 → C} (p : Pure S c) : + toScalar (p.toTensor : S.Tensor c) = 1 := by + rw [Subsingleton.elim p default, toScalar_default] -lemma toField_permT {c c1 : Fin 0 → C} (σ : Fin 0 → Fin 0) +lemma toScalar_permT {c c1 : Fin 0 → C} (σ : Fin 0 → Fin 0) (h : IsReindexing c c1 σ) (t : S.Tensor c) : - toField (permT σ h t) = toField t := by + toScalar (permT σ h t) = toScalar t := by induction' t using induction_on_basis with b r t ht t1 t2 h1 h2 - · simp [toField_pure, basis_apply, permT_pure] + · simp [toScalar_pure, basis_apply, permT_pure] · simp · simp [ht] · simp [h1, h2] @[simp] -lemma toField_basis_default {c : Fin 0 → C} : - toField (basis c (@default (ComponentIdx (S := S) c) Unique.instInhabited)) = 1 := by +lemma toScalar_basis_default {c : Fin 0 → C} : + toScalar (basis c (@default (ComponentIdx (S := S) c) Unique.instInhabited)) = 1 := by simp [basis_apply] -lemma toField_basis {c : Fin 0 → C} (b : ComponentIdx (S := S) c) : - toField (basis c b) = 1 := by +lemma toScalar_basis {c : Fin 0 → C} (b : ComponentIdx (S := S) c) : + toScalar (basis c b) = 1 := by simp [basis_apply] -lemma toField_eq_repr {c : Fin 0 → C} (t : Tensor S c) : - t.toField = (basis c).repr t (fun j => Fin.elim0 j) := by +lemma toScalar_eq_repr {c : Fin 0 → C} (t : Tensor S c) : + t.toScalar = (basis c).repr t (fun j => Fin.elim0 j) := by obtain ⟨t, rfl⟩ := (basis c).repr.symm.surjective t simp only [Basis.repr_symm_apply, Basis.repr_linearCombination] - rw [Finsupp.linearCombination_unique, map_smul, toField_basis_default, smul_eq_mul, mul_one] + rw [Finsupp.linearCombination_unique, map_smul, toScalar_basis_default, smul_eq_mul, mul_one] rfl @[simp] -lemma toField_equivariant {c : Fin 0 → C} (g : G) (t : Tensor S c) : - toField (g • t) = toField t := by +lemma toScalar_equivariant {c : Fin 0 → C} (g : G) (t : Tensor S c) : + toScalar (g • t) = toScalar t := by induction t using induction_on_pure with | h p => simp [actionT_pure] | hsmul r t hp => simp [hp] | hadd t1 t2 hp1 hp2 => simp [hp1, hp2] -lemma eq_smul_toField {c : Fin 0 → C} (t : Tensor S c) : - t = toField t • (basis c (@default (ComponentIdx (S := S) c) Unique.instInhabited)) := by - apply toField_injective +lemma eq_smul_toScalar {c : Fin 0 → C} (t : Tensor S c) : + t = toScalar t • (basis c (@default (ComponentIdx (S := S) c) Unique.instInhabited)) := by + apply toScalar_injective simp end Tensor diff --git a/Physlib/Relativity/Tensors/Evaluation.lean b/Physlib/Relativity/Tensors/Evaluation.lean index 26a6879d29..2a7cab9388 100644 --- a/Physlib/Relativity/Tensors/Evaluation.lean +++ b/Physlib/Relativity/Tensors/Evaluation.lean @@ -382,19 +382,19 @@ set_option backward.isDefEq.respectTransparency false in yields the field element `1` if `b = x` (transported across `![c] 0 = c`) and `0` otherwise: evaluation of a one-index basis tensor is the Kronecker delta. -/ lemma evalT_basis_single {c : C} (b : basisIdx c) (x : basisIdx (![c] 0)) : - (evalT 0 x (basis (S := S) ![c] (ComponentIdx.single.symm b))).toField = + (evalT 0 x (basis (S := S) ![c] (ComponentIdx.single.symm b))).toScalar = if basisIdxCongr (by simp) b = x then 1 else 0 := by rw [evalT_basis] simp only [ComponentIdx.single_symm_apply] split_ifs - · exact toField_basis _ + · exact toScalar_basis _ · simp /-- Basis expansion of a one-index tensor: every `t : Tensor S ![c]` is the sum over basis - indices `i` of its evaluation coefficient `toField (evalT 0 i t)` times the corresponding + indices `i` of its evaluation coefficient `toScalar (evalT 0 i t)` times the corresponding basis tensor. -/ lemma eq_sum_evalT_of_single_tensor_basis {c : C} (t : Tensor S ![c]) : - t = ∑ i, toField (evalT 0 i t) • basis ![c] (ComponentIdx.single.symm + t = ∑ i, toScalar (evalT 0 i t) • basis ![c] (ComponentIdx.single.symm (basisIdxCongr (by simp) i)) := by induction' t using Tensor.induction_on_basis with b a t h t1 t2 h1 h2 · obtain ⟨i, rfl⟩ := ComponentIdx.single.symm.surjective b diff --git a/Physlib/Relativity/Tensors/LeviCivita/Contractions.lean b/Physlib/Relativity/Tensors/LeviCivita/Contractions.lean index 5ac1c2fa8f..c6f3bc956b 100644 --- a/Physlib/Relativity/Tensors/LeviCivita/Contractions.lean +++ b/Physlib/Relativity/Tensors/LeviCivita/Contractions.lean @@ -300,7 +300,7 @@ lemma leviCivita_contract_three : {ε4 | μ ν ρ σ ⊗ ε4 | τ(μ) τ(ν) τ( products of their matching standard-basis components. -/ @[nolint checkType] lemma leviCivita_contract_self_eq_sum : - {ε4 | μ ν ρ σ ⊗ ε4 | τ(μ) τ(ν) τ(ρ) τ(σ)}ᵀ.toField = + {ε4 | μ ν ρ σ ⊗ ε4 | τ(μ) τ(ν) τ(ρ) τ(σ)}ᵀ.toScalar = ∑ b : ComponentIdx (S := realLorentzTensor 3) ![Color.up, Color.up, Color.up, Color.up], (Tensor.basis _).repr ε4 b * @@ -318,7 +318,7 @@ lemma leviCivita_contract_self_eq_sum : (![x0, x1, x2, x3], ![x0, x1, x2, x3]) := by dsimp only apply Prod.ext <;> funext m <;> fin_cases m <;> rfl - rw [Tensor.toField_eq_repr] + rw [Tensor.toScalar_eq_repr] simp only [contrT_basis_repr_apply_eq_fin, prodT_basis_repr_apply, route] let F (b : Fin 4 → Fin 1 ⊕ Fin 3) := (Tensor.basis _).repr ε4 b * @@ -337,7 +337,7 @@ lemma leviCivita_contract_self_eq_sum : /-- Fully contracting the Lorentzian Levi-Civita tensor with a lowered copy gives `-24`. -/ @[nolint checkType] lemma leviCivita_contract_self : - {ε4 | μ ν ρ σ ⊗ ε4 | τ(μ) τ(ν) τ(ρ) τ(σ)}ᵀ.toField = - 24 := by + {ε4 | μ ν ρ σ ⊗ ε4 | τ(μ) τ(ν) τ(ρ) τ(σ)}ᵀ.toScalar = - 24 := by rw [leviCivita_contract_self_eq_sum] calc _ = - ∑ b : ComponentIdx (S := realLorentzTensor 3) diff --git a/Physlib/Relativity/Tensors/Product.lean b/Physlib/Relativity/Tensors/Product.lean index 4723c72a5d..c213cba576 100644 --- a/Physlib/Relativity/Tensors/Product.lean +++ b/Physlib/Relativity/Tensors/Product.lean @@ -605,8 +605,8 @@ lemma prodT_default_right {n} {c : Fin n → C} lemma prodT_zero_right {n} {c : Fin n → C} {c1 : Fin 0 → C} (t : S.Tensor c) (t1 : S.Tensor c1) : - prodT t t1 = (toField t1) • permT id (IsReindexing.append_zero_right) t := by - conv_lhs => rw [Tensor.eq_smul_toField t1] + prodT t t1 = (toScalar t1) • permT id (IsReindexing.append_zero_right) t := by + conv_lhs => rw [Tensor.eq_smul_toScalar t1] rw [map_smul] congr 1 convert prodT_default_right _ diff --git a/Physlib/Relativity/Tensors/RealTensor/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Basic.lean index c550403afd..34e0ea8eb8 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Basic.lean +++ b/Physlib/Relativity/Tensors/RealTensor/Basic.lean @@ -219,13 +219,13 @@ lemma contrT_eq_sum_evalT {n} {d} (c : Fin (n + 1 + 1) → Color) (i j : Fin (n · simp [Finset.smul_sum, h] · simp [h1, h2, Finset.sum_add_distrib] -lemma contrT_toField {d} (c : Fin 2 → Color) +lemma contrT_toScalar {d} (c : Fin 2 → Color) (h : 0 ≠ 1 ∧ (realLorentzTensor d).τ (c 0) = c 1) (t : ℝT(d, c)) : - (contrT 0 0 1 h t).toField = ∑ (μ : Fin 1 ⊕ Fin d), {t | [μ] [μ]}ᵀ.toField := by + (contrT 0 0 1 h t).toScalar = ∑ (μ : Fin 1 ⊕ Fin d), {t | [μ] [μ]}ᵀ.toScalar := by rw [contrT_eq_sum_evalT, map_sum] congr ext μ - simp only [toField_permT] + simp only [toScalar_permT] rfl open ComponentIdx in diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/MinkowskiProduct.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/MinkowskiProduct.lean index f964243460..06a6269545 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Vector/MinkowskiProduct.lean +++ b/Physlib/Relativity/Tensors/RealTensor/Vector/MinkowskiProduct.lean @@ -38,13 +38,13 @@ open Tensor /-- The Minkowski product of Lorentz vectors in the +--- convention.. -/ def minkowskiProductMap {d : ℕ} (p q : Vector d) : ℝ := - {η' d | μ ν ⊗ p | μ ⊗ q | ν}ᵀ.toField + {η' d | μ ν ⊗ p | μ ⊗ q | ν}ᵀ.toScalar lemma minkowskiProductMap_toCoord {d : ℕ} (p q : Vector d) : minkowskiProductMap p q = p (Sum.inl 0) * q (Sum.inl 0) - ∑ i, p (Sum.inr i) * q (Sum.inr i) := by dsimp only [minkowskiProductMap, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue] - rw [toField_eq_repr, contrT_basis_repr_apply_eq_fin] + rw [toScalar_eq_repr, contrT_basis_repr_apply_eq_fin] conv_lhs => enter [2, x] rw [prodT_basis_repr_apply, contrT_basis_repr_apply_eq_fin] @@ -149,7 +149,7 @@ lemma minkowskiProduct_invariant {d : ℕ} (p q : Vector d) (Λ : LorentzGroup d rw [minkowskiProduct_apply, minkowskiProductMap, ← actionT_coMetric Λ] simp only [Tensorial.toTensor_smul] rw [prodT_equivariant, contrT_equivariant, prodT_equivariant, contrT_equivariant, - toField_equivariant] + toScalar_equivariant] rfl open InnerProductSpace in diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/Tensorial.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/Tensorial.lean index 79ab182cd1..fe0834ed3c 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Vector/Tensorial.lean +++ b/Physlib/Relativity/Tensors/RealTensor/Vector/Tensorial.lean @@ -131,9 +131,9 @@ lemma tensor_basis_repr_toTensor_apply {d : ℕ} (p : Vector d) (μ : ComponentI /-- Evaluating both indices of an element of `Vector d ⊗ Vector d` gives its coefficient in the tensor-product basis. -/ -lemma toField_eval_eval_eq_tensorProduct_repr {d} (F : Vector d ⊗[ℝ] Vector d) +lemma toScalar_eval_eval_eq_tensorProduct_repr {d} (F : Vector d ⊗[ℝ] Vector d) (μ ν : Fin 1 ⊕ Fin d) : - toField {F | [μ] [ν]}ᵀ = (basis.tensorProduct basis).repr F (μ, ν) := by + toScalar {F | [μ] [ν]}ᵀ = (basis.tensorProduct basis).repr F (μ, ν) := by conv_rhs => rw [Tensorial.prod_eq_sum_eval basis_eq_map_tensor_basis basis_eq_map_tensor_basis F] simp [-Fintype.sum_sum_type, Basis.tensorProduct_repr_tmul_apply, Finsupp.single_apply] rfl diff --git a/Physlib/Relativity/Tensors/Tensorial.lean b/Physlib/Relativity/Tensors/Tensorial.lean index e5afc34091..97e4064467 100644 --- a/Physlib/Relativity/Tensors/Tensorial.lean +++ b/Physlib/Relativity/Tensors/Tensorial.lean @@ -323,7 +323,7 @@ set_option backward.isDefEq.respectTransparency false in /-- Double basis expansion of an element of a tensor product `M ⊗[k] M₂` of two `Tensorial` one-index spaces. Given bases `b`, `b2` of `M`, `M₂` coming from the single-index tensor bases, every `x : M ⊗[k] M₂` is the double sum over `i, j` of the iterated evaluation coefficient - `toField (evalT 0 j (evalT 0 i (toTensor x)))` times `b i ⊗ₜ b2 j`. -/ + `toScalar (evalT 0 j (evalT 0 i (toTensor x)))` times `b i ⊗ₜ b2 j`. -/ lemma prod_eq_sum_eval {c c2 : C} {M₂ : Type} [Tensorial S ![c] M] [AddCommMonoid M₂] [Module k M₂] [Tensorial S ![c2] M₂] {b : Module.Basis (basisIdx c) k M} @@ -331,7 +331,7 @@ lemma prod_eq_sum_eval {c c2 : C} {M₂ : Type} (h : b = ((Tensor.basis (S := S) ![c]).map toTensor.symm).reindex ComponentIdx.single) (h2 : b2 = ((Tensor.basis (S := S) ![c2]).map toTensor.symm).reindex ComponentIdx.single) (x : M ⊗[k] M₂) : x = ∑ i : (basisIdx c), ∑ j : (basisIdx c2), - toField (evalT 0 (basisIdxCongr (by rfl) j) + toScalar (evalT 0 (basisIdxCongr (by rfl) j) (evalT 0 (basisIdxCongr (by rfl) i) (toTensor x))) • b i ⊗ₜ[k] b2 j := by apply toTensor.injective conv_lhs => rw [eq_sum_evalT_zero (toTensor x)]