PhysLean Documentation

PhysLean.Relativity.Tensors.TensorSpecies.Basic

Tensor species #

structure TensorSpecies (k : Type) [CommRing k] (C G : Type) [Group G] :

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.

Instances For
    instance TensorSpecies.instNeZeroNatRepDim {G k : Type} [CommRing k] {C : Type} [Group G] (S : TensorSpecies k C G) (c : C) :

    The field repDim of a TensorSpecies is non-zero for all colors.

    @[simp]
    theorem TensorSpecies.τ_τ_apply {G k : Type} [CommRing k] {C : Type} [Group G] (S : TensorSpecies k C G) (c : C) :
    S.τ (S.τ c) = c
    theorem TensorSpecies.basis_congr {G k : Type} [CommRing k] {C : Type} [Group G] (S : TensorSpecies k C G) {c c1 : C} (h : c = c1) (i : Fin (S.repDim c)) :
    theorem TensorSpecies.basis_congr_repr {G k : Type} [CommRing k] {C : Type} [Group G] (S : TensorSpecies k C G) {c c1 : C} (h : c = c1) (i : Fin (S.repDim c)) (t : (S.FD.obj { as := c }).V) :
    theorem TensorSpecies.FD_map_basis {G k : Type} [CommRing k] {C : Type} [Group G] (S : TensorSpecies k C G) {c c1 : C} (h : c = c1) (i : Fin (S.repDim c)) :

    The lift of the functor S.F to functor.

    Equations
    Instances For
      instance TensorSpecies.F_braided {G k : Type} [CommRing k] {C : Type} [Group G] (S : TensorSpecies k C G) :

      The functor F is braided.

      Equations

      Casts an element of the monoidal unit of Rep k G to the field k.

      Equations
      Instances For
        def TensorSpecies.castFin0ToField {G k : Type} [CommRing k] {C : Type} [Group G] (S : TensorSpecies k C G) {c : Fin 0C} :

        Casts an element of (S.F.obj (OverColor.mk c)).V for c a map from Fin 0 to an element of the field.

        Equations
        Instances For
          theorem TensorSpecies.castFin0ToField_tprod {G k : Type} [CommRing k] {C : Type} [Group G] (S : TensorSpecies k C G) {c : Fin 0C} (x : (i : Fin 0) → (S.FD.obj { as := c i }).V) :

          Some properties of contractions #

          def TensorSpecies.numIndices {G k : Type} [CommRing k] {C : Type} [Group G] {S : TensorSpecies k C G} {n : } {c : Fin nC} :

          The number of indices n from a tensor.

          Equations
          Instances For