Constructors of tensors.

There are a number of ways to construct explicit tensors.

Tensors with a single index.

noncomputable def TensorSpecies.Tensor.Pure.fromSingleP {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} : ↑(S.FD.obj { as := c }).V ≃ₗ[k] Pure S ![c]

The equivalence between S.FD.obj {as := c} and Pure S ![c].

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TensorSpecies.Tensor.fromSingleT {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} : ↑(S.FD.obj { as := c }).V ≃ₗ[k] S.Tensor ![c]

The equivalence between S.FD.obj {as := c} and S.Tensor ![c].

Equations

• One or more equations did not get rendered due to their size.

theorem TensorSpecies.Tensor.fromSingleT_symm_pure {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} (p : Pure S ![c]) : fromSingleT.symm p.toTensor = Pure.fromSingleP.symm p

theorem TensorSpecies.Tensor.fromSingleT_eq_pureT {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} (x : ↑(S.FD.obj { as := c }).V) : fromSingleT x = Pure.toTensor fun (x_1 : Fin (Nat.succ 0)) => match x_1 with | 0 => x

theorem TensorSpecies.Tensor.actionT_fromSingleT {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} (x : ↑(S.FD.obj { as := c }).V) (g : G) : g • fromSingleT x = fromSingleT (((S.FD.obj { as := c }).ρ g) x)

theorem TensorSpecies.Tensor.fromSingleT_map {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c c1 : S.C} (h : { as := c } = { as := c1 }) (x : ↑(S.FD.obj { as := c }).V) : fromSingleT ((CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom h))) x) = (permT id ⋯) (fromSingleT x)

theorem TensorSpecies.Tensor.contrT_fromSingleT_fromSingleT {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} (x : ↑(S.FD.obj { as := c }).V) (y : ↑(S.FD.obj { as := S.τ c }).V) : (contrT 0 0 1 ⋯) ((prodT (fromSingleT x)) (fromSingleT y)) = (CategoryTheory.ConcreteCategory.hom (S.contr.app { as := c })) (x ⊗ₜ[k] y) • default.toTensor

Tensors with two indices.

fromPairT

noncomputable def TensorSpecies.Tensor.fromPairT {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c1 c2 : S.C} : TensorProduct k ↑(S.FD.obj { as := c1 }).V ↑(S.FD.obj { as := c2 }).V →ₗ[k] S.Tensor ![c1, c2]

The construction of a tensor with two indices from the tensor product (S.FD.obj (Discrete.mk c1)).V ⊗[k] (S.FD.obj (Discrete.mk c2)).V defined categorically.

Equations

• One or more equations did not get rendered due to their size.

theorem TensorSpecies.Tensor.fromPairT_tmul {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c1 c2 : S.C} (x : ↑(S.FD.obj { as := c1 }).V) (y : ↑(S.FD.obj { as := c2 }).V) : fromPairT (x ⊗ₜ[k] y) = (permT id ⋯) ((prodT (fromSingleT x)) (fromSingleT y))

theorem TensorSpecies.Tensor.actionT_fromPairT {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c1 c2 : S.C} (x : TensorProduct k ↑(S.FD.obj { as := c1 }).V ↑(S.FD.obj { as := c2 }).V) (g : G) : g • fromPairT x = fromPairT ((TensorProduct.map ((S.FD.obj { as := c1 }).ρ g) ((S.FD.obj { as := c2 }).ρ g)) x)

theorem TensorSpecies.Tensor.fromPairT_map_right {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c1 c2 c2' : S.C} (h : c2 = c2') (x : TensorProduct k ↑(S.FD.obj { as := c1 }).V ↑(S.FD.obj { as := c2 }).V) : fromPairT ((TensorProduct.map LinearMap.id (S.FD.map (CategoryTheory.eqToHom ⋯)).hom.hom') x) = (permT id ⋯) (fromPairT x)

theorem TensorSpecies.Tensor.fromPairT_comm {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c1 c2 : S.C} (x : TensorProduct k ↑(S.FD.obj { as := c1 }).V ↑(S.FD.obj { as := c2 }).V) : fromPairT ((TensorProduct.comm k ↑(S.FD.obj { as := c1 }).V ↑(S.FD.obj { as := c2 }).V) x) = (permT ![1, 0] ⋯) (fromPairT x)

Contraction of fromPairT with fromSingleT

noncomputable def TensorSpecies.Tensor.fromSingleTContrFromPairT {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c c2 : S.C} (x : ↑(S.FD.obj { as := c }).V) (y : TensorProduct k ↑(S.FD.obj { as := S.τ c }).V ↑(S.FD.obj { as := c2 }).V) : S.Tensor ![c2]

The contraction of tensors with one index with one with two indices defined categorically.

Equations

• One or more equations did not get rendered due to their size.

theorem TensorSpecies.Tensor.fromSingleTContrFromPairT_tmul {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c c2 : S.C} (x : ↑(S.FD.obj { as := c }).V) (y1 : ↑(S.FD.obj { as := S.τ c }).V) (y2 : ↑(S.FD.obj { as := c2 }).V) : fromSingleTContrFromPairT x (y1 ⊗ₜ[k] y2) = (CategoryTheory.ConcreteCategory.hom (S.contr.app { as := c })) (x ⊗ₜ[k] y1) • fromSingleT y2

theorem TensorSpecies.Tensor.fromSingleT_contr_fromPairT_tmul {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c c2 : S.C} (x : ↑(S.FD.obj { as := c }).V) (y1 : ↑(S.FD.obj { as := S.τ c }).V) (y2 : ↑(S.FD.obj { as := c2 }).V) : (contrT 1 0 1 ⋯) ((prodT (fromSingleT x)) (fromPairT (y1 ⊗ₜ[k] y2))) = (permT id ⋯) (fromSingleTContrFromPairT x (y1 ⊗ₜ[k] y2))

theorem TensorSpecies.Tensor.contrT_fromSingleT_fromPairT {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c c2 : S.C} (x : ↑(S.FD.obj { as := c }).V) (y : TensorProduct k ↑(S.FD.obj { as := S.τ c }).V ↑(S.FD.obj { as := c2 }).V) : (contrT 1 0 1 ⋯) ((prodT (fromSingleT x)) (fromPairT y)) = (permT id ⋯) (fromSingleTContrFromPairT x y)

Contraction of fromPairT with fromPairT

noncomputable def TensorSpecies.Tensor.fromPairTContr {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c c1 c2 : S.C} (x : TensorProduct k ↑(S.FD.obj { as := c1 }).V ↑(S.FD.obj { as := c }).V) (y : TensorProduct k ↑(S.FD.obj { as := S.τ c }).V ↑(S.FD.obj { as := c2 }).V) : S.Tensor ![c1, c2]

The contraction of tensors with two indices defined categorically.

Equations

• One or more equations did not get rendered due to their size.

theorem TensorSpecies.Tensor.fromPairTContr_tmul_tmul {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c c1 c2 : S.C} (x1 : ↑(S.FD.obj { as := c1 }).V) (x2 : ↑(S.FD.obj { as := c }).V) (y1 : ↑(S.FD.obj { as := S.τ c }).V) (y2 : ↑(S.FD.obj { as := c2 }).V) : fromPairTContr (x1 ⊗ₜ[k] x2) (y1 ⊗ₜ[k] y2) = (CategoryTheory.ConcreteCategory.hom (S.contr.app { as := c })) (x2 ⊗ₜ[k] y1) • fromPairT (x1 ⊗ₜ[k] y2)

theorem TensorSpecies.Tensor.fromPairT_contr_fromPairT_eq_fromPairTContr_tmul {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} (c c1 c2 : S.C) (x1 : ↑(S.FD.obj { as := c1 }).V) (x2 : ↑(S.FD.obj { as := c }).V) (y1 : ↑(S.FD.obj { as := S.τ c }).V) (y2 : ↑(S.FD.obj { as := c2 }).V) : (contrT 2 1 2 ⋯) ((prodT (fromPairT (x1 ⊗ₜ[k] x2))) (fromPairT (y1 ⊗ₜ[k] y2))) = (permT id ⋯) (fromPairTContr (x1 ⊗ₜ[k] x2) (y1 ⊗ₜ[k] y2))

theorem TensorSpecies.Tensor.fromPairT_contr_fromPairT_eq_fromPairTContr {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} (c c1 c2 : S.C) (x : TensorProduct k ↑(S.FD.obj { as := c1 }).V ↑(S.FD.obj { as := c }).V) (y : TensorProduct k ↑(S.FD.obj { as := S.τ c }).V ↑(S.FD.obj { as := c2 }).V) : (contrT 2 1 2 ⋯) ((prodT (fromPairT x)) (fromPairT y)) = (permT id ⋯) (fromPairTContr x y)

theorem TensorSpecies.Tensor.fromPairT_basis_repr {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c c1 : S.C} (x : TensorProduct k ↑(S.FD.obj { as := c }).V ↑(S.FD.obj { as := c1 }).V) (b : ComponentIdx ![c, c1]) : ((basis ![c, c1]).repr (fromPairT x)) b = (((S.basis c).tensorProduct (S.basis c1)).repr x) (b 0, b 1)

theorem TensorSpecies.Tensor.fromPairT_apply_basis_repr {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c c1 : S.C} (b0 : Fin (S.repDim c)) (b1 : Fin (S.repDim c1)) : fromPairT ((S.basis c) b0 ⊗ₜ[k] (S.basis c1) b1) = (basis ![c, c1]) fun (x : Fin (Nat.succ 0).succ) => match x with | 0 => b0 | 1 => b1

fromConstPair

noncomputable def TensorSpecies.Tensor.fromConstPair {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c1 c2 : S.C} (v : 𝟙_ (Rep k G) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c1 }) (S.FD.obj { as := c2 })) : S.Tensor ![c1, c2]

