Basis for tensors in a tensor species

def TensorSpecies.coordinateMultiLinearSingle (S : TensorSpecies) {n : ℕ} (c : Fin n → S.C) (b : (j : Fin n) → Fin (S.repDim (c j))) : MultilinearMap S.k (fun (i : Fin n) => ↑(S.FD.obj { as := c i }).V) S.k

The multi-linear map from (fun i => S.FD.obj (Discrete.mk (c i))) to S.k giving the coordinate with respect to the basis described by b.

Equations

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

def TensorSpecies.coordinateMultiLinear (S : TensorSpecies) {n : ℕ} (c : Fin n → S.C) : MultilinearMap S.k (fun (i : Fin n) => ↑(S.FD.obj { as := c i }).V) (((j : Fin n) → Fin (S.repDim (c j))) → S.k)

The multi-linear map from (fun i => S.FD.obj (Discrete.mk (c i))) to ((Π j, Fin (S.repDim (c j))) → S.k) giving the coordinates with respect to the basis defined in S.

Equations

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

def TensorSpecies.coordinate (S : TensorSpecies) {n : ℕ} (c : Fin n → S.C) : ↑(S.F.obj (IndexNotation.OverColor.mk c)).V →ₗ[S.k] ((j : Fin n) → Fin (S.repDim (c j))) → S.k

The linear map from tensors to coordinates.

Equations

• S.coordinate c = (↑S.liftTensor).toFun (S.coordinateMultiLinear c)

theorem TensorSpecies.coordinate_tprod (S : TensorSpecies) {n : ℕ} (c : Fin n → S.C) (x : (i : Fin n) → ↑(S.FD.obj { as := c i }).V) : (S.coordinate c) ((PiTensorProduct.tprod S.k) x) = (S.coordinateMultiLinear c) x

def TensorSpecies.basisVector (S : TensorSpecies) {n : ℕ} (c : Fin n → S.C) (b : (j : Fin n) → Fin (S.repDim (c j))) : ↑(S.F.obj (IndexNotation.OverColor.mk c)).V

The basis vector of tensors given a b : Π j, Fin (S.repDim (c j)) .

Equations

• S.basisVector c b = (PiTensorProduct.tprod S.k) fun (i : (CategoryTheory.Functor.id Type).obj (IndexNotation.OverColor.mk c).left) => (S.basis (c i)) (b i)

theorem TensorSpecies.coordinate_basisVector (S : TensorSpecies) {n : ℕ} (c : Fin n → S.C) (b1 b2 : (j : Fin n) → Fin (S.repDim (c j))) : (S.coordinate c) (S.basisVector c b1) b2 = if b1 = b2 then 1 else 0

def TensorSpecies.fromCoordinates (S : TensorSpecies) {n : ℕ} (c : Fin n → S.C) : (((j : Fin n) → Fin (S.repDim (c j))) → S.k) →ₗ[S.k] ↑(S.F.obj (IndexNotation.OverColor.mk c)).V

The linear map taking a ((Π j, Fin (S.repDim (c j))) → S.k) to a tensor, defined by summing over basis.

Equations

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

theorem TensorSpecies.coordinate_fromCoordinate_left_inv (S : TensorSpecies) {n : ℕ} (c : Fin n → S.C) : Function.LeftInverse ⇑(S.fromCoordinates c) ⇑(S.coordinate c)

theorem TensorSpecies.coordinate_fromCoordinate_right_inv (S : TensorSpecies) {n : ℕ} (c : Fin n → S.C) : Function.RightInverse ⇑(S.fromCoordinates c) ⇑(S.coordinate c)

def TensorSpecies.tensorBasis (S : TensorSpecies) {n : ℕ} (c : Fin n → S.C) : Basis ((j : Fin n) → Fin (S.repDim (c j))) S.k ↑(S.F.obj (IndexNotation.OverColor.mk c)).V

The basis of tensors.

Equations

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

theorem TensorSpecies.tensorBasis_eq_basisVector (S : TensorSpecies) {n : ℕ} (c : Fin n → S.C) (b : (j : Fin n) → Fin (S.repDim (c j))) : (S.tensorBasis c) b = S.basisVector c b

theorem TensorSpecies.TensorBasis.tensorBasis_repr_tprod {S : TensorSpecies} {n : ℕ} {c : Fin n → S.C} (x : (i : Fin n) → ↑(S.FD.obj { as := c i }).V) (b : (j : Fin n) → Fin (S.repDim (c j))) : ((S.tensorBasis c).repr ((PiTensorProduct.tprod S.k) x)) b = ∏ i : Fin n, ((S.basis (c i)).repr (x i)) (b i)

