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 typeM.Tensorial.numIndices: The number of indices of an element of anMcarrying a tensorial instance.Tensorial.mulAction: The action of the groupGon a typeMcarrying 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
- 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
iv. References #
There are no known references for this material.
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]
:
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.
The equivalence between
MandS.Tensor cin a tensorial instance.
Instances
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)
:
Equations
- TensorSpecies.Tensorial.self S c = { toTensor := LinearEquiv.refl k (S.Tensor c) }
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
Instances For
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.
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 = { smul := fun (g : G) (m : M) => TensorSpecies.Tensorial.toTensor.symm (g • TensorSpecies.Tensorial.toTensor m), one_smul := ⋯, mul_smul := ⋯ }
B.1. Relation between the action and the equivalence to tensors #
B.2. Linear properties of the action #
@[simp]
theorem
TensorSpecies.Tensorial.smul_zero
{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]
{g : G}
:
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]
:
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' := ⋯ }
Instances For
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)
:
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)
:
D. Products of tensorial instances #
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₂)
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₂)
:
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₂)
:
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