1. Physlib
  2. Relativity
  3. Tensors
  4. MetricTensor
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.UnitTensor

The metric tensors

@[expose] public sectionattribute [-simp] LinearEquiv.cast_applylemma metricTensor_congr {c c1 : C} (h : c = c1) : S.metricTensor c = permT 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 bc:Cc1:Ch:c = c1⊢ IsReindexing ![c1, c1] ![c, c] id All goals completed! 🐙) (metricTensor c1) := 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:Cc1:Ch:c = c1⊢ metricTensor c = (permT id ⋯) (metricTensor c1) 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⊢ metricTensor c = (permT id ⋯) (metricTensor c) All goals completed! 🐙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 bc:C⊢ fromPairT ((TensorProduct.comm k (V c) (V (S.τ c))) ((LinearEquiv.lTensor (V c) (TensorProduct.lid k (V (S.τ c)))) ((LinearMap.lTensor (V c) (LinearMap.rTensor (V (S.τ c)) (S.contr c).toLinearMap)) ((LinearEquiv.lTensor (V c) (TensorProduct.assoc k (V c) (V (S.τ c)) (V (S.τ c))).symm) ((TensorProduct.assoc k (V c) (V c) (TensorProduct k (V (S.τ c)) (V (S.τ c)))) ((S.metric c) 1 ⊗ₜ[k] (S.metric (S.τ c)) 1)))))) = fromPairT ((TensorProduct.comm k (V c) (V (S.τ c))) ((LinearEquiv.lTensor (V c) (TensorProduct.lid k (V (S.τ c)))) ((LinearMap.lTensor (V c) (LinearMap.rTensor (V (S.τ c)) (S.contr c).toLinearMap)) ((LinearMap.lTensor (V c) ↑(TensorProduct.assoc k (V c) (V (S.τ c)) (V (S.τ c))).symm) ((TensorProduct.assoc k (V c) (V c) (TensorProduct k (V (S.τ c)) (V (S.τ c)))) ((S.metric c) 1 ⊗ₜ[k] (S.metric (S.τ c)) 1)))))) 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 bc:C⊢ fromPairTContr ((S.metric c) 1) ((S.metric (S.τ c)) 1) = (permT (![1, 0] ∘ ![1, 0]) ⋯) (fromPairTContr ((S.metric c) 1) ((S.metric (S.τ c)) 1)) 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 (![1, 0] ∘ ![1, 0]) ⋯) (fromPairTContr ((S.metric c) 1) ((S.metric (S.τ c)) 1)) = fromPairTContr ((S.metric c) 1) ((S.metric (S.τ c)) 1) 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⊢ ![1, 0] ∘ ![1, 0] = id All goals completed! 🐙

The contraction of the metric tensor with its dual gives the unit tensor. This is the de-categorification of S.contr_metric.

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 (![1, 0] ∘ id) ⋯) (unitTensor c) = (permT ![1, 0] ⋯) (unitTensor c) 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 bc:C⊢ (permT (![1, 0] ∘ ![1, 0]) ⋯) (unitTensor (S.τ c)) = (permT ![0, 1] ⋯) (unitTensor (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⊢ ![1, 0] ∘ ![1, 0] = ![0, 1]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⊢ unitTensor (S.τ c) = unitTensor (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⊢ ![1, 0] ∘ ![1, 0] = ![0, 1] 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 bc:C⊢ unitTensor (S.τ c) = unitTensor (S.τ c) 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 bc:Chm:metricTensor c = (permT id ⋯) (metricTensor (S.τ (S.τ c)))⊢ (permT (![1, 0] ∘ Fin.funPredPredAbove 1 2 ⋯ (Fin.append (Fin.castAdd 2) (Fin.natAdd 2 ∘ id)) ⋯) ⋯) (unitTensor (S.τ c)) = (permT ![1, 0] ⋯) (unitTensor (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:Chm:metricTensor c = (permT id ⋯) (metricTensor (S.τ (S.τ c)))⊢ ![1, 0] ∘ Fin.funPredPredAbove 1 2 ⋯ (Fin.append (Fin.castAdd 2) (Fin.natAdd 2 ∘ id)) ⋯ = ![1, 0]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:Chm:metricTensor c = (permT id ⋯) (metricTensor (S.τ (S.τ c)))⊢ unitTensor (S.τ c) = unitTensor (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:Chm:metricTensor c = (permT id ⋯) (metricTensor (S.τ (S.τ c)))⊢ ![1, 0] ∘ Fin.funPredPredAbove 1 2 ⋯ (Fin.append (Fin.castAdd 2) (Fin.natAdd 2 ∘ id)) ⋯ = ![1, 0] 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:Chm:metricTensor c = (permT id ⋯) (metricTensor (S.τ (S.τ c)))i:Fin 2⊢ ↑((![1, 0] ∘ Fin.funPredPredAbove 1 2 ⋯ (Fin.append (Fin.castAdd 2) (Fin.natAdd 2 ∘ id)) ⋯) i) = ↑(![1, 0] i) 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:Chm:metricTensor c = (permT id ⋯) (metricTensor (S.τ (S.τ c)))⊢ ↑((![1, 0] ∘ Fin.funPredPredAbove 1 2 ⋯ (Fin.append (Fin.castAdd 2) (Fin.natAdd 2 ∘ id)) ⋯) ((fun i => i) ⟨0, ⋯⟩)) = ↑(![1, 0] ((fun i => i) ⟨0, ⋯⟩))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:Chm:metricTensor c = (permT id ⋯) (metricTensor (S.τ (S.τ c)))⊢ ↑((![1, 0] ∘ Fin.funPredPredAbove 1 2 ⋯ (Fin.append (Fin.castAdd 2) (Fin.natAdd 2 ∘ id)) ⋯) ((fun i => i) ⟨1, ⋯⟩)) = ↑(![1, 0] ((fun i => i) ⟨1, ⋯⟩)) 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:Chm:metricTensor c = (permT id ⋯) (metricTensor (S.τ (S.τ c)))⊢ ↑((![1, 0] ∘ Fin.funPredPredAbove 1 2 ⋯ (Fin.append (Fin.castAdd 2) (Fin.natAdd 2 ∘ id)) ⋯) ((fun i => i) ⟨0, ⋯⟩)) = ↑(![1, 0] ((fun i => i) ⟨0, ⋯⟩))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:Chm:metricTensor c = (permT id ⋯) (metricTensor (S.τ (S.τ c)))⊢ ↑((![1, 0] ∘ Fin.funPredPredAbove 1 2 ⋯ (Fin.append (Fin.castAdd 2) (Fin.natAdd 2 ∘ id)) ⋯) ((fun i => i) ⟨1, ⋯⟩)) = ↑(![1, 0] ((fun i => i) ⟨1, ⋯⟩)) 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 bc:Chm:metricTensor c = (permT id ⋯) (metricTensor (S.τ (S.τ c)))⊢ unitTensor (S.τ c) = unitTensor (S.τ c) All goals completed! 🐙