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 Mathlib.RepresentationTheory.Rep.Basic
public import Physlib.Mathematics.PiTensorProduct
public import Mathlib.Algebra.Lie.OfAssociative
public import Physlib.Meta.TODO.BasicTensor species
A tensor species is a structure including all of the ingredients needed to define a type of tensor.
Examples of tensor species will include real Lorentz tensors, complex Lorentz tensors, and Einstein tensors.
Tensor species are built upon symmetric monoidal categories.
@[expose] public sectionTODO "Include in the condition of `TensorSpecies` a relationship between
the metrics and the basis vectors."
The structure TensorSpecies contains the necessary structure needed to define
a system of tensors with index notation. Examples of TensorSpecies include real Lorentz tensors,
complex Lorentz tensors, and ordinary Euclidean tensors.
A map from C to C. An involution.
The condition that τ is an involution.
The contraction of vectors with dual colors.
The invariant unit tensor for a given color.
The invariant metric tensor for a given color.
Contraction is symmetric with respect to duals.
The unit is symmetric.
Contraction with unit leaves invariant.
On contracting metrics we get the unit.
structure TensorSpecies (k : Type) [CommRing k] (C : Type) (G : Type) [Group G]
(V : C → Type) [∀ c, AddCommGroup (V c)] [∀ c, Module k (V c)]
(basisIdx : C → Type) [∀ c, Fintype (basisIdx c)] [∀ c, DecidableEq (basisIdx c)]
(rep : (c : C) → Representation k G (V c)) (basis : (c : C) → Basis (basisIdx c) k (V c)) where τ : C → C τ_involution : Function.Involutive τ contr : (c : C) → ((rep c).tprod (rep (τ c))).IntertwiningMap (Representation.trivial k G k) unit : (c : C) → ((Representation.trivial k G k)).IntertwiningMap ((rep (τ c)).tprod (rep c)) metric : (c : C) → ((Representation.trivial k G k)).IntertwiningMap ((rep c).tprod (rep c)) contr_tmul_symm : ∀ c (x : V c) (y : V (τ c)),
contr c (x ⊗ₜ[k] y) = contr (τ c) (y ⊗ₜ Equiv.cast (congrArg V (τ_involution c).symm) x) unit_symm : ∀ c, unit c (1 : k) =
LinearMap.lTensor _ (LinearEquiv.cast (τ_involution c)).toLinearMap
(TensorProduct.comm k _ _ (unit (τ c) (1 : k))) contr_unit : ∀ c (x : V c),
(TensorProduct.lid k _ <|
(contr c).toLinearMap.rTensor _ <|
(TensorProduct.assoc k (V c) (V (τ c)) (V c)).symm <|
x ⊗ₜ[k] (unit c (1 : k))) = x contr_metric : ∀ c,
(TensorProduct.comm k _ _ <|
(TensorProduct.lid k _).lTensor _ <|
((contr c).toLinearMap.rTensor (V (τ c))).lTensor (V c) <|
(TensorProduct.assoc k (V c) (V (τ c)) (V (τ c))).symm.toLinearMap.lTensor (V c) <|
TensorProduct.assoc k (V c) (V c) (V (τ c) ⊗[k] V (τ c)) <|
(metric c 1) ⊗ₜ[k] (metric (τ c) 1)) = unit c (1 : k)Properties of the basis
The casting between basisIdx c and basisIdx c1.
def basisIdxCongr {c c1 : C} (h : c = c1) :
basisIdx c ≃ basisIdx c1 := Equiv.cast (G:Type ?u.7k:Typeinst✝¹:CommRing kC:Typeinst✝:Group GbasisIdx:C → Typec:Cc1:Ch:c = c1⊢ basisIdx c = basisIdx c1 All goals completed! 🐙)@[simp]
lemma basisIdxCongr_rfl (c : C) (i : basisIdx c) :
basisIdxCongr (Eq.refl c) i = i := rfllemma basisIdxCongr_symm {c c1 : C} (h : c = c1) (i : basisIdx c1) :
(basisIdxCongr h).symm i = basisIdxCongr h.symm i := C:TypebasisIdx:C → Typec:Cc1:Ch:c = c1i:basisIdx c1⊢ (basisIdxCongr h).symm i = (basisIdxCongr ⋯) i
C:TypebasisIdx:C → Typec:Ci:basisIdx c⊢ (basisIdxCongr ⋯).symm i = (basisIdxCongr ⋯) i
All goals completed! 🐙@[simp]
lemma basisIdxCongr_apply_apply {c c1 c2 : C} (h1 : c = c1) (h2 : c1 = c2) (i : basisIdx c) :
basisIdxCongr h2 (basisIdxCongr h1 i) = basisIdxCongr (G:Type ?u.7k:Typeinst✝¹:CommRing kC:Typeinst✝:Group GbasisIdx:C → Typec:Cc1:Cc2:Ch1:c = c1h2:c1 = c2i:basisIdx c⊢ c = c2 All goals completed! 🐙) i := C:TypebasisIdx:C → Typec:Cc1:Cc2:Ch1:c = c1h2:c1 = c2i:basisIdx c⊢ (basisIdxCongr h2) ((basisIdxCongr h1) i) = (basisIdxCongr ⋯) i
All goals completed! 🐙
basisIdxCongr only depends on its endpoints up to HEq of the arguments: equal target
colours and heterogeneously equal labels give equal casts.
lemma basisIdxCongr_heq_arg {c1 c2 d : C} (h1 : c1 = d) (h2 : c2 = d)
{x : basisIdx c1} {y : basisIdx c2} (hxy : HEq x y) :
basisIdxCongr h1 x = basisIdxCongr h2 y := C:TypebasisIdx:C → Typec1:Cc2:Cd:Ch1:c1 = dh2:c2 = dx:basisIdx c1y:basisIdx c2hxy:x ≍ y⊢ (basisIdxCongr h1) x = (basisIdxCongr h2) y
C:TypebasisIdx:C → Typec1:Cc2:Cx:basisIdx c1y:basisIdx c2hxy:x ≍ yh2:c2 = c1⊢ (basisIdxCongr ⋯) x = (basisIdxCongr h2) y; C:TypebasisIdx:C → Typec2:Cy:basisIdx c2x:basisIdx c2hxy:x ≍ y⊢ (basisIdxCongr ⋯) x = (basisIdxCongr ⋯) y; C:TypebasisIdx:C → Typec2:Cy:basisIdx c2⊢ (basisIdxCongr ⋯) y = (basisIdxCongr ⋯) y; All goals completed! 🐙@[simp]
lemma τ_τ_apply (c : C) : S.τ (S.τ c) = c := S.τ_involution comit [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] in
lemma basis_congr {c c1 : C} (h : c = c1) (i : basisIdx c) :
basis c i = LinearEquiv.cast (R := k) h.symm (basis c1 (basisIdxCongr h i)) := k:Typeinst✝²:CommRing kC:TypeV:C → Typeinst✝¹:(c : C) → AddCommGroup (V c)inst✝:(c : C) → Module k (V c)basisIdx:C → Typebasis:(c : C) → Basis (basisIdx c) k (V c)c:Cc1:Ch:c = c1i:basisIdx c⊢ (basis c) i = (LinearEquiv.cast ⋯) ((basis c1) ((basisIdxCongr h) i))
k:Typeinst✝²:CommRing kC:TypeV:C → Typeinst✝¹:(c : C) → AddCommGroup (V c)inst✝:(c : C) → Module k (V c)basisIdx:C → Typebasis:(c : C) → Basis (basisIdx c) k (V c)c:Ci:basisIdx c⊢ (basis c) i = (LinearEquiv.cast ⋯) ((basis c) ((basisIdxCongr ⋯) i))
All goals completed! 🐙omit [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] in
lemma map_basis_eq {c c1 : C} (h : c = c1) (i : basisIdx c) :
LinearEquiv.cast (R := k) h (basis c i) = basis c1 (basisIdxCongr h i) := k:Typeinst✝²:CommRing kC:TypeV:C → Typeinst✝¹:(c : C) → AddCommGroup (V c)inst✝:(c : C) → Module k (V c)basisIdx:C → Typebasis:(c : C) → Basis (basisIdx c) k (V c)c:Cc1:Ch:c = c1i:basisIdx c⊢ (LinearEquiv.cast h) ((basis c) i) = (basis c1) ((basisIdxCongr h) i)
k:Typeinst✝²:CommRing kC:TypeV:C → Typeinst✝¹:(c : C) → AddCommGroup (V c)inst✝:(c : C) → Module k (V c)basisIdx:C → Typebasis:(c : C) → Basis (basisIdx c) k (V c)c:Ci:basisIdx c⊢ (LinearEquiv.cast ⋯) ((basis c) i) = (basis c) ((basisIdxCongr ⋯) i)
All goals completed! 🐙
The number of indices n from a tensor.
set_option linter.unusedVariables false in@[nolint unusedArguments]
def numIndices {S : TensorSpecies k C G V basisIdx rep basis} {n : ℕ} {c : Fin n → C}
(_ : PiTensorProduct k (fun i => V (c i))) : ℕ := n