refactor: lint
This commit is contained in:
jstoobysmith
parent
ce0805bbdd
commit
dcf6b774d4
12 changed files with 126 additions and 61 deletions
|
|
@ -299,14 +299,15 @@ lemma β_inv_toEquiv (f : X → C) (g : Y → C) :
|
|||
lemma whiskeringLeft_toEquiv (f : X → C) (g : Y → C) (h : Z → C)
|
||||
(σ : OverColor.mk f ⟶ OverColor.mk g) :
|
||||
Hom.toEquiv (OverColor.mk h ◁ σ) = (Equiv.refl Z).sumCongr (Hom.toEquiv σ) := by
|
||||
simp [MonoidalCategory.whiskerLeft]
|
||||
simp only [instMonoidalCategoryStruct_tensorObj_left, mk_left, MonoidalCategory.whiskerLeft,
|
||||
Functor.id_obj, mk_hom]
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma whiskeringRight_toEquiv (f : X → C) (g : Y → C) (h : Z → C)
|
||||
(σ : OverColor.mk f ⟶ OverColor.mk g) :
|
||||
Hom.toEquiv (σ ▷ OverColor.mk h) = (Hom.toEquiv σ).sumCongr (Equiv.refl Z) := by
|
||||
simp [MonoidalCategory.whiskerLeft]
|
||||
simp only [instMonoidalCategoryStruct_tensorObj_left, mk_left]
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
|
|
@ -321,7 +322,6 @@ lemma α_inv_toEquiv (f : X → C) (g : Y → C) (h : Z → C) :
|
|||
(Equiv.sumAssoc X Y Z).symm := by
|
||||
rfl
|
||||
|
||||
|
||||
end OverColor
|
||||
|
||||
end IndexNotation
|
||||
|
|
|
|||
|
|
@ -188,9 +188,16 @@ lemma pairIsoSep_β {c1 c2 : C} (x : ↑(F.obj { as := c1 } ⊗ F.obj { as := c2
|
|||
apply congrArg
|
||||
funext i
|
||||
fin_cases i
|
||||
· simp [lift.discreteFunctorMapEqIso]
|
||||
· simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue, mk_hom,
|
||||
Matrix.cons_val_zero, Fin.cases_zero, mk_left, equivToHomEq_toEquiv, finMapToEquiv_symm_apply,
|
||||
Matrix.cons_val_one, Matrix.head_cons, lift.discreteFunctorMapEqIso, eqToIso_refl,
|
||||
Functor.mapIso_refl, Iso.refl_hom, Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
|
||||
rfl
|
||||
· simp [lift.discreteFunctorMapEqIso]
|
||||
· simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.mk_one, Fin.isValue, mk_hom,
|
||||
Matrix.cons_val_one, Matrix.head_cons, mk_left, equivToHomEq_toEquiv,
|
||||
finMapToEquiv_symm_apply, Matrix.cons_val_zero, lift.discreteFunctorMapEqIso, eqToIso_refl,
|
||||
Functor.mapIso_refl, Iso.refl_hom, Action.id_hom, Iso.refl_inv, Fin.cases_zero,
|
||||
LinearEquiv.ofLinear_apply]
|
||||
rfl
|
||||
exact congrFun (congrArg (fun f => f.toFun) h1) _
|
||||
|
||||
|
|
|
|||
|
|
@ -201,15 +201,17 @@ lemma extractTwo_hom_left_apply {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fin n.
|
|||
@[simp]
|
||||
lemma extractTwo_toEquiv {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fin n.succ.succ)
|
||||
{c1 c2 : Fin n.succ.succ.succ → C} (σ : mk c1 ⟶ mk c2) :
|
||||
(Hom.toEquiv (extractTwo i j σ)) = (finExtractOnePerm ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)
|
||||
(finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ))) := by
|
||||
(Hom.toEquiv (extractTwo i j σ)) =
|
||||
(finExtractOnePerm ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)
|
||||
(finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ))) := by
|
||||
simp only [extractTwo, extractOne]
|
||||
rfl
|
||||
|
||||
lemma extractTwo_toEquiv_symm {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fin n.succ.succ)
|
||||
{c1 c2 : Fin n.succ.succ.succ → C} (σ : mk c1 ⟶ mk c2) :
|
||||
(Hom.toEquiv (extractTwo i j σ)).symm = (finExtractOnePerm ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)
|
||||
(finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ))).symm := by
|
||||
(Hom.toEquiv (extractTwo i j σ)).symm =
|
||||
(finExtractOnePerm ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)
|
||||
(finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ))).symm := by
|
||||
simp
|
||||
|
||||
/-- Removes a given `i : Fin n.succ.succ` and `j : Fin n.succ` from a morphism in `OverColor C`.
|
||||
|
|
|
|||
|
|
@ -814,14 +814,14 @@ def forgetLiftApp (c : C) : (lift.obj F).obj (OverColor.mk (fun (_ : Fin 1) => c
|
|||
erw [PiTensorProduct.subsingletonEquiv_apply_tprod]
|
||||
rfl)
|
||||
|
||||
lemma forgetLiftApp_naturality_eqToHom (c c1 : C) (h : c = c1):
|
||||
lemma forgetLiftApp_naturality_eqToHom (c c1 : C) (h : c = c1) :
|
||||
(forgetLiftApp F c).hom ≫ F.map (Discrete.eqToHom h) =
|
||||
(lift.obj F).map (OverColor.mkIso (by rw [h])).hom ≫ (forgetLiftApp F c1).hom := by
|
||||
subst h
|
||||
simp [mkIso_refl_hom]
|
||||
|
||||
lemma forgetLiftApp_naturality_eqToHom_apply (c c1 : C) (h : c = c1)
|
||||
(x : (lift.obj F).obj (OverColor.mk (fun (_ : Fin 1) => c))) :
|
||||
(x : (lift.obj F).obj (OverColor.mk (fun (_ : Fin 1) => c))) :
|
||||
(F.map (Discrete.eqToHom h)).hom ((forgetLiftApp F c).hom.hom x) =
|
||||
(forgetLiftApp F c1).hom.hom (((lift.obj F).map (OverColor.mkIso (by rw [h])).hom).hom x) := by
|
||||
change ((forgetLiftApp F c).hom ≫ F.map (Discrete.eqToHom h)).hom x = _
|
||||
|
|
@ -836,6 +836,9 @@ lemma forgetLiftApp_hom_hom_apply_eq (c : C)
|
|||
erw [LinearEquiv.eq_symm_apply]
|
||||
rfl
|
||||
|
||||
/-- The isomorphism between the representation `(lift.obj F).obj (OverColor.mk ![c])`
|
||||
and the representation `F.obj (Discrete.mk c)`. See `forgetLiftApp` for
|
||||
an alternative version. -/
|
||||
def forgetLiftAppCon (c : C) : (lift.obj F).obj (OverColor.mk ![c])
|
||||
≅ F.obj (Discrete.mk c) := ((lift.obj F).mapIso (OverColor.mkIso (by
|
||||
funext i
|
||||
|
|
@ -847,13 +850,13 @@ lemma forgetLiftAppCon_inv_apply_expand (c : C) (x : F.obj (Discrete.mk c)) :
|
|||
((lift.obj F).map (OverColor.mkIso (by
|
||||
funext i
|
||||
fin_cases i
|
||||
rfl)).hom).hom ((forgetLiftApp F c).inv.hom x):= by
|
||||
rfl)).hom).hom ((forgetLiftApp F c).inv.hom x) := by
|
||||
rw [forgetLiftAppCon]
|
||||
simp_all only [Nat.succ_eq_add_one, Nat.reduceAdd, Iso.trans_inv, Functor.mapIso_inv, Action.comp_hom,
|
||||
simp_all only [Nat.succ_eq_add_one, Iso.trans_inv, Functor.mapIso_inv, Action.comp_hom,
|
||||
ModuleCat.coe_comp, Function.comp_apply]
|
||||
rfl
|
||||
|
||||
lemma forgetLiftAppCon_naturality_eqToHom (c c1 : C) (h : c = c1):
|
||||
lemma forgetLiftAppCon_naturality_eqToHom (c c1 : C) (h : c = c1) :
|
||||
(forgetLiftAppCon F c).hom ≫ F.map (Discrete.eqToHom h) =
|
||||
(lift.obj F).map (OverColor.mkIso (by rw [h])).hom ≫ (forgetLiftAppCon F c1).hom := by
|
||||
subst h
|
||||
|
|
@ -862,7 +865,8 @@ lemma forgetLiftAppCon_naturality_eqToHom (c c1 : C) (h : c = c1):
|
|||
lemma forgetLiftAppCon_naturality_eqToHom_apply (c c1 : C) (h : c = c1)
|
||||
(x : (lift.obj F).obj (OverColor.mk ![c])) :
|
||||
(F.map (Discrete.eqToHom h)).hom ((forgetLiftAppCon F c).hom.hom x) =
|
||||
(forgetLiftAppCon F c1).hom.hom (((lift.obj F).map (OverColor.mkIso (by rw [h])).hom).hom x) := by
|
||||
(forgetLiftAppCon F c1).hom.hom
|
||||
(((lift.obj F).map (OverColor.mkIso (by rw [h])).hom).hom x) := by
|
||||
change ((forgetLiftAppCon F c).hom ≫ F.map (Discrete.eqToHom h)).hom x = _
|
||||
rw [forgetLiftAppCon_naturality_eqToHom]
|
||||
rfl
|
||||
|
|
|
|||
|
|
@ -556,7 +556,7 @@ lemma tensorToVec_inv_apply_expand (c : S.C) (x : S.FD.obj (Discrete.mk c)) :
|
|||
rfl)).hom).hom ((OverColor.forgetLiftApp S.FD c).inv.hom x) :=
|
||||
forgetLiftAppCon_inv_apply_expand S.FD c x
|
||||
|
||||
lemma tensorToVec_naturality_eqToHom (c c1 : S.C) (h : c = c1):
|
||||
lemma tensorToVec_naturality_eqToHom (c c1 : S.C) (h : c = c1) :
|
||||
(S.tensorToVec c).hom ≫ S.FD.map (Discrete.eqToHom h) =
|
||||
S.F.map (OverColor.mkIso (by rw [h])).hom ≫ (S.tensorToVec c1).hom :=
|
||||
OverColor.forgetLiftAppCon_naturality_eqToHom S.FD c c1 h
|
||||
|
|
|
|||
|
|
@ -25,14 +25,14 @@ open TensorTree
|
|||
|
||||
variable {S : TensorSpecies}
|
||||
|
||||
/-- Th map built contracting a 1-tensor with a 2-tensor using basic categorical consstructions. -/
|
||||
/-- Th map built contracting a 1-tensor with a 2-tensor using basic categorical consstructions.s -/
|
||||
def contrOneTwoLeft {c1 c2 : S.C}
|
||||
(x : S.F.obj (OverColor.mk ![c1])) (y : S.F.obj (OverColor.mk ![S.τ c1, c2])) :
|
||||
S.F.obj (OverColor.mk ![c2]) :=
|
||||
(S.tensorToVec c2).inv.hom <|
|
||||
(λ_ (S.FD.obj (Discrete.mk c2))).hom.hom <|
|
||||
((S.contr.app (Discrete.mk c1)) ▷ (S.FD.obj (Discrete.mk (c2 )))).hom <|
|
||||
(α_ _ _ (S.FD.obj (Discrete.mk (c2 )))).inv.hom <|
|
||||
((S.contr.app (Discrete.mk c1)) ▷ (S.FD.obj (Discrete.mk c2))).hom <|
|
||||
(α_ _ _ (S.FD.obj (Discrete.mk (c2)))).inv.hom <|
|
||||
(S.tensorToVec c1).hom.hom (x) ⊗ₜ
|
||||
(OverColor.Discrete.pairIsoSep S.FD).inv.hom y
|
||||
|
||||
|
|
@ -70,8 +70,8 @@ lemma contrOneTwoLeft_tprod_eq {c1 c2 : S.C}
|
|||
(fy : (i : (𝟭 Type).obj (OverColor.mk ![S.τ c1, c2]).left)
|
||||
→ CoeSort.coe (S.FD.obj { as := (OverColor.mk ![S.τ c1, c2]).hom i })) :
|
||||
contrOneTwoLeft (PiTensorProduct.tprod S.k fx) (PiTensorProduct.tprod S.k fy) =
|
||||
((S.tensorToVec c2).inv.hom (
|
||||
((S.contr.app (Discrete.mk c1)).hom (fx (0 : Fin 1) ⊗ₜ fy (0 : Fin 2)) •
|
||||
((S.tensorToVec c2).inv.hom
|
||||
(((S.contr.app (Discrete.mk c1)).hom (fx (0 : Fin 1) ⊗ₜ fy (0 : Fin 2)) •
|
||||
fy (1 : Fin 2)))) := by
|
||||
rw [contrOneTwoLeft]
|
||||
apply congrArg
|
||||
|
|
@ -89,7 +89,9 @@ lemma contrOneTwoLeft_tprod_eq {c1 c2 : S.C}
|
|||
funext x
|
||||
match x with
|
||||
| (0 : Fin 1) =>
|
||||
simp [lift.discreteFunctorMapEqIso]
|
||||
simp only [mk_hom, Fin.isValue, mk_left, equivToIso_mkIso_hom, Equiv.refl_symm,
|
||||
Equiv.refl_apply, Matrix.cons_val_zero, lift.discreteFunctorMapEqIso, eqToIso_refl,
|
||||
Functor.mapIso_refl, Iso.refl_hom, Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
|
||||
rfl
|
||||
|
||||
lemma contr_one_two_left_eq_contrOneTwoLeft_tprod {c1 c2 : S.C} (x : S.F.obj (OverColor.mk ![c1]))
|
||||
|
|
@ -100,7 +102,8 @@ lemma contr_one_two_left_eq_contrOneTwoLeft_tprod {c1 c2 : S.C} (x : S.F.obj (Ov
|
|||
→ CoeSort.coe (S.FD.obj { as := (OverColor.mk ![S.τ c1, c2]).hom i }))
|
||||
(hx : x = PiTensorProduct.tprod S.k fx)
|
||||
(hy : y = PiTensorProduct.tprod S.k fy) :
|
||||
{x | μ ⊗ y | μ ν}ᵀ.tensor = (S.F.mapIso (OverColor.mkIso (by funext x; fin_cases x; rfl))).hom.hom
|
||||
{x | μ ⊗ y | μ ν}ᵀ.tensor =
|
||||
(S.F.mapIso (OverColor.mkIso (by funext x; fin_cases x; rfl))).hom.hom
|
||||
(contrOneTwoLeft x y) := by
|
||||
subst hx
|
||||
subst hy
|
||||
|
|
@ -126,7 +129,7 @@ lemma contr_one_two_left_eq_contrOneTwoLeft_tprod {c1 c2 : S.C} (x : S.F.obj (Ov
|
|||
instMonoidalCategoryStruct_tensorObj_hom, Fin.zero_succAbove, Fin.succ_zero_eq_one,
|
||||
eqToHom_refl, Discrete.functor_map_id, Action.id_hom]
|
||||
congr 1
|
||||
/- The contraction. -/
|
||||
/- The contraction. -/
|
||||
· congr
|
||||
· simp only [Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor, Fin.isValue,
|
||||
Function.comp_apply, Action.FunctorCategoryEquivalence.functor_obj_obj, mk_hom,
|
||||
|
|
@ -158,15 +161,17 @@ lemma contr_one_two_left_eq_contrOneTwoLeft_tprod {c1 c2 : S.C} (x : S.F.obj (Ov
|
|||
|
||||
lemma contr_one_two_left_eq_contrOneTwoLeft {c1 c2 : S.C} (x : S.F.obj (OverColor.mk ![c1]))
|
||||
(y : S.F.obj (OverColor.mk ![S.τ c1, c2])) :
|
||||
{x | μ ⊗ y | μ ν}ᵀ.tensor = (S.F.map (OverColor.mkIso (by funext x; fin_cases x; rfl)).hom).hom
|
||||
{x | μ ⊗ y | μ ν}ᵀ.tensor = (S.F.map (OverColor.mkIso (by funext x; fin_cases x; rfl)).hom).hom
|
||||
(contrOneTwoLeft x y) := by
|
||||
simp [contr_tensor, prod_tensor]
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Fin.succAbove_zero, contr_tensor,
|
||||
prod_tensor, mk_left, Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V,
|
||||
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, tensorNode_tensor]
|
||||
refine PiTensorProduct.induction_on' x ?_ (by
|
||||
intro a b hx hy
|
||||
rw [contrOneTwoLeft_add_left, map_add, ← hx, ← hy]
|
||||
simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, mk_left, Functor.id_obj, mk_hom,
|
||||
add_tmul, map_add]
|
||||
)
|
||||
add_tmul, map_add])
|
||||
intro rx fx
|
||||
refine PiTensorProduct.induction_on' y ?_ (by
|
||||
intro a b hx hy
|
||||
|
|
@ -175,10 +180,11 @@ lemma contr_one_two_left_eq_contrOneTwoLeft {c1 c2 : S.C} (x : S.F.obj (OverColo
|
|||
PiTensorProduct.tprodCoeff_eq_smul_tprod, tmul_add, map_add])
|
||||
intro ry fy
|
||||
simp only [PiTensorProduct.tprodCoeff_eq_smul_tprod, tmul_smul, LinearMapClass.map_smul]
|
||||
rw [ contrOneTwoLeft_smul_right]
|
||||
simp
|
||||
rw [contrOneTwoLeft_smul_right]
|
||||
simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, mk_left, Functor.id_obj, mk_hom,
|
||||
map_smul]
|
||||
apply congrArg
|
||||
rw [ contrOneTwoLeft_smul_left]
|
||||
rw [contrOneTwoLeft_smul_left]
|
||||
simp only [smul_tmul, tmul_smul, LinearMapClass.map_smul]
|
||||
apply congrArg
|
||||
simpa using contr_one_two_left_eq_contrOneTwoLeft_tprod (PiTensorProduct.tprod S.k fx)
|
||||
|
|
@ -188,7 +194,7 @@ lemma contr_one_two_left_eq_contrOneTwoLeft {c1 c2 : S.C} (x : S.F.obj (OverColo
|
|||
lemma contrOneTwoLeft_tensorTree {c1 c2 : S.C} (x : S.F.obj (OverColor.mk ![c1]))
|
||||
(y : S.F.obj (OverColor.mk ![S.τ c1, c2])) :
|
||||
(contrOneTwoLeft x y) = ({x | μ ⊗ y | μ ν}ᵀ |>
|
||||
perm (OverColor.equivToHomEq (Equiv.refl _) (fun x => by fin_cases x; rfl ))).tensor := by
|
||||
perm (OverColor.equivToHomEq (Equiv.refl _) (fun x => by fin_cases x; rfl))).tensor := by
|
||||
change (tensorNode (contrOneTwoLeft x y)).tensor = _
|
||||
symm
|
||||
rw [perm_eq_iff_eq_perm]
|
||||
|
|
|
|||
|
|
@ -67,7 +67,7 @@ lemma toDualRep_tensorTree (c : S.C) (x : S.FD.obj (Discrete.mk c)) :
|
|||
let y : S.F.obj (OverColor.mk ![c]) := (S.tensorToVec c).inv.hom x
|
||||
(S.toDualRep c).hom x = (S.tensorToVec (S.τ c)).hom.hom
|
||||
({y | μ ⊗ S.metricTensor (S.τ c) | μ ν}ᵀ
|
||||
|> perm (OverColor.equivToHomEq (Equiv.refl _) (fun x => by fin_cases x; rfl ))).tensor := by
|
||||
|> perm (OverColor.equivToHomEq (Equiv.refl _) (fun x => by fin_cases x; rfl))).tensor := by
|
||||
simp only
|
||||
rw [toDualRep_apply_eq_contrOneTwoLeft]
|
||||
apply congrArg
|
||||
|
|
@ -78,7 +78,7 @@ lemma fromDualRep_tensorTree (c : S.C) (x : S.FD.obj (Discrete.mk (S.τ c))) :
|
|||
(S.fromDualRep c).hom x = (S.tensorToVec c).hom.hom
|
||||
({y | μ ⊗ S.metricTensor (S.τ (S.τ c))| μ ν}ᵀ
|
||||
|> perm (OverColor.equivToHomEq (Equiv.refl _)
|
||||
(fun x => by fin_cases x; exact (S.τ_involution c).symm ))).tensor := by
|
||||
(fun x => by fin_cases x; exact (S.τ_involution c).symm))).tensor := by
|
||||
simp only
|
||||
rw [fromDualRep]
|
||||
simp only [Action.comp_hom, ModuleCat.coe_comp, Function.comp_apply, Nat.succ_eq_add_one,
|
||||
|
|
@ -106,7 +106,15 @@ lemma toDualRep_fromDualRep_tensorTree_metrics (c : S.C) (x : S.FD.obj (Discrete
|
|||
conv_lhs =>
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_fst <| tensorNode_of_tree _]
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| prod_perm_left _ _ _ _]
|
||||
rw [perm_tensor_eq <| perm_contr_congr 0 0 (by simp) (by simp; decide)]
|
||||
rw [perm_tensor_eq <| perm_contr_congr 0 0 (by simp) (by
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Fin.succAbove_zero,
|
||||
OverColor.mk_left, Functor.id_obj, OverColor.mk_hom, Equiv.refl_symm, Equiv.coe_refl,
|
||||
Function.comp_apply, id_eq, Fin.zero_eta, List.pmap.eq_1, Matrix.cons_val_zero,
|
||||
Fin.succ_zero_eq_one, Fin.succ_one_eq_two, OverColor.extractOne_homToEquiv,
|
||||
permProdLeft_toEquiv, OverColor.equivToHomEq_toEquiv, Equiv.sumCongr_refl, Equiv.refl_trans,
|
||||
Equiv.symm_trans_self, Equiv.refl_apply, HepLean.Fin.finExtractOnePerm_symm_apply,
|
||||
HepLean.Fin.finExtractOne_symm_inr_apply, Fin.zero_succAbove]
|
||||
decide)]
|
||||
rw [perm_perm]
|
||||
apply perm_congr _ rfl
|
||||
apply OverColor.Hom.fin_ext
|
||||
|
|
@ -136,14 +144,44 @@ lemma toDualRep_fromDualRep_tensorTree_unitTensor (c : S.C) (x : S.FD.obj (Discr
|
|||
conv_lhs =>
|
||||
rw [perm_tensor_eq <| assoc_one_two_two _ _ _]
|
||||
rw [perm_perm]
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_snd <| metricTensor_contr_dual_metricTensor_eq_unit _]
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_snd <|
|
||||
metricTensor_contr_dual_metricTensor_eq_unit _]
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| prod_perm_right _ _ _ _]
|
||||
rw [perm_tensor_eq <| perm_contr_congr 0 1 (by simp; rfl) (by simp; rfl)]
|
||||
rw [perm_tensor_eq <| perm_contr_congr 0 1 (by
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, OverColor.mk_left, Functor.id_obj,
|
||||
OverColor.mk_hom, permProdRight_toEquiv, OverColor.equivToHomEq_toEquiv,
|
||||
Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.sumCongr_symm, Equiv.refl_symm,
|
||||
Equiv.sumCongr_apply, Equiv.coe_refl]
|
||||
rfl) (by
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Fin.succAbove_zero,
|
||||
OverColor.mk_left, Functor.id_obj, OverColor.mk_hom, OverColor.extractOne_homToEquiv,
|
||||
permProdRight_toEquiv, OverColor.equivToHomEq_toEquiv, Equiv.symm_trans_apply,
|
||||
Equiv.symm_symm, Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.sumCongr_apply, Equiv.coe_refl,
|
||||
HepLean.Fin.finExtractOnePerm_symm_apply, Equiv.trans_apply, Equiv.symm_apply_apply,
|
||||
Sum.map_map, CompTriple.comp_eq, Equiv.self_comp_symm, Sum.map_id_id, id_eq,
|
||||
Equiv.apply_symm_apply, HepLean.Fin.finExtractOne_symm_inr_apply, Fin.zero_succAbove,
|
||||
Fin.succ_zero_eq_one]
|
||||
rfl)]
|
||||
rw [perm_perm]
|
||||
conv_rhs =>
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| prod_tensor_eq_snd <| unitTensor_eq_dual_perm _]
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| prod_perm_right _ _ _ _]
|
||||
rw [perm_tensor_eq <| perm_contr_congr 0 1 (by simp; rfl) (by simp; rfl)]
|
||||
rw [perm_tensor_eq <| perm_contr_congr 0 1 (by
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, OverColor.mk_left, Functor.id_obj,
|
||||
OverColor.mk_hom, permProdRight_toEquiv, OverColor.equivToHomEq_toEquiv,
|
||||
Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.sumCongr_symm, Equiv.refl_symm,
|
||||
Equiv.sumCongr_apply, Equiv.coe_refl]
|
||||
rfl) (by
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Fin.succAbove_zero,
|
||||
OverColor.mk_left, Functor.id_obj, OverColor.mk_hom, Function.comp_apply,
|
||||
HepLean.Fin.finMapToEquiv_symm_apply, Matrix.cons_val_zero, OverColor.extractOne_homToEquiv,
|
||||
permProdRight_toEquiv, OverColor.equivToHomEq_toEquiv, Equiv.symm_trans_apply,
|
||||
Equiv.symm_symm, Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.sumCongr_apply, Equiv.coe_refl,
|
||||
HepLean.Fin.finExtractOnePerm_symm_apply, Equiv.trans_apply, Equiv.symm_apply_apply,
|
||||
Sum.map_map, CompTriple.comp_eq, Equiv.self_comp_symm, Sum.map_id_id, id_eq,
|
||||
Equiv.apply_symm_apply, HepLean.Fin.finExtractOne_symm_inr_apply, Fin.zero_succAbove,
|
||||
Fin.succ_zero_eq_one]
|
||||
rfl)]
|
||||
rw [perm_perm]
|
||||
refine perm_congr (OverColor.Hom.fin_ext _ _ fun i => ?_) rfl
|
||||
fin_cases i
|
||||
|
|
@ -170,21 +208,22 @@ lemma toDualRep_fromDualRep_tensorTree (c : S.C) (x : S.FD.obj (Discrete.mk c))
|
|||
rw [perm_perm]
|
||||
rw [perm_eq_id]
|
||||
|
||||
lemma toDualRep_fromDualRep_eq_self (c : S.C) (x : S.FD.obj (Discrete.mk c)) :
|
||||
lemma toDualRep_fromDualRep_eq_self (c : S.C) (x : S.FD.obj (Discrete.mk c)) :
|
||||
(S.fromDualRep c).hom ((S.toDualRep c).hom x) = x := by
|
||||
rw [toDualRep_fromDualRep_tensorTree]
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, tensorNode_tensor,
|
||||
OverColor.Discrete.rep_iso_hom_inv_apply]
|
||||
|
||||
lemma fromDualRep_toDualRep_eq_self (c : S.C) (x : S.FD.obj (Discrete.mk (S.τ c))) :
|
||||
lemma fromDualRep_toDualRep_eq_self (c : S.C) (x : S.FD.obj (Discrete.mk (S.τ c))) :
|
||||
(S.toDualRep c).hom ((S.fromDualRep c).hom x) = x := by
|
||||
rw [S.toDualRep_congr (S.τ_involution c).symm, fromDualRep]
|
||||
simp
|
||||
change (S.FD.map (Discrete.eqToHom _)).hom ((S.toDualRep (S.τ (S.τ c))).hom
|
||||
simp only [Action.comp_hom, ModuleCat.coe_comp, Function.comp_apply]
|
||||
change (S.FD.map (Discrete.eqToHom _)).hom ((S.toDualRep (S.τ (S.τ c))).hom
|
||||
(((S.FD.map (Discrete.eqToHom _)) ≫ S.FD.map (Discrete.eqToHom _)).hom
|
||||
(((S.toDualRep (S.τ c)).hom x)))) = _
|
||||
rw [← S.FD.map_comp]
|
||||
simp
|
||||
simp only [eqToHom_trans, eqToHom_refl, Discrete.functor_map_id, Action.id_hom,
|
||||
ModuleCat.id_apply]
|
||||
conv_rhs => rw [← S.toDualRep_fromDualRep_eq_self (S.τ c) x]
|
||||
rfl
|
||||
|
||||
|
|
@ -202,8 +241,8 @@ def dualRepIsoDiscrete (c : S.C) : S.FD.obj (Discrete.mk c) ≅ S.FD.obj (Discre
|
|||
|
||||
informal_definition dualRepIso where
|
||||
math :≈ "Given a `i : Fin n` the isomorphism between `S.F.obj (OverColor.mk c)` and
|
||||
`S.F.obj (OverColor.mk (Function.update c i (S.τ (c i))))` induced by `dualRepIsoDiscrete`
|
||||
acting on the `i`-th component of the color."
|
||||
`S.F.obj (OverColor.mk (Function.update c i (S.τ (c i))))` induced by `dualRepIsoDiscrete`
|
||||
acting on the `i`-th component of the color."
|
||||
deps :≈ [``dualRepIsoDiscrete]
|
||||
|
||||
informal_lemma dualRepIso_unitTensor_fst where
|
||||
|
|
|
|||
|
|
@ -113,7 +113,7 @@ lemma dual_unitTensor_eq_perm (c : S.C) :
|
|||
rfl
|
||||
|
||||
/-- Applying `contrOneTwoLeft` with the unit tensor is the identity map. -/
|
||||
lemma contrOneTwoLeft_unitTensor {c1 : S.C} (x : S.F.obj (OverColor.mk ![c1])) :
|
||||
lemma contrOneTwoLeft_unitTensor {c1 : S.C} (x : S.F.obj (OverColor.mk ![c1])) :
|
||||
contrOneTwoLeft x (S.unitTensor c1) = x := by
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, contrOneTwoLeft,
|
||||
Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
|
|
@ -131,14 +131,14 @@ lemma contrOneTwoLeft_unitTensor {c1 : S.C} (x : S.F.obj (OverColor.mk ![c1]))
|
|||
/-- Contracting a vector with a unit tensor returns the vector. -/
|
||||
lemma vec_contr_unitTensor_eq_self {c1 : S.C} (x : S.F.obj (OverColor.mk ![c1])) :
|
||||
{x | μ ⊗ S.unitTensor c1 | μ ν}ᵀ.tensor = ({x | ν}ᵀ |>
|
||||
perm (OverColor.equivToHomEq (Equiv.refl _) (fun x => by fin_cases x; rfl ))).tensor := by
|
||||
perm (OverColor.equivToHomEq (Equiv.refl _) (fun x => by fin_cases x; rfl))).tensor := by
|
||||
rw [contr_one_two_left_eq_contrOneTwoLeft, contrOneTwoLeft_unitTensor]
|
||||
rfl
|
||||
|
||||
/-- Contracting a unit tensor with a vector returns the unit vector. -/
|
||||
lemma unitTensor_contr_vec_eq_self {c1 : S.C} (x : S.F.obj (OverColor.mk ![S.τ c1])) :
|
||||
{S.unitTensor c1 | ν μ ⊗ x | μ}ᵀ.tensor = ({x | ν}ᵀ |>
|
||||
perm (OverColor.equivToHomEq (Equiv.refl _) (fun x => by fin_cases x; rfl ))).tensor := by
|
||||
perm (OverColor.equivToHomEq (Equiv.refl _) (fun x => by fin_cases x; rfl))).tensor := by
|
||||
conv_lhs =>
|
||||
rw [contr_tensor_eq <| prod_comm _ _ _ _]
|
||||
rw [perm_contr_congr 2 0 (by simp; decide) (by simp; decide)]
|
||||
|
|
|
|||
|
|
@ -44,19 +44,28 @@ lemma assoc_one_two_two {c1 c2 c3 : S.C} (t1 : S.F.obj (OverColor.mk ![c1]))
|
|||
rw [contr_tensor_eq <| contr_prod _ _ _]
|
||||
rw [perm_contr_congr 0 0 (by rfl) (by rfl)]
|
||||
erw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <|
|
||||
perm_tensor_eq <| prod_assoc' _ _ _ _ _ _ ]
|
||||
perm_tensor_eq <| prod_assoc' _ _ _ _ _ _]
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| contr_tensor_eq <| perm_perm _ _ _]
|
||||
rw [perm_tensor_eq <| contr_tensor_eq <| perm_contr_congr 0 0 (by
|
||||
simp only [Nat.succ_eq_add_one,
|
||||
Nat.reduceAdd, Fin.isValue, mk_left, Functor.id_obj, mk_hom, Equiv.toFun_as_coe,
|
||||
Hom.toEquiv_comp, equivToIso_homToEquiv, Equiv.symm_trans_apply]
|
||||
rfl) (by simp; rfl)]
|
||||
rfl) (by
|
||||
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, mk_left, Functor.id_obj, mk_hom,
|
||||
Equiv.toFun_as_coe, Fin.zero_succAbove, Fin.succ_zero_eq_one, Function.comp_apply,
|
||||
Hom.toEquiv_comp, equivToIso_homToEquiv, Equiv.symm_trans_apply, extractOne_homToEquiv,
|
||||
assocPerm_toHomEquiv_inv, Equiv.symm_symm, Equiv.sumCongr_symm, Equiv.refl_symm,
|
||||
Equiv.sumCongr_apply, Equiv.coe_refl, finExtractOnePerm_symm_apply, Equiv.trans_apply,
|
||||
Equiv.symm_apply_apply, Sum.map_map, CompTriple.comp_eq, Equiv.symm_comp_self,
|
||||
Sum.map_id_id, id_eq, Equiv.self_comp_symm, Equiv.apply_symm_apply,
|
||||
finExtractOne_symm_inr_apply]
|
||||
rfl)]
|
||||
rw [perm_tensor_eq <| perm_contr_congr 0 2 (by
|
||||
simp only [Nat.succ_eq_add_one,
|
||||
Nat.reduceAdd, Fin.isValue, mk_left, Functor.id_obj, mk_hom, Equiv.toFun_as_coe,
|
||||
Hom.toEquiv_comp, equivToIso_homToEquiv, Equiv.symm_trans_apply, equivToIso_mkIso_hom,
|
||||
extractTwo_toEquiv]
|
||||
simp only [ Equiv.refl_symm, mk_left,
|
||||
simp only [Equiv.refl_symm, mk_left,
|
||||
Hom.toEquiv_comp, assocPerm_toHomEquiv_inv, equivToIso_homToEquiv, ContrPair.leftContr,
|
||||
Equiv.toFun_as_coe, ContrPair.leftContrI, ContrPair.leftContrJ, Equiv.symm_trans_apply,
|
||||
Equiv.symm_apply_apply, Equiv.symm_symm, Equiv.sumCongr_symm, Equiv.sumCongr_apply,
|
||||
|
|
@ -86,17 +95,15 @@ lemma assoc_one_two_two {c1 c2 c3 : S.C} (t1 : S.F.obj (OverColor.mk ![c1]))
|
|||
rw [perm_tensor_eq <| contr_tensor_eq <| prod_contr _ _ _]
|
||||
rw [perm_tensor_eq <| perm_contr_congr 0 0 (by rfl) (by rfl)]
|
||||
rw [perm_perm]
|
||||
apply perm_congr (OverColor.Hom.fin_ext _ _ fun i => ?_) rfl
|
||||
apply perm_congr (OverColor.Hom.fin_ext _ _ fun i => ?_) rfl
|
||||
fin_cases i
|
||||
simp only [Hom.hom_comp, types_comp_apply, Over.comp_left, extractTwo_hom_left_apply]
|
||||
simp only [mkIso_hom_hom_left_apply]
|
||||
simp only [Hom.toEquiv_comp, extractTwo_toEquiv, assocPerm_toHomEquiv_inv,
|
||||
ContrPair.leftContrI, ContrPair.leftContrJ, ContrPair.leftContr]
|
||||
simp only [mk_left, equivToIso_mkIso_hom]
|
||||
simp only [ equivToIso_homToEquiv, equivToHomEq_hom_left]
|
||||
simp only [equivToIso_homToEquiv, equivToHomEq_hom_left]
|
||||
simp only [contrContrPerm_hom_left_apply]
|
||||
decide
|
||||
|
||||
|
||||
|
||||
end TensorTree
|
||||
|
|
|
|||
|
|
@ -297,10 +297,11 @@ def contrContrPerm {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} {i : Fin n.
|
|||
(ContrQuartet.mk i j k l hij hkl).contrSwapHom
|
||||
|
||||
@[simp]
|
||||
lemma contrContrPerm_hom_left_apply {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} {i : Fin n.succ.succ.succ.succ}
|
||||
lemma contrContrPerm_hom_left_apply {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C}
|
||||
{i : Fin n.succ.succ.succ.succ}
|
||||
{j : Fin n.succ.succ.succ} {k : Fin n.succ.succ} {l : Fin n.succ}
|
||||
(hij : c (i.succAbove j) = S.τ (c i)) (hkl : (c ∘ i.succAbove ∘ j.succAbove) (k.succAbove l) =
|
||||
S.τ ((c ∘ i.succAbove ∘ j.succAbove) k)) (x : Fin n):
|
||||
S.τ ((c ∘ i.succAbove ∘ j.succAbove) k)) (x : Fin n) :
|
||||
(contrContrPerm hij hkl).hom.left x = x := by
|
||||
simp [contrContrPerm, ContrQuartet.contrSwapHom]
|
||||
|
||||
|
|
|
|||
|
|
@ -30,11 +30,10 @@ def permProdLeft := (equivToIso finSumFinEquiv).inv ≫ σ ▷ OverColor.mk c2
|
|||
≫ (equivToIso finSumFinEquiv).hom
|
||||
|
||||
@[simp]
|
||||
lemma permProdLeft_toEquiv : Hom.toEquiv (permProdLeft c2 σ) = finSumFinEquiv.symm.trans
|
||||
(((Hom.toEquiv σ).sumCongr (Equiv.refl (Fin n2))).trans finSumFinEquiv) := by
|
||||
lemma permProdLeft_toEquiv : Hom.toEquiv (permProdLeft c2 σ) = finSumFinEquiv.symm.trans
|
||||
(((Hom.toEquiv σ).sumCongr (Equiv.refl (Fin n2))).trans finSumFinEquiv) := by
|
||||
simp [permProdLeft]
|
||||
|
||||
|
||||
/-- The permutation that arises when moving a `perm` node in the right entry through a `prod` node.
|
||||
This permutation is defined using left-whiskering and composition with `finSumFinEquiv`
|
||||
based-isomorphisms. -/
|
||||
|
|
|
|||
|
|
@ -54,7 +54,7 @@ lemma assocPerm_toHomEquiv_hom : Hom.toEquiv (assocPerm c c2 c3).hom = finSumFin
|
|||
lemma assocPerm_toHomEquiv_inv : Hom.toEquiv (assocPerm c c2 c3).inv = finSumFinEquiv.symm.trans
|
||||
(((Equiv.refl (Fin n)).sumCongr finSumFinEquiv.symm).trans
|
||||
((Equiv.sumAssoc (Fin n) (Fin n2) (Fin n3)).symm.trans
|
||||
((finSumFinEquiv.sumCongr (Equiv.refl (Fin n3))).trans finSumFinEquiv))) := by
|
||||
((finSumFinEquiv.sumCongr (Equiv.refl (Fin n3))).trans finSumFinEquiv))) := by
|
||||
simp [assocPerm]
|
||||
|
||||
/-- The `prod` obeys associativity. -/
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue