Contractions on pure tensors

Pure.contrPCoeff

dropPairEmb

def TensorSpecies.Tensor.Pure.dropPairEmb {n : ℕ} (i j : Fin (n + 1 + 1)) (m : Fin n) : Fin (n + 1 + 1)

The embedding of Fin n into Fin (n + 1 + 1) which leaves a hole at i and j.

Equations

• TensorSpecies.Tensor.Pure.dropPairEmb i j m = if ↑m < ↑i ∧ ↑m < ↑j then ⟨↑m, ⋯⟩ else if ↑m + 1 < ↑i ∧ ↑j ≤ ↑m then ⟨↑m + 1, ⋯⟩ else if ↑i ≤ ↑m ∧ ↑m + 1 < ↑j then ⟨↑m + 1, ⋯⟩ else ⟨↑m + 2, ⋯⟩

theorem TensorSpecies.Tensor.Pure.dropPairEmb_self_apply {n : ℕ} (i : Fin (n + 1 + 1)) (m : Fin n) : dropPairEmb i i m = if ↑m < ↑i then ⟨↑m, ⋯⟩ else ⟨↑m + 2, ⋯⟩

theorem TensorSpecies.Tensor.Pure.dropPairEmb_eq_succAbove_succAbove {n : ℕ} (i : Fin (n + 1 + 1)) (j : Fin (n + 1)) : dropPairEmb i (i.succAbove j) = i.succAbove ∘ j.succAbove

theorem TensorSpecies.Tensor.Pure.dropPairEmb_injective {n : ℕ} (i j : Fin (n + 1 + 1)) : Function.Injective (dropPairEmb i j)

@[simp]

theorem TensorSpecies.Tensor.Pure.dropPairEmb_eq_iff_eq {n : ℕ} (i j : Fin (n + 1 + 1)) (m1 m2 : Fin n) : dropPairEmb i j m1 = dropPairEmb i j m2 ↔ m1 = m2

@[simp]

theorem TensorSpecies.Tensor.Pure.dropPairEmb_leq_iff_leq {n : ℕ} (i j : Fin (n + 1 + 1)) (m1 m2 : Fin n) : dropPairEmb i j m1 ≤ dropPairEmb i j m2 ↔ m1 ≤ m2

@[simp]

theorem TensorSpecies.Tensor.Pure.dropPairEmb_lt_iff_lt {n : ℕ} (i j : Fin (n + 1 + 1)) (m1 m2 : Fin n) : dropPairEmb i j m1 < dropPairEmb i j m2 ↔ m1 < m2

@[simp]

theorem TensorSpecies.Tensor.Pure.dropPairEmb_monotone {n : ℕ} (i j : Fin (n + 1 + 1)) : Monotone (dropPairEmb i j)

theorem TensorSpecies.Tensor.Pure.dropPairEmb_eq_orderEmbOfFin {n : ℕ} (i j : Fin (n + 1 + 1)) (hij : i ≠ j) : dropPairEmb i j = ⇑({i, j}ᶜ.orderEmbOfFin ⋯)

theorem TensorSpecies.Tensor.Pure.dropPairEmb_symm {n : ℕ} (i j : Fin (n + 1 + 1)) : dropPairEmb i j = dropPairEmb j i

@[simp]

theorem TensorSpecies.Tensor.Pure.permCond_dropPairEmb_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)) (k✝ : Fin n) : c (dropPairEmb i j k✝) = c (dropPairEmb j i k✝)

theorem TensorSpecies.Tensor.Pure.dropPairEmb_apply_eq_orderIsoOfFin {n : ℕ} {i j : Fin (n + 1 + 1)} (hij : i ≠ j) (m : Fin n) : dropPairEmb i j m = ↑(({i, j}ᶜ.orderIsoOfFin ⋯) m)

@[simp]

