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

refactor: Fix imports and some lint

Browse source
This commit is contained in:
jstoobysmith 2024-10-19 08:49:26 +00:00
parent 14bf127335
commit b2ac704d80
14 changed files with 47 additions and 69 deletions
Download patch file Download diff file Expand all files Collapse all files

5
HepLean.lean
View file

@ -62,6 +62,7 @@ import HepLean.FlavorPhysics.CKMMatrix.Relations
import HepLean.FlavorPhysics.CKMMatrix.Rows
import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
import HepLean.Mathematics.Fin
import HepLean.Mathematics.LinearMaps
import HepLean.Mathematics.PiTensorProduct
import HepLean.Mathematics.SO3.Basic
@ -108,6 +109,7 @@ import HepLean.StandardModel.HiggsBoson.Potential
import HepLean.StandardModel.Representations
import HepLean.Tensors.ComplexLorentz.Basic
import HepLean.Tensors.ComplexLorentz.Examples
import HepLean.Tensors.ComplexLorentz.Lemmas
import HepLean.Tensors.OverColor.Basic
import HepLean.Tensors.OverColor.Discrete
import HepLean.Tensors.OverColor.Functors
@ -116,3 +118,6 @@ import HepLean.Tensors.OverColor.Lift
import HepLean.Tensors.Tree.Basic
import HepLean.Tensors.Tree.Dot
import HepLean.Tensors.Tree.Elab
import HepLean.Tensors.Tree.NodeIdentities.Basic
import HepLean.Tensors.Tree.NodeIdentities.ContrContr
import HepLean.Tensors.Tree.NodeIdentities.PermContr

7
HepLean/Mathematics/Fin.lean
View file

@ -67,7 +67,6 @@ lemma succsAbove_predAboveI {i x : Fin n.succ.succ} (h : i ≠ x) :
rw [Fin.le_def] at h1
omega
lemma predAboveI_eq_iff {i x : Fin n.succ.succ} (h : i ≠ x) (y : Fin n.succ) :
y = predAboveI i x ↔ i.succAbove y = x := by
apply Iff.intro
@ -87,7 +86,6 @@ lemma predAboveI_ge {i x : Fin n.succ.succ} (h : i.val < x.val) :
simp [predAboveI, h]
omega
lemma succAbove_succAbove_predAboveI (i : Fin n.succ.succ) (j : Fin n.succ) (x : Fin n) :
i.succAbove (j.succAbove x) =
(i.succAbove j).succAbove ((predAboveI (i.succAbove j) i).succAbove x) := by
@ -178,7 +176,7 @@ def finExtractOne {n : ℕ} (i : Fin n.succ) : Fin n.succ ≃ Fin 1 ⊕ Fin n :=
lemma finExtractOne_apply_eq {n : ℕ} (i : Fin n.succ) :
finExtractOne i i = Sum.inl 0 := by
simp [finExtractOne]
have h1 : Fin.cast (finExtractOne.proof_1 i) i = Fin.castAdd ((n - ↑i) ) ⟨i.1, lt_add_one i.1⟩ := by
have h1 : Fin.cast (finExtractOne.proof_1 i) i = Fin.castAdd ((n - ↑i)) ⟨i.1, lt_add_one i.1⟩ := by
simp [Fin.ext_iff]
rw [h1, finSumFinEquiv_symm_apply_castAdd]
simp
@ -246,7 +244,6 @@ lemma finExtractOne_symm_inl_apply {n : ℕ} (i : Fin n.succ) :
ext
rfl
def finExtractOnPermHom (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ) :
Fin n.succ → Fin n.succ := fun x => predAboveI (σ i) (σ ((finExtractOne i).symm (Sum.inr x)))
@ -282,7 +279,6 @@ def finExtractOnePerm (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ
right_inv x := by
simpa using congrFun (finExtractOnPermHom_inv (σ i) σ.symm) x
/-- The equivalence of types `Fin n.succ.succ ≃ (Fin 1 ⊕ Fin 1) ⊕ Fin n` extracting
the `i` and `(i.succAbove j)`. -/
def finExtractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
@ -291,7 +287,6 @@ def finExtractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
(Equiv.sumCongr (Equiv.refl (Fin 1)) (finExtractOne j)).trans <|
(Equiv.sumAssoc (Fin 1) (Fin 1) (Fin n)).symm
@[simp]
lemma finExtractTwo_apply_fst {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ) :
finExtractTwo i j i = Sum.inl (Sum.inl 0) := by

1
HepLean/SpaceTime/LorentzVector/Complex/Metric.lean
View file

@ -105,6 +105,5 @@ lemma coMetric_apply_one : coMetric.hom (1 : ℂ) = coMetricVal := by
change coMetric.hom.toFun (1 : ℂ) = coMetricVal
simp [coMetric]
end Lorentz
end

1
HepLean/SpaceTime/LorentzVector/Complex/Two.lean
View file

@ -46,7 +46,6 @@ lemma coCoToMatrix_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin
rfl
· simp
/-- Equivalence of `complexContr ⊗ complexCo` to `4 x 4` complex matrices. -/
def contrCoToMatrix : (complexContr ⊗ complexCo).V ≃ₗ[ℂ]
Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℂ :=

8
HepLean/Tensors/ComplexLorentz/Examples.lean
View file

@ -34,10 +34,6 @@ 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}ᵀ
@ -55,13 +51,13 @@ open Lean.Elab
open Lean.Elab.Term
open Lean Meta Elab Tactic
open IndexNotation
/-
example : True :=
let f := {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗ PauliMatrix.asConsTensor | ν α' β'}ᵀ
have h1 : {Lorentz.coMetric | μ ν = Lorentz.coMetric | μ ν}ᵀ := by
sorry
sorry
-/
end Fermion
end

