1. Physlib
  2. Relativity
  3. Tensors
  4. Dual
Imports
/- Copyright (c) 2025 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.MetricTensor public import Physlib.Relativity.Tensors.Contraction.UnitTensorContraction

Dual tensors

i. Overview

The metric tensor identifies a tensor with the one obtained by dualising the color of a single index: contracting slot i of t against metricTensor (S.τ (c i)) returns a tensor of color Function.update c i (S.τ (c i)), leaving every other slot alone. This is the raising and lowering of a named index, T^{μν} ↦ T_{μ}{}^{ν}. toDualMapAtIndex i is that contraction, crossToSlot against the metric, at every rank and every named slot.

A metric contracted against the metric at the dual color collapses to the unit tensor, in both orders. So the contraction back against metricTensor (c i), fromDualMapAtIndex i, inverts it, and the two assemble into the linear equivalence toDualAtIndex i: the two color assignments carry the same information. Dualising the same index twice returns the original tensor, up to the reindexing of the colors.

ii. Key results

    TensorSpecies.Tensor.toDualMapAtIndex : dualise the color of the index i by contracting with the metric tensor.

    TensorSpecies.Tensor.fromDualMapAtIndex : the returning contraction, against the metric tensor at c i.

    TensorSpecies.Tensor.toDualMapAtIndex_toDualMapAtIndex : dualising the index i twice returns the original tensor.

    TensorSpecies.Tensor.toDualMapAtIndex_equivariant : dualising an index commutes with the G-action.

    TensorSpecies.Tensor.toDualAtIndex : raising and lowering the index i as a linear equivalence.

iii. Table of contents

    A. Dualising a named index

    B. Contracting a metric against its dual

    C. Dualising twice

    D. The returning contraction

    E. Equivariance

    F. Raising and lowering as an equivalence

iv. References

@[expose] public section

A. Dualising a named index

B. Contracting a metric against its dual

The metric tensor at S.τ c contracted with the metric tensor at c is the unit tensor at c.

k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:C⊢ (permT (id ∘ id) ⋯) (unitTensor c) = (permT id ⋯) (unitTensor c) All goals completed! 🐙

The metric tensor at c contracted with the metric tensor at S.τ c is the unit tensor at S.τ c.

k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:C⊢ (permT (![0, 1] ∘ id) ⋯) (unitTensor (S.τ c)) = (permT id ⋯) (unitTensor (S.τ c)) exact permT_congr (k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:C⊢ ![0, 1] ∘ id = id All goals completed! 🐙) rfl

C. Dualising twice

Dualising the index i twice returns the original tensor, up to the reindexing of the colors.