def TensorSpecies.TensorBasis.congr {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (σ : Fin n ≃ Fin m) (h : ∀ (i : Fin n), c i = c1 (σ i)) : ((j : Fin m) → Fin (S.repDim (c1 j))) ≃ ((j : Fin n) → Fin (S.repDim (c j)))

The equivalence between the indexing set of basis of Lorentz tensors induced by an equivalence on indices.

Equations

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

def TensorSpecies.TensorBasis.elimEquiv {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} : ((j : Fin n ⊕ Fin m) → Fin (S.repDim (Sum.elim c c1 j))) ≃ ((j : Fin n) → Fin (S.repDim (c j))) × ((j : Fin m) → Fin (S.repDim (c1 j)))

The equivalence between the coordinate parameters (Π j, Fin (S.repDim (Sum.elim c c1 j))) and (Π j, Fin (S.repDim (c j))) × (Π j, Fin (S.repDim (c1 j))) formed by splitting up based on j.

Equations

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

def TensorSpecies.TensorBasis.prodEquiv {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} : ((j : Fin (n + m)) → Fin (S.repDim (Sum.elim c c1 (finSumFinEquiv.symm j)))) ≃ ((j : Fin n) → Fin (S.repDim (c j))) × ((j : Fin m) → Fin (S.repDim (c1 j)))

The equivalence between the coordinate parameters (Π j, Fin (S.repDim (Sum.elim c c1 (finSumFinEquiv.symm j)))) and (Π j, Fin (S.repDim (c j))) × (Π j, Fin (S.repDim (c1 j))) formed by splitting up based on j.

Equations

• TensorSpecies.TensorBasis.prodEquiv = (Equiv.piCongrLeft (fun (b : Fin n ⊕ Fin m) => Fin (S.repDim (Sum.elim c c1 b))) finSumFinEquiv.symm).trans TensorSpecies.TensorBasis.elimEquiv

@[simp]

theorem TensorSpecies.TensorBasis.prodEquiv_apply_fst {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (b : (j : Fin (n + m)) → Fin (S.repDim (Sum.elim c c1 (finSumFinEquiv.symm j)))) (j : Fin n) : (prodEquiv b).1 j = Fin.cast ⋯ (b (Fin.castAdd m j))

@[simp]

theorem TensorSpecies.TensorBasis.prodEquiv_apply_snd {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (b : (j : Fin (n + m)) → Fin (S.repDim (Sum.elim c c1 (finSumFinEquiv.symm j)))) (j : Fin m) : (prodEquiv b).2 j = Fin.cast ⋯ (b (Fin.natAdd n j))

theorem TensorSpecies.TensorBasis.tensorBasis_prod {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} (b : (j : Fin (n + m)) → Fin (S.repDim (Sum.elim c c1 (finSumFinEquiv.symm j)))) : (S.tensorBasis (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm)) b = (CategoryTheory.ConcreteCategory.hom (S.F.map (IndexNotation.OverColor.equivToIso finSumFinEquiv).hom).hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.LaxMonoidal.μ S.F (IndexNotation.OverColor.mk c) (IndexNotation.OverColor.mk c1)).hom) ((S.tensorBasis c) (prodEquiv b).1 ⊗ₜ[S.k] (S.tensorBasis c1) (prodEquiv b).2))

theorem TensorSpecies.TensorBasis.map_tensorBasis {S : TensorSpecies} {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C} {σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1} (b : (j : Fin n) → Fin (S.repDim (c j))) : (ModuleCat.Hom.hom (S.F.map σ).hom) ((S.tensorBasis c) b) = (S.tensorBasis c1) ((congr (IndexNotation.OverColor.Hom.toEquiv σ) ⋯).symm b)

theorem TensorSpecies.TensorBasis.contrMap_tensorBasis {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} {h : c (i.succAbove j) = S.τ (c i)} (b : (j : Fin n.succ.succ) → Fin (S.repDim (c j))) : (CategoryTheory.ConcreteCategory.hom (S.contrMap c i j h).hom) ((S.tensorBasis c) b) = (CategoryTheory.ConcreteCategory.hom (S.contr.app { as := c i }).hom) ((S.basis (c i)) (b i) ⊗ₜ[S.k] (S.basis (S.τ (c i))) (Fin.cast ⋯ (b (i.succAbove j)))) • (S.tensorBasis (c ∘ i.succAbove ∘ j.succAbove)) fun (k : Fin n) => b ((i.succAbove ∘ j.succAbove) k)

def TensorSpecies.TensorBasis.ContrSection {S : TensorSpecies} {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ} {j : Fin n.succ} (b : (k : Fin n) → Fin (S.repDim ((c ∘ i.succAbove ∘ j.succAbove) k))) : Finset ((k : Fin n.succ.succ) → Fin (S.repDim (c k)))

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

• TensorSpecies.TensorBasis.ContrSection b = Finset.filter (fun (b' : (k : Fin n.succ.succ) → Fin (S.repDim (c k))) => ∀ (k : Fin n), b' ((i.succAbove ∘ j.succAbove) k) = b k) Finset.univ

theorem TensorSpecies.pairIsoSep_tensorBasis_repr (S : TensorSpecies) {c c1 : S.C} (t : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj (S.FD.obj { as := c }) (S.FD.obj { as := c1 })).V) (b : (j : Fin (Nat.succ 0).succ) → Fin (S.repDim (![c, c1] j))) : ((S.tensorBasis ![c, c1]).repr ((CategoryTheory.ConcreteCategory.hom (IndexNotation.OverColor.Discrete.pairIsoSep S.FD).hom.hom) t)) b = (((S.basis c).tensorProduct (S.basis c1)).repr t) (b 0, b 1)