theorem TensorSpecies.Tensor.Pure.dropPairEmb_range {n : ℕ} {i j : Fin (n + 1 + 1)} (hij : i ≠ j) : Set.range (dropPairEmb i j) = {i, j}ᶜ

theorem TensorSpecies.Tensor.Pure.dropPairEmb_image_compl {n : ℕ} {i j : Fin (n + 1 + 1)} (hij : i ≠ j) (X : Set (Fin n)) : dropPairEmb i j '' Xᶜ = ({i, j} ∪ dropPairEmb i j '' X)ᶜ

@[simp]

theorem TensorSpecies.Tensor.Pure.fst_neq_dropPairEmb_pre {n : ℕ} (i j : Fin (n + 1 + 1)) (m : Fin n) : ¬i = dropPairEmb i j m

@[simp]

theorem TensorSpecies.Tensor.Pure.dropPairEmb_neq_fst {n : ℕ} (i j : Fin (n + 1 + 1)) (m : Fin n) : ¬dropPairEmb i j m = i

@[simp]

theorem TensorSpecies.Tensor.Pure.snd_neq_dropPairEmb_pre {n : ℕ} (i j : Fin (n + 1 + 1)) (m : Fin n) : ¬j = dropPairEmb i j m

@[simp]

theorem TensorSpecies.Tensor.Pure.dropPairEmb_neq_snd {n : ℕ} (i j : Fin (n + 1 + 1)) (m : Fin n) : ¬dropPairEmb i j m = j

theorem TensorSpecies.Tensor.Pure.dropPairEmb_succAbove {n : ℕ} (i : Fin (n + 1 + 1)) (j : Fin (n + 1)) : dropPairEmb i (i.succAbove j) = i.succAbove ∘ j.succAbove

