Products of tensors. #
@[reducible, inline]
noncomputable abbrev
TensorSpecies.Tensor
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
(S : TensorSpecies k C G)
{n : ℕ}
(c : Fin n → C)
:
The tensors associated with a list of indices of a given color
c : Fin n → C.
Instances For
@[reducible, inline]
abbrev
TensorSpecies.Tensor.ComponentIdx
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
(c : Fin n → C)
:
Given a list of indices c : Fin n → C e.g. ![.up, .down], the type
ComponentIdx c is the type of components indexes of a tensor with those indices
e.g. ⟨0, 2⟩ corresponding to T⁰₂.
Equations
- TensorSpecies.Tensor.ComponentIdx c = ((j : Fin n) → Fin (S.repDim (c j)))
Instances For
theorem
TensorSpecies.Tensor.ComponentIdx.congr_right
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
{c : Fin n → C}
(b : ComponentIdx c)
(i j : Fin n)
(h : i = j)
:
def
TensorSpecies.Tensor.ComponentIdx.cast
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n m : ℕ}
{c : Fin n → C}
{cm : Fin m → C}
(h : n = m)
(hc : c = cm ∘ Fin.cast h)
(b : ComponentIdx c)
:
ComponentIdx cm
Casting of a ComponentIdx through equivalent color maps.
Equations
- TensorSpecies.Tensor.ComponentIdx.cast h hc b j = Fin.cast ⋯ (b (Fin.cast ⋯ j))
Instances For
Pure tensors #
@[reducible, inline]
abbrev
TensorSpecies.Tensor.Pure
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{n : ℕ}
(S : TensorSpecies k C G)
(c : Fin n → C)
:
The type of pure tensors associated to a list of indices c : OverColor C.
A pure tensor is a tensor which can be written in the form v1 ⊗ₜ v2 ⊗ₜ v3 ….
Instances For
theorem
TensorSpecies.Tensor.Pure.congr_mid
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
{c : Fin n → C}
(c' : C)
(p : Pure S c)
(i j : Fin n)
(h : i = j)
(hi : c i = c')
(hj : c j = c')
:
(CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) (p i) = (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) (p j)
theorem
TensorSpecies.Tensor.Pure.map_mid_move_left
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n n1 : ℕ}
{c : Fin n → C}
{c1 : Fin n1 → C}
(p : Pure S c)
(p' : Pure S c1)
{c' : C}
(i : Fin n)
(j : Fin n1)
(hi : c i = c')
(hj : c1 j = c')
:
(CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) (p i) = (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) (p' j) ↔ (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) (p i) = p' j
theorem
TensorSpecies.Tensor.Pure.map_map_apply
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
{c : Fin n → C}
(c1 c2 : C)
(p : Pure S c)
(i : Fin n)
(f : { as := c i } ⟶ { as := c1 })
(g : { as := c1 } ⟶ { as := c2 })
:
(CategoryTheory.ConcreteCategory.hom (S.FD.map g)) ((CategoryTheory.ConcreteCategory.hom (S.FD.map f)) (p i)) = (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.CategoryStruct.comp f g))) (p i)
noncomputable def
TensorSpecies.Tensor.Pure.toTensor
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
{c : Fin n → C}
(p : Pure S c)
:
S.Tensor c
The tensor corresponding to a pure tensor.
Equations
- p.toTensor = (PiTensorProduct.tprod k) p
Instances For
theorem
TensorSpecies.Tensor.Pure.toTensor_apply
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
(c : Fin n → C)
(p : Pure S c)
:
def
TensorSpecies.Tensor.Pure.update
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
{c : Fin n → C}
[inst : DecidableEq (Fin n)]
(p : Pure S c)
(i : Fin n)
(x : ↑(S.FD.obj { as := c i }).V)
:
Pure S c
Given a list of indices c of n indices, a pure tensor p, an element i : Fin n and
a x in S.FD.obj (Discrete.mk (c i)) then update p i x corresponds to p where
the ith part of p is replaced with x.
E.g. if n = 2 and p = v₀ ⊗ₜ v₁ then update p 0 x = x ⊗ₜ v₁.
Equations
- p.update i x = Function.update p i x
Instances For
def
TensorSpecies.Tensor.Pure.drop
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
{c : Fin (n + 1) → C}
(p : Pure S c)
(i : Fin (n + 1))
:
Given a list of indices c of length n + 1, a pure tensor p and an i : Fin (n + 1), then
drop p i is the tensor p with it's ith part dropped.
For example, if n = 2 and p = v₀ ⊗ₜ v₁ ⊗ₜ v₂ then drop p 1 = v₀ ⊗ₜ v₂.
Instances For
@[simp]
theorem
TensorSpecies.Tensor.Pure.μ_toTensor_tmul_toTensor
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n1 n2 : ℕ}
{c : Fin n1 → C}
{c1 : Fin n2 → C}
(t : Pure S c)
(t1 : Pure S c1)
:
(CategoryTheory.ConcreteCategory.hom
(CategoryTheory.Functor.LaxMonoidal.μ S.F (IndexNotation.OverColor.mk c) (IndexNotation.OverColor.mk c1)).hom)
(t.toTensor ⊗ₜ[k] t1.toTensor) = (PiTensorProduct.tprod k)
fun
(x :
(CategoryTheory.MonoidalCategoryStruct.tensorObj (IndexNotation.OverColor.mk c)
(IndexNotation.OverColor.mk c1)).left) =>
match x with
| Sum.inl i => t i
| Sum.inr i => t1 i
Components #
noncomputable def
TensorSpecies.Tensor.Pure.component
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
{c : Fin n → C}
(p : Pure S c)
(b : ComponentIdx c)
:
k
Given an element b of ComponentIdx c and a pure tensor p then
component p b is the element of the ring k corresponding to
the component of p in the direction b.
For example, if p = v ⊗ₜ w and b = ⟨0, 1⟩ then component p b = v⁰ ⊗ₜ w¹.
Instances For
theorem
TensorSpecies.Tensor.Pure.component_eq_drop
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
{c : Fin (n + 1) → C}
(p : Pure S c)
(i : Fin (n + 1))
(b : ComponentIdx c)
:
@[simp]
theorem
TensorSpecies.Tensor.Pure.component_update_add
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
[inst : DecidableEq (Fin n)]
{c : Fin n → C}
(p : Pure S c)
(i : Fin n)
(x y : ↑(S.FD.obj { as := c i }).V)
(b : ComponentIdx c)
:
@[simp]
theorem
TensorSpecies.Tensor.Pure.component_update_smul
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
[inst : DecidableEq (Fin n)]
{c : Fin n → C}
(p : Pure S c)
(i : Fin n)
(x : k)
(y : ↑(S.FD.obj { as := c i }).V)
(b : ComponentIdx c)
:
noncomputable def
TensorSpecies.Tensor.Pure.componentMap
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
(c : Fin n → C)
:
MultilinearMap k (fun (i : Fin n) => ↑(S.FD.obj { as := c i }).V) (ComponentIdx c → k)
The multilinear map taking pure tensors p to a map ComponentIdx c → k which when
evaluated returns the components of p.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TensorSpecies.Tensor.Pure.componentMap_apply
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
(c : Fin n → C)
(p : Pure S c)
:
noncomputable def
TensorSpecies.Tensor.Pure.basisVector
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
(c : Fin n → C)
(b : ComponentIdx c)
:
Pure S c
Given an component idx b in ComponentIdx c, basisVector c b is the pure tensor
formed by S.basis (c i) (b i).
Equations
- TensorSpecies.Tensor.Pure.basisVector c b i = (S.basis (c i)) (b i)
Instances For
@[simp]
theorem
TensorSpecies.Tensor.Pure.component_basisVector
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
(c : Fin n → C)
(b1 b2 : ComponentIdx c)
:
theorem
TensorSpecies.Tensor.induction_on_pure
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
{c : Fin n → C}
{P : S.Tensor c → Prop}
(h : ∀ (p : Pure S c), P p.toTensor)
(hsmul : ∀ (r : k) (t : S.Tensor c), P t → P (r • t))
(hadd : ∀ (t1 t2 : S.Tensor c), P t1 → P t2 → P (t1 + t2))
(t : S.Tensor c)
:
P t
The basis #
def
TensorSpecies.Tensor.componentMap
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
(c : Fin n → C)
:
The linear map from tensors to its components.
Equations
Instances For
@[simp]
theorem
TensorSpecies.Tensor.componentMap_pure
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
(c : Fin n → C)
(p : Pure S c)
:
def
TensorSpecies.Tensor.ofComponents
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
(c : Fin n → C)
:
The tensor created from it's components.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TensorSpecies.Tensor.componentMap_ofComponents
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
(c : Fin n → C)
(f : ComponentIdx c → k)
:
@[simp]
theorem
TensorSpecies.Tensor.ofComponents_componentMap
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
(c : Fin n → C)
(t : S.Tensor c)
:
def
TensorSpecies.Tensor.basis
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
(c : Fin n → C)
:
Module.Basis (ComponentIdx c) k (S.Tensor c)
The basis of tensors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TensorSpecies.Tensor.basis_apply
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
(c : Fin n → C)
(b : ComponentIdx c)
:
theorem
TensorSpecies.Tensor.induction_on_basis
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
{c : Fin n → C}
{P : S.Tensor c → Prop}
(h : ∀ (b : ComponentIdx c), P ((basis c) b))
(hzero : P 0)
(hsmul : ∀ (r : k) (t : S.Tensor c), P t → P (r • t))
(hadd : ∀ (t1 t2 : S.Tensor c), P t1 → P t2 → P (t1 + t2))
(t : S.Tensor c)
:
P t
The rank #
theorem
TensorSpecies.Tensor.finrank_tensor_eq
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
[StrongRankCondition k]
(c : Fin n → C)
:
The action #
noncomputable instance
TensorSpecies.Tensor.Pure.actionP
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
{c : Fin n → C}
:
noncomputable instance
TensorSpecies.Tensor.Pure.instSMul
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
{c : Fin n → C}
:
The action on tensors #
noncomputable instance
TensorSpecies.Tensor.actionT
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n : ℕ}
{c : Fin n → C}
:
Equations
- TensorSpecies.Tensor.actionT = { smul := fun (g : G) (t : S.Tensor c) => ((S.F.obj (IndexNotation.OverColor.mk c)).ρ g) t, one_smul := ⋯, mul_smul := ⋯ }
def
TensorSpecies.Tensor.PermCond
{C : Type}
{n m : ℕ}
(c : Fin n → C)
(c1 : Fin m → C)
(σ : Fin m → Fin n)
:
Given two lists of indices c : Fin n → C and c1 : Fin m → C a map
σ : Fin m → Fin n satisfies the condition PermCond c c1 σ if it is:
- A bijection
- Forms a commutative triangle with
candc1.
Equations
- TensorSpecies.Tensor.PermCond c c1 σ = (Function.Bijective σ ∧ ∀ (i : Fin m), c (σ i) = c1 i)
Instances For
def
TensorSpecies.Tensor.PermCond.toEquiv
{C : Type}
{n m : ℕ}
{c : Fin n → C}
{c1 : Fin m → C}
{σ : Fin m → Fin n}
(h : PermCond c c1 σ)
:
For a map σ : Fin m → Fin n satisfying PermCond c c1 σ,
that map lifted to an equivalence between
Fin n and Fin m.
Equations
- h.toEquiv = { toFun := TensorSpecies.Tensor.PermCond.inv σ h, invFun := σ, left_inv := ⋯, right_inv := ⋯ }
Instances For
theorem
TensorSpecies.Tensor.PermCond.ofHom
{C : Type}
{n m : ℕ}
{c : Fin n → C}
{c1 : Fin m → C}
(σ : IndexNotation.OverColor.mk c ⟶ IndexNotation.OverColor.mk c1)
:
PermCond c c1 ⇑(IndexNotation.OverColor.Hom.toEquiv σ).symm
Given a morphism in the OverColor C between c and c1 category the corresponding morphism
(Hom.toEquiv σ).symm satisfies the PermCond.
Permutations #
def
TensorSpecies.Tensor.Pure.permP
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n m : ℕ}
{c : Fin n → C}
{c1 : Fin m → C}
(σ : Fin m → Fin n)
(h : PermCond c c1 σ)
(p : Pure S c)
:
Pure S c1
Given a permutation σ : Fin m → Fin n of indices satisfying PermCond through h,
and a pure tensor p, permP σ h p is the pure tensor permuted according to σ.
For example if m = n = 2 and σ = ![1, 0], and p = v ⊗ₜ w then
permP σ _ p = w ⊗ₜ v.
Equations
- TensorSpecies.Tensor.Pure.permP σ h p i = (CategoryTheory.ConcreteCategory.hom (S.FD.map (CategoryTheory.eqToHom ⋯))) (p (σ i))
Instances For
@[simp]
theorem
TensorSpecies.Tensor.Pure.permP_basisVector
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n m : ℕ}
{c : Fin n → C}
{c1 : Fin m → C}
(σ : Fin m → Fin n)
(h : PermCond c c1 σ)
(b : ComponentIdx c)
:
noncomputable def
TensorSpecies.Tensor.permT
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n m : ℕ}
{c : Fin n → C}
{c1 : Fin m → C}
(σ : Fin m → Fin n)
(h : PermCond c c1 σ)
:
Given a permutation σ : Fin m → Fin n of indices satisfying PermCond through h,
and a tensor t, permT σ h t is the tensor tensor permuted according to σ.
Equations
- TensorSpecies.Tensor.permT σ h = { toFun := fun (t : S.Tensor c) => (CategoryTheory.ConcreteCategory.hom (S.F.map h.toHom).hom) t, map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[simp]
theorem
TensorSpecies.Tensor.permT_basis_repr_symm_apply
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{n m : ℕ}
{c : Fin n → C}
{c1 : Fin m → C}
{σ : Fin m → Fin n}
(h : PermCond c c1 σ)
(t : S.Tensor c)
(b : ComponentIdx c1)
:
field #
noncomputable def
TensorSpecies.Tensor.toField
{k : Type}
[CommRing k]
{C G : Type}
[Group G]
{S : TensorSpecies k C G}
{c : Fin 0 → C}
:
The linear map between tensors with zero indices and the underlying field
k.