Contractions on basis tensors

def TensorSpecies.Tensor.ComponentIdx.dropPair {k : Type} [CommRing k] {C G : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n : ℕ} {c : Fin (n + 1 + 1) → 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] {C G : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n : ℕ} {c : Fin (n + 1 + 1) → 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] {C G : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n : ℕ} {c : Fin (n + 1 + 1) → 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] {C G : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n : ℕ} {c : Fin (n + 1 + 1) → 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] {C G : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n : ℕ} {c : Fin (n + 1 + 1) → C} {i j : Fin (n + 1 + 1)} (hij : i ≠ j) (b : ComponentIdx (c ∘ Pure.dropPairEmb i j)) (x : basisIdx (c i) × basisIdx (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] {C G : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n : ℕ} {c : Fin (n + 1 + 1) → C} {i j : Fin (n + 1 + 1)} (hij : i ≠ j) (b : ComponentIdx (c ∘ Pure.dropPairEmb i j)) (x : basisIdx (c i) × basisIdx (c j)) : ofFin hij b x i = x.1

@[simp]

theorem TensorSpecies.Tensor.ComponentIdx.DropPairSection.ofFin_apply_snd {k : Type} [CommRing k] {C G : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n : ℕ} {c : Fin (n + 1 + 1) → C} {i j : Fin (n + 1 + 1)} (hij : i ≠ j) (b : ComponentIdx (c ∘ Pure.dropPairEmb i j)) (x : basisIdx (c i) × basisIdx (c j)) : ofFin hij b x j = x.2

theorem TensorSpecies.Tensor.ComponentIdx.DropPairSection.ofFin_mem_dropPairEmbSection {k : Type} [CommRing k] {C G : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n : ℕ} {c : Fin (n + 1 + 1) → C} {i j : Fin (n + 1 + 1)} (hij : i ≠ j) (b : ComponentIdx (c ∘ Pure.dropPairEmb i j)) (x : basisIdx (c i) × basisIdx (c j)) : ofFin hij b x ∈ b.DropPairSection

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

The equivalence between ContrSection b and basisIdx (c i) × basisIdx (c 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] {C G : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n : ℕ} {c : Fin (n + 1 + 1) → C} {i j : Fin (n + 1 + 1)} (hij : i ≠ j) (b : ComponentIdx (c ∘ Pure.dropPairEmb i j)) (x : basisIdx (c i) × basisIdx (c j)) : ↑((ofFinEquiv hij b) x) i = x.1

@[simp]

theorem TensorSpecies.Tensor.ComponentIdx.DropPairSection.ofFinEquiv_apply_snd {k : Type} [CommRing k] {C G : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n : ℕ} {c : Fin (n + 1 + 1) → C} {i j : Fin (n + 1 + 1)} (hij : i ≠ j) (b : ComponentIdx (c ∘ Pure.dropPairEmb i j)) (x : basisIdx (c i) × basisIdx (c j)) : ↑((ofFinEquiv hij b) x) j = x.2

theorem TensorSpecies.Tensor.Pure.dropPair_basisVector {k : Type} [CommRing k] {C G : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n : ℕ} {c : Fin (n + 1 + 1) → 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] {C G : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n : ℕ} {c : Fin (n + 1 + 1) → 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' : ↥b.DropPairSection, ((basis c).repr t) ↑b' * castToField ((Rep.Hom.hom (S.contr.app { as := c i })) ((S.basis (c i)) (↑b' i) ⊗ₜ[k] (S.basis (S.τ (c i))) ((basisIdxCongr ⋯) (↑b' j))))

theorem TensorSpecies.Tensor.contrT_basis_repr_apply_eq_sum_fin {k : Type} [CommRing k] {C G : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n : ℕ} {c : Fin (n + 1 + 1) → 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 : basisIdx (c i), ∑ x2 : basisIdx (c j), ((basis c).repr t) ↑((ComponentIdx.DropPairSection.ofFinEquiv ⋯ b) (x1, x2)) * castToField ((Rep.Hom.hom (S.contr.app { as := c i })) ((S.basis (c i)) x1 ⊗ₜ[k] (S.basis (S.τ (c i))) ((basisIdxCongr ⋯) x2)))

theorem TensorSpecies.Tensor.contrT_basis {k : Type} [CommRing k] {C G : Type} [Group G] {basisIdx : C → Type} [(c : C) → Fintype (basisIdx c)] [(c : C) → DecidableEq (basisIdx c)] {S : TensorSpecies k C G basisIdx} {n : ℕ} {c : Fin (n + 1 + 1) → C} {i j : Fin (n + 1 + 1)} (h : i ≠ j ∧ S.τ (c i) = c j) (b : ComponentIdx c) : (contrT n i j h) ((basis c) b) = Pure.contrPCoeff i j h (Pure.basisVector c b) • (basis (c ∘ Pure.dropPairEmb i j)) (ComponentIdx.dropPair i j b)