Tensorial class #
The tensorial class is used to define a tensorial structure on a type M via
a linear equivalence to a tensor of a TensorSpecies.
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
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) }
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 := ⋯ }
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.