Physlib.Relativity.Tensors.ComponentIdx.Product

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

Products of component indices

i. Overview

This file contains the component-index API induced by appending two lists of tensor colors.

The main construction identifies component indices for appended color lists with pairs of component indices for each side of the append.

ii. Key results

TensorSpecies.Tensor.ComponentIdx.prod is the equivalence between ComponentIdx (Fin.append c c1) and ComponentIdx c × ComponentIdx c1.

iii. Table of contents

A. Product equivalence

iv. References

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

@[expose] public section

A. Product equivalence

The equivalence between ComponentIdx (Fin.append c c1) and ComponentIdx c × ComponentIdx c1 formed by products.

unsolved goals
k C G:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1 n2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx c × ComponentIdx c1⊢ (fun i => (basisIdxCongr ⋯) (?m.94 i), fun i => (basisIdxCongr ⋯) (?m.95 i)) = punsolved goals
k C G:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1 n2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx c × ComponentIdx c1⊢ (fun i => (basisIdxCongr ⋯) (?m.94 i), fun i => (basisIdxCongr ⋯) (?m.95 i)) = punsolved goals
k C G:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1 n2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx (Fin.append c c1)⊢ (∀ (i : Fin n1),
    ?m.96 (fun i => (basisIdxCongr ⋯) (p (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (p (Fin.natAdd n1 i))) i =
      p (Fin.castAdd n2 i)) ∧
  ∀ (j : Fin n2),
    ?m.97 (fun i => (basisIdxCongr ⋯) (p (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (p (Fin.natAdd n1 i))) j =
      p (Fin.natAdd n1 j)unsolved goals
k C G:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1 n2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx (Fin.append c c1)⊢ (∀ (i : Fin n1),
    ?m.96 (fun i => (basisIdxCongr ⋯) (p (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (p (Fin.natAdd n1 i))) i =
      p (Fin.castAdd n2 i)) ∧
  ∀ (j : Fin n2),
    ?m.97 (fun i => (basisIdxCongr ⋯) (p (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (p (Fin.natAdd n1 i))) j =
      p (Fin.natAdd n1 j)unsolved goals
k C G:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1 n2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx (Fin.append c c1)⊢ (∀ (i : Fin n1),
    ?m.96 (fun i => (basisIdxCongr ⋯) (p (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (p (Fin.natAdd n1 i))) i =
      p (Fin.castAdd n2 i)) ∧
  ∀ (j : Fin n2),
    ?m.97 (fun i => (basisIdxCongr ⋯) (p (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (p (Fin.natAdd n1 i))) j =
      p (Fin.natAdd n1 j)unsolved goals
k C G:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1 n2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx (Fin.append c c1)⊢ (∀ (i : Fin n1),
    ?m.96 (fun i => (basisIdxCongr ⋯) (p (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (p (Fin.natAdd n1 i))) i =
      p (Fin.castAdd n2 i)) ∧
  ∀ (j : Fin n2),
    ?m.97 (fun i => (basisIdxCongr ⋯) (p (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (p (Fin.natAdd n1 i))) j =
      p (Fin.natAdd n1 j)
def ComponentIdx.prod {n1 n2 : ℕ} {c : Fin n1 → C} {c1 : Fin n2 → C} :
    ComponentIdx (S := S) (Fin.append c c1) ≃
      ComponentIdx (S := S) c × ComponentIdx (S := S) c1 where
  toFun p := (fun i => basisIdxCongr (byk:TypeC:TypeG:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx (Fin.append c c1)i:Fin n1⊢ Fin.append c c1 (Fin.castAdd n2 i) = c i simpAll goals completed! 🐙) (p (Fin.castAdd n2 i)),
    fun i => basisIdxCongr (byk:TypeC:TypeG:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx (Fin.append c c1)i:Fin n2⊢ Fin.append c c1 (Fin.natAdd n1 i) = c1 i simpAll goals completed! 🐙) (p (Fin.natAdd n1 i)))
  invFun p := Fin.addCases (fun i => basisIdxCongr (byk:TypeC:TypeG:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx c × ComponentIdx c1i:Fin n1⊢ c i = Fin.append c c1 (Fin.castAdd n2 i) simpAll goals completed! 🐙) (p.1 i))
    (fun i => basisIdxCongr (byk:TypeC:TypeG:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx c × ComponentIdx c1i:Fin n2⊢ c1 i = Fin.append c c1 (Fin.natAdd n1 i) simpAll goals completed! 🐙) (p.2 i))
  left_inv p := unsolved goals
k C G:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1 n2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx (Fin.append c c1)⊢ (∀ (i : Fin n1),
    ?m.96 (fun i => (basisIdxCongr ⋯) (p (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (p (Fin.natAdd n1 i))) i =
      p (Fin.castAdd n2 i)) ∧
  ∀ (j : Fin n2),
    ?m.97 (fun i => (basisIdxCongr ⋯) (p (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (p (Fin.natAdd n1 i))) j =
      p (Fin.natAdd n1 j)byk:TypeC:TypeG:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx (Fin.append c c1)⊢ (fun p i => Fin.addCases ?m.94 ?m.95 i)
    ((fun p => (fun i => (basisIdxCongr ⋯) (p (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (p (Fin.natAdd n1 i))))
      p) =
  p
    ext1 ik:TypeC:TypeG:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx (Fin.append c c1)i:Fin (n1 + n2)⊢ (fun p i => Fin.addCases ?m.94 ?m.95 i)
    ((fun p => (fun i => (basisIdxCongr ⋯) (p (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (p (Fin.natAdd n1 i)))) p)
    i =
  p i
    revert ik:TypeC:TypeG:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx (Fin.append c c1)⊢ ∀ (i : Fin (n1 + n2)),
  (fun p i => Fin.addCases ?m.94 ?m.95 i)
      ((fun p => (fun i => (basisIdxCongr ⋯) (p (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (p (Fin.natAdd n1 i))))
        p)
      i =
    p i
    simp [Fin.forall_fin_add]k:TypeC:TypeG:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx (Fin.append c c1)⊢ (∀ (i : Fin n1),
    ?m.96 (fun i => (basisIdxCongr ⋯) (p (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (p (Fin.natAdd n1 i))) i =
      p (Fin.castAdd n2 i)) ∧
  ∀ (j : Fin n2),
    ?m.97 (fun i => (basisIdxCongr ⋯) (p (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (p (Fin.natAdd n1 i))) j =
      p (Fin.natAdd n1 j)
  right_inv p := unsolved goals
k C G:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1 n2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx c × ComponentIdx c1⊢ (fun i => (basisIdxCongr ⋯) (?m.94 i), fun i => (basisIdxCongr ⋯) (?m.95 i)) = pbyk:TypeC:TypeG:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx c × ComponentIdx c1⊢ (fun p => (fun i => (basisIdxCongr ⋯) (p (Fin.castAdd n2 i)), fun i => (basisIdxCongr ⋯) (p (Fin.natAdd n1 i))))
    ((fun p i => Fin.addCases ?m.94 ?m.95 i) p) =
  p simpk:TypeC:TypeG:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx c × ComponentIdx c1⊢ (fun i => (basisIdxCongr ⋯) (?m.94 i), fun i => (basisIdxCongr ⋯) (?m.95 i)) = p

@[simp]
lemma ComponentIdx.prod_symm_natAdd {n1 n2 : ℕ} {c : Fin n1 → C} {c1 : Fin n2 → C}
    (p : ComponentIdx (S := S) c) (q : ComponentIdx (S := S) c1) (i : Fin n2) :
    ComponentIdx.prod.symm (p, q) (Fin.natAdd n1 i) =
      basisIdxCongr (byk:TypeC:TypeG:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx cq:ComponentIdx c1i:Fin n2⊢ c1 i = Fin.append c c1 (Fin.natAdd n1 i) simpAll goals completed! 🐙) (q i) := byk:TypeC:TypeG:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx cq:ComponentIdx c1i:Fin n2⊢ prod.symm (p, q) (Fin.natAdd n1 i) = (basisIdxCongr ⋯) (q i) simp [ComponentIdx.prod]All goals completed! 🐙

@[simp]
lemma ComponentIdx.prod_symm_castAdd {n1 n2 : ℕ} {c : Fin n1 → C} {c1 : Fin n2 → C}
    (p : ComponentIdx (S := S) c) (q : ComponentIdx (S := S) c1) (i : Fin n1) :
    ComponentIdx.prod.symm (p, q) (Fin.castAdd n2 i) =
      basisIdxCongr (byk:TypeC:TypeG:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx cq:ComponentIdx c1i:Fin n1⊢ c i = Fin.append c c1 (Fin.castAdd n2 i) simpAll goals completed! 🐙) (p i) := byk:TypeC:TypeG:Typeinst✝⁵:CommRing kinst✝⁴: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 bn1:ℕn2:ℕc:Fin n1 → Cc1:Fin n2 → Cp:ComponentIdx cq:ComponentIdx c1i:Fin n1⊢ prod.symm (p, q) (Fin.castAdd n2 i) = (basisIdxCongr ⋯) (p i) simp [ComponentIdx.prod]All goals completed! 🐙