PhysLean Documentation

PhysLean.Relativity.Tensors.TensorSpecies.UnitTensor

Units as tensors #

source
def TensorSpecies.unitTensor (S : TensorSpecies) (c : S.C) :
↑(S.F.obj (IndexNotation.OverColor.mk ![S.τ c, c])).V

The unit of a tensor species in a PiTensorProduct.

Equations
Instances For
    source
    theorem TensorSpecies.unitTensor_congr {S : TensorSpecies} {c c' : S.C} (h : c = c') :
    (TensorTree.tensorNode (S.unitTensor c)).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (Equiv.refl (Fin (Nat.succ 0).succ)) ⋯) (TensorTree.tensorNode (S.unitTensor c'))).tensor

    The relation between two units of colors which are equal.

    source
    theorem TensorSpecies.pairIsoSep_inv_unitTensor {S : TensorSpecies} (c : S.C) :
    (CategoryTheory.ConcreteCategory.hom (IndexNotation.OverColor.Discrete.pairIsoSep S.FD).inv.hom) (S.unitTensor c) = (CategoryTheory.ConcreteCategory.hom (S.unit.app { as := c }).hom) 1

    Applying Discrete.pairIsoSep inv to unitTensor returns the unit natural transformation evaluated at 1.

    source
    theorem TensorSpecies.unitTensor_eq_dual_perm {S : TensorSpecies} (c : S.C) :
    (TensorTree.tensorNode (S.unitTensor c)).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![1, 0] ![1, 0] ⋯ ⋯) ⋯) (TensorTree.tensorNode (S.unitTensor (S.τ c)))).tensor

    The unit tensor is equal to a permutation of indices of the dual tensor.

    source
    theorem TensorSpecies.dual_unitTensor_eq_perm {S : TensorSpecies} (c : S.C) :
    (TensorTree.tensorNode (S.unitTensor (S.τ c))).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (PhysLean.Fin.finMapToEquiv ![1, 0] ![1, 0] ⋯ ⋯) ⋯) (TensorTree.tensorNode (S.unitTensor c))).tensor

    The unit tensor of the dual of a color c is equal to the unit tensor of c with indices permuted.

    source
    theorem TensorSpecies.contrOneTwoLeft_unitTensor {S : TensorSpecies} {c1 : S.C} (x : ↑(S.F.obj (IndexNotation.OverColor.mk ![c1])).V) :
    contrOneTwoLeft x (S.unitTensor c1) = x

    Applying contrOneTwoLeft with the unit tensor is the identity map.

    source
    theorem TensorSpecies.vec_contr_unitTensor_eq_self {S : TensorSpecies} {c1 : S.C} (x : ↑(S.F.obj (IndexNotation.OverColor.mk ![c1])).V) :
    (TensorTree.contr 0 0 ⋯ ((TensorTree.tensorNode x).prod (TensorTree.tensorNode (S.unitTensor c1)))).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (Equiv.refl (Fin (Nat.succ 0))) ⋯) (TensorTree.tensorNode x)).tensor

    Contracting a vector with a unit tensor returns the vector.

    source
    theorem TensorSpecies.unitTensor_contr_vec_eq_self {S : TensorSpecies} {c1 : S.C} (x : ↑(S.F.obj (IndexNotation.OverColor.mk ![S.τ c1])).V) :
    (TensorTree.contr 1 1 ⋯ ((TensorTree.tensorNode (S.unitTensor c1)).prod (TensorTree.tensorNode x))).tensor = (TensorTree.perm (IndexNotation.OverColor.equivToHomEq (Equiv.refl (Fin (Nat.succ 0))) ⋯) (TensorTree.tensorNode x)).tensor

    Contracting a unit tensor with a vector returns the unit vector.