refactor: Index notation
This commit is contained in:
jstoobysmith
parent
d9f6760541
commit
ec69deaff2
12 changed files with 299 additions and 865 deletions
|
|
@ -4,7 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.Tensors.OverColor.Basic
|
||||
import HepLean.Tensors.Tree.Dot
|
||||
import HepLean.SpaceTime.WeylFermion.Contraction
|
||||
import HepLean.SpaceTime.WeylFermion.Metric
|
||||
import HepLean.SpaceTime.WeylFermion.Unit
|
||||
import HepLean.SpaceTime.LorentzVector.Complex.Contraction
|
||||
import HepLean.SpaceTime.LorentzVector.Complex.Metric
|
||||
import HepLean.SpaceTime.LorentzVector.Complex.Unit
|
||||
import HepLean.Mathematics.PiTensorProduct
|
||||
import HepLean.SpaceTime.PauliMatrices.AsTensor
|
||||
/-!
|
||||
|
||||
## Complex Lorentz tensors
|
||||
|
|
@ -30,34 +38,71 @@ inductive Color
|
|||
| up : Color
|
||||
| down : Color
|
||||
|
||||
/-- The involution taking a colour to its dual. -/
|
||||
def τ : Color → Color
|
||||
| Color.upL => Color.downL
|
||||
| Color.downL => Color.upL
|
||||
| Color.upR => Color.downR
|
||||
| Color.downR => Color.upR
|
||||
| Color.up => Color.down
|
||||
| Color.down => Color.up
|
||||
|
||||
/-- The function taking a color to the dimension of the basis of vectors. -/
|
||||
def evalNo : Color → ℕ
|
||||
| Color.upL => 2
|
||||
| Color.downL => 2
|
||||
| Color.upR => 2
|
||||
| Color.downR => 2
|
||||
| Color.up => 4
|
||||
| Color.down => 4
|
||||
|
||||
noncomputable section
|
||||
/-- The corresponding representations associated with a color. -/
|
||||
def colorToRep (c : Color) : Rep ℂ SL(2, ℂ) :=
|
||||
match c with
|
||||
| Color.upL => Fermion.altLeftHanded
|
||||
| Color.downL => Fermion.leftHanded
|
||||
| Color.upR => Fermion.altRightHanded
|
||||
| Color.downR => Fermion.rightHanded
|
||||
| Color.up => Lorentz.complexContr
|
||||
| Color.down => Lorentz.complexCo
|
||||
|
||||
/-- The tensor structure for complex Lorentz tensors. -/
|
||||
def complexLorentzTensor : TensorStruct where
|
||||
C := Fermion.Color
|
||||
G := SL(2, ℂ)
|
||||
G_group := inferInstance
|
||||
k := ℂ
|
||||
k_commRing := inferInstance
|
||||
FDiscrete := Discrete.functor fun c =>
|
||||
match c with
|
||||
| Color.upL => Fermion.leftHanded
|
||||
| Color.downL => Fermion.altLeftHanded
|
||||
| Color.upR => Fermion.rightHanded
|
||||
| Color.downR => Fermion.altRightHanded
|
||||
| Color.up => Lorentz.complexContr
|
||||
| Color.down => Lorentz.complexCo
|
||||
τ := fun c =>
|
||||
match c with
|
||||
| Color.upL => Color.downL
|
||||
| Color.downL => Color.upL
|
||||
| Color.upR => Color.downR
|
||||
| Color.downR => Color.upR
|
||||
| Color.up => Color.down
|
||||
| Color.down => Color.up
|
||||
τ_involution c := by
|
||||
match c with
|
||||
| Color.upL => rfl
|
||||
| Color.downL => rfl
|
||||
| Color.upR => rfl
|
||||
| Color.downR => rfl
|
||||
| Color.up => rfl
|
||||
| Color.down => rfl
|
||||
contr := Discrete.natTrans fun c =>
|
||||
match c with
|
||||
| Discrete.mk Color.upL => Fermion.leftAltContraction
|
||||
| Discrete.mk Color.downL => Fermion.altLeftContraction
|
||||
| Discrete.mk Color.upR => Fermion.rightAltContraction
|
||||
| Discrete.mk Color.downR => Fermion.altRightContraction
|
||||
| Discrete.mk Color.up => Lorentz.contrCoContraction
|
||||
| Discrete.mk Color.down => Lorentz.coContrContraction
|
||||
metric := Discrete.natTrans fun c =>
|
||||
match c with
|
||||
| Discrete.mk Color.upL => Fermion.leftMetric
|
||||
| Discrete.mk Color.downL => Fermion.altLeftMetric
|
||||
| Discrete.mk Color.upR => Fermion.rightMetric
|
||||
| Discrete.mk Color.downR => Fermion.altRightMetric
|
||||
| Discrete.mk Color.up => Lorentz.contrMetric
|
||||
| Discrete.mk Color.down => Lorentz.coMetric
|
||||
unit := Discrete.natTrans fun c =>
|
||||
match c with
|
||||
| Discrete.mk Color.upL => Fermion.altLeftLeftUnit
|
||||
| Discrete.mk Color.downL => Fermion.leftAltLeftUnit
|
||||
| Discrete.mk Color.upR => Fermion.altRightRightUnit
|
||||
| Discrete.mk Color.downR => Fermion.rightAltRightUnit
|
||||
| Discrete.mk Color.up => Lorentz.coContrUnit
|
||||
| Discrete.mk Color.down => Lorentz.contrCoUnit
|
||||
evalNo := fun c =>
|
||||
match c with
|
||||
| Color.upL => 2
|
||||
| Color.downL => 2
|
||||
| Color.upR => 2
|
||||
| Color.downR => 2
|
||||
| Color.up => 4
|
||||
| Color.down => 4
|
||||
|
||||
end
|
||||
end Fermion
|
||||
|
|
|
|||
|
|
@ -1,497 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.Tensors.ComplexLorentz.Basic
|
||||
import HepLean.Tensors.OverColor.Basic
|
||||
import HepLean.Mathematics.PiTensorProduct
|
||||
/-!
|
||||
|
||||
## Monodial functor from color cat.
|
||||
|
||||
-/
|
||||
namespace Fermion
|
||||
|
||||
noncomputable section
|
||||
|
||||
open Matrix
|
||||
open MatrixGroups
|
||||
open Complex
|
||||
open TensorProduct
|
||||
open IndexNotation
|
||||
open CategoryTheory
|
||||
|
||||
/-- The linear equivalence between `colorToRep c1` and `colorToRep c2` when `c1 = c2`. -/
|
||||
def colorToRepCongr {c1 c2 : Color} (h : c1 = c2) : colorToRep c1 ≃ₗ[ℂ] colorToRep c2 where
|
||||
toFun := Equiv.cast (congrArg (CoeSort.coe ∘ colorToRep) h)
|
||||
invFun := (Equiv.cast (congrArg (CoeSort.coe ∘ colorToRep) h)).symm
|
||||
map_add' x y := by
|
||||
subst h
|
||||
rfl
|
||||
map_smul' x y := by
|
||||
subst h
|
||||
rfl
|
||||
left_inv x := Equiv.symm_apply_apply (Equiv.cast (congrArg (CoeSort.coe ∘ colorToRep) h)) x
|
||||
right_inv x := Equiv.apply_symm_apply (Equiv.cast (congrArg (CoeSort.coe ∘ colorToRep) h)) x
|
||||
|
||||
lemma colorToRepCongr_comm_ρ {c1 c2 : Color} (h : c1 = c2) (M : SL(2, ℂ)) (x : (colorToRep c1)) :
|
||||
(colorToRepCongr h) ((colorToRep c1).ρ M x) = (colorToRep c2).ρ M ((colorToRepCongr h) x) := by
|
||||
subst h
|
||||
rfl
|
||||
|
||||
namespace colorFun
|
||||
|
||||
/-- Given a object in `OverColor Color` the correpsonding tensor product of representations. -/
|
||||
def obj' (f : OverColor Color) : Rep ℂ SL(2, ℂ) := Rep.of {
|
||||
toFun := fun M => PiTensorProduct.map (fun x => (colorToRep (f.hom x)).ρ M),
|
||||
map_one' := by
|
||||
simp
|
||||
map_mul' := fun M N => by
|
||||
simp only [CategoryTheory.Functor.id_obj, _root_.map_mul]
|
||||
ext x : 2
|
||||
simp only [LinearMap.compMultilinearMap_apply, PiTensorProduct.map_tprod, LinearMap.mul_apply]}
|
||||
|
||||
lemma obj'_ρ (f : OverColor Color) (M : SL(2, ℂ)) : (obj' f).ρ M =
|
||||
PiTensorProduct.map (fun x => (colorToRep (f.hom x)).ρ M) := rfl
|
||||
|
||||
lemma obj'_ρ_tprod (f : OverColor Color) (M : SL(2, ℂ))
|
||||
(x : (i : f.left) → CoeSort.coe (colorToRep (f.hom i))) :
|
||||
(obj' f).ρ M ((PiTensorProduct.tprod ℂ) x) =
|
||||
PiTensorProduct.tprod ℂ (fun i => (colorToRep (f.hom i)).ρ M (x i)) := by
|
||||
rw [obj'_ρ]
|
||||
change (PiTensorProduct.map fun x => (colorToRep (f.hom x)).ρ M) ((PiTensorProduct.tprod ℂ) x) =
|
||||
(PiTensorProduct.tprod ℂ) fun i => ((colorToRep (f.hom i)).ρ M) (x i)
|
||||
rw [PiTensorProduct.map_tprod]
|
||||
|
||||
/-- Given a morphism in `OverColor Color` the corresopnding linear equivalence between `obj' _`
|
||||
induced by reindexing. -/
|
||||
def mapToLinearEquiv' {f g : OverColor Color} (m : f ⟶ g) : (obj' f).V ≃ₗ[ℂ] (obj' g).V :=
|
||||
(PiTensorProduct.reindex ℂ (fun x => colorToRep (f.hom x)) (OverColor.Hom.toEquiv m)).trans
|
||||
(PiTensorProduct.congr (fun i => colorToRepCongr (OverColor.Hom.toEquiv_symm_apply m i)))
|
||||
|
||||
lemma mapToLinearEquiv'_tprod {f g : OverColor Color} (m : f ⟶ g)
|
||||
(x : (i : f.left) → CoeSort.coe (colorToRep (f.hom i))) :
|
||||
mapToLinearEquiv' m (PiTensorProduct.tprod ℂ x) =
|
||||
PiTensorProduct.tprod ℂ (fun i => (colorToRepCongr (OverColor.Hom.toEquiv_symm_apply m i))
|
||||
(x ((OverColor.Hom.toEquiv m).symm i))) := by
|
||||
rw [mapToLinearEquiv']
|
||||
simp only [CategoryTheory.Functor.id_obj, LinearEquiv.trans_apply]
|
||||
change (PiTensorProduct.congr fun i => colorToRepCongr _)
|
||||
((PiTensorProduct.reindex ℂ (fun x => CoeSort.coe (colorToRep (f.hom x)))
|
||||
(OverColor.Hom.toEquiv m)) ((PiTensorProduct.tprod ℂ) x)) = _
|
||||
rw [PiTensorProduct.reindex_tprod, PiTensorProduct.congr_tprod]
|
||||
rfl
|
||||
|
||||
/-- Given a morphism in `OverColor Color` the corresopnding map of representations induced by
|
||||
reindexing. -/
|
||||
def map' {f g : OverColor Color} (m : f ⟶ g) : obj' f ⟶ obj' g where
|
||||
hom := (mapToLinearEquiv' m).toLinearMap
|
||||
comm M := by
|
||||
ext x : 2
|
||||
refine PiTensorProduct.induction_on' x ?_ (by
|
||||
intro x y hx hy
|
||||
simp only [CategoryTheory.Functor.id_obj, map_add, hx, ModuleCat.coe_comp,
|
||||
Function.comp_apply, hy])
|
||||
intro r x
|
||||
simp only [CategoryTheory.Functor.id_obj, PiTensorProduct.tprodCoeff_eq_smul_tprod,
|
||||
_root_.map_smul, ModuleCat.coe_comp, Function.comp_apply]
|
||||
apply congrArg
|
||||
change (mapToLinearEquiv' m) (((obj' f).ρ M) ((PiTensorProduct.tprod ℂ) x)) =
|
||||
((obj' g).ρ M) ((mapToLinearEquiv' m) ((PiTensorProduct.tprod ℂ) x))
|
||||
rw [mapToLinearEquiv'_tprod, obj'_ρ_tprod]
|
||||
erw [mapToLinearEquiv'_tprod, obj'_ρ_tprod]
|
||||
apply congrArg
|
||||
funext i
|
||||
rw [colorToRepCongr_comm_ρ]
|
||||
|
||||
end colorFun
|
||||
|
||||
/-- The functor between `OverColor Color` and `Rep ℂ SL(2, ℂ)` taking a map of colors
|
||||
to the corresponding tensor product representation. -/
|
||||
@[simps! obj_V_carrier]
|
||||
def colorFun : OverColor Color ⥤ Rep ℂ SL(2, ℂ) where
|
||||
obj := colorFun.obj'
|
||||
map := colorFun.map'
|
||||
map_id f := by
|
||||
ext x
|
||||
refine PiTensorProduct.induction_on' x (fun r x => ?_) (fun x y hx hy => by
|
||||
simp only [CategoryTheory.Functor.id_obj, map_add, hx, ModuleCat.coe_comp,
|
||||
Function.comp_apply, hy])
|
||||
simp only [CategoryTheory.Functor.id_obj, PiTensorProduct.tprodCoeff_eq_smul_tprod,
|
||||
_root_.map_smul, Action.id_hom, ModuleCat.id_apply]
|
||||
apply congrArg
|
||||
erw [colorFun.mapToLinearEquiv'_tprod]
|
||||
exact congrArg _ (funext (fun i => rfl))
|
||||
map_comp {X Y Z} f g := by
|
||||
ext x
|
||||
refine PiTensorProduct.induction_on' x (fun r x => ?_) (fun x y hx hy => by
|
||||
simp only [CategoryTheory.Functor.id_obj, map_add, hx, ModuleCat.coe_comp,
|
||||
Function.comp_apply, hy])
|
||||
simp only [Functor.id_obj, PiTensorProduct.tprodCoeff_eq_smul_tprod, _root_.map_smul,
|
||||
Action.comp_hom, ModuleCat.coe_comp, Function.comp_apply]
|
||||
apply congrArg
|
||||
rw [colorFun.map', colorFun.map', colorFun.map']
|
||||
change (colorFun.mapToLinearEquiv' (CategoryTheory.CategoryStruct.comp f g))
|
||||
((PiTensorProduct.tprod ℂ) x) =
|
||||
(colorFun.mapToLinearEquiv' g) ((colorFun.mapToLinearEquiv' f) ((PiTensorProduct.tprod ℂ) x))
|
||||
rw [colorFun.mapToLinearEquiv'_tprod, colorFun.mapToLinearEquiv'_tprod]
|
||||
erw [colorFun.mapToLinearEquiv'_tprod]
|
||||
refine congrArg _ (funext (fun i => ?_))
|
||||
simp only [colorToRepCongr, Function.comp_apply, Equiv.cast_symm, LinearEquiv.coe_mk,
|
||||
Equiv.cast_apply, cast_cast, cast_inj]
|
||||
rfl
|
||||
|
||||
namespace colorFun
|
||||
|
||||
open CategoryTheory
|
||||
open MonoidalCategory
|
||||
|
||||
lemma map_tprod {X Y : OverColor Color} (p : (i : X.left) → (colorToRep (X.hom i)))
|
||||
(f : X ⟶ Y) : (colorFun.map f).hom (PiTensorProduct.tprod ℂ p) =
|
||||
PiTensorProduct.tprod ℂ fun (i : Y.left) => colorToRepCongr
|
||||
(OverColor.Hom.toEquiv_comp_inv_apply f i) (p ((OverColor.Hom.toEquiv f).symm i)) := by
|
||||
change (colorFun.map' f).hom ((PiTensorProduct.tprod ℂ) p) = _
|
||||
simp only [map', mapToLinearEquiv', Functor.id_obj]
|
||||
erw [LinearEquiv.trans_apply]
|
||||
change (PiTensorProduct.congr fun i => colorToRepCongr _)
|
||||
((PiTensorProduct.reindex ℂ (fun x => _) (OverColor.Hom.toEquiv f))
|
||||
((PiTensorProduct.tprod ℂ) p)) = _
|
||||
rw [PiTensorProduct.reindex_tprod, PiTensorProduct.congr_tprod]
|
||||
|
||||
lemma obj_ρ_tprod (f : OverColor Color) (M : SL(2, ℂ))
|
||||
(x : (i : f.left) → CoeSort.coe (colorToRep (f.hom i))) :
|
||||
(colorFun.obj f).ρ M ((PiTensorProduct.tprod ℂ) x) =
|
||||
PiTensorProduct.tprod ℂ (fun i => (colorToRep (f.hom i)).ρ M (x i)) := by
|
||||
exact obj'_ρ_tprod _ _ _
|
||||
|
||||
@[simp]
|
||||
lemma obj_ρ_empty (g : SL(2, ℂ)) : (colorFun.obj (𝟙_ (OverColor Color))).ρ g = LinearMap.id := by
|
||||
erw [colorFun.obj'_ρ]
|
||||
ext x
|
||||
refine PiTensorProduct.induction_on' x (fun r x => ?_) <| fun x y hx hy => by
|
||||
simp only [CategoryTheory.Functor.id_obj, map_add, hx, ModuleCat.coe_comp,
|
||||
Function.comp_apply, hy]
|
||||
erw [hx, hy]
|
||||
rfl
|
||||
simp only [OverColor.instMonoidalCategoryStruct_tensorUnit_left, Functor.id_obj,
|
||||
OverColor.instMonoidalCategoryStruct_tensorUnit_hom, PiTensorProduct.tprodCoeff_eq_smul_tprod,
|
||||
_root_.map_smul, PiTensorProduct.map_tprod, LinearMap.id_coe, id_eq]
|
||||
apply congrArg
|
||||
apply congrArg
|
||||
funext i
|
||||
exact Empty.elim i
|
||||
|
||||
/-- The unit natural isomorphism. -/
|
||||
def ε : 𝟙_ (Rep ℂ SL(2, ℂ)) ≅ colorFun.obj (𝟙_ (OverColor Color)) where
|
||||
hom := {
|
||||
hom := (PiTensorProduct.isEmptyEquiv Empty).symm.toLinearMap
|
||||
comm := fun M => by
|
||||
refine LinearMap.ext (fun x => ?_)
|
||||
simp only [colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorUnit_left,
|
||||
OverColor.instMonoidalCategoryStruct_tensorUnit_hom,
|
||||
Action.instMonoidalCategory_tensorUnit_V, Action.tensorUnit_ρ', Functor.id_obj,
|
||||
Category.id_comp, LinearEquiv.coe_coe]
|
||||
erw [obj_ρ_empty M]
|
||||
rfl}
|
||||
inv := {
|
||||
hom := (PiTensorProduct.isEmptyEquiv Empty).toLinearMap
|
||||
comm := fun M => by
|
||||
refine LinearMap.ext (fun x => ?_)
|
||||
simp only [Action.instMonoidalCategory_tensorUnit_V, colorFun_obj_V_carrier,
|
||||
OverColor.instMonoidalCategoryStruct_tensorUnit_left,
|
||||
OverColor.instMonoidalCategoryStruct_tensorUnit_hom, Functor.id_obj, Action.tensorUnit_ρ']
|
||||
erw [obj_ρ_empty M]
|
||||
rfl}
|
||||
hom_inv_id := by
|
||||
ext1
|
||||
simp only [Action.instMonoidalCategory_tensorUnit_V, CategoryStruct.comp,
|
||||
OverColor.instMonoidalCategoryStruct_tensorUnit_hom,
|
||||
OverColor.instMonoidalCategoryStruct_tensorUnit_left, Functor.id_obj, Action.Hom.comp_hom,
|
||||
colorFun_obj_V_carrier, LinearEquiv.comp_coe, LinearEquiv.symm_trans_self,
|
||||
LinearEquiv.refl_toLinearMap, Action.id_hom]
|
||||
rfl
|
||||
inv_hom_id := by
|
||||
ext1
|
||||
simp only [CategoryStruct.comp, OverColor.instMonoidalCategoryStruct_tensorUnit_hom,
|
||||
OverColor.instMonoidalCategoryStruct_tensorUnit_left, Functor.id_obj, Action.Hom.comp_hom,
|
||||
colorFun_obj_V_carrier, Action.instMonoidalCategory_tensorUnit_V, LinearEquiv.comp_coe,
|
||||
LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, Action.id_hom]
|
||||
rfl
|
||||
|
||||
/-- An auxillary equivalence, and trivial, of modules needed to define `μModEquiv`. -/
|
||||
def colorToRepSumEquiv {X Y : OverColor Color} (i : X.left ⊕ Y.left) :
|
||||
Sum.elim (fun i => colorToRep (X.hom i)) (fun i => colorToRep (Y.hom i)) i ≃ₗ[ℂ]
|
||||
colorToRep (Sum.elim X.hom Y.hom i) :=
|
||||
match i with
|
||||
| Sum.inl _ => LinearEquiv.refl _ _
|
||||
| Sum.inr _ => LinearEquiv.refl _ _
|
||||
|
||||
/-- The equivalence of modules corresonding to the tensorate. -/
|
||||
def μModEquiv (X Y : OverColor Color) :
|
||||
(colorFun.obj X ⊗ colorFun.obj Y).V ≃ₗ[ℂ] colorFun.obj (X ⊗ Y) :=
|
||||
HepLean.PiTensorProduct.tmulEquiv ≪≫ₗ PiTensorProduct.congr colorToRepSumEquiv
|
||||
|
||||
lemma μModEquiv_tmul_tprod {X Y : OverColor Color}(p : (i : X.left) → (colorToRep (X.hom i)))
|
||||
(q : (i : Y.left) → (colorToRep (Y.hom i))) :
|
||||
(μModEquiv X Y) ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q) =
|
||||
(PiTensorProduct.tprod ℂ) fun i =>
|
||||
(colorToRepSumEquiv i) (HepLean.PiTensorProduct.elimPureTensor p q i) := by
|
||||
rw [μModEquiv]
|
||||
simp only [colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left,
|
||||
OverColor.instMonoidalCategoryStruct_tensorObj_hom, Action.instMonoidalCategory_tensorObj_V,
|
||||
Functor.id_obj, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj]
|
||||
rw [LinearEquiv.trans_apply]
|
||||
erw [HepLean.PiTensorProduct.tmulEquiv_tmul_tprod]
|
||||
change (PiTensorProduct.congr colorToRepSumEquiv) ((PiTensorProduct.tprod ℂ)
|
||||
(HepLean.PiTensorProduct.elimPureTensor p q)) = _
|
||||
rw [PiTensorProduct.congr_tprod]
|
||||
rfl
|
||||
|
||||
/-- The natural isomorphism corresponding to the tensorate. -/
|
||||
def μ (X Y : OverColor Color) : colorFun.obj X ⊗ colorFun.obj Y ≅ colorFun.obj (X ⊗ Y) where
|
||||
hom := {
|
||||
hom := (μModEquiv X Y).toLinearMap
|
||||
comm := fun M => by
|
||||
refine HepLean.PiTensorProduct.induction_tmul (fun p q => ?_)
|
||||
simp only [colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left,
|
||||
OverColor.instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj, CategoryStruct.comp,
|
||||
Action.instMonoidalCategory_tensorObj_V, Action.tensor_ρ', LinearMap.coe_comp,
|
||||
Function.comp_apply]
|
||||
change (μModEquiv X Y) (((((colorFun.obj X).ρ M) (PiTensorProduct.tprod ℂ p)) ⊗ₜ[ℂ]
|
||||
(((colorFun.obj Y).ρ M) (PiTensorProduct.tprod ℂ q)))) = ((colorFun.obj (X ⊗ Y)).ρ M)
|
||||
((μModEquiv X Y) ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q))
|
||||
rw [μModEquiv_tmul_tprod]
|
||||
erw [obj'_ρ_tprod, obj'_ρ_tprod, obj'_ρ_tprod]
|
||||
rw [μModEquiv_tmul_tprod]
|
||||
apply congrArg
|
||||
funext i
|
||||
match i with
|
||||
| Sum.inl i =>
|
||||
rfl
|
||||
| Sum.inr i =>
|
||||
rfl
|
||||
}
|
||||
inv := {
|
||||
hom := (μModEquiv X Y).symm.toLinearMap
|
||||
comm := fun M => by
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, CategoryStruct.comp,
|
||||
colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left,
|
||||
OverColor.instMonoidalCategoryStruct_tensorObj_hom, Action.tensor_ρ']
|
||||
erw [LinearEquiv.eq_comp_toLinearMap_symm,LinearMap.comp_assoc,
|
||||
LinearEquiv.toLinearMap_symm_comp_eq]
|
||||
refine HepLean.PiTensorProduct.induction_tmul (fun p q => ?_)
|
||||
simp only [colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left,
|
||||
OverColor.instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj, CategoryStruct.comp,
|
||||
Action.instMonoidalCategory_tensorObj_V, Action.tensor_ρ', LinearMap.coe_comp,
|
||||
Function.comp_apply]
|
||||
symm
|
||||
change (μModEquiv X Y) (((((colorFun.obj X).ρ M) (PiTensorProduct.tprod ℂ p)) ⊗ₜ[ℂ]
|
||||
(((colorFun.obj Y).ρ M) (PiTensorProduct.tprod ℂ q)))) = ((colorFun.obj (X ⊗ Y)).ρ M)
|
||||
((μModEquiv X Y) ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q))
|
||||
rw [μModEquiv_tmul_tprod]
|
||||
erw [obj'_ρ_tprod, obj'_ρ_tprod, obj'_ρ_tprod]
|
||||
rw [μModEquiv_tmul_tprod]
|
||||
apply congrArg
|
||||
funext i
|
||||
match i with
|
||||
| Sum.inl i =>
|
||||
rfl
|
||||
| Sum.inr i =>
|
||||
rfl}
|
||||
hom_inv_id := by
|
||||
ext1
|
||||
simp only [Action.instMonoidalCategory_tensorObj_V, CategoryStruct.comp, Action.Hom.comp_hom,
|
||||
colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left,
|
||||
OverColor.instMonoidalCategoryStruct_tensorObj_hom, LinearEquiv.comp_coe,
|
||||
LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, Action.id_hom]
|
||||
rfl
|
||||
inv_hom_id := by
|
||||
ext1
|
||||
simp only [CategoryStruct.comp, Action.instMonoidalCategory_tensorObj_V, Action.Hom.comp_hom,
|
||||
colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left,
|
||||
OverColor.instMonoidalCategoryStruct_tensorObj_hom, LinearEquiv.comp_coe,
|
||||
LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap, Action.id_hom]
|
||||
rfl
|
||||
|
||||
lemma μ_tmul_tprod {X Y : OverColor Color} (p : (i : X.left) → (colorToRep (X.hom i)))
|
||||
(q : (i : Y.left) → (colorToRep (Y.hom i))) :
|
||||
(μ X Y).hom.hom ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q) =
|
||||
(PiTensorProduct.tprod ℂ) fun i =>
|
||||
(colorToRepSumEquiv i) (HepLean.PiTensorProduct.elimPureTensor p q i) := by
|
||||
exact μModEquiv_tmul_tprod p q
|
||||
|
||||
lemma μ_natural_left {X Y : OverColor Color} (f : X ⟶ Y) (Z : OverColor Color) :
|
||||
MonoidalCategory.whiskerRight (colorFun.map f) (colorFun.obj Z) ≫ (μ Y Z).hom =
|
||||
(μ X Z).hom ≫ colorFun.map (MonoidalCategory.whiskerRight f Z) := by
|
||||
ext1
|
||||
refine HepLean.PiTensorProduct.induction_tmul (fun p q => ?_)
|
||||
simp only [colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left,
|
||||
OverColor.instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj, CategoryStruct.comp,
|
||||
Action.Hom.comp_hom, Action.instMonoidalCategory_tensorObj_V,
|
||||
Action.instMonoidalCategory_whiskerRight_hom, LinearMap.coe_comp, Function.comp_apply]
|
||||
change _ = (colorFun.map (MonoidalCategory.whiskerRight f Z)).hom
|
||||
((μ X Z).hom.hom ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q))
|
||||
rw [μ_tmul_tprod]
|
||||
change _ = (colorFun.map (f ▷ Z)).hom
|
||||
((PiTensorProduct.tprod ℂ) fun i => (colorToRepSumEquiv i)
|
||||
(HepLean.PiTensorProduct.elimPureTensor p q i))
|
||||
rw [colorFun.map_tprod]
|
||||
have h1 : (((colorFun.map f).hom ▷ (colorFun.obj Z).V) ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ]
|
||||
(PiTensorProduct.tprod ℂ) q)) = ((colorFun.map f).hom
|
||||
((PiTensorProduct.tprod ℂ) p) ⊗ₜ[ℂ] ((PiTensorProduct.tprod ℂ) q)) := by rfl
|
||||
erw [h1]
|
||||
rw [colorFun.map_tprod]
|
||||
change (μ Y Z).hom.hom (((PiTensorProduct.tprod ℂ) fun i => (colorToRepCongr _)
|
||||
(p ((OverColor.Hom.toEquiv f).symm i))) ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q) = _
|
||||
rw [μ_tmul_tprod]
|
||||
apply congrArg
|
||||
funext i
|
||||
match i with
|
||||
| Sum.inl i => rfl
|
||||
| Sum.inr i => rfl
|
||||
|
||||
lemma μ_natural_right {X Y : OverColor Color} (X' : OverColor Color) (f : X ⟶ Y) :
|
||||
MonoidalCategory.whiskerLeft (colorFun.obj X') (colorFun.map f) ≫ (μ X' Y).hom =
|
||||
(μ X' X).hom ≫ colorFun.map (MonoidalCategory.whiskerLeft X' f) := by
|
||||
ext1
|
||||
refine HepLean.PiTensorProduct.induction_tmul (fun p q => ?_)
|
||||
simp only [colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left,
|
||||
OverColor.instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj, CategoryStruct.comp,
|
||||
Action.Hom.comp_hom, Action.instMonoidalCategory_tensorObj_V,
|
||||
Action.instMonoidalCategory_whiskerLeft_hom, LinearMap.coe_comp, Function.comp_apply]
|
||||
change _ = (colorFun.map (X' ◁ f)).hom ((μ X' X).hom.hom
|
||||
((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q))
|
||||
rw [μ_tmul_tprod]
|
||||
change _ = (colorFun.map (X' ◁ f)).hom ((PiTensorProduct.tprod ℂ) fun i =>
|
||||
(colorToRepSumEquiv i) (HepLean.PiTensorProduct.elimPureTensor p q i))
|
||||
rw [map_tprod]
|
||||
have h1 : (((colorFun.obj X').V ◁ (colorFun.map f).hom)
|
||||
((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q))
|
||||
= ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (colorFun.map f).hom ((PiTensorProduct.tprod ℂ) q)) := by
|
||||
rfl
|
||||
erw [h1]
|
||||
rw [map_tprod]
|
||||
change (μ X' Y).hom.hom ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) fun i =>
|
||||
(colorToRepCongr _) (q ((OverColor.Hom.toEquiv f).symm i))) = _
|
||||
rw [μ_tmul_tprod]
|
||||
apply congrArg
|
||||
funext i
|
||||
match i with
|
||||
| Sum.inl i => rfl
|
||||
| Sum.inr i => rfl
|
||||
|
||||
lemma associativity (X Y Z : OverColor Color) :
|
||||
whiskerRight (μ X Y).hom (colorFun.obj Z) ≫
|
||||
(μ (X ⊗ Y) Z).hom ≫ colorFun.map (associator X Y Z).hom =
|
||||
(associator (colorFun.obj X) (colorFun.obj Y) (colorFun.obj Z)).hom ≫
|
||||
whiskerLeft (colorFun.obj X) (μ Y Z).hom ≫ (μ X (Y ⊗ Z)).hom := by
|
||||
ext1
|
||||
refine HepLean.PiTensorProduct.induction_assoc' (fun p q m => ?_)
|
||||
simp only [colorFun_obj_V_carrier, OverColor.instMonoidalCategoryStruct_tensorObj_left,
|
||||
OverColor.instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj, CategoryStruct.comp,
|
||||
Action.Hom.comp_hom, Action.instMonoidalCategory_tensorObj_V,
|
||||
Action.instMonoidalCategory_whiskerRight_hom, LinearMap.coe_comp, Function.comp_apply,
|
||||
Action.instMonoidalCategory_whiskerLeft_hom, Action.instMonoidalCategory_associator_hom_hom]
|
||||
change (colorFun.map (α_ X Y Z).hom).hom ((μ (X ⊗ Y) Z).hom.hom
|
||||
((((μ X Y).hom.hom ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ]
|
||||
(PiTensorProduct.tprod ℂ) q)) ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) m))) =
|
||||
(μ X (Y ⊗ Z)).hom.hom ((((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] ((μ Y Z).hom.hom
|
||||
((PiTensorProduct.tprod ℂ) q ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) m)))))
|
||||
rw [μ_tmul_tprod, μ_tmul_tprod]
|
||||
change (colorFun.map (α_ X Y Z).hom).hom ((μ (X ⊗ Y) Z).hom.hom
|
||||
(((PiTensorProduct.tprod ℂ) fun i => (colorToRepSumEquiv i)
|
||||
(HepLean.PiTensorProduct.elimPureTensor p q i)) ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) m)) =
|
||||
(μ X (Y ⊗ Z)).hom.hom ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) fun i =>
|
||||
(colorToRepSumEquiv i) (HepLean.PiTensorProduct.elimPureTensor q m i))
|
||||
rw [μ_tmul_tprod, μ_tmul_tprod]
|
||||
erw [map_tprod]
|
||||
apply congrArg
|
||||
funext i
|
||||
match i with
|
||||
| Sum.inl i => rfl
|
||||
| Sum.inr (Sum.inl i) => rfl
|
||||
| Sum.inr (Sum.inr i) => rfl
|
||||
|
||||
lemma left_unitality (X : OverColor Color) : (leftUnitor (colorFun.obj X)).hom =
|
||||
whiskerRight colorFun.ε.hom (colorFun.obj X) ≫
|
||||
(μ (𝟙_ (OverColor Color)) X).hom ≫ colorFun.map (leftUnitor X).hom := by
|
||||
ext1
|
||||
apply HepLean.PiTensorProduct.induction_mod_tmul (fun x q => ?_)
|
||||
simp only [colorFun_obj_V_carrier, Equivalence.symm_inverse,
|
||||
Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
|
||||
Action.instMonoidalCategory_tensorUnit_V, Functor.id_obj,
|
||||
Action.instMonoidalCategory_leftUnitor_hom_hom, CategoryStruct.comp, Action.Hom.comp_hom,
|
||||
Action.instMonoidalCategory_tensorObj_V, OverColor.instMonoidalCategoryStruct_tensorObj_left,
|
||||
OverColor.instMonoidalCategoryStruct_tensorUnit_left,
|
||||
OverColor.instMonoidalCategoryStruct_tensorObj_hom,
|
||||
Action.instMonoidalCategory_whiskerRight_hom, LinearMap.coe_comp, Function.comp_apply]
|
||||
change TensorProduct.lid ℂ (colorFun.obj X) (x ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q) =
|
||||
(colorFun.map (λ_ X).hom).hom ((μ (𝟙_ (OverColor Color)) X).hom.hom
|
||||
((((PiTensorProduct.isEmptyEquiv Empty).symm x) ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q)))
|
||||
simp only [Functor.id_obj, lid_tmul, colorFun_obj_V_carrier,
|
||||
OverColor.instMonoidalCategoryStruct_tensorObj_left,
|
||||
OverColor.instMonoidalCategoryStruct_tensorUnit_left,
|
||||
OverColor.instMonoidalCategoryStruct_tensorObj_hom, Action.instMonoidalCategory_tensorObj_V,
|
||||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj,
|
||||
OverColor.instMonoidalCategoryStruct_tensorUnit_hom, PiTensorProduct.isEmptyEquiv,
|
||||
LinearEquiv.coe_symm_mk]
|
||||
rw [TensorProduct.smul_tmul, TensorProduct.tmul_smul]
|
||||
erw [LinearMap.map_smul, LinearMap.map_smul]
|
||||
apply congrArg
|
||||
change _ = (colorFun.map (λ_ X).hom).hom ((μ (𝟙_ (OverColor Color)) X).hom.hom
|
||||
((PiTensorProduct.tprod ℂ) _ ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) q))
|
||||
rw [μ_tmul_tprod]
|
||||
erw [map_tprod]
|
||||
rfl
|
||||
|
||||
lemma right_unitality (X : OverColor Color) : (MonoidalCategory.rightUnitor (colorFun.obj X)).hom =
|
||||
whiskerLeft (colorFun.obj X) ε.hom ≫
|
||||
(μ X (𝟙_ (OverColor Color))).hom ≫ colorFun.map (MonoidalCategory.rightUnitor X).hom := by
|
||||
ext1
|
||||
apply HepLean.PiTensorProduct.induction_tmul_mod (fun p x => ?_)
|
||||
simp only [colorFun_obj_V_carrier, Functor.id_obj, Equivalence.symm_inverse,
|
||||
Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
|
||||
Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_rightUnitor_hom_hom,
|
||||
CategoryStruct.comp, Action.Hom.comp_hom, Action.instMonoidalCategory_tensorObj_V,
|
||||
OverColor.instMonoidalCategoryStruct_tensorObj_left,
|
||||
OverColor.instMonoidalCategoryStruct_tensorUnit_left,
|
||||
OverColor.instMonoidalCategoryStruct_tensorObj_hom, Action.instMonoidalCategory_whiskerLeft_hom,
|
||||
LinearMap.coe_comp, Function.comp_apply]
|
||||
change TensorProduct.rid ℂ (colorFun.obj X) ((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] x) =
|
||||
(colorFun.map (ρ_ X).hom).hom ((μ X (𝟙_ (OverColor Color))).hom.hom
|
||||
((((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] ((PiTensorProduct.isEmptyEquiv Empty).symm x)))))
|
||||
simp only [Functor.id_obj, rid_tmul, colorFun_obj_V_carrier,
|
||||
OverColor.instMonoidalCategoryStruct_tensorObj_left,
|
||||
OverColor.instMonoidalCategoryStruct_tensorUnit_left,
|
||||
OverColor.instMonoidalCategoryStruct_tensorObj_hom, Action.instMonoidalCategory_tensorObj_V,
|
||||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj,
|
||||
OverColor.instMonoidalCategoryStruct_tensorUnit_hom, PiTensorProduct.isEmptyEquiv,
|
||||
LinearEquiv.coe_symm_mk, tmul_smul]
|
||||
erw [LinearMap.map_smul, LinearMap.map_smul]
|
||||
apply congrArg
|
||||
change _ = (colorFun.map (ρ_ X).hom).hom ((μ X (𝟙_ (OverColor Color))).hom.hom
|
||||
((PiTensorProduct.tprod ℂ) p ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) _))
|
||||
rw [μ_tmul_tprod]
|
||||
erw [map_tprod]
|
||||
rfl
|
||||
|
||||
end colorFun
|
||||
|
||||
/-- The monoidal functor between `OverColor Color` and `Rep ℂ SL(2, ℂ)` taking a map of colors
|
||||
to the corresponding tensor product representation. -/
|
||||
def colorFunMon : MonoidalFunctor (OverColor Color) (Rep ℂ SL(2, ℂ)) where
|
||||
toFunctor := colorFun
|
||||
ε := colorFun.ε.hom
|
||||
μ X Y := (colorFun.μ X Y).hom
|
||||
μ_natural_left := colorFun.μ_natural_left
|
||||
μ_natural_right := colorFun.μ_natural_right
|
||||
associativity := colorFun.associativity
|
||||
left_unitality := colorFun.left_unitality
|
||||
right_unitality := colorFun.right_unitality
|
||||
|
||||
end
|
||||
end Fermion
|
||||
|
|
@ -1,107 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.Tensors.OverColor.Basic
|
||||
import HepLean.Tensors.ComplexLorentz.ColorFun
|
||||
import HepLean.Mathematics.PiTensorProduct
|
||||
/-!
|
||||
|
||||
## The contraction monoidal natural transformation
|
||||
|
||||
-/
|
||||
|
||||
namespace Fermion
|
||||
|
||||
noncomputable section
|
||||
|
||||
open Matrix
|
||||
open MatrixGroups
|
||||
open Complex
|
||||
open TensorProduct
|
||||
open IndexNotation
|
||||
open CategoryTheory
|
||||
open MonoidalCategory
|
||||
|
||||
namespace pairwiseRepFun
|
||||
|
||||
/-- Given an object `c : OverColor Color` the representation defined by
|
||||
`⨂[R] x, colorToRep (c.hom x) ⊗[R] colorToRep (τ (c.hom x))`. -/
|
||||
def obj' (c : OverColor Color) : Rep ℂ SL(2, ℂ) := Rep.of {
|
||||
toFun := fun M => PiTensorProduct.map (fun x =>
|
||||
TensorProduct.map ((colorToRep (c.hom x)).ρ M) ((colorToRep (τ (c.hom x))).ρ M)),
|
||||
map_one' := by
|
||||
simp
|
||||
map_mul' := fun x y => by
|
||||
simp only [Functor.id_obj, _root_.map_mul]
|
||||
ext x' : 2
|
||||
simp only [LinearMap.compMultilinearMap_apply, PiTensorProduct.map_tprod, LinearMap.mul_apply]
|
||||
apply congrArg
|
||||
funext i
|
||||
change _ = (TensorProduct.map _ _ ∘ₗ TensorProduct.map _ _) (x' i)
|
||||
rw [← TensorProduct.map_comp]
|
||||
rfl}
|
||||
|
||||
/-- Given a morphism in `OverColor Color` the corresopnding linear equivalence between `obj' _`
|
||||
induced by reindexing. -/
|
||||
def mapToLinearEquiv' {f g : OverColor Color} (m : f ⟶ g) : (obj' f).V ≃ₗ[ℂ] (obj' g).V :=
|
||||
(PiTensorProduct.reindex ℂ (fun x => (colorToRep (f.hom x)).V ⊗[ℂ] (colorToRep (τ (f.hom x))).V)
|
||||
(OverColor.Hom.toEquiv m)).trans
|
||||
(PiTensorProduct.congr (fun i =>
|
||||
TensorProduct.congr (colorToRepCongr (OverColor.Hom.toEquiv_symm_apply m i))
|
||||
((colorToRepCongr (congrArg τ (OverColor.Hom.toEquiv_symm_apply m i))))))
|
||||
|
||||
lemma mapToLinearEquiv'_tprod {f g : OverColor Color} (m : f ⟶ g)
|
||||
(x : (i : f.left) → (colorToRep (f.hom i)).V ⊗[ℂ] (colorToRep (τ (f.hom i))).V) :
|
||||
mapToLinearEquiv' m (PiTensorProduct.tprod ℂ x) =
|
||||
PiTensorProduct.tprod ℂ fun i =>
|
||||
(TensorProduct.congr (colorToRepCongr (OverColor.Hom.toEquiv_symm_apply m i))
|
||||
(colorToRepCongr (mapToLinearEquiv'.proof_4 m i))) (x ((OverColor.Hom.toEquiv m).symm i)) := by
|
||||
simp only [mapToLinearEquiv', Functor.id_obj, LinearEquiv.trans_apply]
|
||||
change (PiTensorProduct.congr fun i => TensorProduct.congr (colorToRepCongr _)
|
||||
(colorToRepCongr _)) ((PiTensorProduct.reindex ℂ
|
||||
(fun x => ↑(colorToRep (f.hom x)).V ⊗[ℂ] ↑(colorToRep (τ (f.hom x))).V)
|
||||
(OverColor.Hom.toEquiv m)) ((PiTensorProduct.tprod ℂ) x)) = _
|
||||
rw [PiTensorProduct.reindex_tprod]
|
||||
erw [PiTensorProduct.congr_tprod]
|
||||
rfl
|
||||
|
||||
end pairwiseRepFun
|
||||
|
||||
/-
|
||||
|
||||
def contrPairPairwiseRep (c : OverColor Color) :
|
||||
(colorFunMon.obj c) ⊗ colorFunMon.obj ((OverColor.map τ).obj c) ⟶
|
||||
pairwiseRep c where
|
||||
hom := TensorProduct.lift (PiTensorProduct.map₂ (fun x =>
|
||||
TensorProduct.mk ℂ (colorToRep (c.hom x)).V (colorToRep (τ (c.hom x))).V))
|
||||
comm M := by
|
||||
refine HepLean.PiTensorProduct.induction_tmul (fun x y => ?_)
|
||||
simp only [Functor.id_obj, CategoryStruct.comp, Action.instMonoidalCategory_tensorObj_V,
|
||||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, Action.tensor_ρ', LinearMap.coe_comp,
|
||||
Function.comp_apply]
|
||||
change (TensorProduct.lift
|
||||
(PiTensorProduct.map₂ fun x => TensorProduct.mk ℂ ↑(colorToRep (c.hom x)).V
|
||||
↑(colorToRep (τ (c.hom x))).V))
|
||||
((TensorProduct.map _ _)
|
||||
((PiTensorProduct.tprod ℂ) x ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) y)) = _
|
||||
rw [TensorProduct.map_tmul]
|
||||
erw [colorFun.obj_ρ_tprod, colorFun.obj_ρ_tprod]
|
||||
simp only [Functor.id_obj, lift.tmul]
|
||||
erw [PiTensorProduct.map₂_tprod_tprod]
|
||||
change _ = ((pairwiseRep c).ρ M)
|
||||
((TensorProduct.lift
|
||||
(PiTensorProduct.map₂ fun x => TensorProduct.mk ℂ ↑(colorToRep (c.hom x)).V
|
||||
↑(colorToRep (τ (c.hom x))).V))
|
||||
((PiTensorProduct.tprod ℂ) x ⊗ₜ[ℂ] (PiTensorProduct.tprod ℂ) y))
|
||||
simp only [mk_apply, Functor.id_obj, lift.tmul]
|
||||
rw [PiTensorProduct.map₂_tprod_tprod]
|
||||
simp only [pairwiseRep, Functor.id_obj, Rep.coe_of, Rep.of_ρ, MonoidHom.coe_mk, OneHom.coe_mk,
|
||||
mk_apply]
|
||||
erw [PiTensorProduct.map_tprod]
|
||||
rfl
|
||||
-/
|
||||
end
|
||||
end Fermion
|
||||
|
|
@ -3,8 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
|||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.Tensors.Tree.Basic
|
||||
import HepLean.Tensors.ComplexLorentz.TensorStruct
|
||||
import HepLean.Tensors.Tree.Elab
|
||||
import HepLean.Tensors.ComplexLorentz.Basic
|
||||
/-!
|
||||
|
||||
## The tensor structure for complex Lorentz tensors
|
||||
|
|
@ -22,21 +22,36 @@ open CategoryTheory
|
|||
|
||||
noncomputable section
|
||||
|
||||
namespace complexLorentzTensor
|
||||
namespace Fermion
|
||||
|
||||
/-- The color map for a 2d tensor with the first index up and the second index down. -/
|
||||
def upDown : Fin 2 → complexLorentzTensor.C
|
||||
| 0 => Fermion.Color.up
|
||||
| 1 => Fermion.Color.down
|
||||
/-!
|
||||
|
||||
variable (T S : complexLorentzTensor.F.obj (OverColor.mk upDown))
|
||||
## Example tensor trees
|
||||
|
||||
/-
|
||||
import HepLean.Tensors.Tree.Elab
|
||||
|
||||
#check {T | i m ⊗ S | m l}ᵀ.dot
|
||||
#check {T | i m ⊗ S | l τ(m)}ᵀ.dot
|
||||
-/
|
||||
end complexLorentzTensor
|
||||
open MatrixGroups
|
||||
open Matrix
|
||||
example (v : Fermion.leftHanded) : TensorTree complexLorentzTensor ![Color.upL] :=
|
||||
{v | i}ᵀ
|
||||
|
||||
example (v : Fermion.leftHanded ⊗ Lorentz.complexContr) :
|
||||
TensorTree complexLorentzTensor ![Color.upL, Color.up] :=
|
||||
{v | i j}ᵀ
|
||||
|
||||
example :
|
||||
TensorTree complexLorentzTensor ![Color.downR, Color.downR] :=
|
||||
{Fermion.altRightMetric | μ j}ᵀ
|
||||
|
||||
lemma fin_three_expand {R : Type} (f : Fin 3 → R) : f = ![f 0, f 1, f 2]:= by
|
||||
funext x
|
||||
fin_cases x <;> rfl
|
||||
/-
|
||||
example : True :=
|
||||
let f :=
|
||||
{Lorentz.coMetric |
|
||||
μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗ PauliMatrix.asConsTensor | ν α' β'}ᵀ
|
||||
sorry
|
||||
-/
|
||||
end Fermion
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -1,36 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.Tensors.Tree.Basic
|
||||
import HepLean.Tensors.ComplexLorentz.ColorFun
|
||||
/-!
|
||||
|
||||
## The tensor structure for complex Lorentz tensors
|
||||
|
||||
-/
|
||||
open IndexNotation
|
||||
open CategoryTheory
|
||||
open MonoidalCategory
|
||||
open Matrix
|
||||
open MatrixGroups
|
||||
open Complex
|
||||
open TensorProduct
|
||||
open IndexNotation
|
||||
open CategoryTheory
|
||||
|
||||
noncomputable section
|
||||
|
||||
/-- The tensor structure for complex Lorentz tensors. -/
|
||||
def complexLorentzTensor : TensorStruct where
|
||||
C := Fermion.Color
|
||||
G := SL(2, ℂ)
|
||||
G_group := inferInstance
|
||||
k := ℂ
|
||||
k_commRing := inferInstance
|
||||
F := Fermion.colorFunMon
|
||||
τ := Fermion.τ
|
||||
evalNo := Fermion.evalNo
|
||||
|
||||
end
|
||||
|
|
@ -25,10 +25,12 @@ variable {C k : Type} [CommRing k] {G : Type} [Group G]
|
|||
variable (F F' : Discrete C ⥤ Rep k G) (η : F ⟶ F')
|
||||
noncomputable section
|
||||
|
||||
/-- The functor taking `c` to `F c ⊗ F c`. -/
|
||||
def pair : Discrete C ⥤ Rep k G := F ⊗ F
|
||||
|
||||
def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅
|
||||
(lift.obj F).obj (OverColor.mk ![c,c]) := by
|
||||
/-- The isomorphism between the image of `(pair F).obj` and
|
||||
`(lift.obj F).obj (OverColor.mk ![c,c])`. -/
|
||||
def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅ (lift.obj F).obj (OverColor.mk ![c,c]) := by
|
||||
symm
|
||||
apply ((lift.obj F).mapIso fin2Iso).trans
|
||||
apply ((lift.obj F).μIso _ _).symm.trans
|
||||
|
|
@ -46,10 +48,11 @@ def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅
|
|||
fin_cases x
|
||||
rfl
|
||||
|
||||
|
||||
/-- The functor taking `c` to `F c ⊗ F (τ c)`. -/
|
||||
def pairτ (τ : C → C) : Discrete C ⥤ Rep k G :=
|
||||
F ⊗ ((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤ Discrete C) ⋙ F)
|
||||
|
||||
/-- The functor taking `c` to `F (τ c) ⊗ F c`. -/
|
||||
def τPair (τ : C → C) : Discrete C ⥤ Rep k G :=
|
||||
((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤ Discrete C) ⋙ F) ⊗ F
|
||||
|
||||
|
|
|
|||
|
|
@ -40,6 +40,8 @@ def mkIso {c1 c2 : X → C} (h : c1 = c2) : mk c1 ≅ mk c2 :=
|
|||
subst h
|
||||
rfl))
|
||||
|
||||
/-- The isomorphism splitting a `mk c` for `Fin 2 → C` into the tensor product of
|
||||
the `Fin 1 → C` maps defined by `c 0` and `c 1`. -/
|
||||
def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] :=by
|
||||
let e1 : Fin 2 ≃ Fin 1 ⊕ Fin 1 := (finSumFinEquiv (n := 1)).symm
|
||||
apply (equivToIso e1).trans
|
||||
|
|
@ -52,11 +54,6 @@ def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] :=by
|
|||
fin_cases x
|
||||
rfl
|
||||
|
||||
def finSwapTwo {n : ℕ} (i : Fin n) : Fin (2 + n) ≃ Fin n.succ.succ := by
|
||||
let e1 := Equiv.swap (Fin.castAdd n (0 : Fin 2)) (Fin.natAdd 2 i)
|
||||
let e2 := Equiv.swap (Fin.castAdd n (1 : Fin 2)) (Fin.natAdd 2 i)
|
||||
|
||||
|
||||
/-- The equivalence between `Fin n.succ` and `Fin 1 ⊕ Fin n` extracting the
|
||||
`i`th component. -/
|
||||
def finExtractOne {n : ℕ} (i : Fin n.succ) : Fin n.succ ≃ Fin 1 ⊕ Fin n :=
|
||||
|
|
@ -191,5 +188,31 @@ def contrPairEquiv {n : ℕ} (τ : C → C) (c : Fin n.succ.succ → C) (i : Fin
|
|||
(contrPairFin1Fin1 τ ((c ∘ ⇑(finExtractTwo i j).symm) ∘ Sum.inl) (by simpa using h)) <|
|
||||
mkIso (by ext x; simp)
|
||||
|
||||
|
||||
/-- Given a function `c` from `Fin 1` to `C`, this function returns a morphism
|
||||
from `mk c` to `mk ![c 0]`. --/
|
||||
def permFinOne (c : Fin 1 → C) : mk c ⟶ mk ![c 0] :=
|
||||
(mkIso (by
|
||||
funext x
|
||||
fin_cases x
|
||||
rfl)).hom
|
||||
|
||||
/-- This a function that takes a function `c` from `Fin 2` to `C` and
|
||||
returns a morphism from `mk c` to `mk ![c 0, c 1]`. --/
|
||||
def permFinTwo (c : Fin 2 → C) : mk c ⟶ mk ![c 0, c 1] :=
|
||||
(mkIso (by
|
||||
funext x
|
||||
fin_cases x <;>
|
||||
rfl)).hom
|
||||
|
||||
/-- This is a function that takes a function `c` from `Fin 3` to `C` and returns a morphism
|
||||
from `mk c` to `mk ![c 0, c 1, c 2]`. --/
|
||||
def permFinThree (c : Fin 3 → C) : mk c ⟶ mk ![c 0, c 1, c 2] :=
|
||||
(mkIso (by
|
||||
funext x
|
||||
fin_cases x <;>
|
||||
rfl)).hom
|
||||
|
||||
|
||||
end OverColor
|
||||
end IndexNotation
|
||||
|
|
|
|||
|
|
@ -660,11 +660,19 @@ variable (F F' : Discrete C ⥤ Rep k G) (η : F ⟶ F')
|
|||
|
||||
noncomputable section
|
||||
|
||||
/--
|
||||
The `forgetLiftAppV` function takes an object `c` of type `C` and returns a linear equivalence
|
||||
between the vector space obtained by applying the lift of `F` and that obtained by applying
|
||||
`F`.
|
||||
--/
|
||||
def forgetLiftAppV (c : C) : ((lift.obj F).obj (OverColor.mk (fun (_ : Fin 1) => c))).V ≃ₗ[k]
|
||||
(F.obj (Discrete.mk c)).V :=
|
||||
(PiTensorProduct.subsingletonEquiv 0 :
|
||||
(⨂[k] (_ : Fin 1), (F.obj (Discrete.mk c))) ≃ₗ[k] F.obj (Discrete.mk c) )
|
||||
|
||||
/-- The `forgetLiftAppV` function takes an object `c` of type `C` and returns a isomorphism
|
||||
between the objects obtained by applying the lift of `F` and that obtained by applying
|
||||
`F`. -/
|
||||
def forgetLiftApp (c : C) : (lift.obj F).obj (OverColor.mk (fun (_ : Fin 1 ) => c))
|
||||
≅ F.obj (Discrete.mk c) :=
|
||||
Action.mkIso (forgetLiftAppV F c).toModuleIso
|
||||
|
|
|
|||
|
|
@ -38,9 +38,9 @@ structure TensorStruct where
|
|||
τ : C → C
|
||||
τ_involution : Function.Involutive τ
|
||||
/-- The natural transformation describing contraction. -/
|
||||
contr : OverColor.Discrete.pairτ F τ ⟶ 𝟙_ (Discrete C ⥤ Rep k G)
|
||||
contr : OverColor.Discrete.pairτ FDiscrete τ ⟶ 𝟙_ (Discrete C ⥤ Rep k G)
|
||||
/-- The natural transformation describing the metric. -/
|
||||
metricNat : 𝟙_ (Discrete C ⥤ Rep k G) ⟶ OverColor.Discrete.pair FDiscrete
|
||||
metric : 𝟙_ (Discrete C ⥤ Rep k G) ⟶ OverColor.Discrete.pair FDiscrete
|
||||
/-- The natural transformation describing the unit. -/
|
||||
unit : 𝟙_ (Discrete C ⥤ Rep k G) ⟶ OverColor.Discrete.τPair FDiscrete τ
|
||||
/-- A specification of the dimension of each color in C. This will be used for explicit
|
||||
|
|
@ -60,66 +60,18 @@ instance : Group S.G := S.G_group
|
|||
/-- The lift of the functor `S.F` to a monoidal functor. -/
|
||||
def F : MonoidalFunctor (OverColor S.C) (Rep S.k S.G) := (OverColor.lift).obj S.FDiscrete
|
||||
|
||||
/-
|
||||
def metric (c : S.C) : S.F.obj (OverColor.mk ![c, c]) :=
|
||||
(OverColor.Discrete.pairIso S.FDiscrete c).hom.hom <|
|
||||
(S.metricNat.app (Discrete.mk c)).hom (1 : S.k)
|
||||
-/
|
||||
|
||||
def contrNLE {n : ℕ} {i j : Fin n} (h : i ≠ j) : 2 ≤ n := by
|
||||
omega
|
||||
|
||||
def contrNPred {n : ℕ} {i j : Fin n} (h : i ≠ j) : n.pred.pred.succ.succ = n := by
|
||||
simp_all only [ne_eq, Nat.pred_eq_sub_one, Nat.succ_eq_add_one]
|
||||
have hi : i < n := i.isLt
|
||||
have hj : j < n := j.isLt
|
||||
by_contra hn
|
||||
have hn : n = 0 ∨ n =1 := by omega
|
||||
cases hn
|
||||
· omega
|
||||
· omega
|
||||
|
||||
def contrFstSucc {n : ℕ} {i j : Fin n} (hineqj : i ≠ j) :
|
||||
Fin n.pred.pred.succ.succ := Fin.castOrderIso (contrNPred hineqj).symm i
|
||||
|
||||
def contrSndSucc {n : ℕ} {i j : Fin n} (hineqj : i ≠ j) :
|
||||
Fin n.pred.pred.succ := (Fin.predAbove 0 (contrFstSucc hineqj)).predAbove
|
||||
(Fin.castOrderIso (contrNPred hineqj).symm j)
|
||||
|
||||
@[simp]
|
||||
lemma contrSndSucc_succAbove {n : ℕ} {i j : Fin n} (hineqj : i ≠ j) :
|
||||
(contrFstSucc hineqj).succAbove (contrSndSucc hineqj) =
|
||||
Fin.castOrderIso (contrNPred hineqj).symm j := by
|
||||
simp [contrFstSucc, contrSndSucc, Fin.succAbove,
|
||||
Fin.predAbove]
|
||||
split_ifs
|
||||
· rename_i h1 h2
|
||||
rw [Fin.lt_def] at h1 h2
|
||||
simp_all [Fin.lt_def, Fin.ext_iff]
|
||||
intro h
|
||||
omega
|
||||
· rename_i h1 h2
|
||||
rw [Fin.lt_def] at h1 h2
|
||||
simp_all [Fin.ext_iff]
|
||||
rw [Fin.lt_def]
|
||||
simp only [Fin.coe_cast, Fin.val_fin_lt]
|
||||
rw [Fin.lt_def]
|
||||
omega
|
||||
· rename_i h1 h2
|
||||
rw [Fin.lt_def] at h1 h2
|
||||
simp_all [Fin.ext_iff]
|
||||
rw [Fin.lt_def]
|
||||
simp only [Fin.coe_cast, Fin.val_fin_lt]
|
||||
omega
|
||||
· rename_i h1 h2
|
||||
rw [Fin.lt_def] at h1 h2
|
||||
simp_all [Fin.ext_iff]
|
||||
rw [Fin.lt_def]
|
||||
simp only [Fin.coe_cast, Fin.val_fin_lt]
|
||||
omega
|
||||
|
||||
|
||||
/-- The isomorphism of objects in `Rep S.k S.G` given an `i` in `Fin n.succ.succ` and
|
||||
a `j` in `Fin n.succ` allowing us to undertake contraction. -/
|
||||
def contrIso {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)) :
|
||||
S.F.obj (OverColor.mk c) ≅ ((OverColor.Discrete.pairτ S.FDiscrete S.τ).obj (Discrete.mk (c i))) ⊗
|
||||
S.F.obj (OverColor.mk c) ≅ ((OverColor.Discrete.pairτ S.FDiscrete S.τ).obj
|
||||
(Discrete.mk (c i))) ⊗
|
||||
(OverColor.lift.obj S.FDiscrete).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) :=
|
||||
(S.F.mapIso (OverColor.equivToIso (OverColor.finExtractTwo i j))).trans <|
|
||||
(S.F.mapIso (OverColor.mkSum (c ∘ (OverColor.finExtractTwo i j).symm))).trans <|
|
||||
|
|
@ -143,7 +95,13 @@ def contrIso {n : ℕ} (c : Fin n.succ.succ → S.C)
|
|||
fin_cases x
|
||||
simp [h]
|
||||
|
||||
def contrMap' {n : ℕ} (c : Fin n.succ.succ → S.C)
|
||||
/--
|
||||
`contrMap` is a function that takes a natural number `n`, a function `c` from
|
||||
`Fin n.succ.succ` to `S.C`, an index `i` of type `Fin n.succ.succ`, an index `j` of type
|
||||
`Fin n.succ`, and a proof `h` that `c (i.succAbove j) = S.τ (c i)`. It returns a morphism
|
||||
corresponding to the contraction of the `i`th index with the `i.succAbove j` index.
|
||||
--/
|
||||
def contrMap {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)) :
|
||||
S.F.obj (OverColor.mk c) ⟶
|
||||
(OverColor.lift.obj S.FDiscrete).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) :=
|
||||
|
|
@ -151,37 +109,47 @@ def contrMap' {n : ℕ} (c : Fin n.succ.succ → S.C)
|
|||
(tensorHom (S.contr.app (Discrete.mk (c i))) (𝟙 _)) ≫
|
||||
(MonoidalCategory.leftUnitor _).hom
|
||||
|
||||
def contrMap {n : ℕ} (c : Fin n → S.C)
|
||||
(i j : Fin n) (hij : i ≠ j) (h : c j = S.τ (c i)) :
|
||||
S.F.obj (OverColor.mk c) ⟶
|
||||
(OverColor.lift.obj S.FDiscrete).obj
|
||||
(OverColor.mk ((c ∘ Fin.cast (contrNPred hij)) ∘ Fin.succAbove (contrFstSucc hij) ∘
|
||||
Fin.succAbove (contrSndSucc hij))) := by
|
||||
refine (S.F.mapIso (OverColor.equivToIso (Fin.castOrderIso (contrNPred hij)).toEquiv.symm)).hom ≫
|
||||
S.contrMap' (c ∘ Fin.cast (contrNPred hij)) (contrFstSucc hij) (contrSndSucc hij) ?_
|
||||
simp only [Nat.pred_eq_sub_one, Nat.succ_eq_add_one, contrSndSucc_succAbove,
|
||||
Fin.castOrderIso_apply, Function.comp_apply, Fin.cast_trans, Fin.cast_eq_self]
|
||||
simpa [contrFstSucc] using h
|
||||
|
||||
|
||||
end TensorStruct
|
||||
|
||||
/-- A syntax tree for tensor expressions. -/
|
||||
inductive TensorTree (S : TensorStruct) : ∀ {n : ℕ}, (Fin n → S.C) → Type where
|
||||
/-- A general tensor node. -/
|
||||
| tensorNode {n : ℕ} {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) : TensorTree S c
|
||||
/-- A node consisting of a single vector. -/
|
||||
| vecNode {c : S.C} (v : S.FDiscrete.obj (Discrete.mk c)) : TensorTree S ![c]
|
||||
/-- A node consisting of a two tensor. -/
|
||||
| twoNode {c1 c2 : S.C}
|
||||
(v : S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)) :
|
||||
TensorTree S ![c1, c2]
|
||||
/-- A node consisting of a three tensor. -/
|
||||
| threeNode {c1 c2 c3 : S.C}
|
||||
(v : S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2) ⊗
|
||||
S.FDiscrete.obj (Discrete.mk c3)) : TensorTree S ![c1, c2, c3]
|
||||
/-- A general constant node. -/
|
||||
| constNode {n : ℕ} {c : Fin n → S.C} (T : 𝟙_ (Rep S.k S.G) ⟶ S.F.obj (OverColor.mk c)) :
|
||||
TensorTree S c
|
||||
/-- A constant vector. -/
|
||||
| constVecNode {c : S.C} (v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c)) :
|
||||
TensorTree S ![c]
|
||||
/-- A constant two tensor (e.g. metric and unit). -/
|
||||
| constTwoNode {c1 c2 : S.C}
|
||||
(v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)) :
|
||||
TensorTree S ![c1, c2]
|
||||
/-- A constant three tensor (e.g. Pauli-matrices). -/
|
||||
| constThreeNode {c1 c2 c3 : S.C}
|
||||
(v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2) ⊗
|
||||
S.FDiscrete.obj (Discrete.mk c3)) : TensorTree S ![c1, c2, c3]
|
||||
/-- A node corresponding to the addition of two tensors. -/
|
||||
| add {n : ℕ} {c : Fin n → S.C} : TensorTree S c → TensorTree S c → TensorTree S c
|
||||
/-- A node corresponding to the permutation of indices of a tensor. -/
|
||||
| perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (t : TensorTree S c) : TensorTree S c1
|
||||
| prod {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
(t : TensorTree S c) (t1 : TensorTree S c1) : TensorTree S (Sum.elim c c1 ∘ finSumFinEquiv.symm)
|
||||
| smul {n : ℕ} {c : Fin n → S.C} : S.k → TensorTree S c → TensorTree S c
|
||||
| contr {n : ℕ} {c : Fin n → S.C} : (i j : Fin n) →
|
||||
(hij : i ≠ j) → (h : c j = S.τ (c i)) → TensorTree S c →
|
||||
TensorTree S ((c ∘ Fin.cast (TensorStruct.contrNPred hij)) ∘
|
||||
Fin.succAbove (TensorStruct.contrFstSucc hij) ∘
|
||||
Fin.succAbove (TensorStruct.contrSndSucc hij))
|
||||
| jiggle {n : ℕ} {c : Fin n → S.C} : (i : Fin n) → TensorTree S c →
|
||||
TensorTree S (Function.update c i (S.τ (c i)))
|
||||
| contr {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)) → TensorTree S c →
|
||||
TensorTree S (c ∘ Fin.succAbove i ∘ Fin.succAbove j)
|
||||
| eval {n : ℕ} {c : Fin n.succ → S.C} :
|
||||
(i : Fin n.succ) → (x : Fin (S.evalNo (c i))) → TensorTree S c →
|
||||
TensorTree S (c ∘ Fin.succAbove i)
|
||||
|
|
@ -190,19 +158,40 @@ namespace TensorTree
|
|||
|
||||
variable {S : TensorStruct} {n : ℕ} {c : Fin n → S.C} (T : TensorTree S c)
|
||||
|
||||
def metric : TensorTree S ![]
|
||||
open MonoidalCategory
|
||||
open TensorProduct
|
||||
|
||||
/-- The node `twoNode` of a tensor tree, with all arguments explicit. -/
|
||||
abbrev twoNodeE (S : TensorStruct) (c1 c2 : S.C)
|
||||
(v : S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)) :
|
||||
TensorTree S ![c1, c2] := twoNode v
|
||||
|
||||
/-- The node `constTwoNodeE` of a tensor tree, with all arguments explicit. -/
|
||||
abbrev constTwoNodeE (S : TensorStruct) (c1 c2 : S.C)
|
||||
(v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)) :
|
||||
TensorTree S ![c1, c2] := constTwoNode v
|
||||
|
||||
/-- The node `constThreeNodeE` of a tensor tree, with all arguments explicit. -/
|
||||
abbrev constThreeNodeE (S : TensorStruct) (c1 c2 c3 : S.C)
|
||||
(v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2) ⊗
|
||||
S.FDiscrete.obj (Discrete.mk c3)) : TensorTree S ![c1, c2, c3] :=
|
||||
constThreeNode v
|
||||
|
||||
/-- The number of nodes in a tensor tree. -/
|
||||
def size : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → ℕ := fun
|
||||
| tensorNode _ => 1
|
||||
| vecNode _ => 1
|
||||
| twoNode _ => 1
|
||||
| threeNode _ => 1
|
||||
| constNode _ => 1
|
||||
| constVecNode _ => 1
|
||||
| constTwoNode _ => 1
|
||||
| constThreeNode _ => 1
|
||||
| add t1 t2 => t1.size + t2.size + 1
|
||||
| perm _ t => t.size + 1
|
||||
| smul _ t => t.size + 1
|
||||
| prod t1 t2 => t1.size + t2.size + 1
|
||||
| contr _ _ _ _ t => t.size + 1
|
||||
| jiggle _ t => t.size + 1
|
||||
| contr _ _ _ t => t.size + 1
|
||||
| eval _ _ t => t.size + 1
|
||||
|
||||
noncomputable section
|
||||
|
|
@ -216,63 +205,7 @@ def tensor : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → S.F.obj (Over
|
|||
| smul a t => a • t.tensor
|
||||
| prod t1 t2 => (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom
|
||||
((S.F.μ _ _).hom (t1.tensor ⊗ₜ t2.tensor))
|
||||
| contr i j hij h t => (S.contrMap _ i j hij h).hom t.tensor
|
||||
| jiggle i t => by
|
||||
rename_i n c'
|
||||
let T := (tensorNode (S.metric (S.τ (c' i))))
|
||||
let T2 := (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom
|
||||
((S.F.μ _ _).hom (T.tensor ⊗ₜ t.tensor))
|
||||
let e1 : Fin (2 + n) ≃ Fin (2 + n) :=
|
||||
(Equiv.swap (Fin.castAdd n (0 : Fin 2)) (Fin.natAdd 2 i))
|
||||
let T3 := (S.F.map ((OverColor.equivToIso e1).hom)).hom T2
|
||||
let T4 := (S.contrMap _ (Fin.castAdd n (0 : Fin 2)) (Fin.castAdd n (1 : Fin 2))
|
||||
(by
|
||||
simp only [Fin.isValue, ne_eq,
|
||||
Fin.ext_iff, Fin.coe_castAdd, Fin.val_zero, Fin.coe_natAdd]
|
||||
omega)
|
||||
(by
|
||||
simp [e1]
|
||||
rw [Equiv.swap_apply_of_ne_of_ne]
|
||||
· simp [Fin.ext_iff]
|
||||
rfl
|
||||
· simp [Fin.ext_iff]
|
||||
· simp [Fin.ext_iff]
|
||||
omega)).hom T3
|
||||
refine (S.F.map ?_).hom T4
|
||||
refine (OverColor.equivToIso (Fin.castOrderIso (by simp : (2 + n).pred.pred = n)).toEquiv).hom ≫ ?_
|
||||
refine (OverColor.mkIso ?_).hom
|
||||
funext x
|
||||
simp
|
||||
trans Sum.elim ![S.τ (c' i), S.τ (c' i)] c' (finSumFinEquiv.symm
|
||||
(e1.symm (Fin.natAdd 2 x)))
|
||||
congr
|
||||
simp [Fin.ext_iff]
|
||||
simp [Fin.succAbove]
|
||||
split_ifs
|
||||
· rename_i h1 h2
|
||||
rw [Fin.lt_def] at h1 h2
|
||||
simp_all [TensorStruct.contrSndSucc, TensorStruct.contrFstSucc]
|
||||
· rename_i h1 h2
|
||||
rw [Fin.lt_def] at h1 h2
|
||||
simp_all [TensorStruct.contrSndSucc, TensorStruct.contrFstSucc]
|
||||
simp [Fin.predAbove, Fin.lt_def] at h1
|
||||
· rename_i h1 h2
|
||||
rw [Fin.lt_def] at h1 h2
|
||||
simp_all [TensorStruct.contrSndSucc, TensorStruct.contrFstSucc]
|
||||
· simp
|
||||
omega
|
||||
simp [e1]
|
||||
by_cases hi: x= i
|
||||
· subst hi
|
||||
simp
|
||||
· rw [Equiv.swap_apply_of_ne_of_ne]
|
||||
· simp
|
||||
rw [Function.update]
|
||||
simp [hi]
|
||||
· simp [Fin.ext_iff]
|
||||
· simp [Fin.ext_iff]
|
||||
omega
|
||||
|
||||
| contr i j h t => (S.contrMap _ i j h).hom t.tensor
|
||||
| _ => 0
|
||||
|
||||
lemma tensor_tensorNode {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) :
|
||||
|
|
|
|||
|
|
@ -20,6 +20,20 @@ namespace TensorTree
|
|||
def dotString (m : ℕ) (nt : ℕ) : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → String := fun
|
||||
| tensorNode _ =>
|
||||
" node" ++ toString m ++ " [label=\"T" ++ toString nt ++ "\"];\n"
|
||||
| vecNode T =>
|
||||
" node" ++ toString m ++ " [label=\"vec " ++ toString nt ++ "\"];\n"
|
||||
| twoNode T =>
|
||||
" node" ++ toString m ++ " [label=\"vec2\", shape=box];\n"
|
||||
| threeNode T =>
|
||||
" node" ++ toString m ++ " [label=\"vec3\", shape=box];\n"
|
||||
| constNode T =>
|
||||
" node" ++ toString m ++ " [label=\"const " ++ toString nt ++ "\"];\n"
|
||||
| constVecNode T =>
|
||||
" node" ++ toString m ++ " [label=\"constVec " ++ toString nt ++ "\"];\n"
|
||||
| constTwoNode T =>
|
||||
" node" ++ toString m ++ " [label=\"constVec2\", shape=box];\n"
|
||||
| constThreeNode T =>
|
||||
" node" ++ toString m ++ " [label=\"constVec3\", shape=box];\n"
|
||||
| add t1 t2 =>
|
||||
let addNode := " node" ++ toString m ++ " [label=\"+\", shape=box];\n"
|
||||
let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"
|
||||
|
|
@ -39,20 +53,10 @@ def dotString (m : ℕ) (nt : ℕ) : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTr
|
|||
let smulNode := " node" ++ toString m ++ " [label=\"smul\", shape=box];\n"
|
||||
let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"
|
||||
smulNode ++ dotString (m + 1) nt t ++ edge1
|
||||
| mult _ _ t1 t2 =>
|
||||
let multNode := " node" ++ toString m ++ " [label=\"mult\", shape=box];\n"
|
||||
let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"
|
||||
let edge2 := " node" ++ toString m ++ " -> node" ++ toString (t1.size + m + 2) ++ ";\n"
|
||||
multNode ++ dotString (m + 1) nt t1 ++ dotString (2 * t1.size + m + 2) (nt + 1) t2
|
||||
++ edge1 ++ edge2
|
||||
| eval _ _ t1 =>
|
||||
let evalNode := " node" ++ toString m ++ " [label=\"eval\", shape=box];\n"
|
||||
let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"
|
||||
evalNode ++ dotString (m + 1) nt t1 ++ edge1
|
||||
| jiggle i t1 =>
|
||||
let jiggleNode := " node" ++ toString m ++ " [label=\"τ\", shape=box];\n"
|
||||
let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"
|
||||
jiggleNode ++ dotString (m + 1) nt t1 ++ edge1
|
||||
| contr i j _ t1 =>
|
||||
let contrNode := " node" ++ toString m ++ " [label=\"contr " ++ toString i ++ " "
|
||||
++ toString j ++ "\", shape=box];\n"
|
||||
|
|
|
|||
|
|
@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith
|
|||
import HepLean.Tensors.Tree.Basic
|
||||
import Lean.Elab.Term
|
||||
import HepLean.Tensors.Tree.Dot
|
||||
import HepLean.Tensors.ComplexLorentz.Basic
|
||||
/-!
|
||||
|
||||
## Elaboration of tensor trees
|
||||
|
|
@ -82,6 +83,7 @@ def indexToDual (stx : Syntax) : Bool :=
|
|||
match stx with
|
||||
| `(indexExpr| τ($_)) => true
|
||||
| _ => false
|
||||
|
||||
/-!
|
||||
|
||||
## Tensor expressions
|
||||
|
|
@ -136,15 +138,72 @@ partial def getIndices (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) :=
|
|||
def getNoIndicesExact (stx : Syntax) : TermElabM ℕ := do
|
||||
let expr ← elabTerm stx none
|
||||
let type ← inferType expr
|
||||
match type with
|
||||
| Expr.app _ (Expr.app _ (Expr.app _ c)) =>
|
||||
let typeC ← inferType c
|
||||
match typeC with
|
||||
| Expr.forallE _ (Expr.app _ (Expr.app (Expr.app _ (Expr.lit (Literal.natVal n))) _)) _ _ =>
|
||||
return n
|
||||
| _ => throwError "Could not extract number of indices from tensor (getNoIndicesExact). "
|
||||
| _ =>
|
||||
throwError "Could not extract number of indices from tensor (getNoIndicesExact)."
|
||||
let strType := toString type
|
||||
let n := (String.splitOn strType "CategoryTheory.MonoidalCategoryStruct.tensorObj").length
|
||||
match n with
|
||||
| 1 =>
|
||||
match type with
|
||||
| Expr.app _ (Expr.app _ (Expr.app _ c)) =>
|
||||
let typeC ← inferType c
|
||||
match typeC with
|
||||
| Expr.forallE _ (Expr.app _ (Expr.app (Expr.app _ (Expr.lit (Literal.natVal n))) _)) _ _ =>
|
||||
return n
|
||||
| _ => throwError "Could not extract number of indices from tensor (getNoIndicesExact). "
|
||||
| _ => return 1
|
||||
| k => return k
|
||||
|
||||
/-- The construction of an expression corresponding to the type of a given string once parsed. -/
|
||||
def stringToType (str : String) : TermElabM Expr := do
|
||||
let env ← getEnv
|
||||
let stx := Parser.runParserCategory env `term str
|
||||
match stx with
|
||||
| Except.error _ => throwError "Could not create type from string (stringToType). "
|
||||
| Except.ok stx => elabTerm stx none
|
||||
|
||||
/-- The syntax associated with a terminal node of a tensor tree. -/
|
||||
def termNodeSyntax (T : Term) : TermElabM Term := do
|
||||
let expr ← elabTerm T none
|
||||
let type ← inferType expr
|
||||
let strType := toString type
|
||||
let n := (String.splitOn strType "CategoryTheory.MonoidalCategoryStruct.tensorObj").length
|
||||
let const := (String.splitOn strType "Quiver.Hom").length
|
||||
match n, const with
|
||||
| 1, 1 =>
|
||||
match type with
|
||||
| Expr.app _ (Expr.app _ (Expr.app _ c)) =>
|
||||
let typeC ← inferType c
|
||||
match typeC with
|
||||
| Expr.forallE _ (Expr.app _ (Expr.app (Expr.app _ (Expr.lit (Literal.natVal _))) _)) _ _ =>
|
||||
return Syntax.mkApp (mkIdent ``TensorTree.tensorNode) #[T]
|
||||
| _ => throwError "Could not create terminal node syntax (termNodeSyntax). "
|
||||
| _ => return Syntax.mkApp (mkIdent ``TensorTree.vecNode) #[T]
|
||||
| 2, 1 =>
|
||||
match ← isDefEq type (← stringToType "CoeSort.coe leftHanded ⊗ CoeSort.coe Lorentz.complexContr") with
|
||||
| true => return Syntax.mkApp (mkIdent ``TensorTree.twoNodeE)
|
||||
#[mkIdent ``Fermion.complexLorentzTensor, mkIdent ``Fermion.Color.upL, mkIdent ``Fermion.Color.up, T]
|
||||
| _ => return Syntax.mkApp (mkIdent ``TensorTree.twoNode) #[T]
|
||||
| 3, 1 => return Syntax.mkApp (mkIdent ``TensorTree.threeNode) #[T]
|
||||
| 1, 2 => return Syntax.mkApp (mkIdent ``TensorTree.constVecNode) #[T]
|
||||
| 2, 2 =>
|
||||
match ← isDefEq type (← stringToType
|
||||
"𝟙_ (Rep ℂ SL(2, ℂ)) ⟶ Lorentz.complexCo ⊗ Lorentz.complexCo") with
|
||||
| true =>
|
||||
println! "here"
|
||||
return Syntax.mkApp (mkIdent ``TensorTree.constTwoNodeE) #[
|
||||
mkIdent ``Fermion.complexLorentzTensor, mkIdent ``Fermion.Color.down,
|
||||
mkIdent ``Fermion.Color.down, T]
|
||||
| _ => return Syntax.mkApp (mkIdent ``TensorTree.constTwoNode) #[T]
|
||||
| 3, 2 =>
|
||||
/- Specific types. -/
|
||||
match ← isDefEq type (← stringToType
|
||||
"𝟙_ (Rep ℂ SL(2, ℂ)) ⟶ Lorentz.complexContr ⊗ Fermion.leftHanded ⊗ Fermion.rightHanded") with
|
||||
| true =>
|
||||
return Syntax.mkApp (mkIdent ``TensorTree.constThreeNodeE) #[
|
||||
mkIdent ``Fermion.complexLorentzTensor, mkIdent ``Fermion.Color.up,
|
||||
mkIdent ``Fermion.Color.upL, mkIdent ``Fermion.Color.upR, T]
|
||||
| _ =>
|
||||
return Syntax.mkApp (mkIdent ``TensorTree.constThreeNode) #[T]
|
||||
| _, _ => throwError "Could not create terminal node syntax (termNodeSyntax). "
|
||||
|
||||
/-- The positions in getIndicesNode which get evaluated, and the value they take. -/
|
||||
partial def getEvalPos (stx : Syntax) : TermElabM (List (ℕ × ℕ)) := do
|
||||
|
|
@ -159,19 +218,6 @@ def evalSyntax (l : List (ℕ × ℕ)) (T : Term) : Term :=
|
|||
l.foldl (fun T' (x1, x2) => Syntax.mkApp (mkIdent ``TensorTree.eval)
|
||||
#[Syntax.mkNumLit (toString x1), Syntax.mkNumLit (toString x2), T']) T
|
||||
|
||||
/-- The positions in getIndicesNode which get dualized. -/
|
||||
partial def getDualPos (stx : Syntax) : TermElabM (List ℕ) := do
|
||||
let ind ← getIndices stx
|
||||
let indFilt : List (TSyntax `indexExpr) := ind.filter (fun x => ¬ indexExprIsNum x)
|
||||
let indEnum := indFilt.enum
|
||||
let duals := indEnum.filter (fun x => indexToDual x.2)
|
||||
return duals.map (fun x => x.1)
|
||||
|
||||
/-- For each element of `l : List ℕ` applies `TensorTree.jiggle` to the given term. -/
|
||||
def dualSyntax (l : List ℕ) (T : Term) : Term :=
|
||||
l.foldl (fun T' x => Syntax.mkApp (mkIdent ``TensorTree.jiggle)
|
||||
#[Syntax.mkNumLit (toString x), T']) T
|
||||
|
||||
/-- The pairs of positions in getIndicesNode which get contracted. -/
|
||||
partial def getContrPos (stx : Syntax) : TermElabM (List (ℕ × ℕ)) := do
|
||||
let ind ← getIndices stx
|
||||
|
|
@ -192,7 +238,7 @@ def withoutContr (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
|
|||
/-- For each element of `l : List (ℕ × ℕ)` applies `TensorTree.contr` to the given term. -/
|
||||
def contrSyntax (l : List (ℕ × ℕ)) (T : Term) : Term :=
|
||||
l.foldl (fun T' (x0, x1) => Syntax.mkApp (mkIdent ``TensorTree.contr)
|
||||
#[Syntax.mkNumLit (toString x1), Syntax.mkNumLit (toString x0), mkIdent ``rfl, T']) T
|
||||
#[Syntax.mkNumLit (toString x1), Syntax.mkNumLit (toString x0), mkIdent `sorry, mkIdent ``rfl, T']) T
|
||||
|
||||
/-- Creates the syntax associated with a tensor node. -/
|
||||
def syntaxFull (stx : Syntax) : TermElabM Term := do
|
||||
|
|
@ -202,10 +248,9 @@ def syntaxFull (stx : Syntax) : TermElabM Term := do
|
|||
let rawIndex ← getNoIndicesExact T
|
||||
if indices.length ≠ rawIndex then
|
||||
throwError "The number of indices does not match the tensor {T}."
|
||||
let tensorNodeSyntax := Syntax.mkApp (mkIdent ``TensorTree.tensorNode) #[T]
|
||||
let tensorNodeSyntax ← termNodeSyntax T
|
||||
let evalSyntax := evalSyntax (← getEvalPos stx) tensorNodeSyntax
|
||||
let dualSyntax := dualSyntax (← getDualPos stx) evalSyntax
|
||||
let contrSyntax := contrSyntax (← getContrPos stx) dualSyntax
|
||||
let contrSyntax := contrSyntax (← getContrPos stx) evalSyntax
|
||||
return contrSyntax
|
||||
| _ =>
|
||||
throwError "Unsupported tensor expression syntax in elaborateTensorNode: {stx}"
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue