Pure tensors

A pure tensor is one of the form ψ1 ⊗ ψ2 ⊗ ... ⊗ ψn. We say a tensor is pure if it is of this form.

def TensorSpecies.Pure (S : TensorSpecies) (c : IndexNotation.OverColor S.C) : Type

The type of tensors specified by a map to colors c : OverColor S.C.

Equations

• S.Pure c = ((i : c.left) → ↑(S.FD.obj { as := c.hom i }).V)

def TensorSpecies.Pure.ρ {S : TensorSpecies} {c : IndexNotation.OverColor S.C} (g : S.G) (p : S.Pure c) : S.Pure c

The group action on a pure tensor.

Equations

• TensorSpecies.Pure.ρ g p i = ((S.FD.obj { as := c.hom i }).ρ g) (p i)

def TensorSpecies.Pure.tprod {S : TensorSpecies} {c : IndexNotation.OverColor S.C} (p : S.Pure c) : ↑(S.F.obj c).V

The underlying tensor of a pure tensor.

Equations

• p.tprod = (PiTensorProduct.tprod S.k) p

theorem TensorSpecies.Pure.tprod_equivariant {S : TensorSpecies} {c : IndexNotation.OverColor S.C} (g : S.G) (p : S.Pure c) : (ρ g p).tprod = ((S.F.obj c).ρ g) p.tprod

The map tprod is equivariant with respect to the group action.

def TensorSpecies.IsPure (S : TensorSpecies) {c : IndexNotation.OverColor S.C} (t : ↑(S.F.obj c).V) : Prop

A tensor is pure if it is ⨂[S.k] i, p i for some p : Pure c.

Equations

• S.IsPure t = ∃ (p : S.Pure c), t = p.tprod

theorem TensorSpecies.zero_isPure (S : TensorSpecies) {c : IndexNotation.OverColor S.C} [h : Nonempty c.left] : S.IsPure 0

As long as we are dealing with tensors with at least one index, then the zero tensor is pure.

@[simp]

theorem TensorSpecies.Pure.tprod_isPure (S : TensorSpecies) {c : IndexNotation.OverColor S.C} (p : S.Pure c) : S.IsPure p.tprod

@[simp]

theorem TensorSpecies.action_isPure_iff_isPure (S : TensorSpecies) {c : IndexNotation.OverColor S.C} {ψ : ↑(S.F.obj c).V} (g : S.G) : S.IsPure (((S.F.obj c).ρ g) ψ) ↔ S.IsPure ψ