Tensorial class

i. Overview

We define a class called Tensorial. This class is used to enable the use of index notation on a type M via a linear equivalence to a tensor of a TensorSpecies.

We define the class Tensorial here, and provide an API around its use.

ii. Key results

• Tensorial : The class used to allow index notation on a type M.
• Tensorial.numIndices : The number of indices of an element of an M carrying a tensorial instance.
• Tensorial.mulAction : The action of the group G on a type M carrying a tensorial instance.
• Tensorial.prod : The product of two tensorial instances is a tensorial instance.

iii. Table of contents

• A. Defining the tensorial class
  • A.1. Tensors carry a tensorial instance
  • A.2. The number of indices
• B. The action of the group on a module with a tensorial instance
  • B.1. Relation between the action and the equivalence to tensors
  • B.2. Linear properties of the action
  • B.3. The action as a linear map
  • B.4. The SMulCommClass property
• C. Properties of the basis
• D. Products of tensorial instances
  • D.1. The equivalence to tensors on products
  • D.2. The group action on products
  • D.3. The basis on products
• E. Continuous properties
  • E.1. Finite dimensionality
  • E.2. The map to tensors as a continuous linear equivalence
  • E.3. The Lorentz action as a continuous linear equivalence

iv. References

There are no known references for this material.

A. Defining the tensorial class

We first define the Tensorial class.

class TensorSpecies.Tensorial {k : outParam Type} [CommRing k] {C G : outParam Type} [Group G] {n : outParam ℕ} (S : outParam (TensorSpecies k C G)) (c : outParam (Fin n → C)) (M : Type) [AddCommMonoid M] [Module k M] : Type

The tensorial class is used to define a tensor structure on a type M through a linear equivalence with a module S.Tensor c for S a tensor species.

• toTensor : M ≃ₗ[k] S.Tensor c

  The equivalence between M and S.Tensor c in a tensorial instance.

A.1. Tensors carry a tensorial instance

The module of tensors of a tensor species carries a canonical tensorial instance, through the equivalence.

noncomputable instance TensorSpecies.Tensorial.self {k : Type} [CommRing k] {C G : Type} [Group G] {n : ℕ} (S : TensorSpecies k C G) (c : Fin n → C) : S.Tensorial c (S.Tensor c)

Equations

• TensorSpecies.Tensorial.self S c = { toTensor := LinearEquiv.refl k (S.Tensor c) }

@[simp]

theorem TensorSpecies.Tensorial.self_toTensor_apply {k : Type} [CommRing k] {C G : Type} [Group G] {n : ℕ} (S : TensorSpecies k C G) (c : Fin n → C) (t : S.Tensor c) : toTensor t = t

A.2. The number of indices

def TensorSpecies.Tensorial.numIndices {k : Type} [CommRing k] {C G : Type} [Group G] {S : TensorSpecies k C G} {n : ℕ} {c : Fin n → C} {M : Type} [AddCommMonoid M] [Module k M] (t : M) [S.Tensorial c M] : ℕ

The number of indices of a elements t : M where M carries a tensorial instance.

Equations

• TensorSpecies.Tensorial.numIndices t = TensorSpecies.numIndices (TensorSpecies.Tensorial.toTensor t)

B. The action of the group on a module with a tensorial instance

We now define the action of the group G on a type M carrying a tensorial instance.

@[instance 10000]

noncomputable instance TensorSpecies.Tensorial.smulAction {k : Type} [CommRing k] {C G : Type} [Group G] {S : TensorSpecies k C G} {n : ℕ} {c : Fin n → C} {M : Type} [AddCommMonoid M] [Module k M] [S.Tensorial c M] : SMul G M

Equations

• TensorSpecies.Tensorial.smulAction = { smul := fun (g : G) (m : M) => TensorSpecies.Tensorial.toTensor.symm (g • TensorSpecies.Tensorial.toTensor m) }

noncomputable instance TensorSpecies.Tensorial.mulAction {k : Type} [CommRing k] {C G : Type} [Group G] {S : TensorSpecies k C G} {n : ℕ} {c : Fin n → C} {M : Type} [AddCommMonoid M] [Module k M] [S.Tensorial c M] : MulAction G M

Equations

• TensorSpecies.Tensorial.mulAction = { toSMul := TensorSpecies.Tensorial.smulAction, mul_smul := ⋯, one_smul := ⋯ }

