refactor: Simp to simp only ...
This commit is contained in:
jstoobysmith
parent
b2ac704d80
commit
855dc5146d
12 changed files with 257 additions and 192 deletions
|
|
@ -73,7 +73,7 @@ lemma coMetric_prod_antiSymm (A : (Lorentz.complexContr ⊗ Lorentz.complexContr
|
|||
(hA : (twoNodeE complexLorentzTensor Color.up Color.up A).tensor =
|
||||
(TensorTree.neg (perm
|
||||
(OverColor.equivToHomEq (Equality.finMapToEquiv ![1, 0] ![1, 0]) (by decide))
|
||||
(twoNodeE complexLorentzTensor Color.up Color.up A))).tensor)
|
||||
(twoNodeE complexLorentzTensor Color.up Color.up A))).tensor)
|
||||
(hs : {S | μ ν = S | ν μ}ᵀ) : {A | μ ν ⊗ S | μ ν}ᵀ.tensor = 0 := by
|
||||
have h1 : {A | μ ν ⊗ S | μ ν}ᵀ.tensor = - {A | μ ν ⊗ S | μ ν}ᵀ.tensor := by
|
||||
nth_rewrite 1 [contr_tensor_eq (contr_tensor_eq (prod_tensor_eq_fst hA))]
|
||||
|
|
|
|||
|
|
@ -42,7 +42,7 @@ namespace Hom
|
|||
|
||||
variable {C : Type} {f g h : OverColor C}
|
||||
|
||||
lemma ext (m n : f ⟶ g) (h : m.hom = n.hom) : m = n := by
|
||||
lemma ext (m n : f ⟶ g) (h : m.hom = n.hom) : m = n := by
|
||||
apply CategoryTheory.Iso.ext h
|
||||
|
||||
/-- Given a hom in `OverColor C` the underlying equivalence between types. -/
|
||||
|
|
|
|||
|
|
@ -70,7 +70,7 @@ def pairIsoSep {c1 c2 : C} : F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2)
|
|||
|
||||
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
|
||||
PiTensorProduct.tprod k (Fin.cases x (Fin.cases y (fun i => Fin.elim0 i))) := by
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Action.instMonoidalCategory_tensorObj_V,
|
||||
pairIsoSep, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
|
||||
forgetLiftApp, Iso.trans_symm, Iso.symm_symm_eq, Iso.trans_assoc, Iso.trans_hom, Iso.symm_hom,
|
||||
|
|
@ -88,7 +88,7 @@ lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discr
|
|||
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
|
||||
((PiTensorProduct.tprod k) _)) = _
|
||||
((PiTensorProduct.tprod k) _)) = _
|
||||
rw [lift.map_tprod]
|
||||
change ((lift.obj F).map fin2Iso.inv).hom ((PiTensorProduct.tprod k) fun i => _) = _
|
||||
rw [lift.map_tprod]
|
||||
|
|
@ -96,10 +96,18 @@ lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discr
|
|||
funext i
|
||||
match i with
|
||||
| (0 : Fin 2) =>
|
||||
simp [fin2Iso, HepLean.PiTensorProduct.elimPureTensor, mkIso, mkSum]
|
||||
simp only [mk_hom, Fin.isValue, Matrix.cons_val_zero, Nat.succ_eq_add_one, Nat.reduceAdd,
|
||||
Matrix.cons_val_one, Matrix.head_cons, instMonoidalCategoryStruct_tensorObj_left, fin2Iso,
|
||||
Equiv.symm_symm, mkSum, mkIso, Iso.trans_inv, tensorIso_inv,
|
||||
instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj,
|
||||
HepLean.PiTensorProduct.elimPureTensor, Fin.cases_zero]
|
||||
exact (LinearEquiv.eq_symm_apply _).mp rfl
|
||||
| (1 : Fin 2) =>
|
||||
simp [fin2Iso, HepLean.PiTensorProduct.elimPureTensor, mkIso, mkSum]
|
||||
simp only [mk_hom, Fin.isValue, Matrix.cons_val_one, Matrix.head_cons, Nat.succ_eq_add_one,
|
||||
Nat.reduceAdd, Matrix.cons_val_zero, instMonoidalCategoryStruct_tensorObj_left, fin2Iso,
|
||||
Equiv.symm_symm, mkSum, mkIso, Iso.trans_inv, tensorIso_inv,
|
||||
instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj,
|
||||
HepLean.PiTensorProduct.elimPureTensor]
|
||||
exact (LinearEquiv.eq_symm_apply _).mp rfl
|
||||
|
||||
/-- The functor taking `c` to `F c ⊗ F (τ c)`. -/
|
||||
|
|
@ -108,7 +116,7 @@ def pairτ (τ : C → C) : Discrete C ⥤ Rep k G :=
|
|||
|
||||
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):
|
||||
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
|
||||
|
|
|
|||
|
|
@ -74,19 +74,20 @@ def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] := by
|
|||
|
||||
def extractOne {n : ℕ} (i : Fin n.succ.succ)
|
||||
{c1 c2 : Fin n.succ.succ → C} (σ : mk c1 ⟶ mk c2) :
|
||||
mk (c1 ∘ Fin.succAbove ((Hom.toEquiv σ).symm i)) ⟶ mk (c2 ∘ Fin.succAbove i) :=
|
||||
mk (c1 ∘ Fin.succAbove ((Hom.toEquiv σ).symm i)) ⟶ mk (c2 ∘ Fin.succAbove i) :=
|
||||
equivToHomEq ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ))) (by
|
||||
intro x
|
||||
simp_all only [Nat.succ_eq_add_one, Function.comp_apply]
|
||||
have h1 := Hom.toEquiv_comp_inv_apply σ (i.succAbove x)
|
||||
simp at h1
|
||||
simp only [Nat.succ_eq_add_one, Functor.const_obj_obj, mk_hom] at h1
|
||||
rw [← h1]
|
||||
apply congrArg
|
||||
simp [finExtractOnePerm, finExtractOnPermHom]
|
||||
simp only [finExtractOnePerm, Nat.succ_eq_add_one, finExtractOnPermHom,
|
||||
finExtractOne_symm_inr_apply, Equiv.symm_apply_apply, Equiv.coe_fn_symm_mk]
|
||||
erw [Equiv.apply_symm_apply]
|
||||
rw [succsAbove_predAboveI]
|
||||
· rfl
|
||||
simp
|
||||
simp only [Nat.succ_eq_add_one, ne_eq]
|
||||
erw [Equiv.apply_eq_iff_eq]
|
||||
exact (Fin.succAbove_ne i x).symm)
|
||||
|
||||
|
|
@ -98,11 +99,11 @@ lemma extractOne_homToEquiv {n : ℕ} (i : Fin n.succ.succ)
|
|||
|
||||
def extractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
|
||||
{c1 c2 : Fin n.succ.succ → C} (σ : mk c1 ⟶ mk c2) :
|
||||
mk (c1 ∘ Fin.succAbove ((Hom.toEquiv σ).symm i) ∘
|
||||
mk (c1 ∘ Fin.succAbove ((Hom.toEquiv σ).symm i) ∘
|
||||
Fin.succAbove (((Hom.toEquiv (extractOne i σ))).symm j)) ⟶
|
||||
mk (c2 ∘ Fin.succAbove i ∘ Fin.succAbove j) :=
|
||||
match n with
|
||||
| 0 => equivToHomEq (Equiv.refl _) (by simp)
|
||||
| 0 => equivToHomEq (Equiv.refl _) (by simp)
|
||||
| Nat.succ n =>
|
||||
equivToHomEq (Equiv.refl _) (by simp) ≫ extractOne j (extractOne i σ) ≫
|
||||
equivToHomEq (Equiv.refl _) (by simp)
|
||||
|
|
@ -119,27 +120,29 @@ def extractTwoAux' {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
|
|||
mk ((c1 ∘ ⇑(finExtractTwo i j).symm) ∘ Sum.inl) :=
|
||||
equivToHomEq (Equiv.refl _) (by
|
||||
intro x
|
||||
simp
|
||||
simp only [Nat.succ_eq_add_one, Function.comp_apply, extractOne_homToEquiv, Equiv.refl_symm,
|
||||
Equiv.coe_refl, id_eq]
|
||||
match x with
|
||||
| Sum.inl 0=>
|
||||
simp
|
||||
simp only [Fin.isValue, finExtractTwo_symm_inl_inl_apply]
|
||||
have h1 := Hom.toEquiv_comp_inv_apply σ i
|
||||
simpa using h1.symm
|
||||
| Sum.inr 0 =>
|
||||
simp
|
||||
simp only [Fin.isValue, finExtractTwo_symm_inl_inr_apply]
|
||||
have h1 := Hom.toEquiv_comp_inv_apply σ (i.succAbove j)
|
||||
simp at h1
|
||||
simp only [Nat.succ_eq_add_one, Functor.const_obj_obj, mk_hom] at h1
|
||||
rw [← h1]
|
||||
congr
|
||||
simp [finExtractOnePerm, finExtractOnPermHom]
|
||||
simp only [Nat.succ_eq_add_one, finExtractOnePerm, finExtractOnPermHom,
|
||||
finExtractOne_symm_inr_apply, Equiv.symm_apply_apply, Equiv.coe_fn_symm_mk]
|
||||
erw [Equiv.apply_symm_apply]
|
||||
rw [succsAbove_predAboveI]
|
||||
rfl
|
||||
simp
|
||||
simp only [Nat.succ_eq_add_one, ne_eq]
|
||||
erw [Equiv.apply_eq_iff_eq]
|
||||
exact (Fin.succAbove_ne i j).symm)
|
||||
|
||||
lemma extractTwo_finExtractTwo_succ {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fin n.succ.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
|
||||
|
|
@ -147,76 +150,82 @@ lemma extractTwo_finExtractTwo_succ {n : ℕ} (i : Fin n.succ.succ.succ) (j : F
|
|||
≫ ((extractTwoAux' i j σ) ⊗ (extractTwoAux i j σ)) := by
|
||||
apply IndexNotation.OverColor.Hom.ext
|
||||
ext x
|
||||
simp [CategoryStruct.comp,extractTwoAux', extractTwoAux, mkSum,equivToIso, Hom.toIso]
|
||||
simp only [Nat.succ_eq_add_one, instMonoidalCategoryStruct_tensorObj_left, CategoryStruct.comp,
|
||||
equivToIso, Hom.toIso, mkSum, Iso.trans_hom, Over.isoMk_hom_left, Equiv.toIso_hom,
|
||||
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 σ))))
|
||||
(((finExtractTwo ((Hom.toEquiv σ).symm i)
|
||||
((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)) x))
|
||||
simp [extractTwo]
|
||||
simp only [Nat.succ_eq_add_one]
|
||||
obtain ⟨k, hk⟩ := (finExtractTwo ((Hom.toEquiv σ).symm i)
|
||||
((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)).symm.surjective x
|
||||
subst hk
|
||||
simp
|
||||
simp only [Nat.succ_eq_add_one, Equiv.apply_symm_apply]
|
||||
match k with
|
||||
| Sum.inl (Sum.inl 0) =>
|
||||
simp
|
||||
| Sum.inl (Sum.inr 0) =>
|
||||
simp
|
||||
have h1 : ((Hom.toEquiv σ) (Fin.succAbove
|
||||
simp only [Fin.isValue, finExtractTwo_symm_inl_inr_apply, Sum.map_inl, id_eq]
|
||||
have h1 : ((Hom.toEquiv σ) (Fin.succAbove
|
||||
((Hom.toEquiv σ).symm i)
|
||||
((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j))) =
|
||||
i.succAbove j := by
|
||||
simp [finExtractOnePerm, finExtractOnPermHom]
|
||||
simp only [Nat.succ_eq_add_one, finExtractOnePerm, finExtractOnPermHom,
|
||||
finExtractOne_symm_inr_apply, Equiv.symm_apply_apply, Equiv.coe_fn_symm_mk]
|
||||
erw [Equiv.apply_symm_apply]
|
||||
rw [succsAbove_predAboveI]
|
||||
exact Equiv.apply_symm_apply (Hom.toEquiv σ) (i.succAbove j)
|
||||
simp
|
||||
simp only [Nat.succ_eq_add_one, ne_eq]
|
||||
erw [Equiv.apply_eq_iff_eq]
|
||||
exact (Fin.succAbove_ne i j).symm
|
||||
rw [h1]
|
||||
erw [Equiv.apply_eq_iff_eq_symm_apply ]
|
||||
erw [Equiv.apply_eq_iff_eq_symm_apply]
|
||||
simp
|
||||
| Sum.inr x =>
|
||||
simp
|
||||
erw [Equiv.apply_eq_iff_eq_symm_apply ]
|
||||
simp
|
||||
simp [finExtractOnePerm, finExtractOnPermHom]
|
||||
simp only [finExtractTwo_symm_inr_apply, Sum.map_inr]
|
||||
erw [Equiv.apply_eq_iff_eq_symm_apply]
|
||||
simp only [finExtractTwo_symm_inr_apply]
|
||||
simp only [finExtractOnePerm, Nat.succ_eq_add_one, finExtractOnPermHom,
|
||||
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
|
||||
(predAboveI ((Hom.toEquiv σ).symm i) ((Hom.toEquiv σ).symm (i.succAbove j)))))) = j := by
|
||||
rw [succsAbove_predAboveI]
|
||||
· erw [Equiv.apply_symm_apply]
|
||||
simp
|
||||
· 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)
|
||||
let y := (Hom.toEquiv σ) (Fin.succAbove ((Hom.toEquiv σ).symm i)
|
||||
((predAboveI ((Hom.toEquiv σ).symm i) ((Hom.toEquiv σ).symm (i.succAbove j))).succAbove x))
|
||||
change y = i.succAbove (j.succAbove (predAboveI j (predAboveI i y)))
|
||||
change y = i.succAbove (j.succAbove (predAboveI j (predAboveI i y)))
|
||||
have hy : i ≠ y := by
|
||||
simp [y]
|
||||
erw [← Equiv.symm_apply_eq ]
|
||||
simp only [Nat.succ_eq_add_one, ne_eq, y]
|
||||
erw [← Equiv.symm_apply_eq]
|
||||
exact (Fin.succAbove_ne _ _).symm
|
||||
rw [succsAbove_predAboveI, succsAbove_predAboveI]
|
||||
exact hy
|
||||
simp
|
||||
simp only [Nat.succ_eq_add_one, ne_eq]
|
||||
rw [predAboveI_eq_iff]
|
||||
simp [y]
|
||||
erw [← Equiv.symm_apply_eq ]
|
||||
simp only [Nat.succ_eq_add_one, y]
|
||||
erw [← Equiv.symm_apply_eq]
|
||||
have h0 : (Hom.toEquiv σ).symm (i.succAbove j) =
|
||||
Fin.succAbove ((Hom.toEquiv σ).symm i)
|
||||
(predAboveI ((Hom.toEquiv σ).symm i) ((Hom.toEquiv σ).symm (i.succAbove j))) := by
|
||||
rw [succsAbove_predAboveI]
|
||||
simp
|
||||
simp only [Nat.succ_eq_add_one, ne_eq]
|
||||
erw [Equiv.apply_eq_iff_eq]
|
||||
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'
|
||||
exact Fin.succAbove_ne
|
||||
(predAboveI ((Hom.toEquiv σ).symm i) ((Hom.toEquiv σ).symm (i.succAbove j))) x hn'
|
||||
(predAboveI ((Hom.toEquiv σ).symm i) ((Hom.toEquiv σ).symm (i.succAbove j))) x hn'
|
||||
exact hy
|
||||
|
||||
lemma extractTwo_finExtractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
|
||||
|
|
@ -229,14 +238,18 @@ lemma extractTwo_finExtractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
|
|||
| 0 =>
|
||||
apply IndexNotation.OverColor.Hom.ext
|
||||
ext x
|
||||
simp [CategoryStruct.comp,extractTwoAux', extractTwoAux, mkSum,equivToIso, Hom.toIso]
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, instMonoidalCategoryStruct_tensorObj_left,
|
||||
CategoryStruct.comp, equivToIso, Hom.toIso, mkSum, Iso.trans_hom, Over.isoMk_hom_left,
|
||||
Equiv.toIso_hom, 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.left x)) = Sum.map (Equiv.refl _) (Equiv.refl _) _
|
||||
simp
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Equiv.coe_refl, Sum.map_id_id, id_eq]
|
||||
change (finExtractTwo i j) ((Hom.toEquiv σ) x) = ((finExtractTwo ((Hom.toEquiv σ).symm i)
|
||||
((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)) x)
|
||||
obtain ⟨k, hk⟩ := (Hom.toEquiv σ).symm.surjective x
|
||||
subst hk
|
||||
simp
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Equiv.apply_symm_apply]
|
||||
have hk : k = i ∨ k = i.succAbove j := by
|
||||
match i, j, k with
|
||||
| (0 : Fin 2), (0 : Fin 1), (0 : Fin 2) => exact Or.intro_left (0 = Fin.succAbove 0 0) rfl
|
||||
|
|
@ -245,15 +258,17 @@ lemma extractTwo_finExtractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
|
|||
| (1 : Fin 2), (0 : Fin 1), (1 : Fin 2) => exact Or.intro_left (1 = Fin.succAbove 1 0) rfl
|
||||
rcases hk with hk | hk
|
||||
subst hk
|
||||
simp
|
||||
simp only [finExtractTwo_apply_fst, Fin.isValue]
|
||||
subst hk
|
||||
simp
|
||||
simp only [finExtractTwo_apply_snd, Fin.isValue]
|
||||
rw [← Equiv.symm_apply_eq]
|
||||
simp [finExtractOnePerm, finExtractOnPermHom]
|
||||
simp only [finExtractOnePerm, Nat.succ_eq_add_one, Nat.reduceAdd, finExtractOnPermHom,
|
||||
finExtractOne_symm_inr_apply, Equiv.symm_apply_apply, Equiv.coe_fn_symm_mk, Fin.isValue,
|
||||
finExtractTwo_symm_inl_inr_apply]
|
||||
erw [Equiv.apply_symm_apply]
|
||||
rw [succsAbove_predAboveI]
|
||||
rfl
|
||||
simp
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, ne_eq]
|
||||
erw [Equiv.apply_eq_iff_eq]
|
||||
exact (Fin.succAbove_ne i j).symm
|
||||
| Nat.succ n => exact extractTwo_finExtractTwo_succ i j σ
|
||||
|
|
|
|||
|
|
@ -648,15 +648,15 @@ 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
|
||||
(OverColor.Hom.toEquiv_comp_inv_apply f i) (p ((OverColor.Hom.toEquiv f).symm i)) := by
|
||||
simp [lift, obj']
|
||||
simp only [lift, obj', objObj'_V_carrier, Functor.id_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]
|
||||
|
|
@ -709,7 +709,7 @@ def forgetLiftAppV (c : C) : ((lift.obj F).obj (OverColor.mk (fun (_ : Fin 1) =>
|
|||
@[simp]
|
||||
lemma forgetLiftAppV_symm_apply (c : C) (x : (F.obj (Discrete.mk c)).V) :
|
||||
(forgetLiftAppV F c).symm x = PiTensorProduct.tprod k (fun _ => x) := by
|
||||
simp [forgetLiftAppV]
|
||||
simp only [forgetLiftAppV, Fin.isValue, Functor.id_obj]
|
||||
erw [PiTensorProduct.subsingletonEquiv_symm_apply]
|
||||
|
||||
/-- The `forgetLiftAppV` function takes an object `c` of type `C` and returns a isomorphism
|
||||
|
|
|
|||
|
|
@ -70,21 +70,22 @@ lemma perm_contr_cond {n : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n.succ.s
|
|||
c (Fin.succAbove ((Hom.toEquiv σ).symm i) ((Hom.toEquiv (extractOne i σ)).symm j)) =
|
||||
S.τ (c ((Hom.toEquiv σ).symm i)) := by
|
||||
have h1 := Hom.toEquiv_comp_apply σ
|
||||
simp at h1
|
||||
simp only [Nat.succ_eq_add_one, Functor.const_obj_obj, mk_hom] at h1
|
||||
rw [h1, h1]
|
||||
simp
|
||||
simp only [Nat.succ_eq_add_one, extractOne_homToEquiv, Equiv.apply_symm_apply]
|
||||
rw [← h]
|
||||
congr
|
||||
simp [HepLean.Fin.finExtractOnePerm, HepLean.Fin.finExtractOnPermHom]
|
||||
simp only [Nat.succ_eq_add_one, HepLean.Fin.finExtractOnePerm, HepLean.Fin.finExtractOnPermHom,
|
||||
HepLean.Fin.finExtractOne_symm_inr_apply, Equiv.symm_apply_apply, Equiv.coe_fn_symm_mk]
|
||||
erw [Equiv.apply_symm_apply]
|
||||
rw [HepLean.Fin.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
|
||||
|
||||
/-- The isomorphism between the image of a map `Fin 1 ⊕ Fin 1 → S.C` contructed by `finExtractTwo`
|
||||
under `S.F.obj`, and an object in the image of `OverColor.Discrete.pairτ S.FDiscrete`. -/
|
||||
under `S.F.obj`, and an object in the image of `OverColor.Discrete.pairτ S.FDiscrete`. -/
|
||||
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)) ≅
|
||||
|
|
@ -115,35 +116,54 @@ lemma contrFin1Fin1_inv_tmul {n : ℕ} (c : Fin n.succ.succ → S.C)
|
|||
PiTensorProduct.tprod S.k (fun k =>
|
||||
match k with | Sum.inl 0 => x | Sum.inr 0 => (S.FDiscrete.map
|
||||
(eqToHom (by simp [h]))).hom y) := by
|
||||
simp [contrFin1Fin1]
|
||||
simp only [Nat.succ_eq_add_one, contrFin1Fin1, Functor.comp_obj, Discrete.functor_obj_eq_as,
|
||||
Function.comp_apply, Iso.trans_symm, Iso.symm_symm_eq, Iso.trans_inv, tensorIso_inv,
|
||||
Iso.symm_inv, Functor.mapIso_hom, tensor_comp, MonoidalFunctor.μIso_hom, Category.assoc,
|
||||
LaxMonoidalFunctor.μ_natural, Functor.mapIso_inv, Action.comp_hom,
|
||||
Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorHom_hom,
|
||||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Functor.id_obj, mk_hom,
|
||||
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
|
||||
((((OverColor.forgetLiftApp S.FDiscrete (c i)).inv.hom x) ⊗ₜ[S.k]
|
||||
((OverColor.forgetLiftApp S.FDiscrete (S.τ (c i))).inv.hom y))))) = _
|
||||
simp [OverColor.forgetLiftApp]
|
||||
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
|
||||
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))) = _
|
||||
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
|
||||
(((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
|
||||
funext r
|
||||
match r with
|
||||
| Sum.inl 0 =>
|
||||
simp [OverColor.lift.discreteSumEquiv, HepLean.PiTensorProduct.elimPureTensor]
|
||||
simp [OverColor.lift.discreteFunctorMapEqIso]
|
||||
simp only [Nat.succ_eq_add_one, mk_hom, Fin.isValue, Function.comp_apply,
|
||||
instMonoidalCategoryStruct_tensorObj_left, mkSum_inv_homToEquiv, Equiv.refl_symm,
|
||||
instMonoidalCategoryStruct_tensorObj_hom, Functor.id_obj, lift.discreteSumEquiv, Sum.elim_inl,
|
||||
Sum.elim_inr, HepLean.PiTensorProduct.elimPureTensor]
|
||||
simp only [Fin.isValue, lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl,
|
||||
Iso.refl_hom, Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
|
||||
rfl
|
||||
| Sum.inr 0 =>
|
||||
simp [OverColor.lift.discreteFunctorMapEqIso, OverColor.lift.discreteSumEquiv, HepLean.PiTensorProduct.elimPureTensor]
|
||||
simp only [Nat.succ_eq_add_one, mk_hom, Fin.isValue, Function.comp_apply,
|
||||
instMonoidalCategoryStruct_tensorObj_left, mkSum_inv_homToEquiv, Equiv.refl_symm,
|
||||
instMonoidalCategoryStruct_tensorObj_hom, lift.discreteFunctorMapEqIso, eqToIso_refl,
|
||||
Functor.mapIso_refl, Iso.refl_hom, Action.id_hom, Iso.refl_inv, Functor.mapIso_hom,
|
||||
eqToIso.hom, Functor.mapIso_inv, eqToIso.inv, Functor.id_obj, lift.discreteSumEquiv,
|
||||
Sum.elim_inl, Sum.elim_inr, HepLean.PiTensorProduct.elimPureTensor,
|
||||
LinearEquiv.ofLinear_apply]
|
||||
rfl
|
||||
|
||||
lemma contrFin1Fin1_hom_hom_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
|
||||
|
|
@ -163,7 +183,8 @@ lemma contrFin1Fin1_hom_hom_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
|
|||
| Sum.inl 0 =>
|
||||
simp
|
||||
| Sum.inr 0 =>
|
||||
simp
|
||||
simp only [Nat.succ_eq_add_one, Fin.isValue, mk_hom, Function.comp_apply,
|
||||
Discrete.functor_obj_eq_as]
|
||||
change _ = ((S.FDiscrete.map (eqToHom _)) ≫ (S.FDiscrete.map (eqToHom _))).hom (x (Sum.inr 0))
|
||||
rw [← Functor.map_comp]
|
||||
simp
|
||||
|
|
@ -182,17 +203,16 @@ def contrIso {n : ℕ} (c : Fin n.succ.succ → S.C)
|
|||
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)} :
|
||||
(S.contrIso c1 i j h).hom.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.μ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 ≫
|
||||
((S.contrFin1Fin1 c1 i j h).hom.hom ⊗ (S.F.map (mkIso (contrIso.proof_1 S c1 i j)).hom).hom)
|
||||
:= by
|
||||
{i : Fin n.succ.succ} {j : Fin n.succ} {h : c1 (i.succAbove j) = S.τ (c1 i)} :
|
||||
(S.contrIso c1 i j h).hom.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.μ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 ≫
|
||||
((S.contrFin1Fin1 c1 i j h).hom.hom ⊗
|
||||
(S.F.map (mkIso (contrIso.proof_1 S c1 i j)).hom).hom) := by
|
||||
rw [contrIso]
|
||||
simp [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V, Action.comp_hom,
|
||||
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
|
||||
|
|
@ -208,14 +228,14 @@ def contrMap {n : ℕ} (c : Fin n.succ.succ → S.C)
|
|||
(tensorHom (S.contr.app (Discrete.mk (c i))) (𝟙 _)) ≫
|
||||
(MonoidalCategory.leftUnitor _).hom
|
||||
|
||||
def castToField (v : (↑((𝟙_ (Discrete S.C ⥤ Rep S.k S.G)).obj { as := c }).V)) : S.k := v
|
||||
def castToField (v : (↑((𝟙_ (Discrete S.C ⥤ Rep S.k S.G)).obj { as := c }).V)) : S.k := v
|
||||
|
||||
lemma contrMap_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 : (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.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,
|
||||
|
|
@ -261,18 +281,15 @@ lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
|
|||
((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
|
||||
((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)))))))) =
|
||||
_
|
||||
(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)))))))) = _
|
||||
rw [TensorProduct.map_tmul]
|
||||
rw [contrFin1Fin1_hom_hom_tprod]
|
||||
simp only [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V,
|
||||
|
|
@ -280,33 +297,37 @@ lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
|
|||
Discrete.functor_obj_eq_as, instMonoidalCategoryStruct_tensorObj_left, mkSum_homToEquiv,
|
||||
Equiv.refl_symm, Functor.id_obj, ModuleCat.MonoidalCategory.whiskerRight_apply]
|
||||
rw [Action.instMonoidalCategory_leftUnitor_hom_hom]
|
||||
simp
|
||||
simp only [Monoidal.tensorUnit_obj, Action.instMonoidalCategory_tensorUnit_V, Fin.isValue,
|
||||
ModuleCat.MonoidalCategory.leftUnitor_hom_apply]
|
||||
congr 1
|
||||
/- The contraction. -/
|
||||
· simp [castToField]
|
||||
· simp only [Fin.isValue, castToField]
|
||||
congr 2
|
||||
· simp [lift.discreteFunctorMapEqIso]
|
||||
· 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]
|
||||
change (S.FDiscrete.map (eqToHom _)).hom
|
||||
(x (((HepLean.Fin.finExtractTwo i j)).symm ((Sum.inl (Sum.inr 0))))) = _
|
||||
simp [CategoryTheory.Discrete.functor_map_id]
|
||||
simp only [Nat.succ_eq_add_one, Fin.isValue]
|
||||
have h1' {a b d: Fin n.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
|
||||
(S.FDiscrete.map (Discrete.eqToHom (h))).hom (x d) =
|
||||
(S.FDiscrete.map (Discrete.eqToHom h')).hom (x b) := by
|
||||
subst hbd
|
||||
rfl
|
||||
refine h1' ?_ ?_ ?_
|
||||
simp
|
||||
simp only [Nat.succ_eq_add_one, Fin.isValue, HepLean.Fin.finExtractTwo_symm_inl_inr_apply]
|
||||
simp [h]
|
||||
/- The tensor. -/
|
||||
· erw [lift.map_tprod]
|
||||
apply congrArg
|
||||
funext d
|
||||
simp [lift.discreteFunctorMapEqIso]
|
||||
simp only [mk_hom, Function.comp_apply, lift.discreteFunctorMapEqIso, Functor.mapIso_hom,
|
||||
eqToIso.hom, Functor.mapIso_inv, eqToIso.inv, 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.inr (d))))) = _
|
||||
simp [CategoryTheory.Discrete.functor_map_id ]
|
||||
((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' {a b : Fin n.succ.succ} (h : a = b) :
|
||||
|
|
@ -437,14 +458,14 @@ lemma constTwoNode_tensor {c1 c2 : S.C}
|
|||
|
||||
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
|
||||
((S.F.μ _ _).hom (t1.tensor ⊗ₜ t2.tensor)) := rfl
|
||||
|
||||
lemma add_tensor (t1 t2 : TensorTree S c) : (add t1 t2).tensor = t1.tensor + t2.tensor := rfl
|
||||
|
||||
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)}
|
||||
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
|
||||
|
|
@ -462,17 +483,21 @@ lemma contr_tensor_eq {n : ℕ} {c : Fin n.succ.succ → S.C} {T1 T2 : TensorTre
|
|||
rw [h]
|
||||
|
||||
lemma prod_tensor_eq_fst {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
{T1 T1' : TensorTree S c} { T2 : TensorTree S c1}
|
||||
{T1 T1' : TensorTree S c} { T2 : TensorTree S c1}
|
||||
(h : T1.tensor = T1'.tensor) :
|
||||
(prod T1 T2).tensor = (prod T1' T2).tensor := by
|
||||
simp [prod_tensor]
|
||||
simp only [prod_tensor, Functor.id_obj, OverColor.mk_hom, Action.instMonoidalCategory_tensorObj_V,
|
||||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj]
|
||||
rw [h]
|
||||
|
||||
lemma prod_tensor_eq_snd {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
|
||||
{T1 : TensorTree S c} {T2 T2' : TensorTree S c1}
|
||||
(h : T2.tensor = T2'.tensor) :
|
||||
(prod T1 T2).tensor = (prod T1 T2').tensor := by
|
||||
simp [prod_tensor]
|
||||
simp only [prod_tensor, Functor.id_obj, OverColor.mk_hom, Action.instMonoidalCategory_tensorObj_V,
|
||||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj]
|
||||
rw [h]
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -266,13 +266,13 @@ def withoutContr (stx : Syntax) : TermElabM (List (TSyntax `indexExpr)) := do
|
|||
def toPairs (l : List ℕ) : List (ℕ × ℕ) :=
|
||||
match l with
|
||||
| x1 :: x2 :: xs => (x1, x2) :: toPairs xs
|
||||
| [] => []
|
||||
| [x] => [(x, 0)]
|
||||
| [] => []
|
||||
| [x] => [(x, 0)]
|
||||
|
||||
def contrListAdjust (l : List (ℕ × ℕ)) : List (ℕ × ℕ) :=
|
||||
let l' := l.bind (fun p => [p.1, p.2])
|
||||
let l'' := List.mapAccumr
|
||||
(fun x (prev : List ℕ) =>
|
||||
(fun x (prev : List ℕ) =>
|
||||
let e := prev.countP (fun y => y < x)
|
||||
(x :: prev, x - e)) l'.reverse []
|
||||
toPairs l''.2.reverse
|
||||
|
|
@ -419,8 +419,8 @@ def finMapToEquiv (f1 f2 : Fin n → Fin n) (h : ∀ x, f1 (f2 x) = x := by deci
|
|||
def getPermutationSyntax (l1 l2 : List (TSyntax `indexExpr)) : TermElabM Term := do
|
||||
let lPerm ← getPermutation l1 l2
|
||||
let l2Perm ← getPermutation l1 l2
|
||||
let permString := "![" ++ String.intercalate ", " (lPerm.map toString) ++ "]"
|
||||
let perm2String := "![" ++ String.intercalate ", " (l2Perm.map toString) ++ "]"
|
||||
let permString := "![" ++ String.intercalate ", " (lPerm.map toString) ++ "]"
|
||||
let perm2String := "![" ++ String.intercalate ", " (l2Perm.map toString) ++ "]"
|
||||
let P1 ← TensorNode.stringToTerm permString
|
||||
let P2 ← TensorNode.stringToTerm perm2String
|
||||
let stx := Syntax.mkApp (mkIdent ``finMapToEquiv) #[P1, P2]
|
||||
|
|
|
|||
|
|
@ -53,7 +53,7 @@ lemma neg_neg (t : TensorTree S c) : (neg (neg t)).tensor = t.tensor := by
|
|||
simp only [neg_tensor, _root_.neg_neg]
|
||||
|
||||
@[simp]
|
||||
lemma neg_fst_prod {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S c1)
|
||||
lemma neg_fst_prod {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S c1)
|
||||
(T2 : TensorTree S c2) :
|
||||
(prod (neg T1) T2).tensor = (neg (prod T1 T2)).tensor := by
|
||||
simp only [prod_tensor, Functor.id_obj, Action.instMonoidalCategory_tensorObj_V,
|
||||
|
|
@ -61,7 +61,7 @@ lemma neg_fst_prod {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S
|
|||
Action.FunctorCategoryEquivalence.functor_obj_obj, neg_tensor, neg_tmul, map_neg]
|
||||
|
||||
@[simp]
|
||||
lemma neg_snd_prod {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S c1)
|
||||
lemma neg_snd_prod {c1 : Fin n → S.C} {c2 : Fin m → S.C} (T1 : TensorTree S c1)
|
||||
(T2 : TensorTree S c2) :
|
||||
(prod T1 (neg T2)).tensor = (neg (prod T1 T2)).tensor := by
|
||||
simp only [prod_tensor, Functor.id_obj, Action.instMonoidalCategory_tensorObj_V,
|
||||
|
|
|
|||
|
|
@ -38,12 +38,12 @@ def swapI : Fin n.succ.succ.succ.succ := q.i.succAbove (q.j.succAbove q.k)
|
|||
def swapJ : Fin n.succ.succ.succ := (predAboveI (q.i.succAbove (q.j.succAbove q.k)) q.i).succAbove
|
||||
((predAboveI (q.j.succAbove q.k) q.j).succAbove q.l)
|
||||
|
||||
def swapK : Fin n.succ.succ := predAboveI
|
||||
def swapK : Fin n.succ.succ := predAboveI
|
||||
((predAboveI (q.i.succAbove (q.j.succAbove q.k)) q.i).succAbove
|
||||
((predAboveI (q.j.succAbove q.k) q.j).succAbove q.l))
|
||||
(predAboveI (q.i.succAbove (q.j.succAbove q.k)) q.i)
|
||||
|
||||
def swapL : Fin n.succ := predAboveI ((predAboveI (q.j.succAbove q.k) q.j).succAbove q.l)
|
||||
def swapL : Fin n.succ := predAboveI ((predAboveI (q.j.succAbove q.k) q.j).succAbove q.l)
|
||||
(predAboveI (q.j.succAbove q.k) q.j)
|
||||
|
||||
lemma swap_map_eq (x : Fin n) : (q.swapI.succAbove (q.swapJ.succAbove
|
||||
|
|
@ -58,25 +58,25 @@ lemma swap_map_eq (x : Fin n) : (q.swapI.succAbove (q.swapJ.succAbove
|
|||
|
||||
@[simp]
|
||||
lemma swapI_neq_i : ¬ q.swapI = q.i := by
|
||||
simp [swapI]
|
||||
simp only [Nat.succ_eq_add_one, swapI]
|
||||
exact Fin.succAbove_ne q.i (q.j.succAbove q.k)
|
||||
|
||||
@[simp]
|
||||
lemma swapI_neq_succAbove : ¬ q.swapI = q.i.succAbove q.j := by
|
||||
simp [swapI]
|
||||
simp only [Nat.succ_eq_add_one, swapI]
|
||||
apply Function.Injective.ne Fin.succAbove_right_injective
|
||||
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
|
||||
simp [swapI]
|
||||
simp only [Nat.succ_eq_add_one, swapI]
|
||||
apply Function.Injective.ne Fin.succAbove_right_injective
|
||||
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]
|
||||
simp only [swapI, swapJ]
|
||||
rw [← succAbove_succAbove_predAboveI]
|
||||
rw [← succAbove_succAbove_predAboveI]
|
||||
|
||||
|
|
@ -87,7 +87,7 @@ lemma swapJ_eq_swapI_predAbove : q.swapJ = predAboveI q.swapI (q.i.succAbove
|
|||
exact swapI_neq_i_j_k_l_succAbove q
|
||||
|
||||
@[simp]
|
||||
lemma swapK_swapJ_succAbove : (q.swapJ.succAbove q.swapK) = predAboveI q.swapI q.i := by
|
||||
lemma swapK_swapJ_succAbove : (q.swapJ.succAbove q.swapK) = predAboveI q.swapI q.i := by
|
||||
rw [swapJ, swapK]
|
||||
rw [succsAbove_predAboveI]
|
||||
rfl
|
||||
|
|
@ -130,19 +130,19 @@ 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))))):=
|
||||
(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 })) :
|
||||
((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
|
||||
((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
|
||||
(x (q.swap.i.succAbove (q.swap.j.succAbove (q.swap.k.succAbove q.swap.l))))))) •
|
||||
((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
|
||||
= ((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
|
||||
(x (q.swap.i.succAbove (q.swap.j.succAbove (q.swap.k.succAbove q.swap.l))))))) •
|
||||
((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
|
||||
rw [contrMapSnd,TensorStruct.contrMap_tprod]
|
||||
change ((lift.obj S.FDiscrete).map q.contrSwapHom).hom
|
||||
(_ • ((PiTensorProduct.tprod S.k) fun k =>
|
||||
|
|
@ -161,11 +161,11 @@ lemma contrSwapHom_tprod (x : (i : (𝟭 Type).obj (OverColor.mk c).left) → Co
|
|||
rw [lift.map_tprod]
|
||||
apply congrArg
|
||||
funext i
|
||||
simp
|
||||
simp only [Nat.succ_eq_add_one, mk_hom, Function.comp_apply]
|
||||
rw [lift.discreteFunctorMapEqIso]
|
||||
change _ = (S.FDiscrete.map (Discrete.eqToIso _).hom).hom _
|
||||
change _ = (S.FDiscrete.map (Discrete.eqToIso _).hom).hom _
|
||||
have h1' {a b : Fin n.succ.succ.succ.succ} (h : a = b) :
|
||||
x b = (S.FDiscrete.map (Discrete.eqToIso (by rw [h])).hom).hom (x a) := by
|
||||
x b = (S.FDiscrete.map (Discrete.eqToIso (by rw [h])).hom).hom (x a) := by
|
||||
subst h
|
||||
simp
|
||||
exact h1' (q.swap_map_eq i)
|
||||
|
|
@ -179,7 +179,7 @@ lemma contrMapFst_contrMapSnd_swap :
|
|||
refine PiTensorProduct.induction_on' x (fun r x => ?_) <| fun x y hx hy => by
|
||||
simp only [CategoryTheory.Functor.id_obj, map_add, hx, ModuleCat.coe_comp,
|
||||
Function.comp_apply, hy]
|
||||
simp only [Nat.succ_eq_add_one, Functor.id_obj, PiTensorProduct.tprodCoeff_eq_smul_tprod,
|
||||
simp only [Nat.succ_eq_add_one, Functor.id_obj, PiTensorProduct.tprodCoeff_eq_smul_tprod,
|
||||
map_smul]
|
||||
apply congrArg
|
||||
rw [contrMapFst, contrMapFst]
|
||||
|
|
@ -205,21 +205,25 @@ lemma contrMapFst_contrMapSnd_swap :
|
|||
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)) :
|
||||
(S.FDiscrete.map (Discrete.eqToHom (h))).hom (x d) =
|
||||
(S.FDiscrete.map (Discrete.eqToHom h')).hom (x b) := by
|
||||
(S.FDiscrete.map (Discrete.eqToHom (h))).hom (x d) =
|
||||
(S.FDiscrete.map (Discrete.eqToHom h')).hom (x b) := by
|
||||
subst hbd
|
||||
rfl
|
||||
refine h1' ?_ ?_ ?_
|
||||
erw [swapJ_swapI_succAbove]
|
||||
rfl
|
||||
· congr 1
|
||||
simp
|
||||
simp only [Monoidal.tensorUnit_obj, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Nat.succ_eq_add_one, Function.comp_apply, Equivalence.symm_inverse,
|
||||
Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, Functor.comp_obj,
|
||||
Discrete.functor_obj_eq_as]
|
||||
have h' {a a' b b' : Fin n.succ.succ.succ.succ} (hab : c b = S.τ (c a))
|
||||
(hab' : c b' = S.τ (c a')) (ha : a = a') (hb : b= b') :
|
||||
(S.contr.app { as := c a }).hom (x a ⊗ₜ[S.k] (S.FDiscrete.map (Discrete.eqToHom hab)).hom (x b)) =
|
||||
(S.contr.app { as := c a' }).hom (x a' ⊗ₜ[S.k]
|
||||
(S.FDiscrete.map (Discrete.eqToHom hab')).hom
|
||||
(x b')) := by
|
||||
(hab' : c b' = S.τ (c a')) (ha : a = a') (hb : b= b') :
|
||||
(S.contr.app { as := c a }).hom
|
||||
(x a ⊗ₜ[S.k] (S.FDiscrete.map (Discrete.eqToHom hab)).hom (x b)) =
|
||||
(S.contr.app { as := c a' }).hom (x a' ⊗ₜ[S.k]
|
||||
(S.FDiscrete.map (Discrete.eqToHom hab')).hom (x b')) := by
|
||||
subst ha hb
|
||||
rfl
|
||||
apply h'
|
||||
|
|
@ -252,12 +256,12 @@ theorem contr_contr {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} {i : Fin n
|
|||
{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))
|
||||
(t : TensorTree S c) :
|
||||
(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).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
|
||||
|
|
|
|||
|
|
@ -39,9 +39,9 @@ lemma contrFin1Fin1_naturality {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
|
|||
(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 ]
|
||||
erw [← CategoryTheory.Iso.eq_comp_inv]
|
||||
rw [CategoryTheory.Category.assoc]
|
||||
erw [← CategoryTheory.Iso.inv_comp_eq ]
|
||||
erw [← CategoryTheory.Iso.inv_comp_eq]
|
||||
ext1
|
||||
apply TensorProduct.ext'
|
||||
intro x y
|
||||
|
|
@ -51,7 +51,11 @@ lemma contrFin1Fin1_naturality {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
|
|||
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 only [Nat.succ_eq_add_one, Discrete.functor_obj_eq_as, Function.comp_apply,
|
||||
extractOne_homToEquiv, Fin.isValue, mk_hom, finExtractTwo_symm_inl_inr_apply,
|
||||
Discrete.mk.injEq]
|
||||
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]
|
||||
|
|
@ -77,8 +81,11 @@ lemma contrFin1Fin1_naturality {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
|
|||
match i with
|
||||
| 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
|
||||
simp only [Nat.succ_eq_add_one, mk_hom, Fin.isValue, Function.comp_apply,
|
||||
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
|
||||
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]
|
||||
|
|
@ -89,12 +96,11 @@ lemma contrIso_comm_aux_1 {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
|
|||
(σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) :
|
||||
((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)
|
||||
(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
|
||||
≫ (S.F.map (extractTwoAux' i j σ ⊗ extractTwoAux i j σ)).hom
|
||||
:= by
|
||||
≫ (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 = _
|
||||
rw [← Functor.map_comp, ← Functor.map_comp]
|
||||
|
|
@ -109,14 +115,14 @@ lemma contrIso_comm_aux_2 {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
|
|||
(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 =
|
||||
(S.F.μIso _ _).inv.hom ≫ (S.F.map (extractTwoAux' i j σ) ⊗ S.F.map (extractTwoAux i j σ)).hom
|
||||
:= by
|
||||
(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 =
|
||||
(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 ]
|
||||
erw [CategoryTheory.IsIso.eq_inv_comp]
|
||||
exact Eq.symm
|
||||
(LaxMonoidalFunctor.μ_natural S.F.toLaxMonoidalFunctor (extractTwoAux' i j σ)
|
||||
(extractTwoAux i j σ))
|
||||
|
|
@ -143,8 +149,9 @@ lemma contrIso_comm_aux_3 {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.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 σ)))
|
||||
|
||||
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))
|
||||
|
|
@ -155,8 +162,7 @@ lemma contrIso_comm_aux_5 {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 ⊗ (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
|
||||
≫ (S.contrIsoComm σ).hom := by
|
||||
erw [← CategoryTheory.MonoidalCategory.tensor_comp (f₁ := (S.F.map (extractTwoAux' i j σ)).hom)]
|
||||
rw [contrIso_comm_aux_3 S σ]
|
||||
rw [contrFin1Fin1_naturality S h σ]
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue