From 0628c3ded567670cbcd870d3d84ab6bb7081729b Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 21 Apr 2026 10:23:24 +0100 Subject: [PATCH 1/2] refactor: Separate Vector.Basic & CoVector.Basic --- Physlib.lean | 2 + .../Relativity/LorentzGroup/Boosts/Apply.lean | 2 +- .../Tensors/RealTensor/CoVector/Basic.lean | 220 +------------- .../RealTensor/CoVector/Tensorial.lean | 242 +++++++++++++++ .../Tensors/RealTensor/Vector/Basic.lean | 251 +--------------- .../RealTensor/Vector/MinkowskiProduct.lean | 2 +- .../Tensors/RealTensor/Vector/Tensorial.lean | 278 ++++++++++++++++++ Physlib/SpaceAndTime/SpaceTime/Basic.lean | 2 +- .../SpaceAndTime/SpaceTime/Derivatives.lean | 2 +- 9 files changed, 532 insertions(+), 469 deletions(-) create mode 100644 Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean create mode 100644 Physlib/Relativity/Tensors/RealTensor/Vector/Tensorial.lean diff --git a/Physlib.lean b/Physlib.lean index 580bb2490..dddf9bd98 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -325,6 +325,7 @@ public import Physlib.Relativity.Tensors.OfInt public import Physlib.Relativity.Tensors.Product public import Physlib.Relativity.Tensors.RealTensor.Basic public import Physlib.Relativity.Tensors.RealTensor.CoVector.Basic +public import Physlib.Relativity.Tensors.RealTensor.CoVector.Tensorial public import Physlib.Relativity.Tensors.RealTensor.Derivative public import Physlib.Relativity.Tensors.RealTensor.Matrix.Pre public import Physlib.Relativity.Tensors.RealTensor.Metrics.Basic @@ -339,6 +340,7 @@ public import Physlib.Relativity.Tensors.RealTensor.Vector.MinkowskiProduct public import Physlib.Relativity.Tensors.RealTensor.Vector.Pre.Basic public import Physlib.Relativity.Tensors.RealTensor.Vector.Pre.Contraction public import Physlib.Relativity.Tensors.RealTensor.Vector.Pre.Modules +public import Physlib.Relativity.Tensors.RealTensor.Vector.Tensorial public import Physlib.Relativity.Tensors.RealTensor.Velocity.Basic public import Physlib.Relativity.Tensors.TensorSpecies.Basic public import Physlib.Relativity.Tensors.Tensorial diff --git a/Physlib/Relativity/LorentzGroup/Boosts/Apply.lean b/Physlib/Relativity/LorentzGroup/Boosts/Apply.lean index f045af86d..9f7ff3a9e 100644 --- a/Physlib/Relativity/LorentzGroup/Boosts/Apply.lean +++ b/Physlib/Relativity/LorentzGroup/Boosts/Apply.lean @@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith module public import Physlib.Relativity.LorentzGroup.Boosts.Basic -public import Physlib.Relativity.Tensors.RealTensor.Vector.Basic +public import Physlib.Relativity.Tensors.RealTensor.Vector.Tensorial /-! ## Boosts applied to Lorentz vectors diff --git a/Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean index a2fcede80..060da3398 100644 --- a/Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean +++ b/Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean @@ -5,8 +5,7 @@ Authors: Matteo Cipollina, Joseph Tooby-Smith -/ module -public import Physlib.Relativity.Tensors.Tensorial -public import Physlib.Relativity.Tensors.RealTensor.Basic +public import Mathlib.Analysis.InnerProductSpace.PiL2 public import Mathlib.Geometry.Manifold.ChartedSpace /-! @@ -18,28 +17,20 @@ We create an API around Lorentz vectors to make working with them as easy as pos -/ @[expose] public section -open Module IndexNotation -open CategoryTheory -open MonoidalCategory +open Module open Matrix open MatrixGroups open Complex open TensorProduct -open IndexNotation -open CategoryTheory noncomputable section namespace Lorentz -open realLorentzTensor /-- Real contravariant Lorentz vector. -/ def CoVector (d : ℕ := 3) := Fin 1 ⊕ Fin d → ℝ namespace CoVector -open TensorSpecies -open Tensor - instance {d} : AddCommMonoid (CoVector d) := inferInstanceAs (AddCommMonoid (Fin 1 ⊕ Fin d → ℝ)) @@ -134,58 +125,6 @@ lemma neg_apply {d : ℕ} (v : CoVector d) (i : Fin 1 ⊕ Fin d) : @[simp] lemma zero_apply {d : ℕ} (i : Fin 1 ⊕ Fin d) : (0 : CoVector d) i = 0 := rfl -/-! - -## Tensorial - --/ - -/-- The equivalence between the type of indices of a Lorentz vector and - `Fin 1 ⊕ Fin d`. -/ -def indexEquiv {d : ℕ} : - ComponentIdx (S := (realLorentzTensor d)) ![Color.down] ≃ Fin 1 ⊕ Fin d := - let e : (ComponentIdx (S := (realLorentzTensor d)) ![Color.down]) - ≃ Fin (1 + d) := { - toFun := fun f => Fin.cast (by rfl) (f 0) - invFun := fun x => (fun j => Fin.cast (by simp) x) - left_inv := fun f => by - ext j - fin_cases j - simp - right_inv := fun x => by rfl} - e.trans finSumFinEquiv.symm - -instance tensorial {d : ℕ} : Tensorial (realLorentzTensor d) ![.down] (CoVector d) where - toTensor := LinearEquiv.symm <| - Equiv.toLinearEquiv - ((Tensor.basis (S := (realLorentzTensor d)) ![.down]).repr.toEquiv.trans <| - Finsupp.equivFunOnFinite.trans <| - (Equiv.piCongrLeft' _ indexEquiv)) - { map_add := fun x y => by - simp [Nat.succ_eq_add_one, Nat.reduceAdd, map_add] - rfl - map_smul := fun c x => by - simp [Nat.succ_eq_add_one, Nat.reduceAdd, _root_.map_smul] - rfl} - -open Tensorial - -lemma toTensor_symm_apply {d : ℕ} (p : ℝT[d, .down]) : - (toTensor (self := tensorial)).symm p = - (Equiv.piCongrLeft' _ indexEquiv <| - Finsupp.equivFunOnFinite <| - (Tensor.basis (S := (realLorentzTensor d)) _).repr p) := rfl - -lemma toTensor_symm_pure {d : ℕ} (p : Pure (realLorentzTensor d) ![.down]) (i : Fin 1 ⊕ Fin d) : - (toTensor (self := tensorial)).symm p.toTensor i = - ((Lorentz.coBasisFin d).repr (p 0)) (indexEquiv.symm i 0) := by - rw [toTensor_symm_apply] - simp only [Nat.succ_eq_add_one, Nat.reduceAdd, - Equiv.piCongrLeft'_apply, Finsupp.equivFunOnFinite_apply, Fin.isValue] - rw [Tensor.basis_repr_pure] - simp only [Pure.component, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, - Finset.prod_singleton, cons_val_zero] - rfl /-! @@ -205,56 +144,6 @@ lemma basis_apply {d : ℕ} (μ ν : Fin 1 ⊕ Fin d) : congr 1 exact Lean.Grind.eq_congr' rfl rfl -set_option backward.isDefEq.respectTransparency false in -lemma toTensor_symm_basis {d : ℕ} (μ : Fin 1 ⊕ Fin d) : - (toTensor (self := tensorial)).symm (Tensor.basis ![Color.down] (indexEquiv.symm μ)) = - basis μ := by - rw [Tensor.basis_apply] - funext i - rw [toTensor_symm_pure] - simp [coBasisFin, Pure.basisVector] - conv_lhs => - enter [1, 2] - change (coBasisFin d) (indexEquiv.symm μ 0) - simp [coBasisFin, indexEquiv, Finsupp.single_apply] - -lemma toTensor_basis_eq_tensor_basis {d : ℕ} (μ : Fin 1 ⊕ Fin d) : - toTensor (basis μ) = Tensor.basis ![Color.down] (indexEquiv.symm μ) := by - rw [← toTensor_symm_basis] - simp - -lemma basis_eq_map_tensor_basis {d} : basis = - ((Tensor.basis (S := realLorentzTensor d) ![Color.down]).map - toTensor.symm).reindex indexEquiv := by - ext μ - rw [← toTensor_symm_basis] - simp - -lemma tensor_basis_map_eq_basis_reindex {d} : - (Tensor.basis (S := realLorentzTensor d) ![Color.down]).map toTensor.symm = - basis.reindex indexEquiv.symm := by - rw [basis_eq_map_tensor_basis] - ext μ - simp - -lemma tensor_basis_repr_toTensor_apply {d : ℕ} (p : CoVector d) (μ : ComponentIdx ![Color.down]) : - (Tensor.basis ![Color.down]).repr (toTensor p) μ = - p (indexEquiv μ) := by - obtain ⟨p, rfl⟩ := toTensor.symm.surjective p - simp only [Nat.succ_eq_add_one, Nat.reduceAdd, LinearEquiv.apply_symm_apply] - apply induction_on_pure (t := p) - · intro p - rw [Tensor.basis_repr_pure] - simp only [Pure.component, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, - Finset.prod_singleton, cons_val_zero, Nat.succ_eq_add_one, Nat.reduceAdd] - rw [toTensor_symm_pure] - simp - rfl - · intro r t h - simp [h] - · intro t1 t2 h1 h2 - simp [h1, h2] - lemma basis_repr_apply {d : ℕ} (p : CoVector d) (μ : Fin 1 ⊕ Fin d) : basis.repr p μ = p μ := by simp [basis] @@ -264,111 +153,6 @@ lemma map_apply_eq_basis_mulVec {d : ℕ} (f : CoVector d →ₗ[ℝ] CoVector d (f p) = (LinearMap.toMatrix basis basis) f *ᵥ p := by exact Eq.symm (LinearMap.toMatrix_mulVec_repr basis basis f p) -/-! - -## The action of the Lorentz group - --/ - -set_option backward.isDefEq.respectTransparency false in -lemma smul_eq_sum {d : ℕ} (i : Fin 1 ⊕ Fin d) (Λ : LorentzGroup d) (p : CoVector d) : - (Λ • p) i = ∑ j, Λ⁻¹.1 j i * p j := by - obtain ⟨p, rfl⟩ := toTensor.symm.surjective p - rw [smul_toTensor_symm] - apply induction_on_pure (t := p) - · intro p - rw [actionT_pure] - rw [toTensor_symm_pure] - conv_lhs => - enter [1, 2] - change (LorentzGroup.transpose Λ⁻¹) *ᵥ (p 0) - rw [coBasisFin_repr_apply] - conv_lhs => simp [indexEquiv] - - rw [mulVec_eq_sum] - simp only [Finset.sum_apply] - congr - funext j - simp [Fin.isValue, Pi.smul_apply, transpose_apply, MulOpposite.smul_eq_mul_unop, - MulOpposite.unop_op, Nat.succ_eq_add_one, Nat.reduceAdd] - congr - rw [toTensor_symm_pure, coBasisFin_repr_apply] - congr - simp [indexEquiv] - · intro r t h - simp only [actionT_smul, _root_.map_smul] - change r * toTensor (self := tensorial).symm (Λ • t) i = _ - rw [h] - rw [Finset.mul_sum] - congr - funext x - simp only [Nat.succ_eq_add_one, Nat.reduceAdd, apply_smul] - ring - · intro t1 t2 h1 h2 - simp only [actionT_add, map_add, h1, h2, apply_add] - rw [← Finset.sum_add_distrib] - congr - funext x - ring - -lemma smul_eq_mulVec {d} (Λ : LorentzGroup d) (p : CoVector d) : - Λ • p = (LorentzGroup.transpose Λ⁻¹).1 *ᵥ p := by - funext i - rw [smul_eq_sum, mulVec_eq_sum] - simp only [op_smul_eq_smul, Finset.sum_apply, Pi.smul_apply, transpose_apply, smul_eq_mul, - mul_comm] - rfl - -lemma smul_add {d : ℕ} (Λ : LorentzGroup d) (p q : CoVector d) : - Λ • (p + q) = Λ • p + Λ • q := by simp - -set_option backward.isDefEq.respectTransparency false in -@[simp] -lemma smul_sub {d : ℕ} (Λ : LorentzGroup d) (p q : CoVector d) : - Λ • (p - q) = Λ • p - Λ • q := by - rw [smul_eq_mulVec, smul_eq_mulVec, smul_eq_mulVec, Matrix.mulVec_sub] - -set_option backward.isDefEq.respectTransparency false in -lemma smul_zero {d : ℕ} (Λ : LorentzGroup d) : - Λ • (0 : CoVector d) = 0 := by - rw [smul_eq_mulVec, Matrix.mulVec_zero] - -set_option backward.isDefEq.respectTransparency false in -lemma smul_neg {d : ℕ} (Λ : LorentzGroup d) (p : CoVector d) : - Λ • (-p) = - (Λ • p) := by - rw [smul_eq_mulVec, smul_eq_mulVec, Matrix.mulVec_neg] - -/-- The Lorentz action on vectors as a continuous linear map. -/ -def actionCLM {d : ℕ} (Λ : LorentzGroup d) : - CoVector d →L[ℝ] CoVector d := - LinearMap.toContinuousLinearMap - { toFun := fun v => Λ • v - map_add' := smul_add Λ - map_smul' := fun c v => by - simp only [RingHom.id_apply] - funext i - simp [smul_eq_sum] - ring_nf - congr - rw [Finset.mul_sum] - congr - funext j - ring} - -lemma actionCLM_apply {d : ℕ} (Λ : LorentzGroup d) (p : CoVector d) : - actionCLM Λ p = Λ • p := rfl - -set_option backward.isDefEq.respectTransparency false in -lemma smul_basis {d : ℕ} (Λ : LorentzGroup d) (μ : Fin 1 ⊕ Fin d) : - Λ • basis μ = ∑ ν, Λ⁻¹.1 μ ν • basis ν := by - funext i - rw [smul_eq_sum] - simp only [basis_apply, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq, Finset.mem_univ, - ↓reduceIte] - trans ∑ ν, ((Λ⁻¹.1 μ ν • basis ν) i) - · simp - rw [Fintype.sum_apply] - end CoVector end Lorentz diff --git a/Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean b/Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean new file mode 100644 index 000000000..4242c53ec --- /dev/null +++ b/Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean @@ -0,0 +1,242 @@ +/- +Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Tooby-Smith +-/ +module + +public import Physlib.Relativity.Tensors.RealTensor.Basic +public import Physlib.Relativity.Tensors.RealTensor.CoVector.Basic +public import Physlib.Relativity.Tensors.Tensorial +/-! + +# Tensorial nature Lorentz CoVectors + +The instance of a tensor on Lorentz covectors, and +the consequence of results thereof. + +-/ +@[expose] public section + +open Module Matrix + +noncomputable section + +namespace Lorentz.CoVector +open realLorentzTensor TensorSpecies Tensor + +/-! + +## Tensorial + +-/ + +/-- The equivalence between the type of indices of a Lorentz vector and + `Fin 1 ⊕ Fin d`. -/ +def indexEquiv {d : ℕ} : + ComponentIdx (S := (realLorentzTensor d)) ![Color.down] ≃ Fin 1 ⊕ Fin d := + let e : (ComponentIdx (S := (realLorentzTensor d)) ![Color.down]) + ≃ Fin (1 + d) := { + toFun := fun f => Fin.cast (by rfl) (f 0) + invFun := fun x => (fun j => Fin.cast (by simp) x) + left_inv := fun f => by + ext j + fin_cases j + simp + right_inv := fun x => by rfl} + e.trans finSumFinEquiv.symm + +instance tensorial {d : ℕ} : Tensorial (realLorentzTensor d) ![.down] (CoVector d) where + toTensor := LinearEquiv.symm <| + Equiv.toLinearEquiv + ((Tensor.basis (S := (realLorentzTensor d)) ![.down]).repr.toEquiv.trans <| + Finsupp.equivFunOnFinite.trans <| + (Equiv.piCongrLeft' _ indexEquiv)) + { map_add := fun x y => by + simp [Nat.succ_eq_add_one, Nat.reduceAdd, map_add] + rfl + map_smul := fun c x => by + simp [Nat.succ_eq_add_one, Nat.reduceAdd, _root_.map_smul] + rfl} + +open Tensorial + +lemma toTensor_symm_apply {d : ℕ} (p : ℝT[d, .down]) : + (toTensor (self := tensorial)).symm p = + (Equiv.piCongrLeft' _ indexEquiv <| + Finsupp.equivFunOnFinite <| + (Tensor.basis (S := (realLorentzTensor d)) _).repr p) := rfl + +lemma toTensor_symm_pure {d : ℕ} (p : Pure (realLorentzTensor d) ![.down]) (i : Fin 1 ⊕ Fin d) : + (toTensor (self := tensorial)).symm p.toTensor i = + ((Lorentz.coBasisFin d).repr (p 0)) (indexEquiv.symm i 0) := by + rw [toTensor_symm_apply] + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, + Equiv.piCongrLeft'_apply, Finsupp.equivFunOnFinite_apply, Fin.isValue] + rw [Tensor.basis_repr_pure] + simp only [Pure.component, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, + Finset.prod_singleton, cons_val_zero] + rfl + +/-! + +## Poperties of the basis. + +-/ + +set_option backward.isDefEq.respectTransparency false in +lemma toTensor_symm_basis {d : ℕ} (μ : Fin 1 ⊕ Fin d) : + (toTensor (self := tensorial)).symm (Tensor.basis ![Color.down] (indexEquiv.symm μ)) = + basis μ := by + rw [Tensor.basis_apply] + funext i + rw [toTensor_symm_pure] + simp [coBasisFin, Pure.basisVector] + conv_lhs => + enter [1, 2] + change (coBasisFin d) (indexEquiv.symm μ 0) + simp [coBasisFin, indexEquiv, Finsupp.single_apply] + +lemma toTensor_basis_eq_tensor_basis {d : ℕ} (μ : Fin 1 ⊕ Fin d) : + toTensor (basis μ) = Tensor.basis ![Color.down] (indexEquiv.symm μ) := by + rw [← toTensor_symm_basis] + simp + +lemma basis_eq_map_tensor_basis {d} : basis = + ((Tensor.basis (S := realLorentzTensor d) ![Color.down]).map + toTensor.symm).reindex indexEquiv := by + ext μ + rw [← toTensor_symm_basis] + simp + +lemma tensor_basis_map_eq_basis_reindex {d} : + (Tensor.basis (S := realLorentzTensor d) ![Color.down]).map toTensor.symm = + basis.reindex indexEquiv.symm := by + rw [basis_eq_map_tensor_basis] + ext μ + simp + +lemma tensor_basis_repr_toTensor_apply {d : ℕ} (p : CoVector d) (μ : ComponentIdx ![Color.down]) : + (Tensor.basis ![Color.down]).repr (toTensor p) μ = + p (indexEquiv μ) := by + obtain ⟨p, rfl⟩ := toTensor.symm.surjective p + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, LinearEquiv.apply_symm_apply] + apply induction_on_pure (t := p) + · intro p + rw [Tensor.basis_repr_pure] + simp only [Pure.component, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, + Finset.prod_singleton, cons_val_zero, Nat.succ_eq_add_one, Nat.reduceAdd] + rw [toTensor_symm_pure] + simp + rfl + · intro r t h + simp [h] + · intro t1 t2 h1 h2 + simp [h1, h2] + +/-! + +## The action of the Lorentz group + +-/ + +set_option backward.isDefEq.respectTransparency false in +lemma smul_eq_sum {d : ℕ} (i : Fin 1 ⊕ Fin d) (Λ : LorentzGroup d) (p : CoVector d) : + (Λ • p) i = ∑ j, Λ⁻¹.1 j i * p j := by + obtain ⟨p, rfl⟩ := toTensor.symm.surjective p + rw [smul_toTensor_symm] + apply induction_on_pure (t := p) + · intro p + rw [actionT_pure] + rw [toTensor_symm_pure] + conv_lhs => + enter [1, 2] + change (LorentzGroup.transpose Λ⁻¹) *ᵥ (p 0) + rw [coBasisFin_repr_apply] + conv_lhs => simp [indexEquiv] + + rw [mulVec_eq_sum] + simp only [Finset.sum_apply] + congr + funext j + simp [Fin.isValue, Pi.smul_apply, transpose_apply, MulOpposite.smul_eq_mul_unop, + MulOpposite.unop_op, Nat.succ_eq_add_one, Nat.reduceAdd] + congr + rw [toTensor_symm_pure, coBasisFin_repr_apply] + congr + simp [indexEquiv] + · intro r t h + simp only [actionT_smul, _root_.map_smul] + change r * toTensor (self := tensorial).symm (Λ • t) i = _ + rw [h] + rw [Finset.mul_sum] + congr + funext x + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, apply_smul] + ring + · intro t1 t2 h1 h2 + simp only [actionT_add, map_add, h1, h2, apply_add] + rw [← Finset.sum_add_distrib] + congr + funext x + ring + +lemma smul_eq_mulVec {d} (Λ : LorentzGroup d) (p : CoVector d) : + Λ • p = (LorentzGroup.transpose Λ⁻¹).1 *ᵥ p := by + funext i + rw [smul_eq_sum, mulVec_eq_sum] + simp only [op_smul_eq_smul, Finset.sum_apply, Pi.smul_apply, transpose_apply, smul_eq_mul, + mul_comm] + rfl + +lemma smul_add {d : ℕ} (Λ : LorentzGroup d) (p q : CoVector d) : + Λ • (p + q) = Λ • p + Λ • q := by simp + +set_option backward.isDefEq.respectTransparency false in +@[simp] +lemma smul_sub {d : ℕ} (Λ : LorentzGroup d) (p q : CoVector d) : + Λ • (p - q) = Λ • p - Λ • q := by + rw [smul_eq_mulVec, smul_eq_mulVec, smul_eq_mulVec, Matrix.mulVec_sub] + +set_option backward.isDefEq.respectTransparency false in +lemma smul_zero {d : ℕ} (Λ : LorentzGroup d) : + Λ • (0 : CoVector d) = 0 := by + rw [smul_eq_mulVec, Matrix.mulVec_zero] + +set_option backward.isDefEq.respectTransparency false in +lemma smul_neg {d : ℕ} (Λ : LorentzGroup d) (p : CoVector d) : + Λ • (-p) = - (Λ • p) := by + rw [smul_eq_mulVec, smul_eq_mulVec, Matrix.mulVec_neg] + +/-- The Lorentz action on vectors as a continuous linear map. -/ +def actionCLM {d : ℕ} (Λ : LorentzGroup d) : + CoVector d →L[ℝ] CoVector d := + LinearMap.toContinuousLinearMap + { toFun := fun v => Λ • v + map_add' := smul_add Λ + map_smul' := fun c v => by + simp only [RingHom.id_apply] + funext i + simp [smul_eq_sum] + ring_nf + congr + rw [Finset.mul_sum] + congr + funext j + ring} + +lemma actionCLM_apply {d : ℕ} (Λ : LorentzGroup d) (p : CoVector d) : + actionCLM Λ p = Λ • p := rfl + +set_option backward.isDefEq.respectTransparency false in +lemma smul_basis {d : ℕ} (Λ : LorentzGroup d) (μ : Fin 1 ⊕ Fin d) : + Λ • basis μ = ∑ ν, Λ⁻¹.1 μ ν • basis ν := by + funext i + rw [smul_eq_sum] + simp only [basis_apply, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq, Finset.mem_univ, + ↓reduceIte] + trans ∑ ν, ((Λ⁻¹.1 μ ν • basis ν) i) + · simp + rw [Fintype.sum_apply] + +end Lorentz.CoVector diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean index 52e7b1c20..4f08d320d 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean +++ b/Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean @@ -5,9 +5,9 @@ Authors: Matteo Cipollina, Joseph Tooby-Smith -/ module +public import Mathlib.Algebra.Lie.OfAssociative +public import Mathlib.Analysis.InnerProductSpace.PiL2 public import Mathlib.Geometry.Manifold.IsManifold.Basic -public import Physlib.Relativity.Tensors.RealTensor.Basic -public import Physlib.Relativity.Tensors.Tensorial /-! # Lorentz Vectors @@ -18,27 +18,21 @@ We create an API around Lorentz vectors to make working with them as easy as pos -/ @[expose] public section -open Module IndexNotation -open CategoryTheory -open MonoidalCategory +open Module open Matrix open MatrixGroups open Complex open TensorProduct -open IndexNotation -open CategoryTheory + noncomputable section namespace Lorentz -open realLorentzTensor /-- Real contravariant Lorentz vector. -/ def Vector (d : ℕ := 3) := Fin 1 ⊕ Fin d → ℝ namespace Vector -open TensorSpecies -open Tensor instance {d} : AddCommMonoid (Vector d) := inferInstanceAs (AddCommMonoid (Fin 1 ⊕ Fin d → ℝ)) @@ -267,59 +261,6 @@ lemma fderiv_coord {d : ℕ} (μ : Fin 1 ⊕ Fin d) (x : Vector d) : /-! -## Tensorial - --/ - -/-- The equivalence between the type of indices of a Lorentz vector and - `Fin 1 ⊕ Fin d`. -/ -def indexEquiv {d : ℕ} : - ComponentIdx (S := (realLorentzTensor d)) ![Color.up] ≃ Fin 1 ⊕ Fin d := - let e : (ComponentIdx (S := (realLorentzTensor d)) ![Color.up]) - ≃ Fin (1 + d) := { - toFun := fun f => Fin.cast (by rfl) (f 0) - invFun := fun x => (fun j => Fin.cast (by simp) x) - left_inv := fun f => by - ext j - fin_cases j - simp - right_inv := fun x => by rfl} - e.trans finSumFinEquiv.symm - -instance tensorial {d : ℕ} : Tensorial (realLorentzTensor d) ![.up] (Vector d) where - toTensor := LinearEquiv.symm <| - Equiv.toLinearEquiv - ((Tensor.basis (S := (realLorentzTensor d)) ![.up]).repr.toEquiv.trans <| - Finsupp.equivFunOnFinite.trans <| - (Equiv.piCongrLeft' _ indexEquiv)) - { map_add := fun x y => by - simp [Nat.succ_eq_add_one, Nat.reduceAdd, map_add] - rfl - map_smul := fun c x => by - simp [Nat.succ_eq_add_one, Nat.reduceAdd, _root_.map_smul] - rfl} - -open Tensorial - -lemma toTensor_symm_apply {d : ℕ} (p : ℝT[d, .up]) : - (toTensor (self := tensorial)).symm p = - (Equiv.piCongrLeft' _ indexEquiv <| - Finsupp.equivFunOnFinite <| - (Tensor.basis (S := (realLorentzTensor d)) _).repr p) := rfl - -lemma toTensor_symm_pure {d : ℕ} (p : Pure (realLorentzTensor d) ![.up]) (i : Fin 1 ⊕ Fin d) : - (toTensor (self := tensorial)).symm p.toTensor i = - ((Lorentz.contrBasisFin d).repr (p 0)) (indexEquiv.symm i 0) := by - rw [toTensor_symm_apply] - simp only [Nat.succ_eq_add_one, Nat.reduceAdd, - Equiv.piCongrLeft'_apply, Finsupp.equivFunOnFinite_apply, Fin.isValue] - rw [Tensor.basis_repr_pure] - simp only [Pure.component, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, - Finset.prod_singleton, cons_val_zero] - rfl - -/-! - ## Basis -/ @@ -336,56 +277,6 @@ lemma basis_apply {d : ℕ} (μ ν : Fin 1 ⊕ Fin d) : congr 1 exact Lean.Grind.eq_congr' rfl rfl -set_option backward.isDefEq.respectTransparency false in -lemma toTensor_symm_basis {d : ℕ} (μ : Fin 1 ⊕ Fin d) : - (toTensor (self := tensorial)).symm (Tensor.basis ![Color.up] (indexEquiv.symm μ)) = - basis μ := by - rw [Tensor.basis_apply] - funext i - rw [toTensor_symm_pure] - simp [contrBasisFin, Pure.basisVector] - conv_lhs => - enter [1, 2] - change (contrBasisFin d) (indexEquiv.symm μ 0) - simp [contrBasisFin, indexEquiv, Finsupp.single_apply] - -lemma toTensor_basis_eq_tensor_basis {d : ℕ} (μ : Fin 1 ⊕ Fin d) : - toTensor (basis μ) = Tensor.basis ![Color.up] (indexEquiv.symm μ) := by - rw [← toTensor_symm_basis] - simp - -lemma basis_eq_map_tensor_basis {d} : basis = - ((Tensor.basis - (S := realLorentzTensor d) ![Color.up]).map toTensor.symm).reindex indexEquiv := by - ext μ - rw [← toTensor_symm_basis] - simp - -lemma tensor_basis_map_eq_basis_reindex {d} : - (Tensor.basis (S := realLorentzTensor d) ![Color.up]).map toTensor.symm = - basis.reindex indexEquiv.symm := by - rw [basis_eq_map_tensor_basis] - ext μ - simp - -lemma tensor_basis_repr_toTensor_apply {d : ℕ} (p : Vector d) (μ : ComponentIdx ![Color.up]) : - (Tensor.basis ![Color.up]).repr (toTensor p) μ = - p (indexEquiv μ) := by - obtain ⟨p, rfl⟩ := toTensor.symm.surjective p - simp only [Nat.succ_eq_add_one, Nat.reduceAdd, LinearEquiv.apply_symm_apply] - apply induction_on_pure (t := p) - · intro p - rw [Tensor.basis_repr_pure] - simp only [Pure.component, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, - Finset.prod_singleton, cons_val_zero, Nat.succ_eq_add_one, Nat.reduceAdd] - rw [toTensor_symm_pure] - simp - rfl - · intro r t h - simp [h] - · intro t1 t2 h1 h2 - simp [h1, h2] - lemma basis_repr_apply {d : ℕ} (p : Vector d) (μ : Fin 1 ⊕ Fin d) : basis.repr p μ = p μ := by simp [basis] @@ -419,140 +310,6 @@ lemma sum_inl_inr_basis_eq_zero_iff {d : ℕ} (f₀ : ℝ) (f : Fin d → ℝ) : /-! -## The action of the Lorentz group - --/ - -set_option backward.isDefEq.respectTransparency false in -lemma smul_eq_sum {d : ℕ} (i : Fin 1 ⊕ Fin d) (Λ : LorentzGroup d) (p : Vector d) : - (Λ • p) i = ∑ j, Λ.1 i j * p j := by - obtain ⟨p, rfl⟩ := toTensor.symm.surjective p - rw [smul_toTensor_symm] - apply induction_on_pure (t := p) - · intro p - rw [actionT_pure] - rw [toTensor_symm_pure] - conv_lhs => - enter [1, 2] - change Λ.1 *ᵥ (p 0) - rw [contrBasisFin_repr_apply] - conv_lhs => simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, indexEquiv, - cons_val_zero, Fin.cast_eq_self, Equiv.symm_trans_apply, Equiv.symm_symm, - Equiv.coe_fn_symm_mk, Equiv.symm_apply_apply, ContrMod.mulVec_val] - rw [mulVec_eq_sum] - simp only [Finset.sum_apply] - congr - funext j - simp only [Fin.isValue, Pi.smul_apply, transpose_apply, MulOpposite.smul_eq_mul_unop, - MulOpposite.unop_op, Nat.succ_eq_add_one, Nat.reduceAdd, mul_eq_mul_left_iff] - left - rw [toTensor_symm_pure, contrBasisFin_repr_apply] - congr - simp [indexEquiv] - · intro r t h - simp only [actionT_smul, _root_.map_smul] - change r * toTensor (self := tensorial).symm (Λ • t) i = _ - rw [h] - rw [Finset.mul_sum] - congr - funext x - simp only [Nat.succ_eq_add_one, Nat.reduceAdd, apply_smul] - ring - · intro t1 t2 h1 h2 - simp only [actionT_add, map_add, h1, h2, apply_add] - rw [← Finset.sum_add_distrib] - congr - funext x - ring - -lemma smul_eq_mulVec {d} (Λ : LorentzGroup d) (p : Vector d) : - Λ • p = Λ.1 *ᵥ p := by - funext i - rw [smul_eq_sum, mulVec_eq_sum] - simp only [op_smul_eq_smul, Finset.sum_apply, Pi.smul_apply, transpose_apply, smul_eq_mul, - mul_comm] - -lemma smul_add {d : ℕ} (Λ : LorentzGroup d) (p q : Vector d) : - Λ • (p + q) = Λ • p + Λ • q := by simp - -set_option backward.isDefEq.respectTransparency false in -@[simp] -lemma smul_sub {d : ℕ} (Λ : LorentzGroup d) (p q : Vector d) : - Λ • (p - q) = Λ • p - Λ • q := by - rw [smul_eq_mulVec, smul_eq_mulVec, smul_eq_mulVec, Matrix.mulVec_sub] - -set_option backward.isDefEq.respectTransparency false in -lemma smul_zero {d : ℕ} (Λ : LorentzGroup d) : - Λ • (0 : Vector d) = 0 := by - rw [smul_eq_mulVec, Matrix.mulVec_zero] - -set_option backward.isDefEq.respectTransparency false in -lemma smul_neg {d : ℕ} (Λ : LorentzGroup d) (p : Vector d) : - Λ • (-p) = - (Λ • p) := by - rw [smul_eq_mulVec, smul_eq_mulVec, Matrix.mulVec_neg] - -lemma neg_smul {d} (Λ : LorentzGroup d) (p : Vector d) : - (-Λ) • p = - (Λ • p) := by - funext i - rw [smul_eq_sum, neg_apply, smul_eq_sum] - simp - -lemma _root_.LorentzGroup.eq_of_action_vector_eq {d : ℕ} - {Λ Λ' : LorentzGroup d} (h : ∀ p : Vector d, Λ • p = Λ' • p) : - Λ = Λ' := by - apply LorentzGroup.eq_of_mulVec_eq - simpa only [smul_eq_mulVec] using fun x => h x - -/-! - -## B. The continuous action of the Lorentz group - --/ - -/-- The Lorentz action on vectors as a continuous linear map. -/ -def actionCLM {d : ℕ} (Λ : LorentzGroup d) : - Vector d →L[ℝ] Vector d := - LinearMap.toContinuousLinearMap - { toFun := fun v => Λ • v - map_add' := smul_add Λ - map_smul' := fun c v => by - simp only [RingHom.id_apply] - funext i - simp [smul_eq_sum] - ring_nf - congr - rw [Finset.mul_sum] - congr - funext j - ring} - -lemma actionCLM_apply {d : ℕ} (Λ : LorentzGroup d) (p : Vector d) : - actionCLM Λ p = Λ • p := rfl - -lemma actionCLM_injective {d : ℕ} (Λ : LorentzGroup d) : - Function.Injective (actionCLM Λ) := by - intro x1 x2 - simp [actionCLM_apply] - -lemma actionCLM_surjective {d : ℕ} (Λ : LorentzGroup d) : - Function.Surjective (actionCLM Λ) := by - intro x1 - use (actionCLM Λ⁻¹) x1 - simp [actionCLM_apply] - -set_option backward.isDefEq.respectTransparency false in -lemma smul_basis {d : ℕ} (Λ : LorentzGroup d) (μ : Fin 1 ⊕ Fin d) : - Λ • basis μ = ∑ ν, Λ.1 ν μ • basis ν := by - funext i - rw [smul_eq_sum] - simp only [basis_apply, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq, Finset.mem_univ, - ↓reduceIte] - trans ∑ ν, ((Λ.1 ν μ • basis ν) i) - · simp - rw [Fintype.sum_apply] - -/-! - ## C. The Spatial part -/ diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/MinkowskiProduct.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/MinkowskiProduct.lean index 57b41f69e..b3c472929 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Vector/MinkowskiProduct.lean +++ b/Physlib/Relativity/Tensors/RealTensor/Vector/MinkowskiProduct.lean @@ -5,7 +5,7 @@ Authors: Matteo Cipollina, Joseph Tooby-Smith -/ module -public import Physlib.Relativity.Tensors.RealTensor.Vector.Basic +public import Physlib.Relativity.Tensors.RealTensor.Vector.Tensorial public import Physlib.Relativity.Tensors.Elab public import Physlib.Relativity.Tensors.RealTensor.Metrics.Basic /-! diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/Tensorial.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/Tensorial.lean new file mode 100644 index 000000000..a1884a166 --- /dev/null +++ b/Physlib/Relativity/Tensors/RealTensor/Vector/Tensorial.lean @@ -0,0 +1,278 @@ +/- +Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Tooby-Smith +-/ +module + +public import Mathlib.Geometry.Manifold.IsManifold.Basic +public import Physlib.Relativity.Tensors.RealTensor.Vector.Basic +public import Physlib.Relativity.Tensors.Tensorial +public import Physlib.Relativity.Tensors.RealTensor.Basic +/-! + +# Tensorial nature Lorentz Vectors + +The instance of a tensor on Lorentz vectors, and +the consequence of results thereof. + +-/ +@[expose] public section + +open Module Matrix + +noncomputable section + +namespace Lorentz.Vector +open realLorentzTensor + +/-! + +## Tensorial + +-/ +section +open TensorSpecies Tensor + +/-- The equivalence between the type of indices of a Lorentz vector and + `Fin 1 ⊕ Fin d`. -/ +def indexEquiv {d : ℕ} : + ComponentIdx (S := (realLorentzTensor d)) ![Color.up] ≃ Fin 1 ⊕ Fin d := + let e : (ComponentIdx (S := (realLorentzTensor d)) ![Color.up]) + ≃ Fin (1 + d) := { + toFun := fun f => Fin.cast (by rfl) (f 0) + invFun := fun x => (fun j => Fin.cast (by simp) x) + left_inv := fun f => by + ext j + fin_cases j + simp + right_inv := fun x => by rfl} + e.trans finSumFinEquiv.symm + +instance tensorial {d : ℕ} : Tensorial (realLorentzTensor d) ![.up] (Vector d) where + toTensor := LinearEquiv.symm <| + Equiv.toLinearEquiv + ((Tensor.basis (S := (realLorentzTensor d)) ![.up]).repr.toEquiv.trans <| + Finsupp.equivFunOnFinite.trans <| + (Equiv.piCongrLeft' _ indexEquiv)) + { map_add := fun x y => by + simp [Nat.succ_eq_add_one, Nat.reduceAdd, map_add] + rfl + map_smul := fun c x => by + simp [Nat.succ_eq_add_one, Nat.reduceAdd, _root_.map_smul] + rfl} + +open Tensorial + +lemma toTensor_symm_apply {d : ℕ} (p : ℝT[d, .up]) : + (toTensor (self := tensorial)).symm p = + (Equiv.piCongrLeft' _ indexEquiv <| + Finsupp.equivFunOnFinite <| + (Tensor.basis (S := (realLorentzTensor d)) _).repr p) := rfl + +open Tensor in +lemma toTensor_symm_pure {d : ℕ} (p : Pure (realLorentzTensor d) ![.up]) (i : Fin 1 ⊕ Fin d) : + (toTensor (self := tensorial)).symm p.toTensor i = + ((Lorentz.contrBasisFin d).repr (p 0)) (indexEquiv.symm i 0) := by + rw [toTensor_symm_apply] + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, + Equiv.piCongrLeft'_apply, Finsupp.equivFunOnFinite_apply, Fin.isValue] + rw [Tensor.basis_repr_pure] + simp only [Pure.component, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, + Finset.prod_singleton, cons_val_zero] + rfl + +end +/-! + +## Results related to the basis. + +-/ + +open TensorSpecies Tensorial Tensor + +set_option backward.isDefEq.respectTransparency false in +lemma toTensor_symm_basis {d : ℕ} (μ : Fin 1 ⊕ Fin d) : + (toTensor (self := tensorial)).symm (Tensor.basis ![Color.up] (indexEquiv.symm μ)) = + Vector.basis μ := by + rw [Tensor.basis_apply] + funext i + rw [toTensor_symm_pure] + simp [contrBasisFin, Pure.basisVector] + conv_lhs => + enter [1, 2] + change (contrBasisFin d) (indexEquiv.symm μ 0) + simp [contrBasisFin, indexEquiv, Finsupp.single_apply] + +lemma toTensor_basis_eq_tensor_basis {d : ℕ} (μ : Fin 1 ⊕ Fin d) : + toTensor (Vector.basis μ) = Tensor.basis ![Color.up] (indexEquiv.symm μ) := by + rw [← toTensor_symm_basis] + simp + +lemma basis_eq_map_tensor_basis {d} : Vector.basis = + ((Tensor.basis + (S := realLorentzTensor d) ![Color.up]).map toTensor.symm).reindex indexEquiv := by + ext μ + rw [← toTensor_symm_basis] + simp + +lemma tensor_basis_map_eq_basis_reindex {d} : + (Tensor.basis (S := realLorentzTensor d) ![Color.up]).map toTensor.symm = + Vector.basis.reindex indexEquiv.symm := by + rw [basis_eq_map_tensor_basis] + ext μ + simp + +lemma tensor_basis_repr_toTensor_apply {d : ℕ} (p : Vector d) (μ : ComponentIdx ![Color.up]) : + (Tensor.basis ![Color.up]).repr (toTensor p) μ = + p (indexEquiv μ) := by + obtain ⟨p, rfl⟩ := toTensor.symm.surjective p + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, LinearEquiv.apply_symm_apply] + apply induction_on_pure (t := p) + · intro p + rw [Tensor.basis_repr_pure] + simp only [Pure.component, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue, + Finset.prod_singleton, cons_val_zero, Nat.succ_eq_add_one, Nat.reduceAdd] + rw [toTensor_symm_pure] + simp + rfl + · intro r t h + simp [h] + · intro t1 t2 h1 h2 + simp [h1, h2] + +/-! + +## The action of the Lorentz group + +-/ + +set_option backward.isDefEq.respectTransparency false in +lemma smul_eq_sum {d : ℕ} (i : Fin 1 ⊕ Fin d) (Λ : LorentzGroup d) (p : Vector d) : + (Λ • p) i = ∑ j, Λ.1 i j * p j := by + obtain ⟨p, rfl⟩ := toTensor.symm.surjective p + rw [smul_toTensor_symm] + apply induction_on_pure (t := p) + · intro p + rw [actionT_pure] + rw [toTensor_symm_pure] + conv_lhs => + enter [1, 2] + change Λ.1 *ᵥ (p 0) + rw [contrBasisFin_repr_apply] + conv_lhs => simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, indexEquiv, + cons_val_zero, Fin.cast_eq_self, Equiv.symm_trans_apply, Equiv.symm_symm, + Equiv.coe_fn_symm_mk, Equiv.symm_apply_apply, ContrMod.mulVec_val] + rw [mulVec_eq_sum] + simp only [Finset.sum_apply] + congr + funext j + simp only [Fin.isValue, Pi.smul_apply, transpose_apply, MulOpposite.smul_eq_mul_unop, + MulOpposite.unop_op, Nat.succ_eq_add_one, Nat.reduceAdd, mul_eq_mul_left_iff] + left + rw [toTensor_symm_pure, contrBasisFin_repr_apply] + congr + simp [indexEquiv] + · intro r t h + simp only [actionT_smul, _root_.map_smul] + change r * toTensor (self := tensorial).symm (Λ • t) i = _ + rw [h] + rw [Finset.mul_sum] + congr + funext x + simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Vector.apply_smul] + ring + · intro t1 t2 h1 h2 + simp only [actionT_add, map_add, h1, h2, apply_add] + rw [← Finset.sum_add_distrib] + congr + funext x + ring + +lemma smul_eq_mulVec {d} (Λ : LorentzGroup d) (p : Vector d) : + Λ • p = Λ.1 *ᵥ p := by + funext i + rw [smul_eq_sum, mulVec_eq_sum] + simp only [op_smul_eq_smul, Finset.sum_apply, Pi.smul_apply, transpose_apply, smul_eq_mul, + mul_comm] + +lemma smul_add {d : ℕ} (Λ : LorentzGroup d) (p q : Vector d) : + Λ • (p + q) = Λ • p + Λ • q := by simp + +set_option backward.isDefEq.respectTransparency false in +@[simp] +lemma smul_sub {d : ℕ} (Λ : LorentzGroup d) (p q : Vector d) : + Λ • (p - q) = Λ • p - Λ • q := by + rw [smul_eq_mulVec, smul_eq_mulVec, smul_eq_mulVec, Matrix.mulVec_sub] + +set_option backward.isDefEq.respectTransparency false in +lemma smul_zero {d : ℕ} (Λ : LorentzGroup d) : + Λ • (0 : Vector d) = 0 := by + rw [smul_eq_mulVec, Matrix.mulVec_zero] + +set_option backward.isDefEq.respectTransparency false in +lemma smul_neg {d : ℕ} (Λ : LorentzGroup d) (p : Vector d) : + Λ • (-p) = - (Λ • p) := by + rw [smul_eq_mulVec, smul_eq_mulVec, Matrix.mulVec_neg] + +lemma neg_smul {d} (Λ : LorentzGroup d) (p : Vector d) : + (-Λ) • p = - (Λ • p) := by + funext i + rw [smul_eq_sum, neg_apply, smul_eq_sum] + simp + +lemma _root_.LorentzGroup.eq_of_action_vector_eq {d : ℕ} + {Λ Λ' : LorentzGroup d} (h : ∀ p : Vector d, Λ • p = Λ' • p) : + Λ = Λ' := by + apply LorentzGroup.eq_of_mulVec_eq + simpa only [smul_eq_mulVec] using fun x => h x + +/-! + +## B. The continuous action of the Lorentz group + +-/ + +/-- The Lorentz action on vectors as a continuous linear map. -/ +def actionCLM {d : ℕ} (Λ : LorentzGroup d) : + Vector d →L[ℝ] Vector d := + LinearMap.toContinuousLinearMap + { toFun := fun v => Λ • v + map_add' := smul_add Λ + map_smul' := fun c v => by + simp only [RingHom.id_apply] + funext i + simp [smul_eq_sum] + ring_nf + congr + rw [Finset.mul_sum] + congr + funext j + ring} + +lemma actionCLM_apply {d : ℕ} (Λ : LorentzGroup d) (p : Vector d) : + actionCLM Λ p = Λ • p := rfl + +lemma actionCLM_injective {d : ℕ} (Λ : LorentzGroup d) : + Function.Injective (actionCLM Λ) := by + intro x1 x2 + simp [actionCLM_apply] + +lemma actionCLM_surjective {d : ℕ} (Λ : LorentzGroup d) : + Function.Surjective (actionCLM Λ) := by + intro x1 + use (actionCLM Λ⁻¹) x1 + simp [actionCLM_apply] + +set_option backward.isDefEq.respectTransparency false in +lemma smul_basis {d : ℕ} (Λ : LorentzGroup d) (μ : Fin 1 ⊕ Fin d) : + Λ • basis μ = ∑ ν, Λ.1 ν μ • basis ν := by + funext i + rw [smul_eq_sum] + simp only [basis_apply, mul_ite, mul_one, mul_zero, Finset.sum_ite_eq, Finset.mem_univ, + ↓reduceIte] + trans ∑ ν, ((Λ.1 ν μ • basis ν) i) + · simp + rw [Fintype.sum_apply] + +end Lorentz.Vector diff --git a/Physlib/SpaceAndTime/SpaceTime/Basic.lean b/Physlib/SpaceAndTime/SpaceTime/Basic.lean index 57daeea53..ce3070e2b 100644 --- a/Physlib/SpaceAndTime/SpaceTime/Basic.lean +++ b/Physlib/SpaceAndTime/SpaceTime/Basic.lean @@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith module public import Physlib.Relativity.SpeedOfLight -public import Physlib.Relativity.Tensors.RealTensor.Vector.Basic +public import Physlib.Relativity.Tensors.RealTensor.Vector.Tensorial public import Physlib.SpaceAndTime.Space.Integrals.Basic public import Physlib.SpaceAndTime.Time.Basic /-! diff --git a/Physlib/SpaceAndTime/SpaceTime/Derivatives.lean b/Physlib/SpaceAndTime/SpaceTime/Derivatives.lean index 3bc37a82c..0e48a54f2 100644 --- a/Physlib/SpaceAndTime/SpaceTime/Derivatives.lean +++ b/Physlib/SpaceAndTime/SpaceTime/Derivatives.lean @@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith module public import Physlib.SpaceAndTime.SpaceTime.LorentzAction -public import Physlib.Relativity.Tensors.RealTensor.CoVector.Basic +public import Physlib.Relativity.Tensors.RealTensor.CoVector.Tensorial public import Mathlib.Analysis.InnerProductSpace.TensorProduct public import Physlib.SpaceAndTime.Space.Derivatives.Basic public import Physlib.SpaceAndTime.Time.Derivatives From 5fa5d4f79ce9d6bcc918579daa95d4ebfda5bec4 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 21 Apr 2026 10:29:55 +0100 Subject: [PATCH 2/2] Apply suggestion from @jstoobysmith --- Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean b/Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean index 4242c53ec..683247f98 100644 --- a/Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean +++ b/Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean @@ -80,7 +80,7 @@ lemma toTensor_symm_pure {d : ℕ} (p : Pure (realLorentzTensor d) ![.down]) (i /-! -## Poperties of the basis. +## Properties of the basis. -/