Contractions on basis tensors

def TensorSpecies.Tensor.ComponentIdx.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)) (b : ComponentIdx c) : ComponentIdx (c ∘ Pure.dropPairEmb i j)

The ComponentIdx obtained by dropping two components.

Equations

• TensorSpecies.Tensor.ComponentIdx.dropPair i j b m = b (TensorSpecies.Tensor.Pure.dropPairEmb i j m)

def TensorSpecies.Tensor.ComponentIdx.DropPairSection {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)} (b : ComponentIdx (c ∘ Pure.dropPairEmb i j)) : Finset (ComponentIdx c)

Given a coordinate parameter b : Π k, Fin (S.repDim ((c ∘ i.succAbove ∘ j.succAbove) k))), the coordinate parameter Π k, Fin (S.repDim (c k)) which map down to b.

Equations

• b.DropPairSection = {b' : TensorSpecies.Tensor.ComponentIdx c | TensorSpecies.Tensor.ComponentIdx.dropPair i j b' = b}

theorem TensorSpecies.Tensor.ComponentIdx.DropPairSection.mem_iff_apply_dropPairEmb_eq {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)} (b : ComponentIdx (c ∘ Pure.dropPairEmb i j)) (b' : ComponentIdx c) : b' ∈ b.DropPairSection ↔ ∀ (m : Fin n), b' (Pure.dropPairEmb i j m) = b m

@[simp]

theorem TensorSpecies.Tensor.ComponentIdx.DropPairSection.mem_self_of_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)} (b : ComponentIdx c) : b ∈ (dropPair i j b).DropPairSection

def TensorSpecies.Tensor.ComponentIdx.DropPairSection.ofFin {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) (b : ComponentIdx (c ∘ Pure.dropPairEmb i j)) (x : Fin (S.repDim (c i)) × Fin (S.repDim (c j))) : ComponentIdx c

Given a b in ComponentIdx (c ∘ Pure.dropPairEmb i j)) and an x in Fin (S.repDim (c i)) × Fin (S.repDim (c j)), the corresponding coordinate parameter in ComponentIdx c.

Equations

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

@[simp]

theorem TensorSpecies.Tensor.ComponentIdx.DropPairSection.ofFin_apply_fst {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) (b : ComponentIdx (c ∘ Pure.dropPairEmb i j)) (x : Fin (S.repDim (c i)) × Fin (S.repDim (c j))) : ofFin hij b x i = x.1

@[simp]

theorem TensorSpecies.Tensor.ComponentIdx.DropPairSection.ofFin_apply_snd {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) (b : ComponentIdx (c ∘ Pure.dropPairEmb i j)) (x : Fin (S.repDim (c i)) × Fin (S.repDim (c j))) : ofFin hij b x j = x.2

theorem TensorSpecies.Tensor.ComponentIdx.DropPairSection.ofFin_mem_dropPairEmbSection {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) (b : ComponentIdx (c ∘ Pure.dropPairEmb i j)) (x : Fin (S.repDim (c i)) × Fin (S.repDim (c j))) : ofFin hij b x ∈ b.DropPairSection

def TensorSpecies.Tensor.ComponentIdx.DropPairSection.ofFinEquiv {k : Type} [CommRing k] {G : Type} [Group G] {S : TensorSpecies k G} {n : ℕ} {c : Fin n.succ.succ → S.C} {i j : Fin (n + 1 + 1)} (hij : i ≠ j) (b : ComponentIdx (c ∘ Pure.dropPairEmb i j)) : Fin (S.repDim (c i)) × Fin (S.repDim (c j)) ≃ { x : ComponentIdx c // x ∈ b.DropPairSection }

The equivalence between ContrSection b and Fin (S.repDim (c i)) × Fin (S.repDim (c (i.succAbove j))).

Equations

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

@[simp]

theorem TensorSpecies.Tensor.ComponentIdx.DropPairSection.ofFinEquiv_apply_fst {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) (b : ComponentIdx (c ∘ Pure.dropPairEmb i j)) (x : Fin (S.repDim (c i)) × Fin (S.repDim (c j))) : ↑((ofFinEquiv hij b) x) i = x.1

@[simp]

theorem TensorSpecies.Tensor.ComponentIdx.DropPairSection.ofFinEquiv_apply_snd {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) (b : ComponentIdx (c ∘ Pure.dropPairEmb i j)) (x : Fin (S.repDim (c i)) × Fin (S.repDim (c j))) : ↑((ofFinEquiv hij b) x) j = x.2

theorem TensorSpecies.Tensor.Pure.dropPair_basisVector {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) (b : ComponentIdx c) : dropPair i j hij (basisVector c b) = basisVector (c ∘ dropPairEmb i j) fun (m : Fin n) => b (dropPairEmb i j m)

theorem TensorSpecies.Tensor.contrT_basis_repr_apply {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)} (h : i ≠ j ∧ S.τ (c i) = c j) (t : S.Tensor c) (b : ComponentIdx (c ∘ Pure.dropPairEmb i j)) : ((basis (c ∘ Pure.dropPairEmb i j)).repr ((contrT n i j h) t)) b = ∑ b' : { x : ComponentIdx c // x ∈ b.DropPairSection }, ((basis c).repr t) ↑b' * S.castToField ((CategoryTheory.ConcreteCategory.hom (S.contr.app { as := c i }).hom) ((S.basis (c i)) (↑b' i) ⊗ₜ[k] (S.basis (S.τ (c i))) (Fin.cast ⋯ (↑b' j))))

theorem TensorSpecies.Tensor.contrT_basis_repr_apply_eq_sum_fin {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)} (h : i ≠ j ∧ S.τ (c i) = c j) (t : S.Tensor c) (b : ComponentIdx (c ∘ Pure.dropPairEmb i j)) : ((basis (c ∘ Pure.dropPairEmb i j)).repr ((contrT n i j h) t)) b = ∑ x1 : Fin (S.repDim (c i)), ∑ x2 : Fin (S.repDim (c j)), ((basis c).repr t) ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ b) (x1, x2)) * S.castToField ((CategoryTheory.ConcreteCategory.hom (S.contr.app { as := c i }).hom) ((S.basis (c i)) x1 ⊗ₜ[k] (S.basis (S.τ (c i))) (Fin.cast ⋯ x2)))