refactor: Lint
This commit is contained in:
jstoobysmith
parent
4054665c38
commit
05903bc440
5 changed files with 42 additions and 46 deletions
|
|
@ -18,7 +18,6 @@ namespace HepLean.PiTensorProduct
|
|||
|
||||
noncomputable section tmulEquiv
|
||||
|
||||
|
||||
variable {R ι1 ι2 ι3 M N : Type} [CommSemiring R]
|
||||
{s1 : ι1 → Type} [inst1 : (i : ι1) → AddCommMonoid (s1 i)] [inst1' : (i : ι1) → Module R (s1 i)]
|
||||
{s2 : ι2 → Type} [inst2 : (i : ι2) → AddCommMonoid (s2 i)] [inst2' : (i : ι2) → Module R (s2 i)]
|
||||
|
|
@ -69,13 +68,13 @@ lemma induction_assoc
|
|||
simp only [PiTensorProduct.tprodCoeff_eq_smul_tprod]
|
||||
simp only [smul_tmul, tmul_smul, LinearMapClass.map_smul]
|
||||
apply congrArg
|
||||
let f' : ((⨂[R] i : ι2, s2 i) ⊗[R] ⨂[R] i : ι3, s3 i) →ₗ[R] M := {
|
||||
let f' : ((⨂[R] i : ι2, s2 i) ⊗[R] ⨂[R] i : ι3, s3 i) →ₗ[R] M := {
|
||||
toFun := fun y => f (PiTensorProduct.tprod R fx ⊗ₜ[R] y),
|
||||
map_add' := fun y1 y2 => by
|
||||
simp [tmul_add]
|
||||
map_smul' := fun r y => by
|
||||
simp [tmul_smul]}
|
||||
let g' : ((⨂[R] i : ι2, s2 i) ⊗[R] ⨂[R] i : ι3, s3 i) →ₗ[R] M := {
|
||||
let g' : ((⨂[R] i : ι2, s2 i) ⊗[R] ⨂[R] i : ι3, s3 i) →ₗ[R] M := {
|
||||
toFun := fun y => g (PiTensorProduct.tprod R fx ⊗ₜ[R] y),
|
||||
map_add' := fun y1 y2 => by
|
||||
simp [tmul_add]
|
||||
|
|
@ -102,13 +101,13 @@ lemma induction_assoc'
|
|||
intro ry fy
|
||||
simp only [PiTensorProduct.tprodCoeff_eq_smul_tprod, tmul_smul, map_smul]
|
||||
apply congrArg
|
||||
let f' : ((⨂[R] i : ι1, s1 i) ⊗[R] ⨂[R] i : ι2, s2 i) →ₗ[R] M := {
|
||||
let f' : ((⨂[R] i : ι1, s1 i) ⊗[R] ⨂[R] i : ι2, s2 i) →ₗ[R] M := {
|
||||
toFun := fun y => f (y ⊗ₜ[R] PiTensorProduct.tprod R fy),
|
||||
map_add' := fun y1 y2 => by
|
||||
simp [add_tmul]
|
||||
map_smul' := fun r y => by
|
||||
simp [smul_tmul]}
|
||||
let g' : ((⨂[R] i : ι1, s1 i) ⊗[R] ⨂[R] i : ι2, s2 i) →ₗ[R] M := {
|
||||
let g' : ((⨂[R] i : ι1, s1 i) ⊗[R] ⨂[R] i : ι2, s2 i) →ₗ[R] M := {
|
||||
toFun := fun y => g (y ⊗ₜ[R] PiTensorProduct.tprod R fy),
|
||||
map_add' := fun y1 y2 => by
|
||||
simp [add_tmul]
|
||||
|
|
@ -165,7 +164,6 @@ instance : (i : ι1 ⊕ ι2) → Module R ((fun i => Sum.elim s1 s2 i) i) := fun
|
|||
| Sum.inl i => inst1' i
|
||||
| Sum.inr i => inst2' i
|
||||
|
||||
|
||||
/-- Takes a map `(i : ι1 ⊕ ι2) → Sum.elim s1 s2 i` to the underlying map `(i : ι1) → s1 i `. -/
|
||||
private def pureInl (f : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i) : (i : ι1) → s1 i :=
|
||||
fun i => f (Sum.inl i)
|
||||
|
|
@ -215,7 +213,7 @@ lemma pureInl_update_right (f : (i : ι1 ⊕ ι2) → Sum.elim s1 s2 i) (x : ι2
|
|||
|
||||
end
|
||||
|
||||
/-- The multilinear map from `(Sum.elim s1 s2)` to `((⨂[R] i : ι1, s1 i) ⊗[R] ⨂[R] i : ι2, s2 i)`
|
||||
/-- The multilinear map from `(Sum.elim s1 s2)` to `((⨂[R] i : ι1, s1 i) ⊗[R] ⨂[R] i : ι2, s2 i)`
|
||||
defined by splitting elements of `(Sum.elim s1 s2)` into two parts. -/
|
||||
def domCoprod :
|
||||
MultilinearMap R (Sum.elim s1 s2) ((⨂[R] i : ι1, s1 i) ⊗[R] ⨂[R] i : ι2, s2 i) where
|
||||
|
|
@ -340,7 +338,7 @@ def tmul : ((⨂[R] i : ι1, s1 i) ⊗[R] ⨂[R] i : ι2, s2 i) →ₗ[R]
|
|||
|
||||
/-- THe equivalence formed by combining a `TensorProduct` into a `PiTensorProduct`. -/
|
||||
def tmulEquiv : ((⨂[R] i : ι1, s1 i) ⊗[R] ⨂[R] i : ι2, s2 i) ≃ₗ[R]
|
||||
⨂[R] i : ι1 ⊕ ι2, (Sum.elim s1 s2) i :=
|
||||
⨂[R] i : ι1 ⊕ ι2, (Sum.elim s1 s2) i :=
|
||||
LinearEquiv.ofLinear tmul tmulSymm
|
||||
(by
|
||||
apply PiTensorProduct.ext
|
||||
|
|
|
|||
|
|
@ -172,7 +172,7 @@ lemma map_tprod {X Y : OverColor Color} (p : (i : X.left) → (colorToRep (X.hom
|
|||
change (colorFun.map' f).hom ((PiTensorProduct.tprod ℂ) p) = _
|
||||
simp [colorFun.map', mapToLinearEquiv']
|
||||
erw [LinearEquiv.trans_apply]
|
||||
change (PiTensorProduct.congr fun i => colorToRepCongr _)
|
||||
change (PiTensorProduct.congr fun i => colorToRepCongr _)
|
||||
((PiTensorProduct.reindex ℂ (fun x => _) (OverColor.Hom.toEquiv f))
|
||||
((PiTensorProduct.tprod ℂ) p)) = _
|
||||
rw [PiTensorProduct.reindex_tprod, PiTensorProduct.congr_tprod]
|
||||
|
|
@ -244,8 +244,8 @@ 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))) :
|
||||
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
|
||||
|
|
@ -289,8 +289,8 @@ def μ (X Y : OverColor Color) : colorFun.obj X ⊗ colorFun.obj Y ≅ colorFun.
|
|||
hom := (μModEquiv X Y).symm.toLinearMap
|
||||
comm := fun M => by
|
||||
simp [CategoryStruct.comp]
|
||||
erw [LinearEquiv.eq_comp_toLinearMap_symm,LinearMap.comp_assoc ,
|
||||
LinearEquiv.toLinearMap_symm_comp_eq ]
|
||||
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,
|
||||
|
|
@ -325,8 +325,8 @@ def μ (X Y : OverColor Color) : colorFun.obj X ⊗ colorFun.obj Y ≅ colorFun.
|
|||
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))) :
|
||||
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
|
||||
|
|
@ -353,7 +353,7 @@ lemma μ_natural_left {X Y : OverColor Color} (f : X ⟶ Y) (Z : OverColor Color
|
|||
((PiTensorProduct.tprod ℂ) p) ⊗ₜ[ℂ] ((PiTensorProduct.tprod ℂ) q)) := by rfl
|
||||
erw [h1]
|
||||
rw [colorFun.map_tprod]
|
||||
change (μ Y Z).hom.hom (((PiTensorProduct.tprod ℂ) fun i => (colorToRepCongr _)
|
||||
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
|
||||
|
|
@ -363,7 +363,7 @@ lemma μ_natural_left {X Y : OverColor Color} (f : X ⟶ Y) (Z : OverColor Color
|
|||
| 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 =
|
||||
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 => ?_)
|
||||
|
|
@ -384,7 +384,7 @@ lemma μ_natural_right {X Y : OverColor Color} (X' : OverColor Color) (f : X ⟶
|
|||
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))) = _
|
||||
(colorToRepCongr _) (q ((OverColor.Hom.toEquiv f).symm i))) = _
|
||||
rw [μ_tmul_tprod]
|
||||
apply congrArg
|
||||
funext i
|
||||
|
|
@ -410,7 +410,7 @@ lemma associativity (X Y Z : OverColor Color) :
|
|||
(μ 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
|
||||
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 =>
|
||||
|
|
@ -463,7 +463,7 @@ lemma right_unitality (X : OverColor Color) : (MonoidalCategory.rightUnitor (col
|
|||
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 ) =
|
||||
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 [PiTensorProduct.isEmptyEquiv]
|
||||
|
|
@ -477,7 +477,7 @@ lemma right_unitality (X : OverColor Color) : (MonoidalCategory.rightUnitor (col
|
|||
|
||||
end colorFun
|
||||
|
||||
/-- The monoidal functor between `OverColor Color` and `Rep ℂ SL(2, ℂ)` taking a map of colors
|
||||
/-- 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
|
||||
|
|
|
|||
|
|
@ -269,7 +269,7 @@ def map {C D : Type} (f : C → D) : MonoidalFunctor (OverColor C) (OverColor D)
|
|||
| Sum.inr x => rfl
|
||||
|
||||
/-- The tensor product on `OverColor C` as a monoidal functor. -/
|
||||
def tensor : MonoidalFunctor (OverColor C × OverColor C) (OverColor C) where
|
||||
def tensor : MonoidalFunctor (OverColor C × OverColor C) (OverColor C) where
|
||||
toFunctor := MonoidalCategory.tensor (OverColor C)
|
||||
ε := Over.isoMk (Equiv.sumEmpty Empty Empty).symm.toIso (by
|
||||
ext x
|
||||
|
|
@ -344,7 +344,6 @@ def finExtractOne {n : ℕ} (i : Fin n.succ) : Fin n.succ ≃ Fin 1 ⊕ Fin n :=
|
|||
(Equiv.sumAssoc (Fin 1) (Fin i) (Fin (n - i))).trans <|
|
||||
Equiv.sumCongr (Equiv.refl (Fin 1)) (finSumFinEquiv.trans (finCongr (by omega)))
|
||||
|
||||
|
||||
end OverColor
|
||||
|
||||
end IndexNotation
|
||||
|
|
|
|||
|
|
@ -17,46 +17,46 @@ that converts a tensor tree into a dot file.
|
|||
namespace TensorTree
|
||||
|
||||
/-- Turns a nodes of tensor trees into nodes and edges of a dot file. -/
|
||||
def dotString (m : ℕ) (nt : ℕ): ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → String := fun
|
||||
def dotString (m : ℕ) (nt : ℕ) : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → String := fun
|
||||
| tensorNode _ =>
|
||||
" node" ++ toString m ++ " [label=\"T" ++ toString nt ++ "\"];\n"
|
||||
" node" ++ toString m ++ " [label=\"T" ++ toString nt ++ "\"];\n"
|
||||
| add t1 t2 =>
|
||||
let addNode := " node" ++ toString m ++ " [label=\"+\", shape=box];\n"
|
||||
let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"
|
||||
let edge2 := " node" ++ toString m ++ " -> node" ++ toString (m + 2) ++ ";\n"
|
||||
let addNode := " node" ++ toString m ++ " [label=\"+\", shape=box];\n"
|
||||
let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"
|
||||
let edge2 := " node" ++ toString m ++ " -> node" ++ toString (m + 2) ++ ";\n"
|
||||
addNode ++ dotString (m + 1) nt t1 ++ dotString (m + 2) (nt + 1) t2 ++ edge1 ++ edge2
|
||||
| perm σ t =>
|
||||
let permNode := " node" ++ toString m ++ " [label=\"perm\", shape=box];\n"
|
||||
let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"
|
||||
let permNode := " node" ++ toString m ++ " [label=\"perm\", shape=box];\n"
|
||||
let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"
|
||||
permNode ++ dotString (m + 1) nt t ++ edge1
|
||||
| prod t1 t2 =>
|
||||
let prodNode := " node" ++ toString m ++ " [label=\"⊗\", shape=box];\n"
|
||||
let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"
|
||||
let edge2 := " node" ++ toString m ++ " -> node" ++ toString (2 * t1.size + m + 2) ++ ";\n"
|
||||
let prodNode := " node" ++ toString m ++ " [label=\"⊗\", shape=box];\n"
|
||||
let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"
|
||||
let edge2 := " node" ++ toString m ++ " -> node" ++ toString (2 * t1.size + m + 2) ++ ";\n"
|
||||
prodNode ++ dotString (m + 1) nt t1 ++ dotString (2 * t1.size + m + 2) (nt + 1) t2
|
||||
++ edge1 ++ edge2
|
||||
| smul k t =>
|
||||
let smulNode := " node" ++ toString m ++ " [label=\"smul\", shape=box];\n"
|
||||
let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"
|
||||
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"
|
||||
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"
|
||||
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"
|
||||
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 ++ " "
|
||||
let contrNode := " node" ++ toString m ++ " [label=\"contr " ++ toString i ++ " "
|
||||
++ toString j ++ "\", shape=box];\n"
|
||||
let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"
|
||||
let edge1 := " node" ++ toString m ++ " -> node" ++ toString (m + 1) ++ ";\n"
|
||||
contrNode ++ dotString (m + 1) nt t1 ++ edge1
|
||||
|
||||
/-- Used to form a dot graph from a tensor tree. use e.g.
|
||||
|
|
@ -76,7 +76,7 @@ open Lean.Elab.Command Lean Meta Lean.Elab
|
|||
syntax (name := tensorDot) "#tensor_dot " term : command
|
||||
|
||||
/-- Adapted from `Lean.Elab.Command.elabReduce` in file copyright Microsoft Corporation. -/
|
||||
unsafe def dotElab (term : Syntax) : CommandElabM Unit :=
|
||||
unsafe def dotElab (term : Syntax) : CommandElabM Unit :=
|
||||
withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_reduce do
|
||||
let e ← Term.elabTerm term none
|
||||
Term.synthesizeSyntheticMVarsNoPostponing
|
||||
|
|
|
|||
|
|
@ -308,5 +308,4 @@ variable (𝓣 : TensorTree S c4)
|
|||
-/
|
||||
end ProdNode
|
||||
|
||||
|
||||
end TensorTree
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue