Imports
/-
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.Contraction.CrossToEndResult-to-slot contraction against a rank-2 tensor
i. Overview
crossToEnd deposits the surviving index of a slot contraction at the end of the survivor list.
Raising and lowering a named index instead wants the replacement to stay in place: contracting
slot i of t against a rank-2 tensor M (a metric, the unit tensor) should return t with only
slot i's color changed, T^{μ}{}_{νρ} ↦ T_{μνρ}. crossToSlot i j hc M is that operation, and
crossToSlot_eq_crossToEnd is the one place the two conventions meet.
This module stays at the CommRing altitude of crossToEnd; the RCLike round trips built on the
operation live with the unit-tensor collapse theory in
Physlib.Relativity.Tensors.Contraction.UnitTensorContraction.
ii. Key results
TensorSpecies.Tensor.crossToSlot : contract slot i against slot j of a rank-2 tensor and
rotate the survivor back into position i; raising and lowering a named index.
TensorSpecies.Tensor.crossToSlot_eq_crossToEnd : the bridge to the result-to-end convention.
TensorSpecies.Tensor.crossToSlotInv : the returning half of a round trip, the contraction
against the second factor with the round trip's color cast absorbed.
TensorSpecies.Tensor.crossToSlot_permT_right_id : an identity reindexing of the rank-2 tensor
passes through the contraction.
TensorSpecies.Tensor.crossToSlot_equivariant : the contraction commutes with the G-action.
iii. Table of contents
A. The result-to-slot contraction
iv. References
@[expose] public sectionA. The result-to-slot contraction
The survivor color of crossToEnd i j against a rank-2 tensor of color cM is c with
slot i replaced by the surviving color cM (j.succAbove 0), once the survivors are rotated
back by the inverse of the cycle [i, last].
C:TypenA:ℕc:Fin (nA + 1) → CcM:Fin 2 → Ci:Fin (nA + 1)j:Fin 2z:Fin (nA + 1)a:Fin 1⊢ cM (j.succAbove a) = cM (j.succAbove 0)
C:TypenA:ℕc:Fin (nA + 1) → CcM:Fin 2 → Ci:Fin (nA + 1)j:Fin 2z:Fin (nA + 1)⊢ cM (j.succAbove ((fun i => i) ⟨0, ⋯⟩)) = cM (j.succAbove 0)
All goals completed! 🐙
The bridge between the two conventions: crossToSlot i j hc M t is crossToEnd i j hc t M
with the survivor rotated from the last slot back to slot i by the inverse cycle.
lemma crossToSlot_eq_crossToEnd {nA : ℕ} {c : Fin (nA + 1) → C} {cM : Fin 2 → C}
(i : Fin (nA + 1)) (j : Fin 2) (hc : S.τ (c i) = cM j) (M : S.Tensor cM) (t : S.Tensor c) :
crossToSlot i j hc M t =
permT ⇑(Fin.cycleIcc i (Fin.last nA)).symm (IsReindexing.crossToSlot_cycle i j)
(crossToEnd i j hc t M) := rfl
An identity reindexing of the rank-2 tensor becomes the corresponding identity reindexing of
the contracted output: the crossToSlot-level case of crossToEnd_permT_right where the rank-2
tensor's colors are only propositionally recast.
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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bnA:ℕc:Fin (nA + 1) → CcM:Fin 2 → CcM':Fin 2 → Ci:Fin (nA + 1)j:Fin 2hc:S.τ (c i) = cM' jM:S.Tensor cMhM:IsReindexing cM cM' idt:S.Tensor c⊢ (permT ⇑(Equiv.symm (i.cycleIcc (Fin.last nA))) ⋯)
((permT (Fin.append (Fin.castAdd 1) (Fin.natAdd nA ∘ id)) ⋯) (((crossToEnd i (id j) ⋯) t) M)) =
(permT id ⋯) ((permT ⇑(Equiv.symm (i.cycleIcc (Fin.last nA))) ⋯) (((crossToEnd i j ⋯) t) 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bnA:ℕc:Fin (nA + 1) → CcM:Fin 2 → CcM':Fin 2 → Ci:Fin (nA + 1)j:Fin 2hc:S.τ (c i) = cM' jM:S.Tensor cMhM:IsReindexing cM cM' idt:S.Tensor c⊢ (permT (Fin.append (Fin.castAdd 1) (Fin.natAdd nA ∘ id) ∘ ⇑(Equiv.symm (i.cycleIcc (Fin.last nA)))) ⋯)
(((crossToEnd i (id j) ⋯) t) M) =
(permT (⇑(Equiv.symm (i.cycleIcc (Fin.last nA))) ∘ id) ⋯) (((crossToEnd i j ⋯) t) 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bnA:ℕc:Fin (nA + 1) → CcM:Fin 2 → CcM':Fin 2 → Ci:Fin (nA + 1)j:Fin 2hc:S.τ (c i) = cM' jM:S.Tensor cMhM:IsReindexing cM cM' idt:S.Tensor c⊢ Fin.append (Fin.castAdd 1) (Fin.natAdd nA ∘ id) ∘ ⇑(Equiv.symm (i.cycleIcc (Fin.last nA))) =
⇑(Equiv.symm (i.cycleIcc (Fin.last nA))) ∘ idk: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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bnA:ℕc:Fin (nA + 1) → CcM:Fin 2 → CcM':Fin 2 → Ci:Fin (nA + 1)j:Fin 2hc:S.τ (c i) = cM' jM:S.Tensor cMhM:IsReindexing cM cM' idt:S.Tensor c⊢ ((crossToEnd i (id j) ⋯) t) M = ((crossToEnd i j ⋯) t) 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bnA:ℕc:Fin (nA + 1) → CcM:Fin 2 → CcM':Fin 2 → Ci:Fin (nA + 1)j:Fin 2hc:S.τ (c i) = cM' jM:S.Tensor cMhM:IsReindexing cM cM' idt:S.Tensor c⊢ Fin.append (Fin.castAdd 1) (Fin.natAdd nA ∘ id) ∘ ⇑(Equiv.symm (i.cycleIcc (Fin.last nA))) =
⇑(Equiv.symm (i.cycleIcc (Fin.last nA))) ∘ id 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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bnA:ℕc:Fin (nA + 1) → CcM:Fin 2 → CcM':Fin 2 → Ci:Fin (nA + 1)j:Fin 2hc:S.τ (c i) = cM' jM:S.Tensor cMhM:IsReindexing cM cM' idt:S.Tensor cx:Fin (nA + 1)⊢ (Fin.append (Fin.castAdd 1) (Fin.natAdd nA ∘ id) ∘ ⇑(Equiv.symm (i.cycleIcc (Fin.last nA)))) x =
(⇑(Equiv.symm (i.cycleIcc (Fin.last nA))) ∘ id) x
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) → Module.Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep bnA:ℕc:Fin (nA + 1) → CcM:Fin 2 → CcM':Fin 2 → Ci:Fin (nA + 1)j:Fin 2hc:S.τ (c i) = cM' jM:S.Tensor cMhM:IsReindexing cM cM' idt:S.Tensor c⊢ ((crossToEnd i (id j) ⋯) t) M = ((crossToEnd i j ⋯) t) M All goals completed! 🐙
Cross contraction into a slot is G-equivariant, both constituents (crossToEnd, permT)
being so.
All goals completed! 🐙