DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat: Three tensor nodes

Browse source
This commit is contained in:
jstoobysmith 2024-10-22 14:19:43 +00:00
parent 6bca8c295c
commit ed162d7e79
5 changed files with 68 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
HepLean/Tensors/OverColor/Discrete.lean
View file

@ -69,6 +69,14 @@ def pairIsoSep {c1 c2 : C} : F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2)
fin_cases x
rfl
def tripleIsoSep {c1 c2 c3 : C} :
F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2) ⊗ F.obj (Discrete.mk c3) ≅
(lift.obj F).obj (OverColor.mk ![c1,c2,c3]) :=
(whiskerLeftIso (F.obj (Discrete.mk c1)) (pairIsoSep F (c1 := c2) (c2 := c3))).trans <|
(whiskerRightIso (forgetLiftApp F c1).symm _).trans <|
((lift.obj F).μIso _ _).trans <|
(lift.obj F).mapIso fin3Iso'.symm
lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discrete.mk c2)) :
(pairIsoSep F).hom.hom (x ⊗ₜ[k] y) =
PiTensorProduct.tprod k (Fin.cases x (Fin.cases y (fun i => Fin.elim0 i))) := by

27
HepLean/Tensors/OverColor/Iso.lean
View file

@ -76,6 +76,33 @@ def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] := by
fin_cases x
rfl
def fin3Iso {c : Fin 3 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1, c 2] := by
let e1 : Fin 3 ≃ Fin 1 ⊕ Fin 2 := (finSumFinEquiv (n := 2)).symm
apply (equivToIso e1).trans
apply (mkSum _).trans
refine tensorIso (mkIso ?_) (mkIso ?_)
· funext x
fin_cases x
rfl
· funext x
fin_cases x
rfl
rfl
def fin3Iso' {c1 c2 c3 : C} : mk ![c1, c2, c3] ≅ mk (fun (_ : Fin 1) => c1) ⊗ mk ![c2, c3] := by
let e1 : Fin 3 ≃ Fin 1 ⊕ Fin 2 := (finSumFinEquiv (n := 2)).symm
apply (equivToIso e1).trans
apply (mkSum _).trans
refine tensorIso (mkIso ?_) (mkIso ?_)
· funext x
fin_cases x
rfl
· funext x
fin_cases x
rfl
rfl
/-- Removes a given `i : Fin n.succ.succ` from a morphism in `OverColor C`. -/
def extractOne {n : ℕ} (i : Fin n.succ.succ)
{c1 c2 : Fin n.succ.succ → C} (σ : mk c1 ⟶ mk c2) :

28
HepLean/Tensors/Tree/Basic.lean
View file

@ -559,6 +559,18 @@ abbrev twoNodeE (S : TensorSpecies) (c1 c2 : S.C)
(v : (S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)).V) :
TensorTree S ![c1, c2] := twoNode v
/-- A node consisting of a three tensor. -/
def threeNode {c1 c2 c3 : S.C} (t : (S.FDiscrete.obj (Discrete.mk c1) ⊗
S.FDiscrete.obj (Discrete.mk c2) ⊗ S.FDiscrete.obj (Discrete.mk c3)).V) :
TensorTree S ![c1, c2, c3] :=
(tensorNode ((OverColor.Discrete.tripleIsoSep S.FDiscrete).hom.hom t))
/-- The node `threeNode` of a tensor tree, with all arguments explicit. -/
abbrev threeNodeE (S : TensorSpecies) (c1 c2 c3 : S.C)
(v : (S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2) ⊗
S.FDiscrete.obj (Discrete.mk c3)).V) :
TensorTree S ![c1, c2, c3] := threeNode v
/-- A general constant node. -/
def constNode {n : ℕ} {c : Fin n → S.C} (T : 𝟙_ (Rep S.k S.G) ⟶ S.F.obj (OverColor.mk c)) :
TensorTree S c := tensorNode (T.hom (1 : S.k))
@ -567,16 +579,28 @@ def constNode {n : ℕ} {c : Fin n → S.C} (T : 𝟙_ (Rep S.k S.G) ⟶ S.F.obj
def constVecNode {c : S.C} (v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c)) :
TensorTree S ![c] := vecNode (v.hom (1 : S.k))
/-- A constant two tensor (e.g. metric and unit). -/
/-- A constant two tensor (e.g. metric and unit). -/
def 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] := twoNode (v.hom (1 : S.k))
/-- The node `constTwoNodeE` of a tensor tree, with all arguments explicit. -/
/-- The node `constTwoNode` of a tensor tree, with all arguments explicit. -/
abbrev constTwoNodeE (S : TensorSpecies) (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
/-- A constant three tensor (e.g. Pauli matrices). -/
def 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] :=
threeNode (v.hom (1 : S.k))
/-- The node `constThreeNode` of a tensor tree, with all arguments explicit. -/
abbrev constThreeNodeE (S : TensorSpecies) (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
/-!
## Other operations.

7
HepLean/Tensors/Tree/Elab.lean
View file

@ -199,7 +199,12 @@ def specialTypes : List (String × (Term → Term)) := [
("𝟙_ (Rep ℂ SL(2, ℂ)) ⟶ Lorentz.complexCo ⊗ Lorentz.complexCo", fun T =>
Syntax.mkApp (mkIdent ``TensorTree.constTwoNodeE) #[
mkIdent ``Fermion.complexLorentzTensor, mkIdent ``Fermion.Color.down,
mkIdent ``Fermion.Color.down, T])]
mkIdent ``Fermion.Color.down, T]),
("𝟙_ (Rep ℂ SL(2, ℂ)) ⟶ Lorentz.complexContr ⊗ Fermion.leftHanded ⊗ Fermion.rightHanded", fun T =>
Syntax.mkApp (mkIdent ``TensorTree.constThreeNodeE) #[
mkIdent ``Fermion.complexLorentzTensor, mkIdent ``Fermion.Color.up,
mkIdent ``Fermion.Color.upL,
mkIdent ``Fermion.Color.upR, T])]
/-- The syntax associated with a terminal node of a tensor tree. -/
def termNodeSyntax (T : Term) : TermElabM Term := do

2
HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean
View file

@ -36,7 +36,7 @@ lemma finSumFinEquiv_comp_braidPerm :
(β_ (OverColor.mk c2) (OverColor.mk c)).hom
≫ (equivToIso finSumFinEquiv).hom := by
rw [braidPerm]
simp
simp only [Functor.id_obj, mk_hom, Iso.hom_inv_id_assoc]
/-- The arguments of a `prod` node can be commuted using braiding. -/
theorem prod_comm (t : TensorTree S c) (t2 : TensorTree S c2) :