Dual tensors

noncomputable def TensorSpecies.Tensor.fromDualMap {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} : S.Tensor ![S.τ c] →ₗ[k] S.Tensor ![c]

The linear map taking a tensor based on the color S.τ c to a tensor based on the color c, defined by contraction with the metric tensor.

Equations

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

theorem TensorSpecies.Tensor.fromDualMap_apply {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} (t : S.Tensor ![S.τ c]) : fromDualMap t = (permT id ⋯) ((contrT 1 1 2 ⋯) ((prodT (metricTensor c)) t))

noncomputable def TensorSpecies.Tensor.toDualMap {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} : S.Tensor ![c] →ₗ[k] S.Tensor ![S.τ c]

The linear map taking a tensor based on the color c to a tensor based on the color S.τ c, defined by contraction with the metric tensor.

Equations

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

theorem TensorSpecies.Tensor.toDualMap_apply {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} (t : S.Tensor ![c]) : toDualMap t = (permT id ⋯) ((contrT 1 1 2 ⋯) ((prodT (metricTensor (S.τ c))) t))

@[simp]

theorem TensorSpecies.Tensor.toDualMap_fromDualMap {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} (t : S.Tensor ![S.τ c]) : toDualMap (fromDualMap t) = t

theorem TensorSpecies.Tensor.fromDualMap_eq_permT_toDualMap {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} (t : S.Tensor ![S.τ c]) : fromDualMap t = (permT id ⋯) (toDualMap t)

theorem TensorSpecies.Tensor.toDualMap_eq_permT_fromDualMap {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} (t : S.Tensor ![c]) : toDualMap t = fromDualMap ((permT id ⋯) t)

@[simp]

theorem TensorSpecies.Tensor.fromDualMap_toDualMap {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} (t : S.Tensor ![c]) : fromDualMap (toDualMap t) = t

noncomputable def TensorSpecies.Tensor.toDual {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} : S.Tensor ![c] ≃ₗ[k] S.Tensor ![S.τ c]

The linear equivalence between S.Tensor ![c] and S.Tensor ![S.τ c] formed by contracting with metric tensors.

Equations

• TensorSpecies.Tensor.toDual = { toLinearMap := TensorSpecies.Tensor.toDualMap, invFun := TensorSpecies.Tensor.fromDualMap.toFun, left_inv := ⋯, right_inv := ⋯ }

theorem TensorSpecies.Tensor.toDual_equivariant {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} (g : G) (t : S.Tensor ![c]) : toDual (g • t) = g • toDual t

@[simp]

theorem TensorSpecies.repDim_τ {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {c : S.C} [StrongRankCondition k] : S.repDim (S.τ c) = S.repDim c