feat: General properties of contractions
This commit is contained in:
jstoobysmith
parent
dcf6b774d4
commit
9b4cd5d0b8
10 changed files with 366 additions and 269 deletions
|
|
@ -125,7 +125,9 @@ import HepLean.Tensors.OverColor.Functors
|
|||
import HepLean.Tensors.OverColor.Iso
|
||||
import HepLean.Tensors.OverColor.Lift
|
||||
import HepLean.Tensors.TensorSpecies.Basic
|
||||
import HepLean.Tensors.TensorSpecies.ContractLemmas
|
||||
import HepLean.Tensors.TensorSpecies.Contractions.Basic
|
||||
import HepLean.Tensors.TensorSpecies.Contractions.Categorical
|
||||
import HepLean.Tensors.TensorSpecies.Contractions.ContrMap
|
||||
import HepLean.Tensors.TensorSpecies.DualRepIso
|
||||
import HepLean.Tensors.TensorSpecies.MetricTensor
|
||||
import HepLean.Tensors.TensorSpecies.UnitTensor
|
||||
|
|
|
|||
|
|
@ -421,7 +421,7 @@ lemma on_basis (μ ν : Fin 1 ⊕ Fin d) : ⟪ContrMod.stdBasis μ, ContrMod.std
|
|||
mul_zero, off_diag_zero]
|
||||
|
||||
lemma matrix_apply_stdBasis (ν μ : Fin 1 ⊕ Fin d) :
|
||||
Λ ν μ = η ν ν * ⟪ ContrMod.stdBasis ν, Λ *ᵥ ContrMod.stdBasis μ⟫ₘ := by
|
||||
Λ ν μ = η ν ν * ⟪ContrMod.stdBasis ν, Λ *ᵥ ContrMod.stdBasis μ⟫ₘ := by
|
||||
rw [on_basis_mulVec, ← mul_assoc]
|
||||
simp [η_apply_mul_η_apply_diag ν]
|
||||
|
||||
|
|
|
|||
|
|
@ -131,155 +131,6 @@ lemma perm_contr_cond {n : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n.succ.s
|
|||
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.FD`. -/
|
||||
def contrFin1Fin1 {n : ℕ} (c : Fin n.succ.succ → S.C)
|
||||
(i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) :
|
||||
S.F.obj (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) ≅
|
||||
(OverColor.Discrete.pairτ S.FD S.τ).obj { as := c i } := by
|
||||
apply (S.F.mapIso
|
||||
(OverColor.mkSum (((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)))).trans
|
||||
apply (S.F.μIso _ _).symm.trans
|
||||
apply tensorIso ?_ ?_
|
||||
· symm
|
||||
apply (OverColor.forgetLiftApp S.FD (c i)).symm.trans
|
||||
apply S.F.mapIso
|
||||
apply OverColor.mkIso
|
||||
funext x
|
||||
fin_cases x
|
||||
rfl
|
||||
· symm
|
||||
apply (OverColor.forgetLiftApp S.FD (S.τ (c i))).symm.trans
|
||||
apply S.F.mapIso
|
||||
apply OverColor.mkIso
|
||||
funext x
|
||||
fin_cases x
|
||||
simp [h]
|
||||
|
||||
lemma contrFin1Fin1_inv_tmul {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 : S.FD.obj { as := c i })
|
||||
(y : S.FD.obj { as := S.τ (c i) }) :
|
||||
(S.contrFin1Fin1 c i j h).inv.hom (x ⊗ₜ[S.k] y) =
|
||||
PiTensorProduct.tprod S.k (fun k =>
|
||||
match k with | Sum.inl 0 => x | Sum.inr 0 => (S.FD.map
|
||||
(eqToHom (by simp [h]))).hom y) := by
|
||||
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 _ => c i) (OverColor.mk fun _ => S.τ (c i))).hom
|
||||
((((OverColor.forgetLiftApp S.FD (c i)).inv.hom x) ⊗ₜ[S.k]
|
||||
((OverColor.forgetLiftApp S.FD (S.τ (c i))).inv.hom y))))) = _
|
||||
simp only [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse,
|
||||
Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
|
||||
forgetLiftApp, Action.mkIso_inv_hom, LinearEquiv.toModuleIso_inv, Fin.isValue]
|
||||
erw [OverColor.forgetLiftAppV_symm_apply,
|
||||
OverColor.forgetLiftAppV_symm_apply S.FD (S.τ (c i))]
|
||||
change ((OverColor.lift.obj S.FD).map (OverColor.mkSum
|
||||
((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
|
||||
(((OverColor.lift.obj S.FD).map ((OverColor.mkIso _).hom ⊗ (OverColor.mkIso _).hom)).hom
|
||||
(((OverColor.lift.obj S.FD).μ (OverColor.mk fun _ => c i)
|
||||
(OverColor.mk fun _ => S.τ (c i))).hom
|
||||
(((PiTensorProduct.tprod S.k) fun _ => x) ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) fun _ => y))) = _
|
||||
rw [OverColor.lift.obj_μ_tprod_tmul S.FD]
|
||||
change ((OverColor.lift.obj S.FD).map
|
||||
(OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
|
||||
(((OverColor.lift.obj S.FD).map ((OverColor.mkIso _).hom ⊗ (OverColor.mkIso _).hom)).hom
|
||||
((PiTensorProduct.tprod S.k) _)) = _
|
||||
rw [OverColor.lift.map_tprod S.FD]
|
||||
change ((OverColor.lift.obj S.FD).map
|
||||
(OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
|
||||
((PiTensorProduct.tprod S.k _)) = _
|
||||
rw [OverColor.lift.map_tprod S.FD]
|
||||
apply congrArg
|
||||
funext r
|
||||
match r with
|
||||
| Sum.inl 0 =>
|
||||
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 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)
|
||||
(i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i))
|
||||
(x : (k : Fin 1 ⊕ Fin 1) → (S.FD.obj
|
||||
{ as := (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).hom k })) :
|
||||
(S.contrFin1Fin1 c i j h).hom.hom (PiTensorProduct.tprod S.k x) =
|
||||
x (Sum.inl 0) ⊗ₜ[S.k] ((S.FD.map (eqToHom (by simp [h]))).hom (x (Sum.inr 0))) := by
|
||||
change ((Action.forget _ _).mapIso (S.contrFin1Fin1 c i j h)).hom _ = _
|
||||
trans ((Action.forget _ _).mapIso (S.contrFin1Fin1 c i j h)).toLinearEquiv
|
||||
(PiTensorProduct.tprod S.k x)
|
||||
· rfl
|
||||
erw [← LinearEquiv.eq_symm_apply]
|
||||
erw [contrFin1Fin1_inv_tmul]
|
||||
congr
|
||||
funext i
|
||||
match i with
|
||||
| Sum.inl 0 =>
|
||||
rfl
|
||||
| Sum.inr 0 =>
|
||||
simp only [Nat.succ_eq_add_one, Fin.isValue, mk_hom, Function.comp_apply,
|
||||
Discrete.functor_obj_eq_as]
|
||||
change _ = ((S.FD.map (eqToHom _)) ≫ (S.FD.map (eqToHom _))).hom (x (Sum.inr 0))
|
||||
rw [← Functor.map_comp]
|
||||
simp
|
||||
exact h
|
||||
|
||||
/-- The isomorphism of objects in `Rep S.k S.G` given an `i` in `Fin n.succ.succ` and
|
||||
a `j` in `Fin n.succ` allowing us to undertake contraction. -/
|
||||
def contrIso {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) ≅ ((OverColor.Discrete.pairτ S.FD S.τ).obj
|
||||
(Discrete.mk (c i))) ⊗
|
||||
(OverColor.lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) :=
|
||||
(S.F.mapIso (OverColor.equivToIso (HepLean.Fin.finExtractTwo i j))).trans <|
|
||||
(S.F.mapIso (OverColor.mkSum (c ∘ (HepLean.Fin.finExtractTwo i j).symm))).trans <|
|
||||
(S.F.μIso _ _).symm.trans <| by
|
||||
refine tensorIso (S.contrFin1Fin1 c i j h) (S.F.mapIso (OverColor.mkIso (by ext x; simp)))
|
||||
|
||||
lemma contrIso_hom_hom {n : ℕ} {c1 : Fin n.succ.succ → S.C}
|
||||
{i : Fin n.succ.succ} {j : Fin n.succ} {h : c1 (i.succAbove j) = S.τ (c1 i)} :
|
||||
(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
|
||||
rfl
|
||||
|
||||
/-- `contrMap` is a function that takes a natural number `n`, a function `c` from
|
||||
`Fin n.succ.succ` to `S.C`, an index `i` of type `Fin n.succ.succ`, an index `j` of type
|
||||
`Fin n.succ`, and a proof `h` that `c (i.succAbove j) = S.τ (c i)`. It returns a morphism
|
||||
corresponding to the contraction of the `i`th index with the `i.succAbove j` index.
|
||||
--/
|
||||
def contrMap {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) ⟶
|
||||
S.F.obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) :=
|
||||
(S.contrIso c i j h).hom ≫
|
||||
(tensorHom (S.contr.app (Discrete.mk (c i))) (𝟙 _)) ≫
|
||||
(MonoidalCategory.leftUnitor _).hom
|
||||
|
||||
/-- Casts an element of the monoidal unit of `Rep S.k S.G` to the field `S.k`. -/
|
||||
def castToField (v : (↑((𝟙_ (Discrete S.C ⥤ Rep S.k S.G)).obj { as := c }).V)) : S.k := v
|
||||
|
||||
|
|
@ -294,120 +145,6 @@ lemma castFin0ToField_tprod {c : Fin 0 → S.C}
|
|||
simp only [castFin0ToField, mk_hom, Functor.id_obj, LinearEquiv.coe_coe]
|
||||
erw [PiTensorProduct.isEmptyEquiv_apply_tprod]
|
||||
|
||||
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.FD.obj (Discrete.mk (c i))) :
|
||||
(S.contrMap c i j h).hom (PiTensorProduct.tprod S.k x) =
|
||||
(S.castToField ((S.contr.app (Discrete.mk (c i))).hom ((x i) ⊗ₜ[S.k]
|
||||
(S.FD.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,
|
||||
tensorIso_hom, Monoidal.tensorUnit_obj, tensorHom_id,
|
||||
Category.assoc, Action.comp_hom, Action.instMonoidalCategory_tensorObj_V,
|
||||
Action.instMonoidalCategory_tensorHom_hom, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Action.instMonoidalCategory_whiskerRight_hom, Functor.id_obj, mk_hom, ModuleCat.coe_comp,
|
||||
Function.comp_apply, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, Functor.comp_obj, Discrete.functor_obj_eq_as]
|
||||
change (λ_ ((lift.obj S.FD).obj _)).hom.hom
|
||||
(((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FD).obj
|
||||
(OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
|
||||
(((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FD).map (mkIso _).hom).hom)
|
||||
(((lift.obj S.FD).μIso (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)
|
||||
∘ Sum.inl))
|
||||
(OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom
|
||||
(((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom
|
||||
(((lift.obj S.FD).map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom
|
||||
((PiTensorProduct.tprod S.k) x)))))) = _
|
||||
rw [lift.map_tprod]
|
||||
change (λ_ ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)))).hom.hom
|
||||
(((S.contr.app { as := c i }).hom ▷
|
||||
((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
|
||||
(((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FD).map (mkIso _).hom).hom)
|
||||
(((lift.obj S.FD).μIso (OverColor.mk
|
||||
((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
|
||||
(OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom
|
||||
(((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom
|
||||
((PiTensorProduct.tprod S.k) fun i_1 =>
|
||||
(lift.discreteFunctorMapEqIso S.FD _)
|
||||
(x ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm i_1))))))) = _
|
||||
rw [lift.map_tprod]
|
||||
change (λ_ ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)))).hom.hom
|
||||
(((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FD).obj
|
||||
(OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
|
||||
(((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FD).map (mkIso _).hom).hom)
|
||||
(((lift.obj S.FD).μIso
|
||||
(OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
|
||||
(OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom
|
||||
((PiTensorProduct.tprod S.k) fun i_1 =>
|
||||
(lift.discreteFunctorMapEqIso S.FD _)
|
||||
((lift.discreteFunctorMapEqIso S.FD _)
|
||||
(x ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm
|
||||
((Hom.toEquiv (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).symm i_1)))))))) = _
|
||||
rw [lift.μIso_inv_tprod]
|
||||
change (λ_ ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)))).hom.hom
|
||||
(((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FD).obj
|
||||
(OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
|
||||
((TensorProduct.map (S.contrFin1Fin1 c i j h).hom.hom
|
||||
((lift.obj S.FD).map (mkIso _).hom).hom)
|
||||
(((PiTensorProduct.tprod S.k) fun i_1 =>
|
||||
(lift.discreteFunctorMapEqIso S.FD _)
|
||||
((lift.discreteFunctorMapEqIso S.FD _) (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.FD _) ((lift.discreteFunctorMapEqIso S.FD _)
|
||||
(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,
|
||||
Action.instMonoidalCategory_tensorUnit_V, Fin.isValue, mk_hom, Function.comp_apply,
|
||||
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 only [Monoidal.tensorUnit_obj, Action.instMonoidalCategory_tensorUnit_V, Fin.isValue,
|
||||
ModuleCat.MonoidalCategory.leftUnitor_hom_apply]
|
||||
congr 1
|
||||
/- The contraction. -/
|
||||
· simp only [Fin.isValue, castToField]
|
||||
congr 2
|
||||
· 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 only [Fin.isValue, lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl,
|
||||
Iso.refl_hom, Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
|
||||
change (S.FD.map (eqToHom _)).hom
|
||||
(x (((HepLean.Fin.finExtractTwo i j)).symm ((Sum.inl (Sum.inr 0))))) = _
|
||||
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.FD.map (Discrete.eqToHom (h))).hom (x d) =
|
||||
(S.FD.map (Discrete.eqToHom h')).hom (x b) := by
|
||||
subst hbd
|
||||
rfl
|
||||
refine h1' ?_ ?_ ?_
|
||||
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 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.FD.map (eqToHom _)).hom
|
||||
((x ((HepLean.Fin.finExtractTwo i j).symm (Sum.inr (d))))) = _
|
||||
simp only [Nat.succ_eq_add_one]
|
||||
have h1 : ((HepLean.Fin.finExtractTwo i j).symm (Sum.inr d))
|
||||
= (i.succAbove (j.succAbove d)) := HepLean.Fin.finExtractTwo_symm_inr_apply i j d
|
||||
have h1' {a b : Fin n.succ.succ} (h : a = b) :
|
||||
(S.FD.map (eqToHom (by rw [h]))).hom (x a) = x b := by
|
||||
subst h
|
||||
simp
|
||||
exact h1' h1
|
||||
|
||||
/-!
|
||||
|
||||
## Evalutation of indices.
|
||||
|
|
|
|||
63
HepLean/Tensors/TensorSpecies/Contractions/Basic.lean
Normal file
63
HepLean/Tensors/TensorSpecies/Contractions/Basic.lean
Normal file
|
|
@ -0,0 +1,63 @@
|
|||
/-
|
||||
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.DualRepIso
|
||||
/-!
|
||||
|
||||
# Contraction of vectors
|
||||
|
||||
This file is down stream of `TensorTree`.
|
||||
There are other files in `TensorSpecies.Contractions` which are up-stream of `TensorTree`.
|
||||
|
||||
-/
|
||||
|
||||
open IndexNotation
|
||||
open CategoryTheory
|
||||
open MonoidalCategory
|
||||
|
||||
noncomputable section
|
||||
|
||||
namespace TensorSpecies
|
||||
open TensorTree
|
||||
variable (S : TensorSpecies)
|
||||
|
||||
/-- The equivariant map from ` S.FD.obj (Discrete.mk c) ⊗ S.FD.obj (Discrete.mk c)` to
|
||||
the underlying field obtained by contracting. -/
|
||||
def contractSelfHom (c : S.C) : S.FD.obj (Discrete.mk c) ⊗ S.FD.obj (Discrete.mk c) ⟶
|
||||
𝟙_ (Rep S.k S.G) :=
|
||||
(S.FD.obj (Discrete.mk c) ◁ (S.dualRepIsoDiscrete c).hom) ≫ S.contr.app (Discrete.mk c)
|
||||
|
||||
open TensorProduct
|
||||
|
||||
/-- The contraction of two vectors in a tensor species of the same color, as a linear
|
||||
map to the underlying field. -/
|
||||
def contractSelfField {S : TensorSpecies} {c : S.C} :
|
||||
S.FD.obj (Discrete.mk c) ⊗[S.k] S.FD.obj (Discrete.mk c) →ₗ[S.k] S.k :=
|
||||
(S.contractSelfHom c).hom
|
||||
|
||||
/-- Notation for `coCoContract` acting on a tmul. -/
|
||||
scoped[TensorSpecies] notation "⟪" ψ "," φ "⟫ₜₛ" => contractSelfField (ψ ⊗ₜ φ)
|
||||
|
||||
/-- The map `contractSelfField` is equivariant with respect to the group action. -/
|
||||
@[simp]
|
||||
lemma contractSelfField_equivariant {S : TensorSpecies} {c : S.C} {g : S.G}
|
||||
(ψ : S.FD.obj (Discrete.mk c)) (φ : S.FD.obj (Discrete.mk c)) :
|
||||
⟪(S.FD.obj (Discrete.mk c)).ρ g ψ, (S.FD.obj (Discrete.mk c)).ρ g φ⟫ₜₛ = ⟪ψ, φ⟫ₜₛ := by
|
||||
simpa using congrFun (congrArg (fun x => x.toFun) ((S.contractSelfHom c).comm g )) (ψ ⊗ₜ[S.k] φ)
|
||||
|
||||
informal_lemma contractSelfField_non_degenerate where
|
||||
math :≈ "The contraction of two vectors of the same color is non-degenerate.
|
||||
I.e. ⟪ψ, φ⟫ₜₛ = 0 for all φ implies ψ = 0."
|
||||
deps :≈ [``contractSelfField]
|
||||
|
||||
/-- A vector satisfies `IsNormOne` if it has norm equal to one, i.e. if `⟪ψ, ψ⟫ₜₛ = 1`. -/
|
||||
def IsNormOne {c : S.C} (ψ : S.FD.obj (Discrete.mk c)) : Prop := ⟪ψ, ψ⟫ₜₛ = 1
|
||||
|
||||
/-- A vector satisfies `IsNormZero` if it has norm equal to zero, i.e. if `⟪ψ, ψ⟫ₜₛ = 0`. -/
|
||||
def IsNormZero {c : S.C} (ψ : S.FD.obj (Discrete.mk c)) : Prop := ⟪ψ, ψ⟫ₜₛ = 0
|
||||
|
||||
end TensorSpecies
|
||||
|
||||
end
|
||||
|
|
@ -10,6 +10,9 @@ import HepLean.Tensors.Tree.NodeIdentities.Congr
|
|||
|
||||
## Contraction of specific tensor types
|
||||
|
||||
In this file we expand some contractions of given tensors in terms of
|
||||
basic categorical properties of the tensor species.
|
||||
|
||||
-/
|
||||
|
||||
open IndexNotation
|
||||
292
HepLean/Tensors/TensorSpecies/Contractions/ContrMap.lean
Normal file
292
HepLean/Tensors/TensorSpecies/Contractions/ContrMap.lean
Normal file
|
|
@ -0,0 +1,292 @@
|
|||
/-
|
||||
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
|
||||
/-!
|
||||
|
||||
## The contraction map
|
||||
|
||||
-/
|
||||
|
||||
open IndexNotation
|
||||
open CategoryTheory
|
||||
open MonoidalCategory
|
||||
open OverColor
|
||||
open HepLean.Fin
|
||||
open TensorProduct
|
||||
noncomputable section
|
||||
|
||||
namespace TensorSpecies
|
||||
|
||||
variable (S : TensorSpecies)
|
||||
|
||||
|
||||
/-- 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.FD`. -/
|
||||
def contrFin1Fin1 {n : ℕ} (c : Fin n.succ.succ → S.C)
|
||||
(i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i)) :
|
||||
S.F.obj (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)) ≅
|
||||
(OverColor.Discrete.pairτ S.FD S.τ).obj { as := c i } := by
|
||||
apply (S.F.mapIso
|
||||
(OverColor.mkSum (((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)))).trans
|
||||
apply (S.F.μIso _ _).symm.trans
|
||||
apply tensorIso ?_ ?_
|
||||
· symm
|
||||
apply (OverColor.forgetLiftApp S.FD (c i)).symm.trans
|
||||
apply S.F.mapIso
|
||||
apply OverColor.mkIso
|
||||
funext x
|
||||
fin_cases x
|
||||
rfl
|
||||
· symm
|
||||
apply (OverColor.forgetLiftApp S.FD (S.τ (c i))).symm.trans
|
||||
apply S.F.mapIso
|
||||
apply OverColor.mkIso
|
||||
funext x
|
||||
fin_cases x
|
||||
simp [h]
|
||||
|
||||
lemma contrFin1Fin1_inv_tmul {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 : S.FD.obj { as := c i })
|
||||
(y : S.FD.obj { as := S.τ (c i) }) :
|
||||
(S.contrFin1Fin1 c i j h).inv.hom (x ⊗ₜ[S.k] y) =
|
||||
PiTensorProduct.tprod S.k (fun k =>
|
||||
match k with | Sum.inl 0 => x | Sum.inr 0 => (S.FD.map
|
||||
(eqToHom (by simp [h]))).hom y) := by
|
||||
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 _ => c i) (OverColor.mk fun _ => S.τ (c i))).hom
|
||||
((((OverColor.forgetLiftApp S.FD (c i)).inv.hom x) ⊗ₜ[S.k]
|
||||
((OverColor.forgetLiftApp S.FD (S.τ (c i))).inv.hom y))))) = _
|
||||
simp only [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse,
|
||||
Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
|
||||
forgetLiftApp, Action.mkIso_inv_hom, LinearEquiv.toModuleIso_inv, Fin.isValue]
|
||||
erw [OverColor.forgetLiftAppV_symm_apply,
|
||||
OverColor.forgetLiftAppV_symm_apply S.FD (S.τ (c i))]
|
||||
change ((OverColor.lift.obj S.FD).map (OverColor.mkSum
|
||||
((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
|
||||
(((OverColor.lift.obj S.FD).map ((OverColor.mkIso _).hom ⊗ (OverColor.mkIso _).hom)).hom
|
||||
(((OverColor.lift.obj S.FD).μ (OverColor.mk fun _ => c i)
|
||||
(OverColor.mk fun _ => S.τ (c i))).hom
|
||||
(((PiTensorProduct.tprod S.k) fun _ => x) ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) fun _ => y))) = _
|
||||
rw [OverColor.lift.obj_μ_tprod_tmul S.FD]
|
||||
change ((OverColor.lift.obj S.FD).map
|
||||
(OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
|
||||
(((OverColor.lift.obj S.FD).map ((OverColor.mkIso _).hom ⊗ (OverColor.mkIso _).hom)).hom
|
||||
((PiTensorProduct.tprod S.k) _)) = _
|
||||
rw [OverColor.lift.map_tprod S.FD]
|
||||
change ((OverColor.lift.obj S.FD).map
|
||||
(OverColor.mkSum ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).inv).hom
|
||||
((PiTensorProduct.tprod S.k _)) = _
|
||||
rw [OverColor.lift.map_tprod S.FD]
|
||||
apply congrArg
|
||||
funext r
|
||||
match r with
|
||||
| Sum.inl 0 =>
|
||||
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 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)
|
||||
(i : Fin n.succ.succ) (j : Fin n.succ) (h : c (i.succAbove j) = S.τ (c i))
|
||||
(x : (k : Fin 1 ⊕ Fin 1) → (S.FD.obj
|
||||
{ as := (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl)).hom k })) :
|
||||
(S.contrFin1Fin1 c i j h).hom.hom (PiTensorProduct.tprod S.k x) =
|
||||
x (Sum.inl 0) ⊗ₜ[S.k] ((S.FD.map (eqToHom (by simp [h]))).hom (x (Sum.inr 0))) := by
|
||||
change ((Action.forget _ _).mapIso (S.contrFin1Fin1 c i j h)).hom _ = _
|
||||
trans ((Action.forget _ _).mapIso (S.contrFin1Fin1 c i j h)).toLinearEquiv
|
||||
(PiTensorProduct.tprod S.k x)
|
||||
· rfl
|
||||
erw [← LinearEquiv.eq_symm_apply]
|
||||
erw [contrFin1Fin1_inv_tmul]
|
||||
congr
|
||||
funext i
|
||||
match i with
|
||||
| Sum.inl 0 =>
|
||||
rfl
|
||||
| Sum.inr 0 =>
|
||||
simp only [Nat.succ_eq_add_one, Fin.isValue, mk_hom, Function.comp_apply,
|
||||
Discrete.functor_obj_eq_as]
|
||||
change _ = ((S.FD.map (eqToHom _)) ≫ (S.FD.map (eqToHom _))).hom (x (Sum.inr 0))
|
||||
rw [← Functor.map_comp]
|
||||
simp
|
||||
exact h
|
||||
|
||||
/-- The isomorphism of objects in `Rep S.k S.G` given an `i` in `Fin n.succ.succ` and
|
||||
a `j` in `Fin n.succ` allowing us to undertake contraction. -/
|
||||
def contrIso {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) ≅ ((OverColor.Discrete.pairτ S.FD S.τ).obj
|
||||
(Discrete.mk (c i))) ⊗
|
||||
(OverColor.lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) :=
|
||||
(S.F.mapIso (OverColor.equivToIso (HepLean.Fin.finExtractTwo i j))).trans <|
|
||||
(S.F.mapIso (OverColor.mkSum (c ∘ (HepLean.Fin.finExtractTwo i j).symm))).trans <|
|
||||
(S.F.μIso _ _).symm.trans <| by
|
||||
refine tensorIso (S.contrFin1Fin1 c i j h) (S.F.mapIso (OverColor.mkIso (by ext x; simp)))
|
||||
|
||||
lemma contrIso_hom_hom {n : ℕ} {c1 : Fin n.succ.succ → S.C}
|
||||
{i : Fin n.succ.succ} {j : Fin n.succ} {h : c1 (i.succAbove j) = S.τ (c1 i)} :
|
||||
(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
|
||||
rfl
|
||||
|
||||
/-- `contrMap` is a function that takes a natural number `n`, a function `c` from
|
||||
`Fin n.succ.succ` to `S.C`, an index `i` of type `Fin n.succ.succ`, an index `j` of type
|
||||
`Fin n.succ`, and a proof `h` that `c (i.succAbove j) = S.τ (c i)`. It returns a morphism
|
||||
corresponding to the contraction of the `i`th index with the `i.succAbove j` index.
|
||||
--/
|
||||
def contrMap {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) ⟶
|
||||
S.F.obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)) :=
|
||||
(S.contrIso c i j h).hom ≫
|
||||
(tensorHom (S.contr.app (Discrete.mk (c i))) (𝟙 _)) ≫
|
||||
(MonoidalCategory.leftUnitor _).hom
|
||||
|
||||
/-- Acting with `contrMap` on a `tprod` gives a `tprod` multiplied by a scalar. -/
|
||||
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.FD.obj (Discrete.mk (c i))) :
|
||||
(S.contrMap c i j h).hom (PiTensorProduct.tprod S.k x) =
|
||||
(S.castToField ((S.contr.app (Discrete.mk (c i))).hom ((x i) ⊗ₜ[S.k]
|
||||
(S.FD.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,
|
||||
tensorIso_hom, Monoidal.tensorUnit_obj, tensorHom_id,
|
||||
Category.assoc, Action.comp_hom, Action.instMonoidalCategory_tensorObj_V,
|
||||
Action.instMonoidalCategory_tensorHom_hom, Action.instMonoidalCategory_tensorUnit_V,
|
||||
Action.instMonoidalCategory_whiskerRight_hom, Functor.id_obj, mk_hom, ModuleCat.coe_comp,
|
||||
Function.comp_apply, Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
|
||||
Action.FunctorCategoryEquivalence.functor_obj_obj, Functor.comp_obj, Discrete.functor_obj_eq_as]
|
||||
change (λ_ ((lift.obj S.FD).obj _)).hom.hom
|
||||
(((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FD).obj
|
||||
(OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
|
||||
(((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FD).map (mkIso _).hom).hom)
|
||||
(((lift.obj S.FD).μIso (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)
|
||||
∘ Sum.inl))
|
||||
(OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom
|
||||
(((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom
|
||||
(((lift.obj S.FD).map (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).hom
|
||||
((PiTensorProduct.tprod S.k) x)))))) = _
|
||||
rw [lift.map_tprod]
|
||||
change (λ_ ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)))).hom.hom
|
||||
(((S.contr.app { as := c i }).hom ▷
|
||||
((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
|
||||
(((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FD).map (mkIso _).hom).hom)
|
||||
(((lift.obj S.FD).μIso (OverColor.mk
|
||||
((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
|
||||
(OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom
|
||||
(((lift.obj S.FD).map (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).hom
|
||||
((PiTensorProduct.tprod S.k) fun i_1 =>
|
||||
(lift.discreteFunctorMapEqIso S.FD _)
|
||||
(x ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm i_1))))))) = _
|
||||
rw [lift.map_tprod]
|
||||
change (λ_ ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)))).hom.hom
|
||||
(((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FD).obj
|
||||
(OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
|
||||
(((S.contrFin1Fin1 c i j h).hom.hom ⊗ ((lift.obj S.FD).map (mkIso _).hom).hom)
|
||||
(((lift.obj S.FD).μIso
|
||||
(OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
|
||||
(OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom
|
||||
((PiTensorProduct.tprod S.k) fun i_1 =>
|
||||
(lift.discreteFunctorMapEqIso S.FD _)
|
||||
((lift.discreteFunctorMapEqIso S.FD _)
|
||||
(x ((Hom.toEquiv (equivToIso (HepLean.Fin.finExtractTwo i j)).hom).symm
|
||||
((Hom.toEquiv (mkSum (c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)).hom).symm i_1)))))))) = _
|
||||
rw [lift.μIso_inv_tprod]
|
||||
change (λ_ ((lift.obj S.FD).obj (OverColor.mk (c ∘ i.succAbove ∘ j.succAbove)))).hom.hom
|
||||
(((S.contr.app { as := c i }).hom ▷ ((lift.obj S.FD).obj
|
||||
(OverColor.mk (c ∘ i.succAbove ∘ j.succAbove))).V)
|
||||
((TensorProduct.map (S.contrFin1Fin1 c i j h).hom.hom
|
||||
((lift.obj S.FD).map (mkIso _).hom).hom)
|
||||
(((PiTensorProduct.tprod S.k) fun i_1 =>
|
||||
(lift.discreteFunctorMapEqIso S.FD _)
|
||||
((lift.discreteFunctorMapEqIso S.FD _) (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.FD _) ((lift.discreteFunctorMapEqIso S.FD _)
|
||||
(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,
|
||||
Action.instMonoidalCategory_tensorUnit_V, Fin.isValue, mk_hom, Function.comp_apply,
|
||||
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 only [Monoidal.tensorUnit_obj, Action.instMonoidalCategory_tensorUnit_V, Fin.isValue,
|
||||
ModuleCat.MonoidalCategory.leftUnitor_hom_apply]
|
||||
congr 1
|
||||
/- The contraction. -/
|
||||
· simp only [Fin.isValue, castToField]
|
||||
congr 2
|
||||
· 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 only [Fin.isValue, lift.discreteFunctorMapEqIso, eqToIso_refl, Functor.mapIso_refl,
|
||||
Iso.refl_hom, Action.id_hom, Iso.refl_inv, LinearEquiv.ofLinear_apply]
|
||||
change (S.FD.map (eqToHom _)).hom
|
||||
(x (((HepLean.Fin.finExtractTwo i j)).symm ((Sum.inl (Sum.inr 0))))) = _
|
||||
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.FD.map (Discrete.eqToHom (h))).hom (x d) =
|
||||
(S.FD.map (Discrete.eqToHom h')).hom (x b) := by
|
||||
subst hbd
|
||||
rfl
|
||||
refine h1' ?_ ?_ ?_
|
||||
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 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.FD.map (eqToHom _)).hom
|
||||
((x ((HepLean.Fin.finExtractTwo i j).symm (Sum.inr (d))))) = _
|
||||
simp only [Nat.succ_eq_add_one]
|
||||
have h1 : ((HepLean.Fin.finExtractTwo i j).symm (Sum.inr d))
|
||||
= (i.succAbove (j.succAbove d)) := HepLean.Fin.finExtractTwo_symm_inr_apply i j d
|
||||
have h1' {a b : Fin n.succ.succ} (h : a = b) :
|
||||
(S.FD.map (eqToHom (by rw [h]))).hom (x a) = x b := by
|
||||
subst h
|
||||
simp
|
||||
exact h1' h1
|
||||
|
||||
end TensorSpecies
|
||||
|
||||
end
|
||||
|
|
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Joseph Tooby-Smith
|
||||
-/
|
||||
import HepLean.Tensors.TensorSpecies.UnitTensor
|
||||
import HepLean.Tensors.TensorSpecies.ContractLemmas
|
||||
import HepLean.Tensors.TensorSpecies.Contractions.Categorical
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ProdComm
|
||||
import HepLean.Tensors.Tree.NodeIdentities.PermProd
|
||||
import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ 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.TensorSpecies.ContractLemmas
|
||||
import HepLean.Tensors.TensorSpecies.Contractions.Categorical
|
||||
/-!
|
||||
|
||||
## Units as tensors
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ 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.Contractions.ContrMap
|
||||
/-!
|
||||
|
||||
# Tensor trees
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@ 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
|
||||
import HepLean.Tensors.TensorSpecies.Contractions.Categorical
|
||||
/-!
|
||||
|
||||
## Specific associativity results for tensor trees
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue