feat: dualRepIsoDiscrete
This commit is contained in:
jstoobysmith
parent
5fc5946530
commit
ce0805bbdd
11 changed files with 429 additions and 89 deletions
|
|
@ -126,12 +126,13 @@ import HepLean.Tensors.OverColor.Iso
|
|||
import HepLean.Tensors.OverColor.Lift
|
||||
import HepLean.Tensors.TensorSpecies.Basic
|
||||
import HepLean.Tensors.TensorSpecies.ContractLemmas
|
||||
import HepLean.Tensors.TensorSpecies.DualRepIso
|
||||
import HepLean.Tensors.TensorSpecies.MetricTensor
|
||||
import HepLean.Tensors.TensorSpecies.RepIso
|
||||
import HepLean.Tensors.TensorSpecies.UnitTensor
|
||||
import HepLean.Tensors.Tree.Basic
|
||||
import HepLean.Tensors.Tree.Dot
|
||||
import HepLean.Tensors.Tree.Elab
|
||||
import HepLean.Tensors.Tree.NodeIdentities.Assoc
|
||||
import HepLean.Tensors.Tree.NodeIdentities.Basic
|
||||
import HepLean.Tensors.Tree.NodeIdentities.Congr
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ContrContr
|
||||
|
|
|
|||
|
|
@ -309,6 +309,19 @@ lemma whiskeringRight_toEquiv (f : X → C) (g : Y → C) (h : Z → C)
|
|||
simp [MonoidalCategory.whiskerLeft]
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma α_hom_toEquiv (f : X → C) (g : Y → C) (h : Z → C) :
|
||||
Hom.toEquiv (α_ (OverColor.mk f) (OverColor.mk g) (OverColor.mk h)).hom =
|
||||
Equiv.sumAssoc X Y Z := by
|
||||
rfl
|
||||
|
||||
@[simp]
|
||||
lemma α_inv_toEquiv (f : X → C) (g : Y → C) (h : Z → C) :
|
||||
Hom.toEquiv (α_ (OverColor.mk f) (OverColor.mk g) (OverColor.mk h)).inv =
|
||||
(Equiv.sumAssoc X Y Z).symm := by
|
||||
rfl
|
||||
|
||||
|
||||
end OverColor
|
||||
|
||||
end IndexNotation
|
||||
|
|
|
|||
|
|
@ -198,6 +198,20 @@ lemma extractTwo_hom_left_apply {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fin n.
|
|||
simp only [extractTwo, extractOne]
|
||||
rfl
|
||||
|
||||
@[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
|
||||
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
|
||||
simp
|
||||
|
||||
/-- Removes a given `i : Fin n.succ.succ` and `j : Fin n.succ` from a morphism in `OverColor C`.
|
||||
This is from and to different (by equivalent) objects to `extractTwo`. -/
|
||||
def extractTwoAux {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
|
||||
|
|
|
|||
|
|
@ -814,6 +814,20 @@ 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):
|
||||
(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))) :
|
||||
(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 = _
|
||||
rw [forgetLiftApp_naturality_eqToHom]
|
||||
rfl
|
||||
|
||||
lemma forgetLiftApp_hom_hom_apply_eq (c : C)
|
||||
(x : (lift.obj F).obj (OverColor.mk (fun (_ : Fin 1) => c)))
|
||||
(y : (F.obj (Discrete.mk c)).V) :
|
||||
|
|
@ -839,6 +853,20 @@ lemma forgetLiftAppCon_inv_apply_expand (c : C) (x : F.obj (Discrete.mk c)) :
|
|||
ModuleCat.coe_comp, Function.comp_apply]
|
||||
rfl
|
||||
|
||||
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
|
||||
simp [mkIso_refl_hom]
|
||||
|
||||
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
|
||||
change ((forgetLiftAppCon F c).hom ≫ F.map (Discrete.eqToHom h)).hom x = _
|
||||
rw [forgetLiftAppCon_naturality_eqToHom]
|
||||
rfl
|
||||
|
||||
informal_definition forgetLift where
|
||||
math :≈ "The natural isomorphism between `lift (C := C) ⋙ forget` and
|
||||
`Functor.id (Discrete C ⥤ Rep k G)`."
|
||||
|
|
|
|||
|
|
@ -556,6 +556,17 @@ 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):
|
||||
(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
|
||||
|
||||
lemma tensorToVec_naturality_eqToHom_apply (c c1 : S.C) (h : c = c1)
|
||||
(x : S.F.obj (OverColor.mk ![c])) :
|
||||
(S.FD.map (Discrete.eqToHom h)).hom ((S.tensorToVec c).hom.hom x) =
|
||||
(S.tensorToVec c1).hom.hom (((S.F.map (OverColor.mkIso (by rw [h])).hom).hom x)) :=
|
||||
forgetLiftAppCon_naturality_eqToHom_apply S.FD c c1 h x
|
||||
|
||||
end TensorSpecies
|
||||
|
||||
end
|
||||
|
|
|
|||
227
HepLean/Tensors/TensorSpecies/DualRepIso.lean
Normal file
227
HepLean/Tensors/TensorSpecies/DualRepIso.lean
Normal file
|
|
@ -0,0 +1,227 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.Tensors.TensorSpecies.Basic
|
||||
import HepLean.Tensors.TensorSpecies.MetricTensor
|
||||
import HepLean.Tensors.Tree.NodeIdentities.Assoc
|
||||
/-!
|
||||
|
||||
# Isomorphism between rep of color `c` and rep of dual color.
|
||||
|
||||
-/
|
||||
|
||||
open IndexNotation
|
||||
open CategoryTheory
|
||||
open MonoidalCategory
|
||||
|
||||
noncomputable section
|
||||
|
||||
namespace TensorSpecies
|
||||
open TensorTree
|
||||
variable (S : TensorSpecies)
|
||||
|
||||
/-- The morphism from `S.FD.obj (Discrete.mk c)` to `S.FD.obj (Discrete.mk (S.τ c))`
|
||||
defined by contracting with the metric. -/
|
||||
def toDualRep (c : S.C) : S.FD.obj (Discrete.mk c) ⟶ S.FD.obj (Discrete.mk (S.τ c)) :=
|
||||
(ρ_ (S.FD.obj (Discrete.mk c))).inv
|
||||
≫ (S.FD.obj { as := c } ◁ (S.metric.app (Discrete.mk (S.τ c))))
|
||||
≫ (α_ (S.FD.obj (Discrete.mk c)) (S.FD.obj (Discrete.mk (S.τ c)))
|
||||
(S.FD.obj (Discrete.mk (S.τ c)))).inv
|
||||
≫ (S.contr.app (Discrete.mk c) ▷ S.FD.obj { as := S.τ c })
|
||||
≫ (λ_ (S.FD.obj (Discrete.mk (S.τ c)))).hom
|
||||
|
||||
/-- The `toDualRep` for equal colors is the same, up-to conjugation by a trivial equivalence. -/
|
||||
lemma toDualRep_congr {c c' : S.C} (h : c = c') : S.toDualRep c = S.FD.map (Discrete.eqToHom h) ≫
|
||||
S.toDualRep c' ≫ S.FD.map (Discrete.eqToHom (congrArg S.τ h.symm)) := by
|
||||
subst h
|
||||
simp only [eqToHom_refl, Discrete.functor_map_id, Category.comp_id, Category.id_comp]
|
||||
|
||||
/-- The morphism from `S.FD.obj (Discrete.mk (S.τ c))` to `S.FD.obj (Discrete.mk c)`
|
||||
defined by contracting with the metric. -/
|
||||
def fromDualRep (c : S.C) : S.FD.obj (Discrete.mk (S.τ c)) ⟶ S.FD.obj (Discrete.mk c) :=
|
||||
S.toDualRep (S.τ c) ≫ S.FD.map (Discrete.eqToHom (S.τ_involution c))
|
||||
|
||||
/-- The rewriting of `toDualRep` in terms of `contrOneTwoLeft`. -/
|
||||
lemma toDualRep_apply_eq_contrOneTwoLeft (c : S.C) (x : S.FD.obj (Discrete.mk c)) :
|
||||
(S.toDualRep c).hom x = (S.tensorToVec (S.τ c)).hom.hom
|
||||
(contrOneTwoLeft (((S.tensorToVec c).inv.hom x))
|
||||
(S.metricTensor (S.τ c))) := by
|
||||
simp only [toDualRep, Monoidal.tensorUnit_obj, Action.comp_hom,
|
||||
Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Action.instMonoidalCategory_rightUnitor_inv_hom, Action.instMonoidalCategory_whiskerLeft_hom,
|
||||
Action.instMonoidalCategory_associator_inv_hom, Action.instMonoidalCategory_whiskerRight_hom,
|
||||
Action.instMonoidalCategory_leftUnitor_hom_hom, ModuleCat.coe_comp, Function.comp_apply,
|
||||
ModuleCat.MonoidalCategory.rightUnitor_inv_apply, ModuleCat.MonoidalCategory.whiskerLeft_apply,
|
||||
Nat.succ_eq_add_one, Nat.reduceAdd, contrOneTwoLeft, Functor.comp_obj,
|
||||
Discrete.functor_obj_eq_as, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, OverColor.Discrete.rep_iso_hom_inv_apply]
|
||||
repeat apply congrArg
|
||||
erw [pairIsoSep_inv_metricTensor]
|
||||
rfl
|
||||
|
||||
/-- Expansion of `toDualRep` is
|
||||
`(S.tensorToVec c).inv.hom x | μ ⊗ S.metricTensor (S.τ c) | μ ν`. -/
|
||||
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
|
||||
simp only
|
||||
rw [toDualRep_apply_eq_contrOneTwoLeft]
|
||||
apply congrArg
|
||||
exact contrOneTwoLeft_tensorTree ((S.tensorToVec c).inv.hom x) (S.metricTensor (S.τ c))
|
||||
|
||||
lemma fromDualRep_tensorTree (c : S.C) (x : S.FD.obj (Discrete.mk (S.τ c))) :
|
||||
let y : S.F.obj (OverColor.mk ![S.τ c]) := (S.tensorToVec (S.τ c)).inv.hom x
|
||||
(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
|
||||
simp only
|
||||
rw [fromDualRep]
|
||||
simp only [Action.comp_hom, ModuleCat.coe_comp, Function.comp_apply, Nat.succ_eq_add_one,
|
||||
Nat.reduceAdd, Fin.isValue, Fin.succAbove_zero]
|
||||
rw [toDualRep_tensorTree]
|
||||
rw [tensorToVec_naturality_eqToHom_apply]
|
||||
apply congrArg
|
||||
conv_lhs =>
|
||||
rw [← perm_tensor]
|
||||
rw [perm_perm]
|
||||
exact perm_congr rfl rfl
|
||||
|
||||
/-- Applying `toDualRep` followed by `fromDualRep` is equivalent to contracting
|
||||
with two metric tensors on the right. -/
|
||||
lemma toDualRep_fromDualRep_tensorTree_metrics (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.fromDualRep c).hom ((S.toDualRep c).hom x) = (S.tensorToVec c).hom.hom
|
||||
({y | μ ⊗ S.metricTensor (S.τ c) | μ ν ⊗ S.metricTensor (S.τ (S.τ c)) | ν σ}ᵀ
|
||||
|> perm (OverColor.equivToHomEq (Equiv.refl _)
|
||||
(fun x => by fin_cases x; exact (S.τ_involution c).symm))).tensor := by
|
||||
rw [toDualRep_tensorTree, fromDualRep_tensorTree]
|
||||
simp only
|
||||
apply congrArg
|
||||
rw [OverColor.Discrete.rep_iso_inv_hom_apply]
|
||||
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_perm]
|
||||
apply perm_congr _ rfl
|
||||
apply OverColor.Hom.fin_ext
|
||||
intro i
|
||||
fin_cases i
|
||||
simp only [OverColor.mk_left, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Fin.succAbove_zero,
|
||||
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, HepLean.Fin.finExtractOnePerm_symm_apply, Category.assoc,
|
||||
OverColor.Hom.hom_comp, Over.comp_left, OverColor.equivToHomEq_hom_left, Equiv.toFun_as_coe,
|
||||
types_comp_apply, OverColor.mkIso_hom_hom_left_apply, OverColor.extractTwo_hom_left_apply,
|
||||
permProdLeft_toEquiv, OverColor.equivToHomEq_toEquiv, Equiv.sumCongr_refl, Equiv.refl_trans,
|
||||
Equiv.symm_trans_self, Equiv.refl_apply, HepLean.Fin.finExtractOne_symm_inr_apply,
|
||||
Fin.zero_succAbove, HepLean.Fin.finExtractOnePerm_apply]
|
||||
decide
|
||||
|
||||
/-- Applying `toDualRep` followed by `fromDualRep` is equivalent to contracting
|
||||
with a unit tensors on the right. -/
|
||||
lemma toDualRep_fromDualRep_tensorTree_unitTensor (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.fromDualRep c).hom ((S.toDualRep c).hom x) = (S.tensorToVec c).hom.hom
|
||||
({y | μ ⊗ S.unitTensor c | μ ν}ᵀ
|
||||
|> perm (OverColor.equivToHomEq (Equiv.refl _)
|
||||
(fun x => by fin_cases x; rfl))).tensor := by
|
||||
rw [toDualRep_fromDualRep_tensorTree_metrics]
|
||||
apply congrArg
|
||||
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_perm_right _ _ _ _]
|
||||
rw [perm_tensor_eq <| perm_contr_congr 0 1 (by simp; rfl) (by simp; 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_perm]
|
||||
refine perm_congr (OverColor.Hom.fin_ext _ _ fun i => ?_) rfl
|
||||
fin_cases i
|
||||
simp only [OverColor.mk_left, Nat.succ_eq_add_one, Nat.reduceAdd, Functor.id_obj,
|
||||
OverColor.mk_hom, Fin.isValue, Fin.succAbove_zero, OverColor.extractOne_homToEquiv,
|
||||
HepLean.Fin.finExtractOnePerm_symm_apply, Category.assoc, OverColor.Hom.hom_comp, Fin.zero_eta,
|
||||
Over.comp_left, OverColor.equivToHomEq_hom_left, Equiv.toFun_as_coe, Equiv.coe_refl,
|
||||
types_comp_apply, OverColor.mkIso_hom_hom_left_apply, OverColor.extractTwo_hom_left_apply,
|
||||
permProdRight_toEquiv, OverColor.equivToHomEq_toEquiv, Equiv.symm_trans_apply, Equiv.symm_symm,
|
||||
Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.sumCongr_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, HepLean.Fin.finExtractOnePerm_apply, Function.comp_apply,
|
||||
HepLean.Fin.finMapToEquiv_symm_apply, Matrix.cons_val_zero]
|
||||
|
||||
lemma toDualRep_fromDualRep_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.fromDualRep c).hom ((S.toDualRep c).hom x) = (S.tensorToVec c).hom.hom
|
||||
({y | μ}ᵀ).tensor := by
|
||||
rw [toDualRep_fromDualRep_tensorTree_unitTensor]
|
||||
apply congrArg
|
||||
conv_lhs =>
|
||||
rw [perm_tensor_eq <| vec_contr_unitTensor_eq_self _]
|
||||
rw [perm_perm]
|
||||
rw [perm_eq_id]
|
||||
|
||||
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))) :
|
||||
(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
|
||||
(((S.FD.map (Discrete.eqToHom _)) ≫ S.FD.map (Discrete.eqToHom _)).hom
|
||||
(((S.toDualRep (S.τ c)).hom x)))) = _
|
||||
rw [← S.FD.map_comp]
|
||||
simp
|
||||
conv_rhs => rw [← S.toDualRep_fromDualRep_eq_self (S.τ c) x]
|
||||
rfl
|
||||
|
||||
/-- The isomorphism between the representation associated with a color, and that associated with
|
||||
its dual. -/
|
||||
def dualRepIsoDiscrete (c : S.C) : S.FD.obj (Discrete.mk c) ≅ S.FD.obj (Discrete.mk (S.τ c)) where
|
||||
hom := S.toDualRep c
|
||||
inv := S.fromDualRep c
|
||||
hom_inv_id := by
|
||||
ext x
|
||||
exact S.toDualRep_fromDualRep_eq_self c x
|
||||
inv_hom_id := by
|
||||
ext x
|
||||
exact S.fromDualRep_toDualRep_eq_self c x
|
||||
|
||||
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."
|
||||
deps :≈ [``dualRepIsoDiscrete]
|
||||
|
||||
informal_lemma dualRepIso_unitTensor_fst where
|
||||
math :≈ "Acting with `dualRepIso` on the fst component of a `unitTensor` returns a metric."
|
||||
deps :≈ [``dualRepIso, ``unitTensor, ``metricTensor]
|
||||
|
||||
informal_lemma dualRepIso_unitTensor_snd where
|
||||
math :≈ "Acting with `dualRepIso` on the snd component of a `unitTensor` returns a metric."
|
||||
deps :≈ [``dualRepIso, ``unitTensor, ``metricTensor]
|
||||
|
||||
informal_lemma dualRepIso_metricTensor_fst where
|
||||
math :≈ "Acting with `dualRepIso` on the fst component of a `metricTensor` returns a unitTensor."
|
||||
deps :≈ [``dualRepIso, ``unitTensor, ``metricTensor]
|
||||
|
||||
informal_lemma dualRepIso_metricTensor_snd where
|
||||
math :≈ "Acting with `dualRepIso` on the snd component of a `metricTensor` returns a unitTensor."
|
||||
deps :≈ [``dualRepIso, ``unitTensor, ``metricTensor]
|
||||
|
||||
end TensorSpecies
|
||||
|
||||
end
|
||||
|
|
@ -1,88 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.Tensors.TensorSpecies.Basic
|
||||
import HepLean.Tensors.TensorSpecies.MetricTensor
|
||||
/-!
|
||||
|
||||
# Isomorphism between rep of color `c` and rep of dual color.
|
||||
|
||||
-/
|
||||
|
||||
open IndexNotation
|
||||
open CategoryTheory
|
||||
open MonoidalCategory
|
||||
|
||||
noncomputable section
|
||||
|
||||
namespace TensorSpecies
|
||||
open TensorTree
|
||||
variable (S : TensorSpecies)
|
||||
|
||||
/-- The morphism from `S.FD.obj (Discrete.mk c)` to `S.FD.obj (Discrete.mk (S.τ c))`
|
||||
defined by contracting with the metric. -/
|
||||
def toDualRep (c : S.C) : S.FD.obj (Discrete.mk c) ⟶ S.FD.obj (Discrete.mk (S.τ c)) :=
|
||||
(ρ_ (S.FD.obj (Discrete.mk c))).inv
|
||||
≫ (S.FD.obj { as := c } ◁ (S.metric.app (Discrete.mk (S.τ c))))
|
||||
≫ (α_ (S.FD.obj (Discrete.mk c)) (S.FD.obj (Discrete.mk (S.τ c)))
|
||||
(S.FD.obj (Discrete.mk (S.τ c)))).inv
|
||||
≫ (S.contr.app (Discrete.mk c) ▷ S.FD.obj { as := S.τ c })
|
||||
≫ (λ_ (S.FD.obj (Discrete.mk (S.τ c)))).hom
|
||||
|
||||
/-- The `toDualRep` for equal colors is the same, up-to conjugation by a trivial equivalence. -/
|
||||
lemma toDualRep_congr {c c' : S.C} (h : c = c') : S.toDualRep c = S.FD.map (Discrete.eqToHom h) ≫
|
||||
S.toDualRep c' ≫ S.FD.map (Discrete.eqToHom (congrArg S.τ h.symm)) := by
|
||||
subst h
|
||||
simp only [eqToHom_refl, Discrete.functor_map_id, Category.comp_id, Category.id_comp]
|
||||
|
||||
/-- The morphism from `S.FD.obj (Discrete.mk (S.τ c))` to `S.FD.obj (Discrete.mk c)`
|
||||
defined by contracting with the metric. -/
|
||||
def fromDualRep (c : S.C) : S.FD.obj (Discrete.mk (S.τ c)) ⟶ S.FD.obj (Discrete.mk c) :=
|
||||
S.toDualRep (S.τ c) ≫ S.FD.map (Discrete.eqToHom (S.τ_involution c))
|
||||
|
||||
/-- The rewriting of `toDualRep` in terms of `contrOneTwoLeft`. -/
|
||||
lemma toDualRep_apply_eq_contrOneTwoLeft (c : S.C) (x : S.FD.obj (Discrete.mk c)) :
|
||||
(S.toDualRep c).hom x = (S.tensorToVec (S.τ c)).hom.hom
|
||||
(contrOneTwoLeft (((S.tensorToVec c).inv.hom x))
|
||||
(S.metricTensor (S.τ c))) := by
|
||||
simp only [toDualRep, Monoidal.tensorUnit_obj, Action.comp_hom,
|
||||
Action.instMonoidalCategory_tensorObj_V, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Action.instMonoidalCategory_rightUnitor_inv_hom, Action.instMonoidalCategory_whiskerLeft_hom,
|
||||
Action.instMonoidalCategory_associator_inv_hom, Action.instMonoidalCategory_whiskerRight_hom,
|
||||
Action.instMonoidalCategory_leftUnitor_hom_hom, ModuleCat.coe_comp, Function.comp_apply,
|
||||
ModuleCat.MonoidalCategory.rightUnitor_inv_apply, ModuleCat.MonoidalCategory.whiskerLeft_apply,
|
||||
Nat.succ_eq_add_one, Nat.reduceAdd, contrOneTwoLeft, Functor.comp_obj,
|
||||
Discrete.functor_obj_eq_as, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, OverColor.Discrete.rep_iso_hom_inv_apply]
|
||||
repeat apply congrArg
|
||||
erw [pairIsoSep_inv_metricTensor]
|
||||
rfl
|
||||
|
||||
/-- Expansion of `toDualRep` is
|
||||
`(S.tensorToVec c).inv.hom x | μ ⊗ S.metricTensor (S.τ c) | μ ν`. -/
|
||||
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
|
||||
simp only
|
||||
rw [toDualRep_apply_eq_contrOneTwoLeft]
|
||||
apply congrArg
|
||||
exact contrOneTwoLeft_tensorTree ((S.tensorToVec c).inv.hom x) (S.metricTensor (S.τ c))
|
||||
|
||||
lemma fromDualRep_tensorTree (c : S.C) (x : S.FD.obj (Discrete.mk (S.τ c))) :
|
||||
let y : S.F.obj (OverColor.mk ![S.τ c]) := (S.tensorToVec (S.τ c)).inv.hom x
|
||||
(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
|
||||
simp only
|
||||
rw [fromDualRep]
|
||||
simp only [Action.comp_hom, ModuleCat.coe_comp, Function.comp_apply, Nat.succ_eq_add_one,
|
||||
Nat.reduceAdd, Fin.isValue, Fin.succAbove_zero]
|
||||
rw [toDualRep_tensorTree]
|
||||
|
||||
end TensorSpecies
|
||||
|
||||
end
|
||||
102
HepLean/Tensors/Tree/NodeIdentities/Assoc.lean
Normal file
102
HepLean/Tensors/Tree/NodeIdentities/Assoc.lean
Normal file
|
|
@ -0,0 +1,102 @@
|
|||
/-
|
||||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.Tensors.Tree.Elab
|
||||
import HepLean.Tensors.Tree.NodeIdentities.Basic
|
||||
import HepLean.Tensors.Tree.NodeIdentities.Congr
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ProdComm
|
||||
import HepLean.Tensors.Tree.NodeIdentities.PermProd
|
||||
import HepLean.Tensors.Tree.NodeIdentities.PermContr
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ProdContr
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ContrContr
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ProdAssoc
|
||||
import HepLean.Tensors.TensorSpecies.ContractLemmas
|
||||
/-!
|
||||
|
||||
## Specific associativity results for tensor trees
|
||||
|
||||
-/
|
||||
|
||||
open IndexNotation
|
||||
open CategoryTheory
|
||||
open MonoidalCategory
|
||||
open OverColor
|
||||
open HepLean.Fin
|
||||
open TensorProduct
|
||||
|
||||
namespace TensorTree
|
||||
|
||||
variable {S : TensorSpecies}
|
||||
|
||||
set_option maxRecDepth 2000 in
|
||||
/-- The associativity lemma for `t1 | μ ⊗ t2 | μ ν ⊗ t3 | ν σ`. -/
|
||||
lemma assoc_one_two_two {c1 c2 c3 : S.C} (t1 : S.F.obj (OverColor.mk ![c1]))
|
||||
(t2 : S.F.obj (OverColor.mk ![S.τ c1, c2])) (t3 : S.F.obj (OverColor.mk ![S.τ c2, c3])) :
|
||||
{t1 | μ ⊗ t2 | μ ν ⊗ t3 | ν σ}ᵀ.tensor = ({t1 | μ ⊗ (t2 | μ ν ⊗ t3 | ν σ)}ᵀ
|
||||
|> perm (OverColor.equivToHomEq (Equiv.refl (Fin 1)) (by
|
||||
intro x
|
||||
fin_cases x
|
||||
rfl))).tensor := by
|
||||
conv_lhs =>
|
||||
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' _ _ _ _ _ _ ]
|
||||
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)]
|
||||
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,
|
||||
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,
|
||||
Equiv.coe_refl, finExtractOnePerm_symm_apply, Equiv.trans_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, finExtractOnePerm_apply,
|
||||
Equiv.refl_apply]
|
||||
decide) (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]
|
||||
rw [extractOne_homToEquiv]
|
||||
simp only [Hom.toEquiv_comp, extractTwo_toEquiv, assocPerm_toHomEquiv_inv,
|
||||
ContrPair.leftContrI, ContrPair.leftContrJ, ContrPair.leftContr]
|
||||
simp only [mk_left,
|
||||
extractOne_homToEquiv, Hom.toEquiv_comp, equivToIso_homToEquiv, Equiv.symm_trans_apply,
|
||||
finExtractOnePerm_symm_apply, Equiv.trans_apply, equivToIso_mkIso_hom,
|
||||
Equiv.symm_apply_apply, Equiv.symm_symm, Equiv.sumCongr_symm, Equiv.refl_symm,
|
||||
Equiv.sumCongr_apply, Equiv.coe_refl, 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, Equiv.refl_trans, finExtractOnePerm_apply]
|
||||
decide)]
|
||||
rw [perm_perm]
|
||||
rw [perm_tensor_eq <| contr_contr _ _ _]
|
||||
rw [perm_perm]
|
||||
conv_rhs =>
|
||||
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
|
||||
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 [contrContrPerm_hom_left_apply]
|
||||
decide
|
||||
|
||||
|
||||
|
||||
end TensorTree
|
||||
|
|
@ -40,6 +40,16 @@ informal_lemma constTwoNode_eq_twoNode where
|
|||
|
||||
/-!
|
||||
|
||||
## Tensornode
|
||||
|
||||
-/
|
||||
|
||||
/-- The tenor node of a tensor tree's tensor has a tensor which is the tensor tree's tensor. -/
|
||||
lemma tensorNode_of_tree (t : TensorTree S c) : (tensorNode t.tensor).tensor = t.tensor := by
|
||||
simp [tensorNode]
|
||||
|
||||
/-!
|
||||
|
||||
## Negation
|
||||
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -296,6 +296,14 @@ def contrContrPerm {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} {i : Fin n.
|
|||
((c ∘ i.succAbove ∘ j.succAbove) ∘ k.succAbove ∘ l.succAbove) :=
|
||||
(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}
|
||||
{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):
|
||||
(contrContrPerm hij hkl).hom.left x = x := by
|
||||
simp [contrContrPerm, ContrQuartet.contrSwapHom]
|
||||
|
||||
/-- Contraction nodes commute on adjusting indices. -/
|
||||
theorem contr_contr {n : ℕ} {c : Fin n.succ.succ.succ.succ → S.C} {i : Fin n.succ.succ.succ.succ}
|
||||
{j : Fin n.succ.succ.succ} {k : Fin n.succ.succ} {l : Fin n.succ}
|
||||
|
|
|
|||
|
|
@ -43,6 +43,20 @@ lemma finSumFinEquiv_comp_assocPerm :
|
|||
rw [assocPerm]
|
||||
simp
|
||||
|
||||
@[simp]
|
||||
lemma assocPerm_toHomEquiv_hom : Hom.toEquiv (assocPerm c c2 c3).hom = finSumFinEquiv.symm.trans
|
||||
((finSumFinEquiv.symm.sumCongr (Equiv.refl (Fin n3))).trans
|
||||
((Equiv.sumAssoc (Fin n) (Fin n2) (Fin n3)).trans
|
||||
(((Equiv.refl (Fin n)).sumCongr finSumFinEquiv).trans finSumFinEquiv))) := by
|
||||
simp [assocPerm]
|
||||
|
||||
@[simp]
|
||||
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
|
||||
simp [assocPerm]
|
||||
|
||||
/-- The `prod` obeys associativity. -/
|
||||
theorem prod_assoc (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree S c3) :
|
||||
(prod t (prod t2 t3)).tensor = (perm (assocPerm c c2 c3).hom (prod (prod t t2) t3)).tensor := by
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue