feat(Tensors): HasContrDualBases, the dual-basis class, and the component formulas it collapses

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

Physlib/Relativity/Tensors/ComplexTensor/Basic.lean

@@ -271,33 +271,36 @@ lemma repDim_tau {c : complexLorentzTensor.Color} :
     repDim (complexLorentzTensor.τ c) = repDim c := by
   cases c <;> rfl
 
+/-- 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₂
+  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

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) =

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
 
+/-- 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₂
+  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

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]

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