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

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2024-10-22 14:27:44 +00:00
parent ed162d7e79
commit b792be4423
3 changed files with 26 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -49,7 +49,7 @@ def pairIso (c : C) : (pair F).obj (Discrete.mk c) ≅ (lift.obj F).obj (OverCol
rfl
/-- The isomorphism between `F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2)` and
`(lift.obj F).obj (OverColor.mk ![c1,c2])` fored by the tensorate. -/
`(lift.obj F).obj (OverColor.mk ![c1,c2])` formed by the tensorate. -/
def pairIsoSep {c1 c2 : C} : F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2) ≅
(lift.obj F).obj (OverColor.mk ![c1,c2]) := by
symm
@ -69,14 +69,6 @@ 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
@ -119,6 +111,17 @@ lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discr
HepLean.PiTensorProduct.elimPureTensor]
exact (LinearEquiv.eq_symm_apply _).mp rfl
/-- The isomorphism between
`F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2) ⊗ F.obj (Discrete.mk c3)` and
`(lift.obj F).obj (OverColor.mk ![c1,c2])` formed by the tensorate. -/
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
/-- 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)

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

@ -76,6 +76,8 @@ def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] := by
fin_cases x
rfl
/-- The isomorphism splitting a `mk c` for `c : Fin 3 → C` into the tensor product of
a `Fin 1 → C` map `![c 0]` and a `Fin 2 → C` map `![c 1, c 2]`. -/
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
@ -89,7 +91,8 @@ def fin3Iso {c : Fin 3 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1, c 2] := by
rfl
rfl
/-- The isomorphism splitting a `mk ![c1, c2, c3]` into the tensor product of
a `Fin 1 → C` map `fun _ => c1` and a `Fin 2 → C` map `![c 1, c 2]`. -/
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

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

@ -194,17 +194,20 @@ def specialTypes : List (String × (Term → Term)) := [
Syntax.mkApp (mkIdent ``TensorTree.twoNodeE) #[mkIdent ``Fermion.complexLorentzTensor,
mkIdent ``Fermion.Color.down, mkIdent ``Fermion.Color.down, T]),
("ModuleCat.carrier (Lorentz.complexCo ⊗ Lorentz.complexContr).V", fun T =>
Syntax.mkApp (mkIdent ``TensorTree.twoNodeE) #[mkIdent ``Fermion.complexLorentzTensor,
mkIdent ``Fermion.Color.down, mkIdent ``Fermion.Color.up, T]),
Syntax.mkApp (mkIdent ``TensorTree.twoNodeE) #[
mkIdent ``Fermion.complexLorentzTensor,
mkIdent ``Fermion.Color.down,
mkIdent ``Fermion.Color.up, T]),
("𝟙_ (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.complexLorentzTensor,
mkIdent ``Fermion.Color.down,
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])]
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