The interfaction of contractions and products #
Products and contractions #
theorem
TensorSpecies.Tensor.Pure.dropPairEmb_natAdd_image_range_castAdd
{n n1 : ℕ}
(i j : Fin (n + 1 + 1))
(hij : i ≠ j)
:
dropPairEmb (Fin.natAdd n1 i) (Fin.natAdd n1 j) '' Set.range (Fin.castAdd n) = {i : Fin (n1 + n + 1 + 1) | ↑i < n1}
theorem
TensorSpecies.Tensor.Pure.dropPairEmb_comm_natAdd
{n n1 : ℕ}
(i j : Fin (n + 1 + 1))
(hij : i ≠ j)
(m : Fin n)
:
dropPairEmb (Fin.natAdd n1 i) (Fin.natAdd n1 j) (Fin.natAdd n1 m) = Fin.natAdd n1 (dropPairEmb i j m)
theorem
TensorSpecies.Tensor.Pure.dropPairEmb_permCond_prod
{k : Type}
[CommRing k]
{G : Type}
[Group G]
{S : TensorSpecies k G}
{n n1 : ℕ}
{c : Fin (n + 1 + 1) → S.C}
{c1 : Fin n1 → S.C}
(i j : Fin (n + 1 + 1))
(hij : i ≠ j ∧ S.τ (c i) = c j)
:
PermCond
((Sum.elim c1 c ∘ ⇑finSumFinEquiv.symm) ∘ dropPairEmb (finSumFinEquiv (Sum.inr i)) (finSumFinEquiv (Sum.inr j)))
(Sum.elim c1 (c ∘ dropPairEmb i j) ∘ ⇑finSumFinEquiv.symm) id
theorem
TensorSpecies.Tensor.Pure.prodP_dropPair
{k : Type}
[CommRing k]
{G : Type}
[Group G]
{S : TensorSpecies k G}
{n n1 : ℕ}
{c : Fin (n + 1 + 1) → S.C}
{c1 : Fin n1 → S.C}
(i j : Fin (n + 1 + 1))
(hij : i ≠ j ∧ S.τ (c i) = c j)
(p : Pure S c)
(p1 : Pure S c1)
:
p1.prodP (dropPair i j ⋯ p) = permP id ⋯ (dropPair (Fin.natAdd n1 i) (Fin.natAdd n1 j) ⋯ (p1.prodP p))