5
HepLean/Tensors/ComplexLorentz/Lemmas.lean
View file

@ -67,8 +67,7 @@ lemma coMetric_symm : {Lorentz.coMetric | μ ν = Lorentz.coMetric | ν μ}ᵀ :
| (0 : Fin 2) => rfl
| (1 : Fin 2) => rfl
open TensorTree in
/-
lemma coMetric_prod_antiSymm (A : (Lorentz.complexContr ⊗ Lorentz.complexContr).V)
(S : (Lorentz.complexCo ⊗ Lorentz.complexCo).V)
(hA : (twoNodeE complexLorentzTensor Color.up Color.up A).tensor =
@ -85,7 +84,7 @@ lemma coMetric_prod_antiSymm (A : (Lorentz.complexContr ⊗ Lorentz.complexContr
apply congrArg
sorry
sorry
-/
end Fermion
end

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

@ -102,8 +102,6 @@ lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discr
simp [fin2Iso, HepLean.PiTensorProduct.elimPureTensor, mkIso, mkSum]
exact (LinearEquiv.eq_symm_apply _).mp 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)
@ -112,7 +110,7 @@ lemma pairτ_tmul {c : C} (x : F.obj (Discrete.mk c)) (y : ↑(((Action.functorC
((Discrete.functor (Discrete.mk ∘ τ) ⋙ F).obj { as := c })).obj
PUnit.unit)) (h : c = c1):
((pairτ F τ).map (Discrete.eqToHom h)).hom (x ⊗ₜ[k] y)=
((F.map (Discrete.eqToHom h)).hom x) ⊗ₜ[k] ((F.map (Discrete.eqToHom (by simp [h] ))).hom y) := by
((F.map (Discrete.eqToHom h)).hom x) ⊗ₜ[k] ((F.map (Discrete.eqToHom (by simp [h]))).hom y) := by
rfl
/-- The functor taking `c` to `F (τ c) ⊗ F c`. -/
def τPair (τ : C → C) : Discrete C ⥤ Rep k G :=

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

@ -31,8 +31,6 @@ def equivToIso {c : X → C} (e : X ≃ Y) : mk c ≅ mk (c ∘ e.symm) :=
def equivToHom {c : X → C} (e : X ≃ Y) : mk c ⟶ mk (c ∘ e.symm) :=
(equivToIso e).hom
/-- Given a map `X ⊕ Y → C`, the isomorphism `mk c ≅ mk (c ∘ Sum.inl) ⊗ mk (c ∘ Sum.inr)`. -/
def mkSum (c : X ⊕ Y → C) : mk c ≅ mk (c ∘ Sum.inl) ⊗ mk (c ∘ Sum.inr) :=
Hom.toIso (Over.isoMk (Equiv.refl _).toIso (by
@ -56,7 +54,7 @@ def mkIso {c1 c2 : X → C} (h : c1 = c2) : mk c1 ≅ mk c2 :=
subst h
rfl))
def equivToHomEq {c : X → C} {c1 : Y → C} (e : X ≃ Y) (h : ∀ x, c1 x = (c ∘ e.symm ) x := by decide) :
def equivToHomEq {c : X → C} {c1 : Y → C} (e : X ≃ Y) (h : ∀ x, c1 x = (c ∘ e.symm) x := by decide) :
mk c ⟶ mk c1 :=
(equivToHom e).trans (mkIso (funext fun x => (h x).symm)).hom
@ -216,7 +214,7 @@ lemma extractTwo_finExtractTwo_succ {n : ℕ} (i : Fin n.succ.succ.succ) (j : F
exact (Fin.succAbove_ne i j).symm
by_contra hn
have hn' := hn.symm.trans h0
erw [ Fin.succAbove_right_injective.eq_iff] at hn'
erw [Fin.succAbove_right_injective.eq_iff] at hn'
exact Fin.succAbove_ne
(predAboveI ((Hom.toEquiv σ).symm i) ((Hom.toEquiv σ).symm (i.succAbove j))) x hn'
exact hy

6
HepLean/Tensors/OverColor/Lift.lean
View file

@ -648,7 +648,7 @@ noncomputable def lift : (Discrete C ⥤ Rep k G) ⥤ MonoidalFunctor (OverColor
namespace lift
lemma map_tprod (F : Discrete C ⥤ Rep k G ) {X Y : OverColor C} (f : X ⟶ Y)
lemma map_tprod (F : Discrete C ⥤ Rep k G) {X Y : OverColor C} (f : X ⟶ Y)
(p : (i : X.left) → F.obj (Discrete.mk <| X.hom i)) :
((lift.obj F).map f).hom (PiTensorProduct.tprod k p) =
PiTensorProduct.tprod k fun (i : Y.left) => discreteFunctorMapEqIso F
@ -656,7 +656,7 @@ lemma map_tprod (F : Discrete C ⥤ Rep k G ) {X Y : OverColor C} (f : X ⟶ Y)
simp [lift, obj']
erw [objMap'_tprod]
lemma obj_μ_tprod_tmul (F : Discrete C ⥤ Rep k G ) (X Y : OverColor C)
lemma obj_μ_tprod_tmul (F : Discrete C ⥤ Rep k G) (X Y : OverColor C)
(p : (i : X.left) → (F.obj (Discrete.mk <| X.hom i)))
(q : (i : Y.left) → F.obj (Discrete.mk <| Y.hom i)) :
((lift.obj F).μ X Y).hom (PiTensorProduct.tprod k p ⊗ₜ[k] PiTensorProduct.tprod k q) =
@ -664,7 +664,7 @@ lemma obj_μ_tprod_tmul (F : Discrete C ⥤ Rep k G ) (X Y : OverColor C)
discreteSumEquiv F i (HepLean.PiTensorProduct.elimPureTensor p q i) := by
exact μ_tmul_tprod F p q
lemma μIso_inv_tprod (F : Discrete C ⥤ Rep k G ) (X Y : OverColor C)
lemma μIso_inv_tprod (F : Discrete C ⥤ Rep k G) (X Y : OverColor C)
(p : (i : (X ⊗ Y).left) → F.obj (Discrete.mk <| (X ⊗ Y).hom i)) :
((lift.obj F).μIso X Y).inv.hom (PiTensorProduct.tprod k p) =
(PiTensorProduct.tprod k (fun i => p (Sum.inl i))) ⊗ₜ[k]

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

@ -181,7 +181,6 @@ def contrIso {n : ℕ} (c : Fin n.succ.succ → S.C)
(S.F.μIso _ _).symm.trans <| by
refine tensorIso (S.contrFin1Fin1 c i j h) (S.F.mapIso (OverColor.mkIso (by ext x; simp)))
lemma contrIso_hom_hom {n : ℕ} {c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ} {j : Fin n.succ}
{h : c1 (i.succAbove j) = S.τ (c1 i)} :
@ -196,7 +195,6 @@ lemma contrIso_hom_hom {n : ℕ} {c1 : Fin n.succ.succ → S.C}
simp [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V, Action.comp_hom,
extractOne_homToEquiv, Action.instMonoidalCategory_tensorHom_hom]
/-- `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
@ -217,7 +215,7 @@ lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
(x : (i : Fin n.succ.succ) → S.FDiscrete.obj (Discrete.mk (c i))) :
(S.contrMap c i j h).hom (PiTensorProduct.tprod S.k x) =
(S.castToField ((S.contr.app (Discrete.mk (c i))).hom ((x i) ⊗ₜ[S.k]
(S.FDiscrete.map (Discrete.eqToHom h)).hom (x (i.succAbove j)) )): S.k)
(S.FDiscrete.map (Discrete.eqToHom h)).hom (x (i.succAbove j)))): S.k)
• (PiTensorProduct.tprod S.k (fun k => x (i.succAbove (j.succAbove k))) : S.F.obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))) := by
rw [contrMap, contrIso]
simp only [Nat.succ_eq_add_one, S.F_def, Iso.trans_hom, Functor.mapIso_hom, Iso.symm_hom,

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

@ -173,7 +173,6 @@ def stringToTerm (str : String) : TermElabM Term := do
match stx with
| `(term| $e) => return e
/-- The syntax associated with a terminal node of a tensor tree. -/
def termNodeSyntax (T : Term) : TermElabM Term := do
let expr ← elabTerm T none
@ -270,7 +269,7 @@ def toPairs (l : List ℕ) : List (ℕ × ℕ) :=
| [] => []
| [x] => [(x, 0)]
def contrListAdjust (l : List (ℕ × ℕ)) : List (ℕ × ℕ ) :=
def contrListAdjust (l : List (ℕ × ℕ)) : List (ℕ × ℕ) :=
let l' := l.bind (fun p => [p.1, p.2])
let l'' := List.mapAccumr
(fun x (prev : List ℕ) =>

3
HepLean/Tensors/Tree/NodeIdentities/Basic.lean
View file

@ -13,7 +13,6 @@ More compliciated identities appear in there own files.
-/
open IndexNotation
open CategoryTheory
open MonoidalCategory
@ -43,7 +42,6 @@ informal_lemma constThreeNode_eq_threeNode where
math :≈ "A constThreeNode has equal tensor to the threeNode with the map evaluated at 1."
deps :≈ [``constThreeNode, ``threeNode]
/-!
## Negation
@ -80,5 +78,4 @@ lemma neg_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
(perm σ (neg t)).tensor = (neg (perm σ t)).tensor := by
simp only [perm_tensor, neg_tensor, map_neg]
end TensorTree

16
HepLean/Tensors/Tree/NodeIdentities/ContrContr.lean
View file

@ -74,7 +74,6 @@ lemma swapI_neq_i_j_k_l_succAbove : ¬ q.swapI = q.i.succAbove (q.j.succAbove (q
apply Function.Injective.ne Fin.succAbove_right_injective
exact Fin.ne_succAbove q.k q.l
lemma swapJ_swapI_succAbove : q.swapI.succAbove q.swapJ = q.i.succAbove
(q.j.succAbove (q.k.succAbove q.l)) := by
simp [swapI, swapJ]
@ -124,7 +123,6 @@ def swap : ContrQuartet c where
hkl := by
simpa using q.hij
noncomputable section
def contrMapFst := S.contrMap c q.i q.j q.hij
@ -148,9 +146,10 @@ lemma contrSwapHom_contrMapSnd_tprod (x : (i : (𝟭 Type).obj (OverColor.mk c).
rw [contrMapSnd,TensorStruct.contrMap_tprod]
change ((lift.obj S.FDiscrete).map q.contrSwapHom).hom
(_ • ((PiTensorProduct.tprod S.k) fun k =>
x (q.swap.i.succAbove (q.swap.j.succAbove (q.swap.k.succAbove (q.swap.l.succAbove k))
)): S.F.obj (OverColor.mk ((c ∘ q.swap.i.succAbove ∘ q.swap.j.succAbove) ∘
q.swap.k.succAbove ∘ q.swap.l.succAbove)) )) = _
x (q.swap.i.succAbove (q.swap.j.succAbove
(q.swap.k.succAbove (q.swap.l.succAbove k)))) :
S.F.obj (OverColor.mk ((c ∘ q.swap.i.succAbove ∘ q.swap.j.succAbove) ∘
q.swap.k.succAbove ∘ q.swap.l.succAbove)))) = _
rw [map_smul]
rfl
@ -251,13 +250,14 @@ end ContrQuartet
/-- Contraction nodes commute on adjusting indices. -/
theorem contr_contr {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} {i : Fin n.succ.succ.succ.succ}
{j : Fin n.succ.succ.succ} {k : Fin n.succ.succ} {l : Fin n.succ}
(hij : c (i.succAbove j) = S.τ (c i)) (hkl : (c ∘ i.succAbove ∘ j.succAbove) (k.succAbove l) = S.τ ((c ∘ i.succAbove ∘ j.succAbove) k))
(hij : c (i.succAbove j) = S.τ (c i)) (hkl : (c ∘ i.succAbove ∘ j.succAbove) (k.succAbove l) =
S.τ ((c ∘ i.succAbove ∘ j.succAbove) k))
(t : TensorTree S c) :
(contr k l hkl (contr i j hij t)).tensor =
(perm (ContrQuartet.mk i j k l hij hkl).contrSwapHom
(contr (ContrQuartet.mk i j k l hij hkl).swapK (ContrQuartet.mk i j k l hij hkl).swapL
(ContrQuartet.mk i j k l hij hkl).swap.hkl (contr (ContrQuartet.mk i j k l hij hkl).swapI (ContrQuartet.mk i j k l hij hkl).swapJ (ContrQuartet.mk i j k l hij hkl).swap.hij t))).tensor := by
(ContrQuartet.mk i j k l hij hkl).swap.hkl (contr (ContrQuartet.mk i j k l hij hkl).swapI
(ContrQuartet.mk i j k l hij hkl).swapJ (ContrQuartet.mk i j k l hij hkl).swap.hij t))).tensor := by
exact ContrQuartet.contr_contr (ContrQuartet.mk i j k l hij hkl) t
end TensorTree

47
HepLean/Tensors/Tree/NodeIdentities/PermContr.lean
View file

@ -12,7 +12,6 @@ There is very likely a better way to do this using `TensorStruct.contrMap_tprod`
-/
open IndexNotation
open CategoryTheory
open MonoidalCategory
@ -32,34 +31,34 @@ lemma contrFin1Fin1_naturality {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
((HepLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)
(perm_contr_cond S h σ)).hom.hom
≫ ((Discrete.pairτ S.FDiscrete S.τ).map (Discrete.eqToHom (Hom.toEquiv_comp_inv_apply σ i)
: (Discrete.mk (c ((Hom.toEquiv σ).symm i))) ⟶ (Discrete.mk (c1 i)) )).hom
: (Discrete.mk (c ((Hom.toEquiv σ).symm i))) ⟶ (Discrete.mk (c1 i)))).hom
:= by
have h1 : (S.F.map (extractTwoAux' i j σ)) ≫ (S.contrFin1Fin1 c1 i j h).hom
= (S.contrFin1Fin1 c ((Hom.toEquiv σ).symm i)
((HepLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)
(perm_contr_cond S h σ)).hom
≫ ((Discrete.pairτ S.FDiscrete S.τ).map (Discrete.eqToHom (Hom.toEquiv_comp_inv_apply σ i)
: (Discrete.mk (c ((Hom.toEquiv σ).symm i))) ⟶ (Discrete.mk (c1 i)) )) := by
: (Discrete.mk (c ((Hom.toEquiv σ).symm i))) ⟶ (Discrete.mk (c1 i)))) := by
erw [← CategoryTheory.Iso.eq_comp_inv ]
rw [CategoryTheory.Category.assoc]
erw [← CategoryTheory.Iso.inv_comp_eq ]
ext1
apply TensorProduct.ext'
intro x y
intro x y
simp only [Nat.succ_eq_add_one, Equivalence.symm_inverse,
Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
Functor.comp_obj, Discrete.functor_obj_eq_as, Function.comp_apply, CategoryStruct.comp,
extractOne_homToEquiv, Action.Hom.comp_hom, LinearMap.coe_comp]
trans (S.F.map (extractTwoAux' i j σ)).hom (PiTensorProduct.tprod S.k (fun k =>
match k with | Sum.inl 0 => x | Sum.inr 0 => (S.FDiscrete.map
(eqToHom (by simp; erw [perm_contr_cond S h σ]))).hom y) )
(eqToHom (by simp; erw [perm_contr_cond S h σ]))).hom y))
· apply congrArg
have h1' {α :Type} {a b c d : α} (hab : a= b) (hcd : c =d ) (h : a = d) : b = c := by
rw [← hab, hcd]
have h1' {α :Type} {a b c d : α} (hab : a= b) (hcd : c = d) (h : a = d) : b = c := by
rw [← hab, hcd]
exact h
have h1 := S.contrFin1Fin1_inv_tmul c ((Hom.toEquiv σ).symm i)
((HepLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)
(perm_contr_cond S h σ ) x y
(perm_contr_cond S h σ) x y
refine h1' ?_ ?_ h1
congr
apply congrArg
@ -71,7 +70,7 @@ lemma contrFin1Fin1_naturality {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
((S.FDiscrete.map (Discrete.eqToHom (Hom.toEquiv_comp_inv_apply σ i))).hom x ⊗ₜ[S.k]
(S.FDiscrete.map (Discrete.eqToHom (congrArg S.τ (Hom.toEquiv_comp_inv_apply σ i)))).hom y)
rw [contrFin1Fin1_inv_tmul]
change ((lift.obj S.FDiscrete).map (extractTwoAux' i j σ)).hom _ = _
change ((lift.obj S.FDiscrete).map (extractTwoAux' i j σ)).hom _ = _
rw [lift.map_tprod]
apply congrArg
funext i
@ -79,13 +78,12 @@ lemma contrFin1Fin1_naturality {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
| Sum.inl 0 => rfl
| Sum.inr 0 =>
simp [lift.discreteFunctorMapEqIso]
change ((S.FDiscrete.map (eqToHom _)) ≫ S.FDiscrete.map (eqToHom _)).hom y = ((S.FDiscrete.map (eqToHom _)) ≫ S.FDiscrete.map (eqToHom _)).hom y
change ((S.FDiscrete.map (eqToHom _)) ≫ S.FDiscrete.map (eqToHom _)).hom y = ((S.FDiscrete.map (eqToHom _)) ≫ S.FDiscrete.map (eqToHom _)).hom y
rw [← Functor.map_comp, ← Functor.map_comp]
simp only [Fin.isValue, Nat.succ_eq_add_one, Discrete.functor_obj_eq_as, Function.comp_apply,
eqToHom_trans]
exact congrArg (λ f => Action.Hom.hom f) h1
lemma contrIso_comm_aux_1 {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ} {j : Fin n.succ}
(σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) :
@ -110,12 +108,12 @@ lemma contrIso_comm_aux_2 {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
(σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) :
(S.F.map (extractTwoAux' i j σ ⊗ extractTwoAux i j σ)).hom ≫
(S.F.μIso (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
(OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom =
(OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom =
(S.F.μIso _ _).inv.hom ≫ (S.F.map (extractTwoAux' i j σ) ⊗ S.F.map (extractTwoAux i j σ)).hom
:= by
have h1 : (S.F.map (extractTwoAux' i j σ ⊗ extractTwoAux i j σ)) ≫
(S.F.μIso (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
(OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv =
(OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv =
(S.F.μIso _ _).inv ≫ (S.F.map (extractTwoAux' i j σ) ⊗ S.F.map (extractTwoAux i j σ)) := by
erw [CategoryTheory.IsIso.comp_inv_eq, CategoryTheory.Category.assoc]
erw [CategoryTheory.IsIso.eq_inv_comp ]
@ -132,31 +130,31 @@ lemma contrIso_comm_aux_3 {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
PUnit.unit ≫
(S.F.map (mkIso (contrIso.proof_1 S c1 i j)).hom).hom
= (S.F.map (mkIso (contrIso.proof_1 S c ((Hom.toEquiv σ).symm i)
((HepLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j) )).hom).hom ≫
((HepLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j))).hom).hom ≫
(S.F.map (extractTwo i j σ)).hom := by
change (S.F.map (extractTwoAux i j σ)).hom ≫ _ = _
change (S.F.map (extractTwoAux i j σ)).hom ≫ _ = _
have h1 : (S.F.map (extractTwoAux i j σ)) ≫ (S.F.map (mkIso (contrIso.proof_1 S c1 i j)).hom) =
(S.F.map (mkIso (contrIso.proof_1 S c ((Hom.toEquiv σ).symm i)
((HepLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j) )).hom) ≫ (S.F.map (extractTwo i j σ)) := by
((HepLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j))).hom) ≫ (S.F.map (extractTwo i j σ)) := by
rw [← Functor.map_comp, ← Functor.map_comp]
apply congrArg
rfl
exact congrArg (λ f => Action.Hom.hom f) h1
def contrIsoComm {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
def contrIsoComm {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ} {j : Fin n.succ} (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) :=
(((Discrete.pairτ S.FDiscrete S.τ).map (Discrete.eqToHom (Hom.toEquiv_comp_inv_apply σ i)
: (Discrete.mk (c ((Hom.toEquiv σ).symm i))) ⟶ (Discrete.mk (c1 i)) )) ⊗ (S.F.map (extractTwo i j σ)))
: (Discrete.mk (c ((Hom.toEquiv σ).symm i))) ⟶ (Discrete.mk (c1 i)))) ⊗ (S.F.map (extractTwo i j σ)))
lemma contrIso_comm_aux_5 {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ} {j : Fin n.succ} (h : c1 (i.succAbove j) = S.τ (c1 i))
(σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) :
(S.F.map (extractTwoAux' i j σ) ⊗ S.F.map (extractTwoAux i j σ)).hom ≫
((S.contrFin1Fin1 c1 i j h).hom.hom ⊗ (S.F.map (mkIso (contrIso.proof_1 S c1 i j)).hom).hom)
= ((S.contrFin1Fin1 c ((Hom.toEquiv σ).symm i)
= ((S.contrFin1Fin1 c ((Hom.toEquiv σ).symm i)
((HepLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)
(perm_contr_cond S h σ)).hom.hom ⊗ (S.F.map (mkIso (contrIso.proof_1 S c ((Hom.toEquiv σ).symm i)
((HepLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j) )).hom).hom)
((HepLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j))).hom).hom)
≫ (S.contrIsoComm σ).hom
:= by
erw [← CategoryTheory.MonoidalCategory.tensor_comp (f₁ := (S.F.map (extractTwoAux' i j σ)).hom)]
@ -164,15 +162,14 @@ lemma contrIso_comm_aux_5 {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
rw [contrFin1Fin1_naturality S h σ]
simp [contrIsoComm]
lemma contrIso_comm_map {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ} {j : Fin n.succ}
{h : c1 (i.succAbove j) = S.τ (c1 i)}
(σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) :
(S.F.map σ) ≫ (S.contrIso c1 i j h).hom =
(S.contrIso c ((OverColor.Hom.toEquiv σ).symm i)
(((Hom.toEquiv (extractOne i σ))).symm j) (S.perm_contr_cond h σ)).hom ≫
contrIsoComm S σ := by
(((Hom.toEquiv (extractOne i σ))).symm j) (S.perm_contr_cond h σ)).hom ≫
contrIsoComm S σ := by
ext1
simp only [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V, Action.comp_hom,
extractOne_homToEquiv, Action.instMonoidalCategory_tensorHom_hom]
@ -196,7 +193,6 @@ lemma contrIso_comm_map {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
Action.functorCategoryEquivalence_functor,
Action.FunctorCategoryEquivalence.functor_obj_obj] using contrIso_comm_aux_5 S h σ
/-- Contraction commutes with `S.F.map σ` on removing corresponding indices from `σ`. -/
lemma contrMap_naturality {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ} {j : Fin n.succ} {h : c1 (i.succAbove j) = S.τ (c1 i)}
@ -221,7 +217,7 @@ lemma contrMap_naturality {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
apply congrArg
rw [contrIsoComm]
rw [← tensor_comp]
have h1 : 𝟙_ (Rep S.k S.G) ◁ S.F.map (extractTwo i j σ) = 𝟙 _ ⊗ S.F.map (extractTwo i j σ) := by
have h1 : 𝟙_ (Rep S.k S.G) ◁ S.F.map (extractTwo i j σ) = 𝟙 _ ⊗ S.F.map (extractTwo i j σ) := by
rfl
rw [h1, ← tensor_comp]
erw [CategoryTheory.Category.id_comp, CategoryTheory.Category.comp_id]
@ -233,7 +229,6 @@ lemma contrMap_naturality {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
end
end TensorStruct
namespace TensorTree
variable {S : TensorStruct}