1. Physlib
  2. Relativity
  3. Tensors
  4. Contraction
  5. Basis
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.Contraction.Basic public import Physlib.Relativity.Tensors.ComponentIdx.Contraction

Contractions on basis tensors

@[expose] public sectionset_option backward.isDefEq.respectTransparency false in lemma Pure.dropPair_basisVector {n : ℕ} {c : Fin (n + 1 + 1) → C} {i j : Fin (n + 1 + 1)} (hij : i ≠ j) (b : ComponentIdx c) : Pure.dropPair i j hij (basisVector c b) = basisVector (S := S) (c ∘ Fin.succSuccAbove i j) fun m => b (Fin.succSuccAbove i j m) := k:Typeinst✝⁵:CommRing 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx c⊢ dropPair i j hij (basisVector c b) = basisVector (c ∘ i.succSuccAbove j) fun m => b (i.succSuccAbove j m) k:Typeinst✝⁵:CommRing 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)hij:i ≠ jb:ComponentIdx cl:Fin n⊢ dropPair i j hij (basisVector c b) l = basisVector (c ∘ i.succSuccAbove j) (fun m => b (i.succSuccAbove j m)) l All goals completed! 🐙attribute [-simp] LinearEquiv.cast_applyk:Typeinst✝⁵:CommRing 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cφ:ComponentIdx (c ∘ i.succSuccAbove j)b':ComponentIdx chd:¬dropPair i j b' = φb'':↥φ.DropPairSectiona✝:b'' ∈ Finset.univ⊢ ↑b'' ≠ b' All goals completed! 🐙 k:Typeinst✝⁵:CommRing 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cφ:ComponentIdx (c ∘ i.succSuccAbove j)⊢ ((basis (c ∘ i.succSuccAbove j)).repr ((contrT n i j h) 0)) φ = ∑ b', ((basis c).repr 0) ↑b' * (S.contr (c i)) ((b (c i)) (↑b' i) ⊗ₜ[k] (b (S.τ (c i))) ((basisIdxCongr ⋯) (↑b' j))) All goals completed! 🐙 k:Typeinst✝⁵:CommRing 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cφ:ComponentIdx (c ∘ i.succSuccAbove j)⊢ ∀ (r : k) (t : S.Tensor c), ((basis (c ∘ i.succSuccAbove j)).repr ((contrT n i j h) t)) φ = ∑ b', ((basis c).repr t) ↑b' * (S.contr (c i)) ((b (c i)) (↑b' i) ⊗ₜ[k] (b (S.τ (c i))) ((basisIdxCongr ⋯) (↑b' j))) → ((basis (c ∘ i.succSuccAbove j)).repr ((contrT n i j h) (r • t))) φ = ∑ b', ((basis c).repr (r • t)) ↑b' * (S.contr (c i)) ((b (c i)) (↑b' i) ⊗ₜ[k] (b (S.τ (c i))) ((basisIdxCongr ⋯) (↑b' j))) k:Typeinst✝⁵:CommRing 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ S.τ (c i) = c jt✝:S.Tensor cφ:ComponentIdx (c ∘ i.succSuccAbove j)r:kt:S.Tensor ch1:((basis (c ∘ i.succSuccAbove j)).repr ((contrT n i j h) t)) φ = ∑ b', ((basis c).repr t) ↑b' * (S.contr (c i)) ((b (c i)) (↑b' i) ⊗ₜ[k] (b (S.τ (c i))) ((basisIdxCongr ⋯) (↑b' j)))⊢ ((basis (c ∘ i.succSuccAbove j)).repr ((contrT n i j h) (r • t))) φ = ∑ b', ((basis c).repr (r • t)) ↑b' * (S.contr (c i)) ((b (c i)) (↑b' i) ⊗ₜ[k] (b (S.τ (c i))) ((basisIdxCongr ⋯) (↑b' j))) All goals completed! 🐙 k:Typeinst✝⁵:CommRing 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cφ:ComponentIdx (c ∘ i.succSuccAbove j)⊢ ∀ (t1 t2 : S.Tensor c), ((basis (c ∘ i.succSuccAbove j)).repr ((contrT n i j h) t1)) φ = ∑ b', ((basis c).repr t1) ↑b' * (S.contr (c i)) ((b (c i)) (↑b' i) ⊗ₜ[k] (b (S.τ (c i))) ((basisIdxCongr ⋯) (↑b' j))) → ((basis (c ∘ i.succSuccAbove j)).repr ((contrT n i j h) t2)) φ = ∑ b', ((basis c).repr t2) ↑b' * (S.contr (c i)) ((b (c i)) (↑b' i) ⊗ₜ[k] (b (S.τ (c i))) ((basisIdxCongr ⋯) (↑b' j))) → ((basis (c ∘ i.succSuccAbove j)).repr ((contrT n i j h) (t1 + t2))) φ = ∑ b', ((basis c).repr (t1 + t2)) ↑b' * (S.contr (c i)) ((b (c i)) (↑b' i) ⊗ₜ[k] (b (S.τ (c i))) ((basisIdxCongr ⋯) (↑b' j))) k:Typeinst✝⁵:CommRing 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cφ:ComponentIdx (c ∘ i.succSuccAbove j)t1:S.Tensor ct2:S.Tensor ch1:((basis (c ∘ i.succSuccAbove j)).repr ((contrT n i j h) t1)) φ = ∑ b', ((basis c).repr t1) ↑b' * (S.contr (c i)) ((b (c i)) (↑b' i) ⊗ₜ[k] (b (S.τ (c i))) ((basisIdxCongr ⋯) (↑b' j)))h2:((basis (c ∘ i.succSuccAbove j)).repr ((contrT n i j h) t2)) φ = ∑ b', ((basis c).repr t2) ↑b' * (S.contr (c i)) ((b (c i)) (↑b' i) ⊗ₜ[k] (b (S.τ (c i))) ((basisIdxCongr ⋯) (↑b' j)))⊢ ((basis (c ∘ i.succSuccAbove j)).repr ((contrT n i j h) (t1 + t2))) φ = ∑ b', ((basis c).repr (t1 + t2)) ↑b' * (S.contr (c i)) ((b (c i)) (↑b' i) ⊗ₜ[k] (b (S.τ (c i))) ((basisIdxCongr ⋯) (↑b' j))) All goals completed! 🐙k:Typeinst✝⁵:CommRing 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bn:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ S.τ (c i) = c jt:S.Tensor cφ:ComponentIdx (c ∘ i.succSuccAbove j)⊢ ∑ x, ∑ y, ((basis c).repr t) ↑((DropPairSection.ofFinEquiv ⋯ φ) (x, y)) * (S.contr (c i)) ((b (c i)) (↑((DropPairSection.ofFinEquiv ⋯ φ) (x, y)) i) ⊗ₜ[k] (b (S.τ (c i))) ((basisIdxCongr ⋯) (↑((DropPairSection.ofFinEquiv ⋯ φ) (x, y)) j))) = ∑ x1, ∑ x2, ((basis c).repr t) ↑((DropPairSection.ofFinEquiv ⋯ φ) (x1, x2)) * (S.contr (c i)) ((b (c i)) x1 ⊗ₜ[k] (b (S.τ (c i))) ((basisIdxCongr ⋯) x2)) All goals completed! 🐙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) = Pure.contrPCoeff i j h (Pure.basisVector c b) • basis (c ∘ Fin.succSuccAbove i j) (b.dropPair i j) := k:Typeinst✝⁵:CommRing 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ S.τ (c i) = c jb:ComponentIdx c⊢ (contrT n i j h) ((basis c) b) = Pure.contrPCoeff i j h (Pure.basisVector c b) • (basis (c ∘ i.succSuccAbove j)) (dropPair i j b) k:Typeinst✝⁵:CommRing 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin (n + 1 + 1) → Ci:Fin (n + 1 + 1)j:Fin (n + 1 + 1)h:i ≠ j ∧ S.τ (c i) = c jb:ComponentIdx c⊢ Pure.contrPCoeff i j h (Pure.basisVector c b) • (Pure.basisVector (c ∘ i.succSuccAbove j) fun m => b (i.succSuccAbove j m)).toTensor = Pure.contrPCoeff i j h (Pure.basisVector c b) • (Pure.basisVector (c ∘ i.succSuccAbove j) (dropPair i j b)).toTensor All goals completed! 🐙