Physlib.Relativity.Tensors.OfInt

Imports

/-
Copyright (c) 2024 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.Basic

Basis for tensors in a tensor species

@[expose] public section

A tensor with integer components with respect to the basis.

abbrev TensorInt {n : ℕ} (c : Fin n → C) := (ComponentIdx (S := S) c) → ℤ

lemma basis_repr_apply {n : ℕ} {c : Fin n → C}
    (f : TensorInt S c) (b : ComponentIdx c) :
    (Tensor.basis c).repr (toTensor f) b = Int.cast (f 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin n → Cf:TensorInt S cb:ComponentIdx c⊢ ((basis c).repr f.toTensor) b = ↑(f b)
  simp only [toTensor, Basis.repr_symm_apply, Basis.repr_linearCombination]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 → Cf:TensorInt S cb:ComponentIdx c⊢ ((Finsupp.linearEquivFunOnFinite k k ((j : Fin n) → basisIdx (c j))).symm fun j => ↑(f j)) b = ↑(f b)
  rflAll goals completed! 🐙



lemma basis_eq_tensorInt {n : ℕ} {c : Fin n → C}
    (b : ComponentIdx c) :
    Tensor.basis c b = TensorInt.toTensor (S := S) (fun b' => if b = b' then 1 else 0) := 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) → Basis (basisIdx c) k (V c)S:TensorSpecies k C G V basisIdx rep b✝n:ℕc:Fin n → Cb:ComponentIdx c⊢ (basis c) b = TensorInt.toTensor fun b' => if b = b' then 1 else 0
  apply (Tensor.basis c).repr.injectivek: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 → Cb:ComponentIdx c⊢ (basis c).repr ((basis c) b) = (basis c).repr (TensorInt.toTensor fun b' => if b = b' then 1 else 0)
  simp only [Basis.repr_self]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 → Cb:ComponentIdx c⊢ Finsupp.single b 1 = (basis c).repr (TensorInt.toTensor fun b' => if b = b' then 1 else 0)
  ext 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 → Cb:ComponentIdx cb':ComponentIdx c⊢ (Finsupp.single b 1) b' = ((basis c).repr (TensorInt.toTensor fun b' => if b = b' then 1 else 0)) b'
  simp only [TensorInt.basis_repr_apply, Int.cast_ite, Int.cast_one, Int.cast_zero]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 → Cb:ComponentIdx cb':ComponentIdx c⊢ (Finsupp.single b 1) b' = if b = b' then 1 else 0
  rw [Finsupp.single_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 b✝n:ℕc:Fin n → Cb:ComponentIdx cb':ComponentIdx c⊢ (if b = b' then 1 else 0) = if b = b' then 1 else 0All goals completed! 🐙]All goals completed! 🐙