B.1. Relation between the action and the equivalence to tensors

theorem TensorSpecies.Tensorial.smul_eq {k : Type} [CommRing k] {C G : Type} [Group G] {S : TensorSpecies k C G} {n : ℕ} {c : Fin n → C} {M : Type} [AddCommMonoid M] [Module k M] {g : G} {t : M} [S.Tensorial c M] : g • t = toTensor.symm (g • toTensor t)

theorem TensorSpecies.Tensorial.toTensor_smul {k : Type} [CommRing k] {C G : Type} [Group G] {S : TensorSpecies k C G} {n : ℕ} {c : Fin n → C} {M : Type} [AddCommMonoid M] [Module k M] {g : G} {t : M} [S.Tensorial c M] : toTensor (g • t) = g • toTensor t

theorem TensorSpecies.Tensorial.smul_toTensor_symm {k : Type} [CommRing k] {C G : Type} [Group G] {S : TensorSpecies k C G} {n : ℕ} {c : Fin n → C} {M : Type} [AddCommMonoid M] [Module k M] {g : G} {t : S.Tensor c} [self : S.Tensorial c M] : g • toTensor.symm t = toTensor.symm (g • t)

B.2. Linear properties of the action

@[instance 10000]

noncomputable instance TensorSpecies.Tensorial.distribMulAction {k : Type} [CommRing k] {C G : Type} [Group G] {S : TensorSpecies k C G} {n : ℕ} {c : Fin n → C} {M : Type} [AddCommMonoid M] [Module k M] [S.Tensorial c M] : DistribMulAction G M

Equations

• TensorSpecies.Tensorial.distribMulAction = { toMulAction := TensorSpecies.Tensorial.mulAction, smul_zero := ⋯, smul_add := ⋯ }

B.3. The action as a linear map

noncomputable def TensorSpecies.Tensorial.smulLinearMap {k : Type} [CommRing k] {C G : Type} [Group G] {S : TensorSpecies k C G} {n : ℕ} {c : Fin n → C} {M : Type} [AddCommMonoid M] [Module k M] (g : G) [S.Tensorial c M] : M →ₗ[k] M

The action of the group on a Tensorial instance as a linear map.

Equations

• TensorSpecies.Tensorial.smulLinearMap g = { toFun := fun (m : M) => g • m, map_add' := ⋯, map_smul' := ⋯ }

theorem TensorSpecies.Tensorial.smulLinearMap_apply {k : Type} [CommRing k] {C G : Type} [Group G] {S : TensorSpecies k C G} {n : ℕ} {c : Fin n → C} {M : Type} [AddCommMonoid M] [Module k M] {g : G} [S.Tensorial c M] (m : M) : (smulLinearMap g) m = g • m

B.4. The SMulCommClass property

instance TensorSpecies.Tensorial.instSMulCommClass {k : Type} [CommRing k] {C G : Type} [Group G] {S : TensorSpecies k C G} {n : ℕ} {c : Fin n → C} {M : Type} [AddCommMonoid M] [Module k M] [S.Tensorial c M] : SMulCommClass k G M

C. Properties of the basis

We now prove some properties of the basis induced on a Tensorial instance.

theorem TensorSpecies.Tensorial.basis_toTensor_apply {k : Type} [CommRing k] {C G : Type} [Group G] {S : TensorSpecies k C G} {n : ℕ} {c : Fin n → C} {M : Type} [AddCommMonoid M] [Module k M] [S.Tensorial c M] (m : M) : (Tensor.basis c).repr (toTensor m) = ((Tensor.basis c).map toTensor.symm).repr m

D. Products of tensorial instances

@[instance 10000]

noncomputable instance TensorSpecies.Tensorial.prod {k : Type} [CommRing k] {C G : Type} [Group G] {S : TensorSpecies k C G} {n : ℕ} {c : Fin n → C} {M : Type} [AddCommMonoid M] [Module k M] [S.Tensorial c M] {n2 : ℕ} {c2 : Fin n2 → C} {M₂ : Type} [AddCommMonoid M₂] [Module k M₂] [S.Tensorial c2 M₂] : S.Tensorial (Fin.append c c2) (TensorProduct k M M₂)

Equations

• TensorSpecies.Tensorial.prod = { toTensor := (TensorProduct.congr TensorSpecies.Tensorial.toTensor TensorSpecies.Tensorial.toTensor).trans TensorSpecies.Tensor.tensorEquivProd }

D.1. The equivalence to tensors on products

theorem TensorSpecies.Tensorial.toTensor_tprod {k : Type} [CommRing k] {C G : Type} [Group G] {S : TensorSpecies k C G} {n : ℕ} {c : Fin n → C} {M : Type} [AddCommMonoid M] [Module k M] {n2 : ℕ} {c2 : Fin n2 → C} {M₂ : Type} [S.Tensorial c M] [AddCommMonoid M₂] [Module k M₂] [S.Tensorial c2 M₂] (m : M) (m2 : M₂) : toTensor (m ⊗ₜ[k] m2) = (Tensor.prodT (toTensor m)) (toTensor m2)

D.2. The group action on products

theorem TensorSpecies.Tensorial.smul_prod {k : Type} [CommRing k] {C G : Type} [Group G] {S : TensorSpecies k C G} {n : ℕ} {c : Fin n → C} {M : Type} [AddCommMonoid M] [Module k M] {n2 : ℕ} {c2 : Fin n2 → C} {M₂ : Type} [S.Tensorial c M] [AddCommMonoid M₂] [Module k M₂] [S.Tensorial c2 M₂] (g : G) (m : M) (m2 : M₂) : g • m ⊗ₜ[k] m2 = (g • m) ⊗ₜ[k] (g • m2)

D.3. The basis on products

theorem TensorSpecies.Tensorial.basis_map_prod {k : Type} [CommRing k] {C G : Type} [Group G] {S : TensorSpecies k C G} {n : ℕ} {c : Fin n → C} {M : Type} [AddCommMonoid M] [Module k M] {n2 : ℕ} {c2 : Fin n2 → C} {M₂ : Type} [S.Tensorial c M] [AddCommMonoid M₂] [Module k M₂] [S.Tensorial c2 M₂] : (Tensor.basis (Fin.append c c2)).map toTensor.symm = (((Tensor.basis c).map toTensor.symm).tensorProduct ((Tensor.basis c2).map toTensor.symm)).reindex Tensor.ComponentIdx.prodEquiv.symm

E. Continuous properties

E.1. Finite dimensionality

instance TensorSpecies.Tensorial.instFiniteDimensional {n : ℕ} {k : Type} [RCLike k] {C G : Type} [Group G] (S : TensorSpecies k C G) {c : Fin n → C} {M : Type} [AddCommGroup M] [Module k M] [S.Tensorial c M] : FiniteDimensional k M

E.2. The map to tensors as a continuous linear equivalence

def TensorSpecies.Tensorial.toTensorCLM {n : ℕ} {k : Type} [RCLike k] {C G : Type} [Group G] (S : TensorSpecies k C G) {c : Fin n → C} {M : Type} [AddCommGroup M] [Module k M] [TopologicalSpace M] [IsTopologicalAddGroup M] [ContinuousSMul k M] [S.Tensorial c M] [T2Space M] : M ≃L[k] S.Tensor c

The map from a type carrying an Tensorial instance to tensors, as a continuous linear map.

Equations

• One or more equations did not get rendered due to their size.

E.3. The Lorentz action as a continuous linear equivalence

noncomputable def TensorSpecies.Tensorial.actionCLM {n : ℕ} {k : Type} [RCLike k] {C G : Type} [Group G] (S : TensorSpecies k C G) {c : Fin n → C} {M : Type} [AddCommGroup M] [Module k M] [TopologicalSpace M] (g : G) [IsTopologicalAddGroup M] [ContinuousSMul k M] [S.Tensorial c M] [T2Space M] : M →L[k] M

The Lorentz action on types carrying a tensorial instance as a continuous linear map.

Equations

• TensorSpecies.Tensorial.actionCLM S g = LinearMap.toContinuousLinearMap (TensorSpecies.Tensorial.smulLinearMap g)

theorem TensorSpecies.Tensorial.actionCLM_apply {n : ℕ} {k : Type} [RCLike k] {C G : Type} [Group G] (S : TensorSpecies k C G) {c : Fin n → C} {M : Type} [AddCommGroup M] [Module k M] [TopologicalSpace M] {g : G} [IsTopologicalAddGroup M] [ContinuousSMul k M] [S.Tensorial c M] [T2Space M] (m : M) : (actionCLM S g) m = g • m