theorem TensorSpecies.Tensor.Pure.eq_or_exists_dropPairEmb {n : ℕ} (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (m : Fin (n + 1 + 1)) : m = i ∨ m = j ∨ ∃ (m' : Fin n), m = dropPairEmb i j m'

dropPairEmbPre

def TensorSpecies.Tensor.Pure.dropPairEmbPre {n : ℕ} (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (m : Fin (n + 1 + 1)) (hm : m ≠ i ∧ m ≠ j) : Fin n

The preimage of m under dropPairEmb i j hij given that m is not equal to i or j.

Equations

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

@[simp]

theorem TensorSpecies.Tensor.Pure.dropPairEmb_dropPairEmbPre {n : ℕ} (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (m : Fin (n + 1 + 1)) (hm : m ≠ i ∧ m ≠ j) : dropPairEmb i j (dropPairEmbPre i j hij m hm) = m

theorem TensorSpecies.Tensor.Pure.dropPairEmbPre_eq_orderIsoOfFin {n : ℕ} (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (m : Fin (n + 1 + 1)) (hm : m ≠ i ∧ m ≠ j) : dropPairEmbPre i j hij m hm = ({i, j}ᶜ.orderIsoOfFin ⋯).symm ⟨m, ⋯⟩

@[simp]

theorem TensorSpecies.Tensor.Pure.dropPairEmbPre_injective {n : ℕ} (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (m1 m2 : Fin (n + 1 + 1)) (hm1 : m1 ≠ i ∧ m1 ≠ j) (hm2 : m2 ≠ i ∧ m2 ≠ j) : dropPairEmbPre i j hij m1 hm1 = dropPairEmbPre i j hij m2 hm2 ↔ m1 = m2

theorem TensorSpecies.Tensor.Pure.dropPairEmbPre_surjective {n : ℕ} (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (m : Fin n) : ∃ (m' : Fin (n + 1 + 1)) (h : m' ≠ i ∧ m' ≠ j), dropPairEmbPre i j hij m' h = m

@[simp]

theorem TensorSpecies.Tensor.Pure.dropPairEmbPre_dropPairEmb {n : ℕ} (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (m : Fin n) : dropPairEmbPre i j hij (dropPairEmb i j m) ⋯ = m

commuativity of dropPairEmb

theorem TensorSpecies.Tensor.Pure.dropPairEmb_comm {n : ℕ} (i1 j1 : Fin (n + 1 + 1 + 1 + 1)) (i2 j2 : Fin (n + 1 + 1)) (hij1 : i1 ≠ j1) (hij2 : i2 ≠ j2) : let i2' := dropPairEmb i1 j1 i2; let j2' := dropPairEmb i1 j1 j2; let_fun hi2j2' := ⋯; let i1' := dropPairEmbPre i2' j2' hi2j2' i1 ⋯; let j1' := dropPairEmbPre i2' j2' hi2j2' j1 ⋯; dropPairEmb i1 j1 ∘ dropPairEmb i2 j2 = dropPairEmb i2' j2' ∘ dropPairEmb i1' j1'

theorem TensorSpecies.Tensor.Pure.dropPairEmb_comm_apply {n : ℕ} (i1 j1 : Fin (n + 1 + 1 + 1 + 1)) (i2 j2 : Fin (n + 1 + 1)) (hij1 : i1 ≠ j1) (hij2 : i2 ≠ j2) (m : Fin n) : let i2' := dropPairEmb i1 j1 i2; let j2' := dropPairEmb i1 j1 j2; let_fun hi2j2' := ⋯; let i1' := dropPairEmbPre i2' j2' hi2j2' i1 ⋯; let j1' := dropPairEmbPre i2' j2' hi2j2' j1 ⋯; dropPairEmb i2' j2' (dropPairEmb i1' j1' m) = dropPairEmb i1 j1 (dropPairEmb i2 j2 m)

theorem TensorSpecies.Tensor.Pure.permCond_dropPairEmb_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) (hij2 : i2 ≠ j2) : let i2' := dropPairEmb i1 j1 i2; let j2' := dropPairEmb i1 j1 j2; let_fun hi2j2' := ⋯; let i1' := dropPairEmbPre i2' j2' hi2j2' i1 ⋯; let j1' := dropPairEmbPre i2' j2' hi2j2' j1 ⋯; PermCond ((c ∘ dropPairEmb i2' j2') ∘ dropPairEmb i1' j1') ((c ∘ dropPairEmb i1 j1) ∘ dropPairEmb i2 j2) id

dropPairOfMap

def TensorSpecies.Tensor.Pure.dropPairOfMap {n n1 : ℕ} (i j : Fin (n1 + 1 + 1)) (hij : i ≠ j) (σ : Fin (n1 + 1 + 1) → Fin (n + 1 + 1)) (hσ : Function.Bijective σ) (m : Fin n1) : Fin n

Given a bijection Fin (n1 + 1 + 1) → Fin (n + 1 + 1)) and a pair i j : Fin (n1 + 1 + 1), then dropPairOfMap i j _ σ _ : Fin n1 → Fin n corressponds to the induced bijection formed by dropping i and j in the source and their image in the target.

Equations

• TensorSpecies.Tensor.Pure.dropPairOfMap i j hij σ hσ m = TensorSpecies.Tensor.Pure.dropPairEmbPre (σ i) (σ j) ⋯ (σ (TensorSpecies.Tensor.Pure.dropPairEmb i j m)) ⋯

theorem TensorSpecies.Tensor.Pure.dropPairOfMap_injective {n n1 : ℕ} (i j : Fin (n1 + 1 + 1)) (hij : i ≠ j) (σ : Fin (n1 + 1 + 1) → Fin (n + 1 + 1)) (hσ : Function.Bijective σ) : Function.Injective (dropPairOfMap i j hij σ hσ)

theorem TensorSpecies.Tensor.Pure.dropPairOfMap_surjective {n n1 : ℕ} (i j : Fin (n1 + 1 + 1)) (hij : i ≠ j) (σ : Fin (n1 + 1 + 1) → Fin (n + 1 + 1)) (hσ : Function.Bijective σ) : Function.Surjective (dropPairOfMap i j hij σ hσ)

theorem TensorSpecies.Tensor.Pure.dropPairOfMap_bijective {n n1 : ℕ} (i j : Fin (n1 + 1 + 1)) (hij : i ≠ j) (σ : Fin (n1 + 1 + 1) → Fin (n + 1 + 1)) (hσ : Function.Bijective σ) : Function.Bijective (dropPairOfMap i j hij σ hσ)

theorem TensorSpecies.Tensor.Pure.permCond_dropPairOfMap {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) (σ : Fin (n1 + 1 + 1) → Fin (n + 1 + 1)) (hσ : PermCond c c1 σ) : PermCond (c ∘ dropPairEmb (σ i) (σ j)) (c1 ∘ dropPairEmb i j) (dropPairOfMap i j hij σ ⋯)

@[simp]

theorem TensorSpecies.Tensor.Pure.dropPairOfMap_id {n1 : ℕ} (i j : Fin (n1 + 1 + 1)) (hij : i ≠ j) : dropPairOfMap i j hij id ⋯ = id

dropPair

def TensorSpecies.Tensor.Pure.dropPair {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) (p : Pure S c) : Pure S (c ∘ dropPairEmb i j)

Given i j : Fin (n + 1 + 1), c : Fin (n + 1 + 1) → S.C and a pure tensor p : Pure S c, dropPair i j _ p is the tensor formed by dropping the ith and jth parts of p.

Equations

• TensorSpecies.Tensor.Pure.dropPair i j hij p m = p (TensorSpecies.Tensor.Pure.dropPairEmb i j m)

@[simp]

theorem TensorSpecies.Tensor.Pure.dropPair_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) (p : Pure S c) (g : G) : dropPair i j hij (g • p) = g • dropPair i j hij p

theorem TensorSpecies.Tensor.Pure.dropPair_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) (p : Pure S c) : dropPair i j hij p = permP id ⋯ (dropPair j i ⋯ p)

theorem TensorSpecies.Tensor.Pure.dropPair_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) (hij2 : i2 ≠ j2) (p : Pure S c) : let i2' := dropPairEmb i1 j1 i2; let j2' := dropPairEmb i1 j1 j2; let_fun hi2j2' := ⋯; let i1' := dropPairEmbPre i2' j2' hi2j2' i1 ⋯; let j1' := dropPairEmbPre i2' j2' hi2j2' j1 ⋯; dropPair i2 j2 hij2 (dropPair i1 j1 hij1 p) = permP id ⋯ (dropPair i1' j1' ⋯ (dropPair i2' j2' hi2j2' p))

@[simp]

theorem TensorSpecies.Tensor.Pure.dropPair_update_fst {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} [inst : DecidableEq (Fin (n + 1 + 1))] {c : Fin (n + 1 + 1) → S.C} (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (p : Pure S c) (x : ↑(S.FD.obj { as := c i }).V) : dropPair i j hij (p.update i x) = dropPair i j hij p

@[simp]

theorem TensorSpecies.Tensor.Pure.dropPair_update_snd {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} [inst : DecidableEq (Fin (n + 1 + 1))] {c : Fin (n + 1 + 1) → S.C} (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (p : Pure S c) (x : ↑(S.FD.obj { as := c j }).V) : dropPair i j hij (p.update j x) = dropPair i j hij p

@[simp]

theorem TensorSpecies.Tensor.Pure.dropPair_update_dropPairEmb {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} [inst : DecidableEq (Fin (n + 1 + 1))] {c : Fin (n + 1 + 1) → S.C} (i j : Fin (n + 1 + 1)) (hij : i ≠ j) (p : Pure S c) (m : Fin n) (x : ↑(S.FD.obj { as := c (dropPairEmb i j m) }).V) : dropPair i j hij (p.update (dropPairEmb i j m) x) = (dropPair i j hij p).update m x

@[simp]

theorem TensorSpecies.Tensor.Pure.dropPair_permP {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) (σ : Fin (n1 + 1 + 1) → Fin (n + 1 + 1)) (hσ : PermCond c c1 σ) (p : Pure S c) : dropPair i j hij (permP σ hσ p) = permP (dropPairOfMap i j hij σ ⋯) ⋯ (dropPair (σ i) (σ j) ⋯ p)

Contraction coefficent

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

Given a pure tensor p : Pure S c and a i j : Fin n corresponding to dual colors in c, contrPCoeff i j _ p is the element of the underlying ring k formed by contracting p i and p j.

Equations

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

@[simp]

theorem TensorSpecies.Tensor.Pure.contrPCoeff_permP {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n n1 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C} (i j : Fin n1) (hij : i ≠ j ∧ S.τ (c1 i) = c1 j) (σ : Fin n1 → Fin n) (hσ : PermCond c c1 σ) (p : Pure S c) : contrPCoeff i j hij (permP σ hσ p) = contrPCoeff (σ i) (σ j) ⋯ p

@[simp]

theorem TensorSpecies.Tensor.Pure.contrPCoeff_update_dropPairEmb {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} [inst : DecidableEq (Fin (n + 1 + 1))] {c : Fin (n + 1 + 1) → S.C} (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j) (m : Fin n) (p : Pure S c) (x : ↑(S.FD.obj { as := c (dropPairEmb i j m) }).V) : contrPCoeff i j hij (p.update (dropPairEmb i j m) x) = contrPCoeff i j hij p

@[simp]

theorem TensorSpecies.Tensor.Pure.contrPCoeff_update_fst_add {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} [inst : DecidableEq (Fin n)] {c : Fin n → S.C} (i j : Fin n) (hij : i ≠ j ∧ S.τ (c i) = c j) (p : Pure S c) (x y : ↑(S.FD.obj { as := c i }).V) : contrPCoeff i j hij (p.update i (x + y)) = contrPCoeff i j hij (p.update i x) + contrPCoeff i j hij (p.update i y)

@[simp]

theorem TensorSpecies.Tensor.Pure.contrPCoeff_update_snd_add {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} [inst : DecidableEq (Fin n)] {c : Fin n → S.C} (i j : Fin n) (hij : i ≠ j ∧ S.τ (c i) = c j) (p : Pure S c) (x y : ↑(S.FD.obj { as := c j }).V) : contrPCoeff i j hij (p.update j (x + y)) = contrPCoeff i j hij (p.update j x) + contrPCoeff i j hij (p.update j y)

@[simp]

theorem TensorSpecies.Tensor.Pure.contrPCoeff_update_fst_smul {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} [inst : DecidableEq (Fin n)] {c : Fin n → S.C} (i j : Fin n) (hij : i ≠ j ∧ S.τ (c i) = c j) (p : Pure S c) (r : k) (x : ↑(S.FD.obj { as := c i }).V) : contrPCoeff i j hij (p.update i (r • x)) = r * contrPCoeff i j hij (p.update i x)

@[simp]

theorem TensorSpecies.Tensor.Pure.contrPCoeff_update_snd_smul {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} [inst : DecidableEq (Fin n)] {c : Fin n → S.C} (i j : Fin n) (hij : i ≠ j ∧ S.τ (c i) = c j) (p : Pure S c) (r : k) (x : ↑(S.FD.obj { as := c j }).V) : contrPCoeff i j hij (p.update j (r • x)) = r * contrPCoeff i j hij (p.update j x)

theorem TensorSpecies.Tensor.Pure.contrPCoeff_dropPair {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin (n + 1 + 1) → S.C} (a b : Fin (n + 1 + 1)) (hab : a ≠ b) (i j : Fin n) (hij : i ≠ j ∧ S.τ (c (dropPairEmb a b i)) = c (dropPairEmb a b j)) (p : Pure S c) : contrPCoeff i j hij (dropPair a b hab p) = contrPCoeff (dropPairEmb a b i) (dropPairEmb a b j) ⋯ p

theorem TensorSpecies.Tensor.Pure.contrPCoeff_symm {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin n → S.C} {i j : Fin n} {hij : i ≠ j ∧ S.τ (c i) = c j} {p : Pure S c} : contrPCoeff i j hij p = contrPCoeff j i ⋯ p

theorem TensorSpecies.Tensor.Pure.contrPCoeff_mul_dropPair {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 (dropPairEmb i1 j1 i2)) = c (dropPairEmb i1 j1 j2)) (p : Pure S c) : let i2' := dropPairEmb i1 j1 i2; let j2' := dropPairEmb i1 j1 j2; let_fun hi2j2' := ⋯; let i1' := dropPairEmbPre i2' j2' hi2j2' i1 ⋯; let j1' := dropPairEmbPre i2' j2' hi2j2' j1 ⋯; contrPCoeff i1 j1 hij1 p * contrPCoeff i2 j2 hij2 (dropPair i1 j1 ⋯ p) = contrPCoeff i2' j2' ⋯ p * contrPCoeff i1' j1' ⋯ (dropPair i2' j2' ⋯ p)

@[simp]

theorem TensorSpecies.Tensor.Pure.contrPCoeff_invariant {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin n → S.C} {i j : Fin n} {hij : i ≠ j ∧ S.τ (c i) = c j} {p : Pure S c} (g : G) : contrPCoeff i j hij (g • p) = contrPCoeff i j hij p

Contractions

noncomputable def TensorSpecies.Tensor.Pure.contrP {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) : S.Tensor (c ∘ dropPairEmb i j)

For c : Fin (n + 1 + 1) → S.C, i j : Fin (n + 1 + 1) with dual color, and a pure tensor p : Pure S c, contrP i j _ p is the tensor (not pure due to the n = 0 case) formed by contracting the ith index of p with the jth index.

Equations

• TensorSpecies.Tensor.Pure.contrP i j hij p = TensorSpecies.Tensor.Pure.contrPCoeff i j hij p • (TensorSpecies.Tensor.Pure.dropPair i j ⋯ p).toTensor

@[simp]

theorem TensorSpecies.Tensor.Pure.contrP_update_add {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} [inst : DecidableEq (Fin (n + 1 + 1))] {c : Fin (n + 1 + 1) → S.C} (i j m : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j) (p : Pure S c) (x y : ↑(S.FD.obj { as := c m }).V) : contrP i j hij (p.update m (x + y)) = contrP i j hij (p.update m x) + contrP i j hij (p.update m y)

@[simp]

theorem TensorSpecies.Tensor.Pure.contrP_update_smul {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} [inst : DecidableEq (Fin (n + 1 + 1))] {c : Fin (n + 1 + 1) → S.C} (i j m : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j) (p : Pure S c) (r : k) (x : ↑(S.FD.obj { as := c m }).V) : contrP i j hij (p.update m (r • x)) = r • contrP i j hij (p.update m x)

@[simp]

theorem TensorSpecies.Tensor.Pure.contrP_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) (p : Pure S c) (g : G) : contrP i j hij (g • p) = g • contrP i j hij p

theorem TensorSpecies.Tensor.Pure.contrP_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} {p : Pure S c} : contrP i j hij p = (permT id ⋯) (contrP j i ⋯ p)

contrP as a multilinear map

noncomputable def TensorSpecies.Tensor.Pure.contrPMultilinear {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) : MultilinearMap k (fun (i : Fin (n + 1 + 1)) => ↑(S.FD.obj { as := c i }).V) (S.Tensor (c ∘ dropPairEmb i j))

The multi-linear map formed by contracting a pair of indices of pure tensors.

Equations

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