DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: free_simps

Browse source
This commit is contained in:
jstoobysmith 2024-12-10 14:05:41 +00:00
parent 9d4c21fd6d
commit 0595ceddff
2 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
HepLean/Tensors/OverColor/Lift.lean
View file

@ -707,7 +707,8 @@ noncomputable def lift : (Discrete C ⥤ Rep k G) ⥤ LaxBraidedFunctor (OverCol
simp only [lift.map']
refine LaxMonoidalFunctor.hom_ext ?_
ext X : 2
simp
simp only [LaxBraidedFunctor.toLaxMonoidalFunctor_toFunctor, LaxBraidedFunctor.of_toFunctor,
LaxMonoidalFunctor.homMk_hom, LaxBraidedFunctor.id_hom, NatTrans.id_app]
ext x
refine PiTensorProduct.induction_on' x ?_ (by
intro x y hx hy

4
HepLean/Tensors/TensorSpecies/UnitTensor.lean
View file

@ -56,7 +56,9 @@ lemma unitTensor_eq_dual_perm (c : S.C) : {S.unitTensor c | μ ν}ᵀ.tensor =
({S.unitTensor (S.τ c) | ν μ }ᵀ |>
perm (OverColor.equivToHomEq (finMapToEquiv ![1,0] ![1, 0])
(fun x => match x with | 0 => by rfl | 1 => (S.τ_involution c).symm))).tensor := by
simp [unitTensor, tensorNode_tensor, perm_tensor]
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, unitTensor,
Action.instMonoidalCategory_tensorObj_V, Monoidal.tensorUnit_obj,
Action.instMonoidalCategory_tensorUnit_V, tensorNode_tensor, Fin.isValue, perm_tensor]
have h1 := S.unit_symm c
erw [h1]
have hg : (Discrete.pairIsoSep S.FD).hom.hom ∘ₗ (S.FD.obj { as := S.τ c } ◁