Contractions on tensors

contrT

theorem TensorSpecies.Tensor.contrT_decide {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin (n + 1 + 1) → S.C} {i j : Fin (n + 1 + 1)} (hx : S.τ (c i) = c j) (hij : i ≠ j := by decide) : i ≠ j ∧ S.τ (c i) = c j

noncomputable def TensorSpecies.Tensor.contrT {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} (n : ℕ) {c : Fin (n + 1 + 1) → S.C} (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j) : S.Tensor c →ₗ[k] S.Tensor (c ∘ Pure.dropPairEmb i j)

For c : Fin (n + 1 + 1) → S.C, i j : Fin (n + 1 + 1) with dual color, and a tensor t : Tensor S c, contrT i j _ t is the tensor formed by contracting the ith index of t with the jth index.

Equations

• TensorSpecies.Tensor.contrT n i j hij = PiTensorProduct.lift (TensorSpecies.Tensor.Pure.contrPMultilinear i j hij)

theorem TensorSpecies.Tensor.contrT_congr {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin (n + 1 + 1) → S.C} {i j : Fin (n + 1 + 1)} {hij : i ≠ j ∧ S.τ (c i) = c j} (i' j' : Fin (n + 1 + 1)) (t : S.Tensor c) (hii' : i = i' := by decide) (hjj' : j = j' := by decide) : (contrT n i j hij) t = (permT id ⋯) ((contrT n i' j' ⋯) t)

@[simp]

theorem TensorSpecies.Tensor.contrT_pure {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin (n + 1 + 1) → S.C} (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j) (p : Pure S c) : (contrT n i j hij) p.toTensor = Pure.contrP i j hij p

@[simp]

theorem TensorSpecies.Tensor.contrT_equivariant {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin (n + 1 + 1) → S.C} (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j) (g : G) (t : S.Tensor c) : (contrT n i j hij) (g • t) = g • (contrT n i j hij) t

theorem TensorSpecies.Tensor.contrT_permT {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n n1 : ℕ} {c : Fin (n + 1 + 1) → S.C} {c1 : Fin (n1 + 1 + 1) → S.C} (i j : Fin (n1 + 1 + 1)) (hij : i ≠ j ∧ S.τ (c1 i) = c1 j) (σ : Fin (n1 + 1 + 1) → Fin (n + 1 + 1)) (hσ : PermCond c c1 σ) (t : S.Tensor c) : (contrT n1 i j hij) ((permT σ hσ) t) = (permT (Pure.dropPairOfMap i j ⋯ σ ⋯) ⋯) ((contrT n (σ i) (σ j) ⋯) t)

theorem TensorSpecies.Tensor.contrT_symm {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin (n + 1 + 1) → S.C} {i j : Fin (n + 1 + 1)} {hij : i ≠ j ∧ S.τ (c i) = c j} (t : S.Tensor c) : (contrT n i j hij) t = (permT id ⋯) ((contrT n j i ⋯) t)

theorem TensorSpecies.Tensor.contrT_comm {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin (n + 1 + 1 + 1 + 1) → S.C} (i1 j1 : Fin (n + 1 + 1 + 1 + 1)) (i2 j2 : Fin (n + 1 + 1)) (hij1 : i1 ≠ j1 ∧ S.τ (c i1) = c j1) (hij2 : i2 ≠ j2 ∧ S.τ (c (Pure.dropPairEmb i1 j1 i2)) = c (Pure.dropPairEmb i1 j1 j2)) (t : S.Tensor c) : let i2' := Pure.dropPairEmb i1 j1 i2; let j2' := Pure.dropPairEmb i1 j1 j2; let_fun hi2j2' := ⋯; let i1' := Pure.dropPairEmbPre i2' j2' hi2j2' i1 ⋯; let j1' := Pure.dropPairEmbPre i2' j2' hi2j2' j1 ⋯; (contrT n i2 j2 hij2) ((contrT (n + 1 + 1) i1 j1 hij1) t) = (permT id ⋯) ((contrT n i1' j1' ⋯) ((contrT (n + 1 + 1) i2' j2' ⋯) t))