Physlib.Relativity.Tensors.ComponentIdx.Single

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.ComponentIdx.Basic

Component indices for one-index tensors

i. Overview

This file defines the canonical equivalence between component indices for a single color and the basis indices of that color.

ii. Key results

TensorSpecies.Tensor.ComponentIdx.single is the equivalence between ComponentIdx ![c] and basisIdx c.

TensorSpecies.Tensor.ComponentIdx.single_apply and TensorSpecies.Tensor.ComponentIdx.single_symm_apply are simp lemmas for the two directions of this equivalence.

iii. Table of contents

A. Single-index equivalence

iv. References

There are no known references for the material in this module.

@[expose] public section

A. Single-index equivalence

The equivalence between component indices for a single color and the basis indices of that color.

def ComponentIdx.single {c : C} :
    ComponentIdx (S := S) ![c] ≃ basisIdx c where
  toFun b := basisIdxCongr (byk: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 b✝c:Cb:ComponentIdx ![c]⊢ ![c] 0 = c simpAll goals completed! 🐙) (b 0)
  invFun b := fun _ => basisIdxCongr (byk: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 b✝c:Cb:basisIdx cx✝:Fin (Nat.succ 0)⊢ c = ![c] x✝ simpAll goals completed! 🐙) b
  left_inv b := byk: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 b✝c:Cb:ComponentIdx ![c]⊢ (fun b x => (basisIdxCongr ⋯) b) ((fun b => (basisIdxCongr ⋯) (b 0)) b) = b
    ext ik: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 b✝c:Cb:ComponentIdx ![c]i:Fin (Nat.succ 0)⊢ (fun b x => (basisIdxCongr ⋯) b) ((fun b => (basisIdxCongr ⋯) (b 0)) b) i = b i
    cases Fin.fin_one_eq_zero ireflk: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 b✝c:Cb:ComponentIdx ![c]⊢ (fun b x => (basisIdxCongr ⋯) b) ((fun b => (basisIdxCongr ⋯) (b 0)) b) 0 = b 0
    simp [basisIdxCongr]reflk: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 b✝c:Cb:ComponentIdx ![c]⊢ (Equiv.refl (basisIdx c)) ((Equiv.refl (basisIdx c)) (b 0)) = b 0
    rflAll goals completed! 🐙
  right_inv b := byk: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 b✝c:Cb:basisIdx c⊢ (fun b => (basisIdxCongr ⋯) (b 0)) ((fun b x => (basisIdxCongr ⋯) b) b) = b
    simp [basisIdxCongr]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 b✝c:Cb:basisIdx c⊢ (Equiv.refl (basisIdx c)) ((Equiv.refl (basisIdx c)) b) = b
    rflAll goals completed! 🐙

@[simp]
lemma ComponentIdx.single_apply {c : C} (b : ComponentIdx (S := S) ![c]) :
    ComponentIdx.single (S := S) b = basisIdxCongr (byk: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 b✝c:Cb:ComponentIdx ![c]⊢ ![c] 0 = c simpAll goals completed! 🐙) (b 0) := rfl

@[simp]
lemma ComponentIdx.single_symm_apply {c : C} (b : basisIdx c) (i : Fin 1) :
    (ComponentIdx.single (S := S) (c := c)).symm b i = basisIdxCongr (byk: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 b✝c:Cb:basisIdx ci:Fin 1⊢ c = ![c] i simpAll goals completed! 🐙) b := rfl