A constant two tensor (e.g. metric and unit).

Equations

• TensorSpecies.Tensor.fromConstPair v = TensorSpecies.Tensor.fromPairT ((CategoryTheory.ConcreteCategory.hom v.hom) 1)

@[simp]

theorem TensorSpecies.Tensor.actionT_fromConstPair {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c1 c2 : S.C} (v : 𝟙_ (Rep k G) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c1 }) (S.FD.obj { as := c2 })) (g : G) : g • fromConstPair v = fromConstPair v

Tensors formed by fromConstPair are invariant under the group action.

@[simp]

theorem TensorSpecies.Tensor.fromConstPair_whiskerLeft {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c1 c2 c2' : S.C} (h : c2 = c2') (v : 𝟙_ (Rep k G) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c1 }) (S.FD.obj { as := c2 })) : fromConstPair (CategoryTheory.CategoryStruct.comp v (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (S.FD.obj { as := c1 }) (S.FD.map (CategoryTheory.Discrete.eqToHom h)))) = (permT id ⋯) (fromConstPair v)

@[simp]

theorem TensorSpecies.Tensor.fromConstPair_braid {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c1 c2 : S.C} (v : 𝟙_ (Rep k G) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c1 }) (S.FD.obj { as := c2 })) : fromConstPair (CategoryTheory.CategoryStruct.comp v (β_ (S.FD.obj { as := c1 }) (S.FD.obj { as := c2 })).hom) = (permT ![1, 0] ⋯) (fromConstPair v)

fromTripleT

noncomputable def TensorSpecies.Tensor.fromTripleT {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c1 c2 c3 : S.C} : TensorProduct k (↑(S.FD.obj { as := c1 }).V) (TensorProduct k ↑(S.FD.obj { as := c2 }).V ↑(S.FD.obj { as := c3 }).V) →ₗ[k] S.Tensor ![c1, c2, c3]

The construction of a tensor with two indices from the tensor product (S.FD.obj (Discrete.mk c1)).V ⊗[k] (S.FD.obj (Discrete.mk c2)).V defined categorically.

