refactor: Lint text
This commit is contained in:
jstoobysmith
parent
855dc5146d
commit
1f3ba14462
12 changed files with 168 additions and 127 deletions
|
|
@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith
|
|||
import Mathlib.LinearAlgebra.PiTensorProduct
|
||||
import Mathlib.Tactic.Polyrith
|
||||
import Mathlib.Tactic.Linarith
|
||||
import LLMLean
|
||||
/-!
|
||||
# Fin lemmas
|
||||
|
||||
|
|
@ -177,7 +176,8 @@ lemma finExtractOne_apply_eq {n : ℕ} (i : Fin n.succ) :
|
|||
finExtractOne i i = Sum.inl 0 := by
|
||||
simp only [Nat.succ_eq_add_one, finExtractOne, Equiv.trans_apply, finCongr_apply,
|
||||
Equiv.sumCongr_apply, Equiv.coe_trans, Equiv.sumComm_apply, Equiv.coe_refl, Fin.isValue]
|
||||
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 only [Nat.succ_eq_add_one, Sum.map_inl, Function.comp_apply, Fin.isValue]
|
||||
|
|
@ -249,7 +249,7 @@ def finExtractOnPermHom (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.su
|
|||
Fin n.succ → Fin n.succ := fun x => predAboveI (σ i) (σ ((finExtractOne i).symm (Sum.inr x)))
|
||||
|
||||
lemma finExtractOnPermHom_inv (i : Fin n.succ.succ) (σ : Fin n.succ.succ ≃ Fin n.succ.succ) :
|
||||
(finExtractOnPermHom (σ i) σ.symm) ∘ (finExtractOnPermHom i σ) = id := by
|
||||
(finExtractOnPermHom (σ i) σ.symm) ∘ (finExtractOnPermHom i σ) = id := by
|
||||
funext x
|
||||
simp only [Nat.succ_eq_add_one, Function.comp_apply, finExtractOnPermHom, Equiv.symm_apply_apply,
|
||||
finExtractOne_symm_inr_apply, id_eq]
|
||||
|
|
|
|||
|
|
@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
|
|||
-/
|
||||
import HepLean.SpaceTime.LorentzVector.Complex.Two
|
||||
import HepLean.SpaceTime.MinkowskiMetric
|
||||
import LLMLean
|
||||
/-!
|
||||
|
||||
# Metric for complex Lorentz vectors
|
||||
|
|
|
|||
|
|
@ -385,7 +385,7 @@ lemma σSAL_repr_inr_2 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
|
|||
real_smul, zero_add, neg_neg, isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
|
||||
IsUnit.mul_div_cancel_right] at h0
|
||||
linear_combination (norm := ring_nf) -h0
|
||||
simp [σSAL]
|
||||
simp only [σSAL, Basis.mk_repr, Fin.isValue, sub_self]
|
||||
|
||||
lemma σSA_minkowskiMetric_σSAL (i : Fin 1 ⊕ Fin 3) :
|
||||
(σSA i) = minkowskiMatrix i i • (σSAL i) := by
|
||||
|
|
|
|||
|
|
@ -53,7 +53,8 @@ open Lean Meta Elab Tactic
|
|||
open IndexNotation
|
||||
/-
|
||||
example : True :=
|
||||
let f := {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗ PauliMatrix.asConsTensor | ν α' β'}ᵀ
|
||||
let f := {Lorentz.coMetric | μ ν ⊗ PauliMatrix.asConsTensor | μ α β ⊗
|
||||
PauliMatrix.asConsTensor | ν α' β'}ᵀ
|
||||
have h1 : {Lorentz.coMetric | μ ν = Lorentz.coMetric | μ ν}ᵀ := by
|
||||
sorry
|
||||
sorry
|
||||
|
|
|
|||
|
|
@ -7,7 +7,6 @@ import HepLean.Tensors.OverColor.Basic
|
|||
import HepLean.Tensors.OverColor.Lift
|
||||
import HepLean.Mathematics.PiTensorProduct
|
||||
import HepLean.Tensors.OverColor.Iso
|
||||
import LLMLean
|
||||
/-!
|
||||
|
||||
# Discrete color category
|
||||
|
|
@ -84,7 +83,7 @@ lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discr
|
|||
change ((lift.obj F).map fin2Iso.inv).hom
|
||||
(((lift.obj F).map ((mkIso _).hom ⊗ (mkIso _).hom)).hom
|
||||
(((lift.obj F).μ (mk fun _ => c1) (mk fun _ => c2)).hom
|
||||
(((PiTensorProduct.tprod k) fun _ => x) ⊗ₜ[k] (PiTensorProduct.tprod k) fun x => y))) = _
|
||||
(((PiTensorProduct.tprod k) fun _ => x) ⊗ₜ[k] (PiTensorProduct.tprod k) fun _ => y))) = _
|
||||
rw [lift.obj_μ_tprod_tmul F (mk fun _ => c1) (mk fun _ => c2)]
|
||||
change ((lift.obj F).map fin2Iso.inv).hom
|
||||
(((lift.obj F).map ((mkIso _).hom ⊗ (mkIso _).hom)).hom
|
||||
|
|
@ -114,12 +113,13 @@ lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discr
|
|||
def pairτ (τ : C → C) : Discrete C ⥤ Rep k G :=
|
||||
F ⊗ ((Discrete.functor (Discrete.mk ∘ τ) : Discrete C ⥤ Discrete C) ⋙ F)
|
||||
|
||||
lemma pairτ_tmul {c : C} (x : F.obj (Discrete.mk c)) (y : ↑(((Action.functorCategoryEquivalence (ModuleCat k) (MonCat.of G)).symm.inverse.obj
|
||||
((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
|
||||
lemma pairτ_tmul {c : C} (x : F.obj (Discrete.mk c))
|
||||
(y : ↑(((Action.functorCategoryEquivalence (ModuleCat k) (MonCat.of G)).symm.inverse.obj
|
||||
((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
|
||||
rfl
|
||||
|
||||
/-- 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
|
||||
|
|
|
|||
|
|
@ -6,7 +6,6 @@ Authors: Joseph Tooby-Smith
|
|||
import HepLean.Tensors.OverColor.Functors
|
||||
import HepLean.Tensors.OverColor.Lift
|
||||
import HepLean.Mathematics.Fin
|
||||
import LLMLean
|
||||
/-!
|
||||
|
||||
## Isomorphisms in the OverColor category
|
||||
|
|
@ -54,8 +53,8 @@ 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) :
|
||||
mk c ⟶ mk c1 :=
|
||||
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
|
||||
|
||||
/-- The isomorphism splitting a `mk c` for `Fin 2 → C` into the tensor product of
|
||||
|
|
@ -93,8 +92,8 @@ def extractOne {n : ℕ} (i : Fin n.succ.succ)
|
|||
|
||||
@[simp]
|
||||
lemma extractOne_homToEquiv {n : ℕ} (i : Fin n.succ.succ)
|
||||
{c1 c2 : Fin n.succ.succ → C} (σ : mk c1 ⟶ mk c2) :
|
||||
Hom.toEquiv (extractOne i σ) = (finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)) := by
|
||||
{c1 c2 : Fin n.succ.succ → C} (σ : mk c1 ⟶ mk c2) : Hom.toEquiv (extractOne i σ) =
|
||||
(finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)) := by
|
||||
rfl
|
||||
|
||||
def extractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
|
||||
|
|
@ -110,13 +109,15 @@ def extractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
|
|||
|
||||
def extractTwoAux {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
|
||||
{c c1 : Fin n.succ.succ → C} (σ : mk c ⟶ mk c1) :
|
||||
mk ((c ∘ ⇑(finExtractTwo ((Hom.toEquiv σ).symm i) ((Hom.toEquiv (extractOne i σ)).symm j)).symm) ∘ Sum.inr) ⟶
|
||||
mk ((c ∘ ⇑(finExtractTwo ((Hom.toEquiv σ).symm i)
|
||||
((Hom.toEquiv (extractOne i σ)).symm j)).symm) ∘ Sum.inr) ⟶
|
||||
mk ((c1 ∘ ⇑(finExtractTwo i j).symm) ∘ Sum.inr) :=
|
||||
equivToHomEq (Equiv.refl _) (by simp) ≫ extractTwo i j σ ≫ equivToHomEq (Equiv.refl _) (by simp)
|
||||
|
||||
def extractTwoAux' {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
|
||||
{c c1 : Fin n.succ.succ → C} (σ : mk c ⟶ mk c1) :
|
||||
mk ((c ∘ ⇑(finExtractTwo ((Hom.toEquiv σ).symm i) ((Hom.toEquiv (extractOne i σ)).symm j)).symm) ∘ Sum.inl) ⟶
|
||||
mk ((c ∘ ⇑(finExtractTwo ((Hom.toEquiv σ).symm i)
|
||||
((Hom.toEquiv (extractOne i σ)).symm j)).symm) ∘ Sum.inl) ⟶
|
||||
mk ((c1 ∘ ⇑(finExtractTwo i j).symm) ∘ Sum.inl) :=
|
||||
equivToHomEq (Equiv.refl _) (by
|
||||
intro x
|
||||
|
|
@ -144,9 +145,12 @@ def extractTwoAux' {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
|
|||
|
||||
lemma extractTwo_finExtractTwo_succ {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fin n.succ.succ)
|
||||
{c c1 : Fin n.succ.succ.succ → C} (σ : mk c ⟶ mk c1) :
|
||||
σ ≫ (equivToIso (HepLean.Fin.finExtractTwo i j)).hom ≫ (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom =
|
||||
(equivToIso (HepLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i) (((Hom.toEquiv (extractOne i σ))).symm j))).hom
|
||||
≫ (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i) (((Hom.toEquiv (extractOne i σ))).symm j)).symm)).hom
|
||||
σ ≫ (equivToIso (HepLean.Fin.finExtractTwo i j)).hom ≫
|
||||
(mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom =
|
||||
(equivToIso (HepLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i)
|
||||
(((Hom.toEquiv (extractOne i σ))).symm j))).hom
|
||||
≫ (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i)
|
||||
(((Hom.toEquiv (extractOne i σ))).symm j)).symm)).hom
|
||||
≫ ((extractTwoAux' i j σ) ⊗ (extractTwoAux i j σ)) := by
|
||||
apply IndexNotation.OverColor.Hom.ext
|
||||
ext x
|
||||
|
|
@ -155,8 +159,9 @@ lemma extractTwo_finExtractTwo_succ {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fi
|
|||
Discrete.mk_as, instMonoidalCategoryStruct_tensorObj_right_as, CostructuredArrow.right_eq_id,
|
||||
ULift.rec.constant, Function.comp_apply, extractOne_homToEquiv, extractTwoAux', extractTwoAux,
|
||||
instMonoidalCategoryStruct_tensorHom_hom_left]
|
||||
change ((finExtractTwo i j) ((Hom.toEquiv σ) x)) = Sum.map id ((finExtractOnePerm ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)
|
||||
(finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ))))
|
||||
change ((finExtractTwo i j) ((Hom.toEquiv σ) x)) = Sum.map id
|
||||
((finExtractOnePerm ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)
|
||||
(finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ))))
|
||||
(((finExtractTwo ((Hom.toEquiv σ).symm i)
|
||||
((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)) x))
|
||||
simp only [Nat.succ_eq_add_one]
|
||||
|
|
@ -192,14 +197,14 @@ lemma extractTwo_finExtractTwo_succ {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fi
|
|||
finExtractOne_symm_inr_apply, Equiv.symm_apply_apply, Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk]
|
||||
erw [Equiv.apply_symm_apply]
|
||||
have h1 : (predAboveI i ((Hom.toEquiv σ)
|
||||
(Fin.succAbove ((Hom.toEquiv σ).symm i)
|
||||
(predAboveI ((Hom.toEquiv σ).symm i) ((Hom.toEquiv σ).symm (i.succAbove j)))))) = j := by
|
||||
rw [succsAbove_predAboveI]
|
||||
· erw [Equiv.apply_symm_apply]
|
||||
simp
|
||||
· simp only [Nat.succ_eq_add_one, ne_eq]
|
||||
erw [Equiv.apply_eq_iff_eq]
|
||||
exact (Fin.succAbove_ne i j).symm
|
||||
(Fin.succAbove ((Hom.toEquiv σ).symm i)
|
||||
(predAboveI ((Hom.toEquiv σ).symm i) ((Hom.toEquiv σ).symm (i.succAbove j)))))) = j := by
|
||||
rw [succsAbove_predAboveI]
|
||||
· erw [Equiv.apply_symm_apply]
|
||||
simp
|
||||
· simp only [Nat.succ_eq_add_one, ne_eq]
|
||||
erw [Equiv.apply_eq_iff_eq]
|
||||
exact (Fin.succAbove_ne i j).symm
|
||||
erw [h1]
|
||||
let y := (Hom.toEquiv σ) (Fin.succAbove ((Hom.toEquiv σ).symm i)
|
||||
((predAboveI ((Hom.toEquiv σ).symm i) ((Hom.toEquiv σ).symm (i.succAbove j))).succAbove x))
|
||||
|
|
@ -230,9 +235,12 @@ lemma extractTwo_finExtractTwo_succ {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fi
|
|||
|
||||
lemma extractTwo_finExtractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
|
||||
{c c1 : Fin n.succ.succ → C} (σ : mk c ⟶ mk c1) :
|
||||
σ ≫ (equivToIso (HepLean.Fin.finExtractTwo i j)).hom ≫ (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom =
|
||||
(equivToIso (HepLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i) (((Hom.toEquiv (extractOne i σ))).symm j))).hom
|
||||
≫ (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i) (((Hom.toEquiv (extractOne i σ))).symm j)).symm)).hom
|
||||
σ ≫ (equivToIso (HepLean.Fin.finExtractTwo i j)).hom ≫
|
||||
(mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom =
|
||||
(equivToIso (HepLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i)
|
||||
(((Hom.toEquiv (extractOne i σ))).symm j))).hom
|
||||
≫ (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i)
|
||||
(((Hom.toEquiv (extractOne i σ))).symm j)).symm)).hom
|
||||
≫ ((extractTwoAux' i j σ) ⊗ (extractTwoAux i j σ)) := by
|
||||
match n with
|
||||
| 0 =>
|
||||
|
|
|
|||
|
|
@ -670,7 +670,8 @@ lemma μIso_inv_tprod (F : Discrete C ⥤ Rep k G) (X Y : OverColor C)
|
|||
(PiTensorProduct.tprod k (fun i => p (Sum.inl i))) ⊗ₜ[k]
|
||||
(PiTensorProduct.tprod k (fun i => p (Sum.inr i))) := by
|
||||
change ((Action.forget _ _).mapIso ((lift.obj F).μIso X Y)).inv (PiTensorProduct.tprod k p) = _
|
||||
trans ((Action.forget _ _).mapIso ((lift.obj F).μIso X Y)).toLinearEquiv.symm (PiTensorProduct.tprod k p)
|
||||
trans ((Action.forget _ _).mapIso ((lift.obj F).μIso X Y)).toLinearEquiv.symm
|
||||
(PiTensorProduct.tprod k p)
|
||||
· congr
|
||||
erw [← LinearEquiv.eq_symm_apply]
|
||||
change _ = ((lift.obj F).μ X Y).hom _
|
||||
|
|
|
|||
|
|
@ -7,7 +7,6 @@ import HepLean.Tensors.OverColor.Iso
|
|||
import HepLean.Tensors.OverColor.Discrete
|
||||
import HepLean.Tensors.OverColor.Lift
|
||||
import Mathlib.CategoryTheory.Monoidal.NaturalTransformation
|
||||
import LLMLean
|
||||
/-!
|
||||
|
||||
## Tensor trees
|
||||
|
|
@ -90,7 +89,8 @@ def contrFin1Fin1 {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 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) ≅
|
||||
(OverColor.Discrete.pairτ S.FDiscrete S.τ).obj { as := c i } := by
|
||||
apply (S.F.mapIso (OverColor.mkSum (((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)))).trans
|
||||
apply (S.F.mapIso
|
||||
(OverColor.mkSum (((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)))).trans
|
||||
apply (S.F.μIso _ _).symm.trans
|
||||
apply tensorIso ?_ ?_
|
||||
· symm
|
||||
|
|
@ -126,23 +126,28 @@ lemma contrFin1Fin1_inv_tmul {n : ℕ} (c : Fin n.succ.succ → S.C)
|
|||
Fin.isValue]
|
||||
change (S.F.map (OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
|
||||
((S.F.map ((OverColor.mkIso _).hom ⊗ (OverColor.mkIso _).hom)).hom
|
||||
((S.F.μ (OverColor.mk fun x => c i) (OverColor.mk fun x => S.τ (c i))).hom
|
||||
((S.F.μ (OverColor.mk fun _ => c i) (OverColor.mk fun _ => S.τ (c i))).hom
|
||||
((((OverColor.forgetLiftApp S.FDiscrete (c i)).inv.hom x) ⊗ₜ[S.k]
|
||||
((OverColor.forgetLiftApp S.FDiscrete (S.τ (c i))).inv.hom y))))) = _
|
||||
simp only [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse,
|
||||
Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
|
||||
forgetLiftApp, Action.mkIso_inv_hom, LinearEquiv.toModuleIso_inv, Fin.isValue]
|
||||
erw [OverColor.forgetLiftAppV_symm_apply, OverColor.forgetLiftAppV_symm_apply S.FDiscrete (S.τ (c i))]
|
||||
change ((OverColor.lift.obj S.FDiscrete).map (OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
|
||||
erw [OverColor.forgetLiftAppV_symm_apply,
|
||||
OverColor.forgetLiftAppV_symm_apply S.FDiscrete (S.τ (c i))]
|
||||
change ((OverColor.lift.obj S.FDiscrete).map (OverColor.mkSum
|
||||
((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
|
||||
(((OverColor.lift.obj S.FDiscrete).map ((OverColor.mkIso _).hom ⊗ (OverColor.mkIso _).hom)).hom
|
||||
(((OverColor.lift.obj S.FDiscrete).μ (OverColor.mk fun x => c i) (OverColor.mk fun x => S.τ (c i))).hom
|
||||
(((PiTensorProduct.tprod S.k) fun x_1 => x) ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) fun x => y))) = _
|
||||
(((OverColor.lift.obj S.FDiscrete).μ (OverColor.mk fun _ => c i)
|
||||
(OverColor.mk fun _ => S.τ (c i))).hom
|
||||
(((PiTensorProduct.tprod S.k) fun _ => x) ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) fun _ => y))) = _
|
||||
rw [OverColor.lift.obj_μ_tprod_tmul S.FDiscrete]
|
||||
change ((OverColor.lift.obj S.FDiscrete).map (OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
|
||||
change ((OverColor.lift.obj S.FDiscrete).map
|
||||
(OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
|
||||
(((OverColor.lift.obj S.FDiscrete).map ((OverColor.mkIso _).hom ⊗ (OverColor.mkIso _).hom)).hom
|
||||
((PiTensorProduct.tprod S.k) _)) = _
|
||||
((PiTensorProduct.tprod S.k) _)) = _
|
||||
rw [OverColor.lift.map_tprod S.FDiscrete]
|
||||
change ((OverColor.lift.obj S.FDiscrete).map (OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
|
||||
change ((OverColor.lift.obj S.FDiscrete).map
|
||||
(OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
|
||||
((PiTensorProduct.tprod S.k _)) = _
|
||||
rw [OverColor.lift.map_tprod S.FDiscrete]
|
||||
apply congrArg
|
||||
|
|
@ -168,14 +173,15 @@ lemma contrFin1Fin1_inv_tmul {n : ℕ} (c : Fin n.succ.succ → S.C)
|
|||
|
||||
lemma contrFin1Fin1_hom_hom_tprod {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))
|
||||
(x : (k : Fin 1 ⊕ Fin 1) → (S.FDiscrete.obj { as := (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).hom k })) :
|
||||
(x : (k : Fin 1 ⊕ Fin 1) → (S.FDiscrete.obj
|
||||
{ as := (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).hom k })) :
|
||||
(S.contrFin1Fin1 c i j h).hom.hom (PiTensorProduct.tprod S.k x) =
|
||||
x (Sum.inl 0) ⊗ₜ[S.k] ((S.FDiscrete.map (eqToHom (by simp [h]))).hom (x (Sum.inr 0))) := by
|
||||
change ((Action.forget _ _).mapIso (S.contrFin1Fin1 c i j h)).hom _ = _
|
||||
trans ((Action.forget _ _).mapIso (S.contrFin1Fin1 c i j h)).toLinearEquiv (PiTensorProduct.tprod S.k x)
|
||||
trans ((Action.forget _ _).mapIso (S.contrFin1Fin1 c i j h)).toLinearEquiv
|
||||
(PiTensorProduct.tprod S.k x)
|
||||
· congr
|
||||
erw [← LinearEquiv.eq_symm_apply]
|
||||
|
||||
erw [contrFin1Fin1_inv_tmul]
|
||||
congr
|
||||
funext i
|
||||
|
|
@ -236,7 +242,8 @@ lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
|
|||
(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)
|
||||
• (PiTensorProduct.tprod S.k (fun k => x (i.succAbove (j.succAbove k))) : S.F.obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))) := by
|
||||
• (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,
|
||||
tensorIso_hom, Monoidal.tensorUnit_obj, tensorHom_id,
|
||||
|
|
@ -246,47 +253,53 @@ lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
|
|||
Function.comp_apply, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, Functor.comp_obj, Discrete.functor_obj_eq_as]
|
||||
change (λ_ ((lift.obj S.FDiscrete).obj _)).hom.hom
|
||||
(((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FDiscrete).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
|
||||
(((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FDiscrete).map (mkIso ⋯).hom).hom)
|
||||
(((lift.obj S.FDiscrete).μIso (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
|
||||
(OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom
|
||||
(((lift.obj S.FDiscrete).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom
|
||||
(((lift.obj S.FDiscrete).map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom
|
||||
((PiTensorProduct.tprod S.k) x)))))) = _
|
||||
(((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FDiscrete).obj
|
||||
(OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
|
||||
(((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FDiscrete).map (mkIso _).hom).hom)
|
||||
(((lift.obj S.FDiscrete).μIso (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)
|
||||
∘ Sum.inl))
|
||||
(OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom
|
||||
(((lift.obj S.FDiscrete).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom
|
||||
(((lift.obj S.FDiscrete).map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom
|
||||
((PiTensorProduct.tprod S.k) x)))))) = _
|
||||
rw [lift.map_tprod]
|
||||
change (λ_ ((lift.obj S.FDiscrete).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)))).hom.hom
|
||||
(((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FDiscrete).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
|
||||
(((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FDiscrete).map (mkIso ⋯).hom).hom)
|
||||
(((lift.obj S.FDiscrete).μIso (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
|
||||
(OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom
|
||||
(((lift.obj S.FDiscrete).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom
|
||||
((PiTensorProduct.tprod S.k) fun i_1 =>
|
||||
(lift.discreteFunctorMapEqIso S.FDiscrete ⋯)
|
||||
(x ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm i_1))))))) = _
|
||||
(((S.contr.app { as := c i }).hom ▷
|
||||
((lift.obj S.FDiscrete).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
|
||||
(((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FDiscrete).map (mkIso _).hom).hom)
|
||||
(((lift.obj S.FDiscrete).μIso (OverColor.mk
|
||||
((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
|
||||
(OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom
|
||||
(((lift.obj S.FDiscrete).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom
|
||||
((PiTensorProduct.tprod S.k) fun i_1 =>
|
||||
(lift.discreteFunctorMapEqIso S.FDiscrete _)
|
||||
(x ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm i_1))))))) = _
|
||||
rw [lift.map_tprod]
|
||||
change (λ_ ((lift.obj S.FDiscrete).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)))).hom.hom
|
||||
(((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FDiscrete).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
|
||||
(((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FDiscrete).map (mkIso ⋯).hom).hom)
|
||||
(((lift.obj S.FDiscrete).μIso (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
|
||||
(OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom
|
||||
((PiTensorProduct.tprod S.k) fun i_1 =>
|
||||
(lift.discreteFunctorMapEqIso S.FDiscrete ⋯)
|
||||
((lift.discreteFunctorMapEqIso S.FDiscrete ⋯)
|
||||
(x
|
||||
((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm
|
||||
((Hom.toEquiv (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).symm i_1)))))))) = _
|
||||
(((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FDiscrete).obj
|
||||
(OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
|
||||
(((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FDiscrete).map (mkIso _).hom).hom)
|
||||
(((lift.obj S.FDiscrete).μIso
|
||||
(OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
|
||||
(OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom
|
||||
((PiTensorProduct.tprod S.k) fun i_1 =>
|
||||
(lift.discreteFunctorMapEqIso S.FDiscrete _)
|
||||
((lift.discreteFunctorMapEqIso S.FDiscrete _)
|
||||
(x ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm
|
||||
((Hom.toEquiv (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).symm i_1)))))))) = _
|
||||
rw [lift.μIso_inv_tprod]
|
||||
change (λ_ ((lift.obj S.FDiscrete).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)))).hom.hom
|
||||
(((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FDiscrete).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
|
||||
((TensorProduct.map (S.contrFin1Fin1 c i j h).hom.hom ((lift.obj S.FDiscrete).map (mkIso ⋯).hom).hom)
|
||||
(((PiTensorProduct.tprod S.k) fun i_1 =>
|
||||
(lift.discreteFunctorMapEqIso S.FDiscrete ⋯)
|
||||
((lift.discreteFunctorMapEqIso S.FDiscrete ⋯) (x
|
||||
((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm
|
||||
((Hom.toEquiv (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).symm
|
||||
(Sum.inl i_1)))))) ⊗ₜ[S.k]
|
||||
(PiTensorProduct.tprod S.k) fun i_1 =>
|
||||
(lift.discreteFunctorMapEqIso S.FDiscrete ⋯) ((lift.discreteFunctorMapEqIso S.FDiscrete ⋯)
|
||||
(((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FDiscrete).obj
|
||||
(OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
|
||||
((TensorProduct.map (S.contrFin1Fin1 c i j h).hom.hom
|
||||
((lift.obj S.FDiscrete).map (mkIso _).hom).hom)
|
||||
(((PiTensorProduct.tprod S.k) fun i_1 =>
|
||||
(lift.discreteFunctorMapEqIso S.FDiscrete _)
|
||||
((lift.discreteFunctorMapEqIso S.FDiscrete _) (x
|
||||
((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm
|
||||
((Hom.toEquiv (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).symm
|
||||
(Sum.inl i_1)))))) ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) fun i_1 =>
|
||||
(lift.discreteFunctorMapEqIso S.FDiscrete _) ((lift.discreteFunctorMapEqIso S.FDiscrete _)
|
||||
(x ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm
|
||||
((Hom.toEquiv
|
||||
(mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).symm (Sum.inr i_1)))))))) = _
|
||||
|
|
@ -306,7 +319,8 @@ lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
|
|||
· simp only [Fin.isValue, lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl,
|
||||
Iso.refl_hom, Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
|
||||
rfl
|
||||
· simp [lift.discreteFunctorMapEqIso, h]
|
||||
· simp only [Fin.isValue, lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl,
|
||||
Iso.refl_hom, Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
|
||||
change (S.FDiscrete.map (eqToHom _)).hom
|
||||
(x (((HepLean.Fin.finExtractTwo i j)).symm ((Sum.inl (Sum.inr 0))))) = _
|
||||
simp only [Nat.succ_eq_add_one, Fin.isValue]
|
||||
|
|
@ -328,8 +342,8 @@ lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
|
|||
change (S.FDiscrete.map (eqToHom _)).hom
|
||||
((x ((HepLean.Fin.finExtractTwo i j).symm (Sum.inr (d))))) = _
|
||||
simp only [Nat.succ_eq_add_one]
|
||||
have h1 : ((HepLean.Fin.finExtractTwo i j).symm (Sum.inr d)) = (i.succAbove (j.succAbove d)) := by
|
||||
exact HepLean.Fin.finExtractTwo_symm_inr_apply i j d
|
||||
have h1 : ((HepLean.Fin.finExtractTwo i j).symm (Sum.inr d))
|
||||
= (i.succAbove (j.succAbove d)) := HepLean.Fin.finExtractTwo_symm_inr_apply i j d
|
||||
have h1' {a b : Fin n.succ.succ} (h : a = b) :
|
||||
(S.FDiscrete.map (eqToHom (by rw [h]))).hom (x a) = x b := by
|
||||
subst h
|
||||
|
|
@ -453,10 +467,12 @@ lemma tensoreNode_tensor {c : Fin n → S.C} (T : S.F.obj (OverColor.mk c)) :
|
|||
@[simp]
|
||||
lemma constTwoNode_tensor {c1 c2 : S.C}
|
||||
(v : 𝟙_ (Rep S.k S.G) ⟶ S.FDiscrete.obj (Discrete.mk c1) ⊗ S.FDiscrete.obj (Discrete.mk c2)) :
|
||||
(constTwoNode v).tensor = (OverColor.Discrete.pairIsoSep S.FDiscrete).hom.hom (v.hom (1 : S.k)) :=
|
||||
(constTwoNode v).tensor =
|
||||
(OverColor.Discrete.pairIsoSep S.FDiscrete).hom.hom (v.hom (1 : S.k)) :=
|
||||
rfl
|
||||
|
||||
lemma prod_tensor {c1 : Fin n → S.C} {c2 : Fin m → S.C} (t1 : TensorTree S c1) (t2 : TensorTree S c2) :
|
||||
lemma prod_tensor {c1 : Fin n → S.C} {c2 : Fin m → S.C} (t1 : TensorTree S c1)
|
||||
(t2 : TensorTree S c2) :
|
||||
(prod t1 t2).tensor = (S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom
|
||||
((S.F.μ _ _).hom (t1.tensor ⊗ₜ t2.tensor)) := rfl
|
||||
|
||||
|
|
@ -465,8 +481,9 @@ lemma add_tensor (t1 t2 : TensorTree S c) : (add t1 t2).tensor = t1.tensor + t2.
|
|||
lemma perm_tensor (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (t : TensorTree S c) :
|
||||
(perm σ t).tensor = (S.F.map σ).hom t.tensor := rfl
|
||||
|
||||
lemma contr_tensor {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)}
|
||||
(t : TensorTree S c) : (contr i j h t).tensor = (S.contrMap c i j h).hom t.tensor := rfl
|
||||
lemma contr_tensor {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)} (t : TensorTree S c) :
|
||||
(contr i j h t).tensor = (S.contrMap c i j h).hom t.tensor := rfl
|
||||
|
||||
lemma neg_tensor (t : TensorTree S c) : (neg t).tensor = - t.tensor := rfl
|
||||
|
||||
|
|
|
|||
|
|
@ -406,7 +406,8 @@ def getPermutation (l1 l2 : List (TSyntax `indexExpr)) : TermElabM (List (ℕ))
|
|||
let l1' ← l1.mapM (fun x => indexToIdent x)
|
||||
let l2' ← l2.mapM (fun x => indexToIdent x)
|
||||
let l1enum := l1'.enum
|
||||
let l2'' := l2'.filterMap (fun x => l1enum.find? (fun y => Lean.TSyntax.getId y.2 = Lean.TSyntax.getId x))
|
||||
let l2'' := l2'.filterMap
|
||||
(fun x => l1enum.find? (fun y => Lean.TSyntax.getId y.2 = Lean.TSyntax.getId x))
|
||||
return l2''.map fun x => x.1
|
||||
|
||||
def finMapToEquiv (f1 f2 : Fin n → Fin n) (h : ∀ x, f1 (f2 x) = x := by decide)
|
||||
|
|
|
|||
|
|
@ -69,7 +69,8 @@ lemma neg_snd_prod {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S
|
|||
Action.FunctorCategoryEquivalence.functor_obj_obj, neg_tensor, tmul_neg, map_neg]
|
||||
|
||||
@[simp]
|
||||
lemma neg_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)}
|
||||
lemma neg_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)}
|
||||
(t : TensorTree S c) : (contr i j h (neg t)).tensor = (neg (contr i j h t)).tensor := by
|
||||
simp only [Nat.succ_eq_add_one, contr_tensor, neg_tensor, map_neg]
|
||||
|
||||
|
|
|
|||
|
|
@ -68,7 +68,8 @@ lemma swapI_neq_succAbove : ¬ q.swapI = q.i.succAbove q.j := by
|
|||
exact Fin.succAbove_ne q.j q.k
|
||||
|
||||
@[simp]
|
||||
lemma swapI_neq_i_j_k_l_succAbove : ¬ q.swapI = q.i.succAbove (q.j.succAbove (q.k.succAbove q.l)) := by
|
||||
lemma swapI_neq_i_j_k_l_succAbove :
|
||||
¬ q.swapI = q.i.succAbove (q.j.succAbove (q.k.succAbove q.l)) := by
|
||||
simp only [Nat.succ_eq_add_one, swapI]
|
||||
apply Function.Injective.ne Fin.succAbove_right_injective
|
||||
apply Function.Injective.ne Fin.succAbove_right_injective
|
||||
|
|
@ -100,8 +101,8 @@ lemma swapK_swapJ_swapI_succAbove : (q.swapI).succAbove (predAboveI q.swapI q.i)
|
|||
simp
|
||||
|
||||
@[simp]
|
||||
lemma swapL_swapK_swapJ_swapI_succAbove : q.swapI.succAbove (q.swapJ.succAbove (q.swapK.succAbove q.swapL)) =
|
||||
q.i.succAbove q.j := by
|
||||
lemma swapL_swapK_swapJ_swapI_succAbove :
|
||||
q.swapI.succAbove (q.swapJ.succAbove (q.swapK.succAbove q.swapL)) = q.i.succAbove q.j := by
|
||||
rw [swapJ, swapK]
|
||||
rw [← succAbove_succAbove_predAboveI]
|
||||
rw [swapI]
|
||||
|
|
@ -129,14 +130,16 @@ def contrMapFst := S.contrMap c q.i q.j q.hij
|
|||
|
||||
def contrMapSnd := S.contrMap (c ∘ q.i.succAbove ∘ q.j.succAbove) q.k q.l q.hkl
|
||||
|
||||
def contrSwapHom : (OverColor.mk ((c ∘ q.swap.i.succAbove ∘ q.swap.j.succAbove) ∘ q.swap.k.succAbove ∘ q.swap.l.succAbove)) ⟶
|
||||
(OverColor.mk fun x => c (q.i.succAbove (q.j.succAbove (q.k.succAbove (q.l.succAbove x))))) :=
|
||||
def contrSwapHom : (OverColor.mk ((c ∘ q.swap.i.succAbove ∘ q.swap.j.succAbove) ∘
|
||||
q.swap.k.succAbove ∘ q.swap.l.succAbove)) ⟶
|
||||
(OverColor.mk fun x => c (q.i.succAbove (q.j.succAbove (q.k.succAbove (q.l.succAbove x))))) :=
|
||||
(mkIso (funext fun x => congrArg c (swap_map_eq q x))).hom
|
||||
|
||||
lemma contrSwapHom_contrMapSnd_tprod (x : (i : (𝟭 Type).obj (OverColor.mk c).left) → CoeSort.coe (S.FDiscrete.obj { as := (OverColor.mk c).hom i })) :
|
||||
lemma contrSwapHom_contrMapSnd_tprod (x : (i : (𝟭 Type).obj (OverColor.mk c).left) →
|
||||
CoeSort.coe (S.FDiscrete.obj { as := (OverColor.mk c).hom i })) :
|
||||
((lift.obj S.FDiscrete).map q.contrSwapHom).hom
|
||||
(q.swap.contrMapSnd.hom ((PiTensorProduct.tprod S.k) fun k => x (q.swap.i.succAbove (q.swap.j.succAbove k))))
|
||||
= ((S.castToField
|
||||
(q.swap.contrMapSnd.hom ((PiTensorProduct.tprod S.k) fun k =>
|
||||
x (q.swap.i.succAbove (q.swap.j.succAbove k)))) = ((S.castToField
|
||||
((S.contr.app { as := (c ∘ q.swap.i.succAbove ∘ q.swap.j.succAbove) q.swap.k }).hom
|
||||
(x (q.swap.i.succAbove (q.swap.j.succAbove q.swap.k)) ⊗ₜ[S.k]
|
||||
(S.FDiscrete.map (Discrete.eqToHom q.swap.hkl)).hom
|
||||
|
|
@ -153,8 +156,10 @@ lemma contrSwapHom_contrMapSnd_tprod (x : (i : (𝟭 Type).obj (OverColor.mk c).
|
|||
rw [map_smul]
|
||||
rfl
|
||||
|
||||
lemma contrSwapHom_tprod (x : (i : (𝟭 Type).obj (OverColor.mk c).left) → CoeSort.coe (S.FDiscrete.obj { as := (OverColor.mk c).hom i })) :
|
||||
((PiTensorProduct.tprod S.k) fun k => x (q.i.succAbove (q.j.succAbove (q.k.succAbove (q.l.succAbove k))))) =
|
||||
lemma contrSwapHom_tprod (x : (i : (𝟭 Type).obj (OverColor.mk c).left) →
|
||||
CoeSort.coe (S.FDiscrete.obj { as := (OverColor.mk c).hom i })) :
|
||||
((PiTensorProduct.tprod S.k)
|
||||
fun k => x (q.i.succAbove (q.j.succAbove (q.k.succAbove (q.l.succAbove k))))) =
|
||||
((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))))) := by
|
||||
|
|
@ -185,7 +190,8 @@ lemma contrMapFst_contrMapSnd_swap :
|
|||
rw [contrMapFst, contrMapFst]
|
||||
change q.contrMapSnd.hom ((S.contrMap c q.i q.j _).hom ((PiTensorProduct.tprod S.k) x)) =
|
||||
(S.F.map q.contrSwapHom).hom
|
||||
(q.swap.contrMapSnd.hom ((S.contrMap c q.swap.i q.swap.j _).hom ((PiTensorProduct.tprod S.k) x)))
|
||||
(q.swap.contrMapSnd.hom ((S.contrMap c q.swap.i q.swap.j _).hom
|
||||
((PiTensorProduct.tprod S.k) x)))
|
||||
rw [TensorStruct.contrMap_tprod, TensorStruct.contrMap_tprod]
|
||||
simp only [Nat.succ_eq_add_one, Monoidal.tensorUnit_obj, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
|
|
@ -196,7 +202,8 @@ lemma contrMapFst_contrMapSnd_swap :
|
|||
S.castToField
|
||||
_ •
|
||||
((lift.obj S.FDiscrete).map q.contrSwapHom).hom
|
||||
(q.swap.contrMapSnd.hom ((PiTensorProduct.tprod S.k) fun k => x (q.swap.i.succAbove (q.swap.j.succAbove k))))
|
||||
(q.swap.contrMapSnd.hom ((PiTensorProduct.tprod S.k)
|
||||
fun k => x (q.swap.i.succAbove (q.swap.j.succAbove k))))
|
||||
rw [contrMapSnd, TensorStruct.contrMap_tprod, q.contrSwapHom_contrMapSnd_tprod]
|
||||
rw [smul_smul, smul_smul]
|
||||
congr 1
|
||||
|
|
@ -204,7 +211,8 @@ lemma contrMapFst_contrMapSnd_swap :
|
|||
· nth_rewrite 1 [mul_comm]
|
||||
congr 1
|
||||
· congr 3
|
||||
have h1' {a b d: Fin n.succ.succ.succ.succ} (hbd : b =d) (h : c d = S.τ (c a)) (h' : c b = S.τ (c a)) :
|
||||
have h1' {a b d: Fin n.succ.succ.succ.succ} (hbd : b =d) (h : c d = S.τ (c a))
|
||||
(h' : c b = S.τ (c a)) :
|
||||
(S.FDiscrete.map (Discrete.eqToHom (h))).hom (x d) =
|
||||
(S.FDiscrete.map (Discrete.eqToHom h')).hom (x b) := by
|
||||
subst hbd
|
||||
|
|
@ -234,8 +242,8 @@ lemma contrMapFst_contrMapSnd_swap :
|
|||
· exact q.contrSwapHom_tprod _
|
||||
|
||||
lemma contr_contr (t : TensorTree S c) :
|
||||
(contr q.k q.l q.hkl (contr q.i q.j q.hij t)).tensor =
|
||||
(perm q.contrSwapHom (contr q.swapK q.swapL q.swap.hkl (contr q.swapI q.swapJ q.swap.hij t))).tensor := by
|
||||
(contr q.k q.l q.hkl (contr q.i q.j q.hij t)).tensor = (perm q.contrSwapHom
|
||||
(contr q.swapK q.swapL q.swap.hkl (contr q.swapI q.swapJ q.swap.hij t))).tensor := by
|
||||
simp only [contr_tensor, perm_tensor]
|
||||
trans (q.contrMapFst ≫ q.contrMapSnd).hom t.tensor
|
||||
simp only [Nat.succ_eq_add_one, contrMapFst, contrMapSnd, Action.comp_hom, ModuleCat.coe_comp,
|
||||
|
|
@ -261,7 +269,8 @@ theorem contr_contr {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} {i : Fin n
|
|||
(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).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
|
||||
|
|
|
|||
|
|
@ -30,15 +30,14 @@ lemma contrFin1Fin1_naturality {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
|
|||
= (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
|
||||
≫ ((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
|
||||
:= by
|
||||
≫ ((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 := 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
|
||||
((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
|
||||
erw [← CategoryTheory.Iso.eq_comp_inv]
|
||||
rw [CategoryTheory.Category.assoc]
|
||||
erw [← CategoryTheory.Iso.inv_comp_eq]
|
||||
|
|
@ -85,7 +84,8 @@ lemma contrFin1Fin1_naturality {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
|
|||
extractOne_homToEquiv, lift.discreteFunctorMapEqIso, Functor.mapIso_hom, eqToIso.hom,
|
||||
Functor.mapIso_inv, eqToIso.inv, Functor.id_obj, Discrete.functor_obj_eq_as,
|
||||
LinearEquiv.ofLinear_apply]
|
||||
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]
|
||||
|
|
@ -97,12 +97,14 @@ lemma contrIso_comm_aux_1 {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
|
|||
((S.F.map σ).hom ≫ (S.F.map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom) ≫
|
||||
(S.F.map (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom =
|
||||
(S.F.map (equivToIso (HepLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i)
|
||||
((HepLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j))).hom).hom ≫ (S.F.map
|
||||
(mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i)
|
||||
((HepLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)).symm)).hom).hom
|
||||
((HepLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j))).hom).hom ≫
|
||||
(S.F.map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo ((Hom.toEquiv σ).symm i)
|
||||
((HepLean.Fin.finExtractOnePerm
|
||||
((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)).symm)).hom).hom
|
||||
≫ (S.F.map (extractTwoAux' i j σ ⊗ extractTwoAux i j σ)).hom := by
|
||||
ext X
|
||||
change ((S.F.map σ) ≫ (S.F.map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom) ≫ (S.F.map (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom)).hom X = _
|
||||
change ((S.F.map σ) ≫ (S.F.map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom) ≫
|
||||
(S.F.map (mkSum (c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom)).hom X = _
|
||||
rw [← Functor.map_comp, ← Functor.map_comp]
|
||||
erw [extractTwo_finExtractTwo]
|
||||
simp only [Nat.succ_eq_add_one, extractOne_homToEquiv, Functor.map_comp, Action.comp_hom,
|
||||
|
|
@ -140,8 +142,9 @@ lemma contrIso_comm_aux_3 {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
|
|||
(S.F.map (extractTwo i j σ)).hom := by
|
||||
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
|
||||
(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
|
||||
rw [← Functor.map_comp, ← Functor.map_comp]
|
||||
apply congrArg
|
||||
rfl
|
||||
|
|
@ -159,8 +162,9 @@ lemma contrIso_comm_aux_5 {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
|
|||
(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)
|
||||
((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)
|
||||
(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)
|
||||
≫ (S.contrIsoComm σ).hom := by
|
||||
erw [← CategoryTheory.MonoidalCategory.tensor_comp (f₁ := (S.F.map (extractTwoAux' i j σ)).hom)]
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue