From d77a457a857d262ceb0ece12512d4a5a196eacf2 Mon Sep 17 00:00:00 2001 From: Andrea Pari Date: Fri, 2 Oct 2026 12:33:03 +0100 Subject: [PATCH 1/2] feat(Tensors): HasContrDualBases, the dual-basis class, and the component formulas it collapses MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds `TensorSpecies.HasContrDualBases`: at every color some bijection of labels (`IsContrDualMatching`) makes the basis at `S.τ c` dual to the basis at `c` under `S.contr c`. Over a nontrivial ring the bijection is unique (`IsContrDualMatching.unique`), so `contrDualIdxEquiv`, chosen by `Classical.choose`, is identified per species through `contrDualIdxEquiv_eq_of_isContrDualMatching`, and the double-dual law `contrDualIdxEquiv_tau` is a theorem. `contr_tmul_basis_eq_dualBasis` relates the class to `Module.Basis.dualBasis`. `Pure.contrPCoeff_basisVector` and `contrT_basis_repr_apply_eq_sum_dual` give the contraction coefficient and components for any such species. The real and complex Lorentz species instantiate the class, with the identity and `finCongr repDim_tau`, and their `contrPCoeff_basis` and `contrT_basis_repr_apply_eq_fin` now follow from the general lemmas with unchanged statements. Co-authored-by: Claude Opus 5.5 --- Physlib.lean | 1 + .../Tensors/ComplexTensor/Basic.lean | 46 ++--- .../Relativity/Tensors/Contraction/Basis.lean | 28 +++ .../Relativity/Tensors/RealTensor/Basic.lean | 59 +++--- .../Tensors/TensorSpecies/Basic.lean | 7 + .../Tensors/TensorSpecies/DualBasis.lean | 178 ++++++++++++++++++ 6 files changed, 262 insertions(+), 57 deletions(-) create mode 100644 Physlib/Relativity/Tensors/TensorSpecies/DualBasis.lean diff --git a/Physlib.lean b/Physlib.lean index a59270b50d..7a5d514632 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -488,6 +488,7 @@ public import Physlib.Relativity.Tensors.RealTensor.Vector.Tensorial public import Physlib.Relativity.Tensors.RealTensor.Velocity.Basic public import Physlib.Relativity.Tensors.Reindexing public import Physlib.Relativity.Tensors.TensorSpecies.Basic +public import Physlib.Relativity.Tensors.TensorSpecies.DualBasis public import Physlib.Relativity.Tensors.Tensorial public import Physlib.Relativity.Tensors.UnitTensor public import Physlib.SpaceAndTime.GalileanGroup.Basic diff --git a/Physlib/Relativity/Tensors/ComplexTensor/Basic.lean b/Physlib/Relativity/Tensors/ComplexTensor/Basic.lean index 5d798fa1c9..73e23e1bec 100644 --- a/Physlib/Relativity/Tensors/ComplexTensor/Basic.lean +++ b/Physlib/Relativity/Tensors/ComplexTensor/Basic.lean @@ -271,33 +271,37 @@ lemma repDim_tau {c : complexLorentzTensor.Color} : repDim (complexLorentzTensor.τ c) = repDim c := by cases c <;> rfl +/-- A complex Lorentz color and its dual have the same representation dimension (`repDim_tau`), +and the matching `finCongr repDim_tau` satisfies the δ law: it is the basis contraction of each of +the six Weyl and Lorentz pairings. -/ +lemma isContrDualMatching_finCongr (c : complexLorentzTensor.Color) : + IsContrDualMatching complexLorentzTensor c (finCongr repDim_tau) := by + intro x₁ x₂ + cases c <;> refine Eq.trans ?_ (if_congr Fin.ext_iff.symm rfl rfl) + exacts [Fermion.leftDualContraction_basis x₁ x₂, Fermion.dualLeftContraction_basis x₁ x₂, + Fermion.rightDualContraction_basis x₁ x₂, Fermion.dualRightContraction_basis x₁ x₂, + Lorentz.contrCoContraction_basis x₁ x₂, Lorentz.coContrContraction_basis x₁ x₂] + +/-- Complex Lorentz tensors have dual bases under contraction, with the matching +`finCongr repDim_tau`. -/ +instance : HasContrDualBases complexLorentzTensor where + exists_matching c := ⟨_, isContrDualMatching_finCongr c⟩ + +/-- The dual-label matching of complex Lorentz tensors is `finCongr repDim_tau`. -/ +@[simp] +lemma contrDualIdxEquiv_eq_finCongr (c : complexLorentzTensor.Color) : + HasContrDualBases.contrDualIdxEquiv complexLorentzTensor c = finCongr repDim_tau := + HasContrDualBases.contrDualIdxEquiv_eq_of_isContrDualMatching (isContrDualMatching_finCongr c) + lemma contrPCoeff_basis {n : ℕ} {c : Fin n → complexLorentzTensor.Color} (i j : Fin n) (hij : i ≠ j ∧ (complexLorentzTensor.τ (c i) = c j)) (b : ComponentIdx (S := complexLorentzTensor) c) : Pure.contrPCoeff i j hij (Pure.basisVector c b) = if b i = Fin.cast (by simp [← hij.2, repDim_tau]) (b j) then 1 else 0 := by - simp only [Pure.contrPCoeff, Pure.basisVector] - generalize_proofs h1 h2 - generalize b i = b1 at * - generalize b j = b2 at * - generalize c i = ci at * - generalize c j = cj at * - subst h2 - cases ci - all_goals simp only [complexLorentzTensor] - · erw [Fermion.leftDualContraction_basis] - exact if_congr Fin.ext_iff.symm rfl rfl - · erw [Fermion.dualLeftContraction_basis] - exact if_congr Fin.ext_iff.symm rfl rfl - · erw [Fermion.rightDualContraction_basis] - exact if_congr Fin.ext_iff.symm rfl rfl - · erw [Fermion.dualRightContraction_basis] - exact if_congr Fin.ext_iff.symm rfl rfl - · erw [Lorentz.contrCoContraction_basis] - exact if_congr Fin.ext_iff.symm rfl rfl - · erw [Lorentz.coContrContraction_basis] - exact if_congr Fin.ext_iff.symm rfl rfl + rw [Pure.contrPCoeff_basisVector, contrDualIdxEquiv_eq_finCongr] + refine if_congr (Eq.congr_right ?_) rfl rfl + simp [basisIdxCongr_eq_cast] end complexLorentzTensor end diff --git a/Physlib/Relativity/Tensors/Contraction/Basis.lean b/Physlib/Relativity/Tensors/Contraction/Basis.lean index 914a3511af..a637d3b2a6 100644 --- a/Physlib/Relativity/Tensors/Contraction/Basis.lean +++ b/Physlib/Relativity/Tensors/Contraction/Basis.lean @@ -7,6 +7,7 @@ module public import Physlib.Relativity.Tensors.Contraction.Basic public import Physlib.Relativity.Tensors.ComponentIdx.Contraction +public import Physlib.Relativity.Tensors.TensorSpecies.DualBasis /-! # Contractions on basis tensors @@ -36,6 +37,18 @@ lemma Pure.dropPair_basisVector {n : ℕ} {c : Fin (n + 1 + 1) → C} funext l simp [dropPair, basisVector] +/-- For a species with dual bases (`HasContrDualBases`), the contraction coefficient of a basis + vector is the Kronecker δ of its labels at `i` and `j`, the label at `j` read as a label at the + color `c i`. The per-species `contrPCoeff_basis` lemmas follow from it. -/ +lemma Pure.contrPCoeff_basisVector [HasContrDualBases S] {n : ℕ} {c : Fin n → C} (i j : Fin n) + (hij : i ≠ j ∧ S.τ (c i) = c j) (φ : ComponentIdx (S := S) c) : + Pure.contrPCoeff i j hij (Pure.basisVector c φ) = + if φ i = HasContrDualBases.contrDualIdxEquiv S (c i) (basisIdxCongr hij.2.symm (φ j)) then 1 + else 0 := by + simp only [Pure.contrPCoeff, Pure.basisVector] + rw [map_basis_eq] + exact HasContrDualBases.contr_basis_eq_ite (c i) (φ i) _ + attribute [-simp] LinearEquiv.cast_apply lemma contrT_basis_repr_apply {n : ℕ} {c : Fin (n + 1 + 1) → C} {i j : Fin (n + 1 + 1)} (h : i ≠ j ∧ S.τ (c i) = c j) (t : Tensor S c) @@ -87,6 +100,21 @@ lemma contrT_basis_repr_apply_eq_sum_fin {n : ℕ} {c : Fin (n + 1 + 1) → C} { Fintype.sum_prod_type] simp +/-- For a species with dual bases (`HasContrDualBases`), a component of a contraction is a single + sum over the labels at the first contracted index: the δ law + (`HasContrDualBases.contr_basis_eq_ite`) fixes the label at the second. This collapses the double + sum of `contrT_basis_repr_apply_eq_sum_fin`. -/ +lemma contrT_basis_repr_apply_eq_sum_dual [HasContrDualBases S] {n : ℕ} {c : Fin (n + 1 + 1) → C} + {i j : Fin (n + 1 + 1)} (h : i ≠ j ∧ S.τ (c i) = c j) (t : Tensor S c) + (φ : ComponentIdx (c ∘ Fin.succSuccAbove i j)) : + (basis (c ∘ Fin.succSuccAbove i j)).repr (contrT n i j h t) φ = + ∑ x : basisIdx (c i), (basis c).repr t + (DropPairSection.ofFinEquiv h.1 φ + (x, basisIdxCongr h.2 ((HasContrDualBases.contrDualIdxEquiv S (c i)).symm x))).1 := by + rw [contrT_basis_repr_apply_eq_sum_fin] + simp [HasContrDualBases.contr_basis_eq_ite, mul_ite, ← Equiv.symm_apply_eq, + ← basisIdxCongr_symm h.2] + lemma contrT_basis {n : ℕ} {c : Fin (n + 1 + 1) → C} {i j : Fin (n + 1 + 1)} (h : i ≠ j ∧ S.τ (c i) = c j) (b : ComponentIdx (S := S) c) : contrT n i j h (basis c b) = diff --git a/Physlib/Relativity/Tensors/RealTensor/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Basic.lean index c2e4b3095e..397d36d9b1 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Basic.lean +++ b/Physlib/Relativity/Tensors/RealTensor/Basic.lean @@ -164,26 +164,31 @@ lemma τ_down_eq_up {d : ℕ} : (realLorentzTensor d).τ Color.down = Color.up : attribute [-simp] Fintype.sum_sum_type open TensorSpecies Tensor +/-- The basis at every real Lorentz color is indexed by `Fin 1 ⊕ Fin d`, and the identity +matching satisfies the δ law: it is the basis contraction of the two Lorentz pairings. -/ +lemma isContrDualMatching_refl (c : realLorentzTensor.Color) : + IsContrDualMatching (realLorentzTensor d) c (Equiv.refl _) := by + intro x₁ x₂ + cases c + · exact Lorentz.contrCoContract_basis x₁ x₂ + · exact Lorentz.coContrContract_basis x₁ x₂ + +/-- Real Lorentz tensors have dual bases under contraction, with the identity matching. -/ +instance : HasContrDualBases (realLorentzTensor d) where + exists_matching c := ⟨_, isContrDualMatching_refl c⟩ + +/-- The dual-label matching of real Lorentz tensors is the identity. -/ +@[simp] +lemma contrDualIdxEquiv_eq_refl (c : realLorentzTensor.Color) : + HasContrDualBases.contrDualIdxEquiv (realLorentzTensor d) c = Equiv.refl _ := + HasContrDualBases.contrDualIdxEquiv_eq_of_isContrDualMatching (isContrDualMatching_refl c) + lemma contrPCoeff_basis {d n : ℕ} {c : Fin n → realLorentzTensor.Color} (i j : Fin n) (hij : i ≠ j ∧ (realLorentzTensor d).τ (c i) = c j) (b : ComponentIdx (S := realLorentzTensor d) c) : Pure.contrPCoeff i j hij (Pure.basisVector c b) = if b i = b j then 1 else 0 := by - simp only [Pure.contrPCoeff, Pure.basisVector] - generalize_proofs h1 h2 - generalize b i = b1 at * - generalize b j = b2 at * - generalize c i = ci at * - generalize c j = cj at * - subst h2 - fin_cases ci - · simp [realLorentzTensor] - erw [LinearEquiv.cast_apply] - simp only [cast_eq] - erw [Lorentz.contrCoContract_basis] - · simp [realLorentzTensor] - erw [LinearEquiv.cast_apply] - simp only [cast_eq] - erw [Lorentz.coContrContract_basis] + rw [Pure.contrPCoeff_basisVector, contrDualIdxEquiv_eq_refl] + rfl lemma contrT_eq_sum_evalT {n} {d} (c : Fin (n + 1 + 1) → Color) (i j : Fin (n + 1 + 1)) (h : i ≠ j ∧ (realLorentzTensor d).τ (c i) = c j) (t : ℝT(d, c)) : @@ -234,26 +239,8 @@ lemma contrT_basis_repr_apply_eq_fin {n d: ℕ} {c : Fin (n + 1 + 1) → realLor (basis (c ∘ Fin.succSuccAbove i j)).repr (contrT n i j h t) b = ∑ (x : Fin 1 ⊕ Fin d), ((basis c).repr t (DropPairSection.ofFinEquiv h.1 b ⟨x, x⟩)) := by - rw [contrT_basis_repr_apply_eq_sum_fin] - generalize_proofs h h2 h3 - generalize c j = cj at * - generalize c i = ci at * - subst h3 - fin_cases ci - · simp [realLorentzTensor] - congr - funext x - conv_lhs => - enter [2, x]; - erw [Lorentz.contrCoContract_basis] - simp - · simp [realLorentzTensor] - congr - funext x - conv_lhs => - enter [2, x]; - erw [Lorentz.coContrContract_basis] - simp + rw [contrT_basis_repr_apply_eq_sum_dual, contrDualIdxEquiv_eq_refl] + rfl end realLorentzTensor end diff --git a/Physlib/Relativity/Tensors/TensorSpecies/Basic.lean b/Physlib/Relativity/Tensors/TensorSpecies/Basic.lean index 684a4bb09d..0e417bcf11 100644 --- a/Physlib/Relativity/Tensors/TensorSpecies/Basic.lean +++ b/Physlib/Relativity/Tensors/TensorSpecies/Basic.lean @@ -125,6 +125,13 @@ lemma map_basis_eq {c c1 : C} (h : c = c1) (i : basisIdx c) : subst h simp +omit [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] in +/-- `map_basis_eq` with the cast spelled `Equiv.cast`, the form `contr_tmul_symm` applies to its + first vector. -/ +lemma equivCast_basis {c c1 : C} (h : c = c1) (i : basisIdx c) : + Equiv.cast (congrArg V h) (basis c i) = basis c1 (basisIdxCongr h i) := + map_basis_eq h i + set_option linter.unusedVariables false in /-- The number of indices `n` from a tensor. -/ @[nolint unusedArguments] diff --git a/Physlib/Relativity/Tensors/TensorSpecies/DualBasis.lean b/Physlib/Relativity/Tensors/TensorSpecies/DualBasis.lean new file mode 100644 index 0000000000..008d769019 --- /dev/null +++ b/Physlib/Relativity/Tensors/TensorSpecies/DualBasis.lean @@ -0,0 +1,178 @@ +/- +Copyright (c) 2026 Andrea Pari. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Andrea Pari +-/ +module + +public import Physlib.Relativity.Tensors.TensorSpecies.Basic +/-! + +# Species whose bases at dual colors are dual bases + +## i. Overview + +This file defines `HasContrDualBases`: species whose basis at `S.τ c` is dual to the basis at `c` +under the pairing `S.contr c`. + +A matching `e : basisIdx (S.τ c) ≃ basisIdx c` satisfies the δ law (`IsContrDualMatching`) if +`S.contr c (b c x₁ ⊗ₜ b (S.τ c) x₂) = if x₁ = e x₂ then 1 else 0`. The class asks for one such +matching at every color, so the label types need only be in bijection. + +Over a nontrivial ring the matching is unique (`IsContrDualMatching.unique`). Hence +`contrDualIdxEquiv`, although picked by choice, is the only matching, so nothing depends on the +choice. A concrete species identifies it through `contrDualIdxEquiv_eq_of_isContrDualMatching`, +and the double-dual law `contrDualIdxEquiv_tau` is a theorem. + +The contraction functionals are the dual basis of `b c` (`contr_tmul_basis_eq_dualBasis`). +Contracted basis vectors have δ coefficients (`Pure.contrPCoeff_basisVector`), and components of a +contraction are single sums (`contrT_basis_repr_apply_eq_sum_dual`). + +## ii. Key results + +- `TensorSpecies.IsContrDualMatching.unique` : the δ law determines the matching. +- `TensorSpecies.HasContrDualBases` : the class. +- `TensorSpecies.HasContrDualBases.contrDualIdxEquiv` : the matching of the labels at `S.τ c` + with those at `c`. +- `TensorSpecies.HasContrDualBases.contr_basis_eq_ite` : the δ law for `contrDualIdxEquiv`. +- `TensorSpecies.HasContrDualBases.contrDualIdxEquiv_eq_of_isContrDualMatching` : any matching + satisfying the δ law is `contrDualIdxEquiv`. +- `TensorSpecies.HasContrDualBases.contrDualIdxEquiv_tau` : the matching at `S.τ c` is the + inverse of the one at `c`, through `S.τ (S.τ c) = c`. +- `TensorSpecies.HasContrDualBases.contr_tmul_basis_eq_dualBasis` : contracting with a basis vector + at `S.τ c` is an element of `Module.Basis.dualBasis`. + +## iii. Table of contents + +- A. Matchings satisfying the δ law +- B. The class +- C. The matching +- D. The double dual +- E. The dual basis + +## iv. References + +There are no known references for the material in this module. + +-/ + +@[expose] public section + +open Module +open scoped TensorProduct + +namespace TensorSpecies + +variable {k : Type} [CommRing k] {C : Type} {G : Type} [Group G] + {V : C → Type} [∀ c, AddCommGroup (V c)] [∀ c, Module k (V c)] + {basisIdx : C → Type} [∀ c, Fintype (basisIdx c)] [∀ c, DecidableEq (basisIdx c)] + {rep : (c : C) → Representation k G (V c)} {b : (c : C) → Basis (basisIdx c) k (V c)} + +/-! + +## A. Matchings satisfying the δ law + +-/ + +/-- A matching `e` of the basis labels at `S.τ c` with those at `c` satisfies the δ law: + contracting a basis vector at `c` with one at `S.τ c` gives `1` if `e` matches their labels and + `0` otherwise. -/ +def IsContrDualMatching (S : TensorSpecies k C G V basisIdx rep b) (c : C) + (e : basisIdx (S.τ c) ≃ basisIdx c) : Prop := + ∀ x₁ x₂, S.contr c (b c x₁ ⊗ₜ[k] b (S.τ c) x₂) = if x₁ = e x₂ then 1 else 0 + +/-- Over a nontrivial ring the δ law determines the matching: the label matched with `x₂` is the + one whose basis vector pairs with `b (S.τ c) x₂` to `1`. -/ +lemma IsContrDualMatching.unique [Nontrivial k] {S : TensorSpecies k C G V basisIdx rep b} + {c : C} {e e' : basisIdx (S.τ c) ≃ basisIdx c} + (he : IsContrDualMatching S c e) (he' : IsContrDualMatching S c e') : e = e' := by + ext x₂ + have h := (he (e x₂) x₂).symm.trans (he' (e x₂) x₂) + by_contra hne + simp [hne] at h + +/-! + +## B. The class + +-/ + +/-- A tensor species whose basis at `S.τ c` is dual to its basis at `c` under the pairing + `S.contr c`: for every color some matching of the labels satisfies the δ law. -/ +class HasContrDualBases (S : TensorSpecies k C G V basisIdx rep b) : Prop where + /-- At every color, some matching of the labels at `S.τ c` with those at `c` satisfies the δ + law. -/ + exists_matching : ∀ c, ∃ e, IsContrDualMatching S c e + +namespace HasContrDualBases + +variable {S : TensorSpecies k C G V basisIdx rep b} [HasContrDualBases S] + +/-! + +## C. The matching + +-/ + +variable (S) in +/-- A matching of the basis labels at `S.τ c` with those at `c` satisfying the δ law, chosen by + `Classical.choose`. Over a nontrivial ring it is the only one + (`contrDualIdxEquiv_eq_of_isContrDualMatching`). -/ +noncomputable def contrDualIdxEquiv (c : C) : basisIdx (S.τ c) ≃ basisIdx c := + Classical.choose (exists_matching (S := S) c) + +/-- The δ law for `contrDualIdxEquiv`. -/ +lemma contr_basis_eq_ite (c : C) (x₁ : basisIdx c) (x₂ : basisIdx (S.τ c)) : + S.contr c (b c x₁ ⊗ₜ[k] b (S.τ c) x₂) = + if x₁ = contrDualIdxEquiv S c x₂ then 1 else 0 := + Classical.choose_spec (exists_matching (S := S) c) x₁ x₂ + +/-- Any matching satisfying the δ law is `contrDualIdxEquiv`. This is how a concrete species + identifies its matching. -/ +lemma contrDualIdxEquiv_eq_of_isContrDualMatching [Nontrivial k] {c : C} + {e : basisIdx (S.τ c) ≃ basisIdx c} (he : IsContrDualMatching S c e) : + contrDualIdxEquiv S c = e := + IsContrDualMatching.unique (contr_basis_eq_ite c) he + +/-! + +## D. The double dual + +-/ + +/-- The matching at `S.τ c` is the inverse of the one at `c`, once `S.τ (S.τ c)` is identified + with `c` by `S.τ_τ_apply`. The inverse matching satisfies the δ law at `S.τ c` by + `contr_tmul_symm`, so uniqueness identifies the two. -/ +lemma contrDualIdxEquiv_tau [Nontrivial k] (c : C) (x : basisIdx (S.τ (S.τ c))) : + contrDualIdxEquiv S (S.τ c) x = + (contrDualIdxEquiv S c).symm (basisIdxCongr (S.τ_τ_apply c) x) := by + suffices h : IsContrDualMatching S (S.τ c) + ((basisIdxCongr (S.τ_τ_apply c)).trans (contrDualIdxEquiv S c).symm) by + rw [contrDualIdxEquiv_eq_of_isContrDualMatching h] + rfl + intro y x + have key := S.contr_tmul_symm c (b c (basisIdxCongr (S.τ_τ_apply c) x)) (b (S.τ c) y) + rw [equivCast_basis (S.τ_τ_apply c).symm, basisIdxCongr_apply_apply, basisIdxCongr_rfl, + contr_basis_eq_ite] at key + rw [← key, Equiv.trans_apply] + exact if_congr (by rw [Equiv.eq_symm_apply, eq_comm]) rfl rfl + +/-! + +## E. The dual basis + +-/ + +/-- The functional `v ↦ S.contr c (v ⊗ₜ b (S.τ c) x)` is the element of `(b c).dualBasis` at the + label matched with `x`. -/ +lemma contr_tmul_basis_eq_dualBasis (c : C) (x : basisIdx (S.τ c)) (v : V c) : + S.contr c (v ⊗ₜ[k] b (S.τ c) x) = (b c).dualBasis (contrDualIdxEquiv S c x) v := by + have h : (S.contr c).toLinearMap ∘ₗ (TensorProduct.mk k (V c) (V (S.τ c))).flip (b (S.τ c) x) = + (b c).dualBasis (contrDualIdxEquiv S c x) := by + refine (b c).ext fun j => ?_ + simp [contr_basis_eq_ite, Finsupp.single_apply] + exact LinearMap.congr_fun h v + +end HasContrDualBases + +end TensorSpecies From fc1c7db8cfffdd047507d101e879fb015bcfe278 Mon Sep 17 00:00:00 2001 From: Andrea Pari Date: Fri, 2 Oct 2026 15:45:36 +0100 Subject: [PATCH 2/2] docs(Tensors): simplify the docstrings of isContrDualMatching_finCongr and isContrDualMatching_refl State only the result: the bases at a color and its dual are dual bases under the given matching. Co-authored-by: Claude Opus 5.5 --- Physlib/Relativity/Tensors/ComplexTensor/Basic.lean | 5 ++--- Physlib/Relativity/Tensors/RealTensor/Basic.lean | 4 ++-- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/Physlib/Relativity/Tensors/ComplexTensor/Basic.lean b/Physlib/Relativity/Tensors/ComplexTensor/Basic.lean index 73e23e1bec..ad094173d9 100644 --- a/Physlib/Relativity/Tensors/ComplexTensor/Basic.lean +++ b/Physlib/Relativity/Tensors/ComplexTensor/Basic.lean @@ -271,9 +271,8 @@ lemma repDim_tau {c : complexLorentzTensor.Color} : repDim (complexLorentzTensor.τ c) = repDim c := by cases c <;> rfl -/-- A complex Lorentz color and its dual have the same representation dimension (`repDim_tau`), -and the matching `finCongr repDim_tau` satisfies the δ law: it is the basis contraction of each of -the six Weyl and Lorentz pairings. -/ +/-- At every complex Lorentz color, the bases at the color and its dual are dual bases, with +labels matched by `finCongr repDim_tau`. -/ lemma isContrDualMatching_finCongr (c : complexLorentzTensor.Color) : IsContrDualMatching complexLorentzTensor c (finCongr repDim_tau) := by intro x₁ x₂ diff --git a/Physlib/Relativity/Tensors/RealTensor/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Basic.lean index 397d36d9b1..34b0944e87 100644 --- a/Physlib/Relativity/Tensors/RealTensor/Basic.lean +++ b/Physlib/Relativity/Tensors/RealTensor/Basic.lean @@ -164,8 +164,8 @@ lemma τ_down_eq_up {d : ℕ} : (realLorentzTensor d).τ Color.down = Color.up : attribute [-simp] Fintype.sum_sum_type open TensorSpecies Tensor -/-- The basis at every real Lorentz color is indexed by `Fin 1 ⊕ Fin d`, and the identity -matching satisfies the δ law: it is the basis contraction of the two Lorentz pairings. -/ +/-- At every real Lorentz color, the bases at the color and its dual are dual bases, with +labels matched by the identity. -/ lemma isContrDualMatching_refl (c : realLorentzTensor.Color) : IsContrDualMatching (realLorentzTensor d) c (Equiv.refl _) := by intro x₁ x₂