Equations

• One or more equations did not get rendered due to their size.

theorem TensorSpecies.Tensor.fromTripleT_tmul {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c1 c2 c3 : S.C} (x : ↑(S.FD.obj { as := c1 }).V) (y : ↑(S.FD.obj { as := c2 }).V) (z : ↑(S.FD.obj { as := c3 }).V) : fromTripleT (x ⊗ₜ[k] y ⊗ₜ[k] z) = (permT id ⋯) ((prodT (fromSingleT x)) ((prodT (fromSingleT y)) (fromSingleT z)))

theorem TensorSpecies.Tensor.actionT_fromTripleT {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c1 c2 c3 : S.C} (x : TensorProduct k (↑(S.FD.obj { as := c1 }).V) (TensorProduct k ↑(S.FD.obj { as := c2 }).V ↑(S.FD.obj { as := c3 }).V)) (g : G) : g • fromTripleT x = fromTripleT ((TensorProduct.map ((S.FD.obj { as := c1 }).ρ g) (TensorProduct.map ((S.FD.obj { as := c2 }).ρ g) ((S.FD.obj { as := c3 }).ρ g))) x)

theorem TensorSpecies.Tensor.fromTripleT_basis_repr {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c c1 c2 : S.C} (x : TensorProduct k (↑(S.FD.obj { as := c }).V) (TensorProduct k ↑(S.FD.obj { as := c1 }).V ↑(S.FD.obj { as := c2 }).V)) (b : ComponentIdx ![c, c1, c2]) : ((basis ![c, c1, c2]).repr (fromTripleT x)) b = (((S.basis c).tensorProduct ((S.basis c1).tensorProduct (S.basis c2))).repr x) (b 0, b 1, b 2)

theorem TensorSpecies.Tensor.fromTripleT_apply_basis {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c c1 c2 : S.C} (b0 : Fin (S.repDim c)) (b1 : Fin (S.repDim c1)) (b2 : Fin (S.repDim c2)) : fromTripleT ((S.basis c) b0 ⊗ₜ[k] (S.basis c1) b1 ⊗ₜ[k] (S.basis c2) b2) = (basis ![c, c1, c2]) fun (x : Fin (Nat.succ 0).succ.succ) => match x with | 0 => b0 | 1 => b1 | 2 => b2

fromConstTriple

noncomputable def TensorSpecies.Tensor.fromConstTriple {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c1 c2 c3 : S.C} (v : 𝟙_ (Rep k G) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c1 }) (CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c2 }) (S.FD.obj { as := c3 }))) : S.Tensor ![c1, c2, c3]

A constant three tensor (e.g. the Pauli matrices).

Equations

• TensorSpecies.Tensor.fromConstTriple v = TensorSpecies.Tensor.fromTripleT ((CategoryTheory.ConcreteCategory.hom v.hom) 1)

@[simp]

theorem TensorSpecies.Tensor.actionT_fromConstTriple {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c1 c2 c3 : S.C} (v : 𝟙_ (Rep k G) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c1 }) (CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c2 }) (S.FD.obj { as := c3 }))) (g : G) : g • fromConstTriple v = fromConstTriple v

Tensors formed by fromConstPair are invariant under the group action.

Tensors with more indices

def TensorSpecies.Tensor.fromConst {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin n → S.C} (T : 𝟙_ (Rep k G) ⟶ S.F.obj (IndexNotation.OverColor.mk c)) : S.Tensor c

A general constant node.

Equations

• TensorSpecies.Tensor.fromConst T = (CategoryTheory.ConcreteCategory.hom T.hom) 1

Actions on tensors constructed from morphisms

Tensors constructed from morphisms are invariant under the group action.

@[simp]

theorem TensorSpecies.Tensor.actionT_fromConst {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin n → S.C} (T : 𝟙_ (Rep k G) ⟶ S.F.obj (IndexNotation.OverColor.mk c)) (g : G) : g • fromConst T = fromConst T

Tensors formed by fromConst are invariant under the group action.