k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bnA:ℕc:Fin (nA + 1) → Ci:Fin (nA + 1)t:S.Tensor ckey:(crossToSlot i 0 ⋯ (metricTensor (c i))) ((crossToSlot i 0 ⋯ (metricTensor (S.τ (c i)))) t) = (permT id ⋯) t⊢ (crossToSlot i 0 ⋯ ((permT id ⋯) (metricTensor (c i)))) ((crossToSlot i 0 ⋯ (metricTensor (S.τ (c i)))) t) = (permT id ⋯) t erw [k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bnA:ℕc:Fin (nA + 1) → Ci:Fin (nA + 1)t:S.Tensor ckey:(crossToSlot i 0 ⋯ (metricTensor (c i))) ((crossToSlot i 0 ⋯ (metricTensor (S.τ (c i)))) t) = (permT id ⋯) t⊢ (permT id ⋯) ((crossToSlot i 0 ⋯ (metricTensor (c i))) ((crossToSlot i 0 ⋯ (metricTensor (S.τ (c i)))) t)) = (permT id ⋯) t k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bnA:ℕc:Fin (nA + 1) → Ci:Fin (nA + 1)t:S.Tensor ckey:(crossToSlot i 0 ⋯ (metricTensor (c i))) ((crossToSlot i 0 ⋯ (metricTensor (S.τ (c i)))) t) = (permT id ⋯) t⊢ (permT id ⋯) ((permT id ⋯) t) = (permT id ⋯) t k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bnA:ℕc:Fin (nA + 1) → Ci:Fin (nA + 1)t:S.Tensor ckey:(crossToSlot i 0 ⋯ (metricTensor (c i))) ((crossToSlot i 0 ⋯ (metricTensor (S.τ (c i)))) t) = (permT id ⋯) t⊢ (permT (id ∘ id) ⋯) t = (permT id ⋯) tk:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bnA:ℕc:Fin (nA + 1) → Ci:Fin (nA + 1)t:S.Tensor ckey:(crossToSlot i 0 ⋯ (metricTensor (c i))) ((crossToSlot i 0 ⋯ (metricTensor (S.τ (c i)))) t) = (permT id ⋯) t⊢ (permT (id ∘ id) ⋯) t = (permT id ⋯) t exact permT_congr (k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bnA:ℕc:Fin (nA + 1) → Ci:Fin (nA + 1)t:S.Tensor ckey:(crossToSlot i 0 ⋯ (metricTensor (c i))) ((crossToSlot i 0 ⋯ (metricTensor (S.τ (c i)))) t) = (permT id ⋯) t⊢ id ∘ id = id k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bnA:ℕc:Fin (nA + 1) → Ci:Fin (nA + 1)t:S.Tensor ckey:(crossToSlot i 0 ⋯ (metricTensor (c i))) ((crossToSlot i 0 ⋯ (metricTensor (S.τ (c i)))) t) = (permT id ⋯) tj:Fin (nA + 1)⊢ (id ∘ id) j = id j; All goals completed! 🐙) rfl

D. The returning contraction

@[simp] lemma fromDualMapAtIndex_toDualMapAtIndex {n : ℕ} {c : Fin n → C} (i : Fin n) (t : S.Tensor c) : fromDualMapAtIndex (S := S) i (toDualMapAtIndex (S := S) i t) = t := k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → Ci:Fin nt:S.Tensor c⊢ (fromDualMapAtIndex i) ((toDualMapAtIndex i) t) = t cases n with k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Fin 0 → Ci:Fin 0t:S.Tensor c⊢ (fromDualMapAtIndex i) ((toDualMapAtIndex i) t) = t All goals completed! 🐙 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bnA:ℕc:Fin (nA + 1) → Ci:Fin (nA + 1)t:S.Tensor c⊢ (fromDualMapAtIndex i) ((toDualMapAtIndex i) t) = t All goals completed! 🐙@[simp] lemma toDualMapAtIndex_fromDualMapAtIndex {n : ℕ} {c : Fin n → C} (i : Fin n) (t : S.Tensor (Function.update c i (S.τ (c i)))) : toDualMapAtIndex (S := S) i (fromDualMapAtIndex (S := S) i t) = t := k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → Ci:Fin nt:S.Tensor (Function.update c i (S.τ (c i)))⊢ (toDualMapAtIndex i) ((fromDualMapAtIndex i) t) = t cases n with k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Fin 0 → Ci:Fin 0t:S.Tensor (Function.update c i (S.τ (c i)))⊢ (toDualMapAtIndex i) ((fromDualMapAtIndex i) t) = t All goals completed! 🐙 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bnA:ℕc:Fin (nA + 1) → Ci:Fin (nA + 1)t:S.Tensor (Function.update c i (S.τ (c i)))⊢ (toDualMapAtIndex i) ((fromDualMapAtIndex i) t) = t All goals completed! 🐙

E. Equivariance

Dualising the index i commutes with the action of G.

k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bg:GnA:ℕc:Fin (nA + 1) → Ci:Fin (nA + 1)t:S.Tensor c⊢ (crossToSlot i 0 ⋯ (metricTensor (S.τ (c i)))) (g • t) = g • (crossToSlot i 0 ⋯ (metricTensor (S.τ (c i)))) t conv_lhs => k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bg:GnA:ℕc:Fin (nA + 1) → Ci:Fin (nA + 1)t:S.Tensor c| (crossToSlot i 0 ⋯ (g • metricTensor (S.τ (c i)))) (g • t) All goals completed! 🐙

F. Raising and lowering as an equivalence

@[simp] lemma toDualAtIndex_apply {n : ℕ} {c : Fin n → C} (i : Fin n) (t : S.Tensor c) : toDualAtIndex (S := S) i t = toDualMapAtIndex (S := S) i t := k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → Ci:Fin nt:S.Tensor c⊢ (toDualAtIndex i) t = (toDualMapAtIndex i) t cases n with k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Fin 0 → Ci:Fin 0t:S.Tensor c⊢ (toDualAtIndex i) t = (toDualMapAtIndex i) t All goals completed! 🐙 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bnA:ℕc:Fin (nA + 1) → Ci:Fin (nA + 1)t:S.Tensor c⊢ (toDualAtIndex i) t = (toDualMapAtIndex i) t All goals completed! 🐙@[simp] lemma toDualAtIndex_symm_apply {n : ℕ} {c : Fin n → C} (i : Fin n) (t : S.Tensor (Function.update c i (S.τ (c i)))) : (toDualAtIndex (S := S) i).symm t = fromDualMapAtIndex (S := S) i t := k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin n → Ci:Fin nt:S.Tensor (Function.update c i (S.τ (c i)))⊢ (toDualAtIndex i).symm t = (fromDualMapAtIndex i) t cases n with k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bc:Fin 0 → Ci:Fin 0t:S.Tensor (Function.update c i (S.τ (c i)))⊢ (toDualAtIndex i).symm t = (fromDualMapAtIndex i) t All goals completed! 🐙 k:Typeinst✝⁵:RCLike kC:TypeG:Typeinst✝⁴:Group GV:C → Typeinst✝³:(c : C) → AddCommGroup (V c)inst✝²:(c : C) → Module k (V c)basisIdx:C → Typeinst✝¹:(c : C) → Fintype (basisIdx c)inst✝:(c : C) → DecidableEq (basisIdx c)rep:(c : C) → Representation k G (V c)b:(c : C) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bnA:ℕc:Fin (nA + 1) → Ci:Fin (nA + 1)t:S.Tensor (Function.update c i (S.τ (c i)))⊢ (toDualAtIndex i).symm t = (fromDualMapAtIndex i) t All goals completed! 🐙