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

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2024-12-10 14:02:31 +00:00
parent 5dfd29ab8d
commit 9d4c21fd6d
11 changed files with 98 additions and 56 deletions
Download patch file Download diff file Expand all files Collapse all files

50
HepLean/Tensors/OverColor/Functors.lean
View file

@ -19,20 +19,21 @@ open MonoidalCategory
def map {C D : Type} (f : C → D) : Functor (OverColor C) (OverColor D) :=
Core.functorToCore (Core.inclusion (Over C) ⋙ (Over.map f))
/-- The functor `map f` is lax-monoidal. -/
instance map_laxMonoidal {C D : Type} (f : C → D) : Functor.LaxMonoidal (map f) where
ε' := Over.isoMk (Iso.refl _) (by
ext x
exact Empty.elim x)
μ' := fun X Y => Over.isoMk (Iso.refl _) (by
μ' := fun X Y => Over.isoMk (Iso.refl _) (by
ext x
match x with
| Sum.inl x => rfl
| Sum.inr x => rfl)
μ'_natural_left := fun X Y => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
μ'_natural_left X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
rfl
μ'_natural_right := fun X Y => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
μ'_natural_right X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
rfl
associativity' := fun X Y Z => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
associativity' X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl (Sum.inl x) => rfl
| Sum.inl (Sum.inr x) => rfl
@ -46,6 +47,7 @@ instance map_laxMonoidal {C D : Type} (f : C → D) : Functor.LaxMonoidal (map f
| Sum.inl x => rfl
| Sum.inr x => rfl
/-- The functor `map f` is lax-monoidal. -/
noncomputable instance map_monoidal {C D : Type} (f : C → D) : Functor.Monoidal (map f) :=
Functor.Monoidal.ofLaxMonoidal _
@ -53,6 +55,7 @@ noncomputable instance map_monoidal {C D : Type} (f : C → D) : Functor.Monoida
def tensor (C : Type) : Functor (OverColor C × OverColor C) (OverColor C) :=
MonoidalCategory.tensor (OverColor C)
/-- The functor tensor is lax-monoidal. -/
instance tensor_laxMonoidal (C : Type) : Functor.LaxMonoidal (tensor C) where
ε' := Over.isoMk (Equiv.sumEmpty Empty Empty).symm.toIso rfl
μ' := fun X Y => Over.isoMk (Equiv.sumSumSumComm X.1.left X.2.left Y.1.left Y.2.left).toIso (by
@ -62,19 +65,19 @@ instance tensor_laxMonoidal (C : Type) : Functor.LaxMonoidal (tensor C) where
| Sum.inl (Sum.inr x) => rfl
| Sum.inr (Sum.inl x) => rfl
| Sum.inr (Sum.inr x) => rfl)
μ'_natural_left := fun X Y => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
μ'_natural_left X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl (Sum.inl x) => rfl
| Sum.inl (Sum.inr x) => rfl
| Sum.inr (Sum.inl x) => rfl
| Sum.inr (Sum.inr x) => rfl
μ'_natural_right := fun X Y => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
μ'_natural_right X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl (Sum.inl x) => rfl
| Sum.inl (Sum.inr x) => rfl
| Sum.inr (Sum.inl x) => rfl
| Sum.inr (Sum.inr x) => rfl
associativity' := fun X Y Z => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
associativity' X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl (Sum.inl (Sum.inl x)) => rfl
| Sum.inl (Sum.inl (Sum.inr x)) => rfl
@ -82,60 +85,67 @@ instance tensor_laxMonoidal (C : Type) : Functor.LaxMonoidal (tensor C) where
| Sum.inl (Sum.inr (Sum.inr x)) => rfl
| Sum.inr (Sum.inl x) => rfl
| Sum.inr (Sum.inr x) => rfl
left_unitality' := fun X => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
left_unitality' X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl x => exact Empty.elim x
| Sum.inr (Sum.inl x)=> rfl
| Sum.inr (Sum.inr x)=> rfl
right_unitality' := fun X => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
right_unitality' X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
match x with
| Sum.inl (Sum.inl x) => rfl
| Sum.inl (Sum.inr x) => rfl
| Sum.inr x => exact Empty.elim x
/-- The functor tensor is monoidal. -/
noncomputable instance tensor_monoidal (C : Type) : Functor.Monoidal (tensor C) :=
Functor.Monoidal.ofLaxMonoidal _
/-- The constant monoidal functor from `OverColor C` to itself landing on `𝟙_ (OverColor C)`. -/
def const (C : Type) : Functor (OverColor C) (OverColor C) :=
(Functor.const (OverColor C)).obj (𝟙_ (OverColor C))
(Functor.const (OverColor C)).obj (𝟙_ (OverColor C))
/-- The functor `const C` is lax monoidal. -/
instance const_laxMonoidal (C : Type) : Functor.LaxMonoidal (const C) where
ε' := 𝟙 (𝟙_ (OverColor C))
μ' := fun _ _ => (λ_ (𝟙_ (OverColor C))).hom
μ'_natural_left := fun _ _ => by
μ'_natural_left := fun _ _ => by
simp only [Functor.const_obj_obj, Functor.const_obj_map, MonoidalCategory.whiskerRight_id,
Category.id_comp, Iso.hom_inv_id, Category.comp_id, const]
μ'_natural_right := fun _ _ => by
simp only [Functor.const_obj_obj, Functor.const_obj_map, MonoidalCategory.whiskerLeft_id,
Category.id_comp, Category.comp_id, const]
associativity' := fun X Y Z => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by
associativity' X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i =>
match i with
| Sum.inl (Sum.inl i) => rfl
| Sum.inl (Sum.inr i) => rfl
| Sum.inr i => rfl
left_unitality' := fun X => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by
left_unitality' X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i =>
match i with
| Sum.inl i => exact Empty.elim i
| Sum.inr i => exact Empty.elim i
right_unitality' := fun X => CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i => by
| Sum.inl i => Empty.elim i
| Sum.inr i => Empty.elim i
right_unitality' X := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun i =>
match i with
| Sum.inl i => exact Empty.elim i
| Sum.inr i => exact Empty.elim i
| Sum.inl i => Empty.elim i
| Sum.inr i => Empty.elim i
/-- The functor `const C` is monoidal. -/
noncomputable instance const_monoidal (C : Type) : Functor.Monoidal (const C) :=
Functor.Monoidal.ofLaxMonoidal _
/-- The monoidal functor from `OverColor C` to `OverColor C` taking `f` to `f ⊗ τ_* f`. -/
def contrPair (C : Type) (τ : C → C) : Functor (OverColor C) (OverColor C) :=
(Functor.diag (OverColor C))
(Functor.diag (OverColor C))
⋙ (Functor.prod (Functor.id (OverColor C)) (OverColor.map τ))
⋙ (OverColor.tensor C)
/-- The functor `contrPair` is lax-monoidal. -/
instance contrPair_laxMonoidal (C : Type) (τ : C → C) : Functor.LaxMonoidal (contrPair C τ) :=
Functor.LaxMonoidal.comp (Functor.diag (OverColor C)) ((𝟭 (OverColor C)).prod (map τ) ⋙ tensor C)
noncomputable instance contrPair_monoidal (C : Type) (τ : C → C) : Functor.Monoidal (contrPair C τ) :=
/-- The functor `contrPair` is monoidal. -/
noncomputable instance contrPair_monoidal (C : Type) (τ : C → C) :
Functor.Monoidal (contrPair C τ) :=
Functor.Monoidal.ofLaxMonoidal _
end OverColor
end IndexNotation

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

@ -551,13 +551,14 @@ lemma objMap'_comp {X Y Z : OverColor C} (f : X ⟶ Y) (g : Y ⟶ Z) :
rw [discreteFun_hom_trans]
rfl
/-- The `BraidedFunctor (OverColor C) (Rep k G)` from a functor `Discrete C ⥤ Rep k G`. -/
/-- The `Functor (OverColor C) (Rep k G)` from a functor `Discrete C ⥤ Rep k G`. -/
def obj' : Functor (OverColor C) (Rep k G) where
obj := objObj' F
map := objMap' F
map_comp := fun f g => objMap'_comp F f g
map_comp := fun f g => objMap'_comp F f g
map_id := fun f => objMap'_id F f
/-- The lift of a functor is lax braided. -/
instance obj'_laxBraidedFunctor : Functor.LaxBraided (obj' F) where
ε' := (ε F).hom
μ' := fun X Y => (μ F X Y).hom
@ -571,12 +572,17 @@ instance obj'_laxBraidedFunctor : Functor.LaxBraided (obj' F) where
rw [braided F X Y]
simp
/-- The lift of a functor is monoidal. -/
instance obj'_monoidalFunctor : Functor.Monoidal (obj' F) :=
haveI : IsIso (Functor.LaxMonoidal.ε (obj' F)) := Action.isIso_of_hom_isIso (ε F).hom
haveI : (∀ (X Y : OverColor C), IsIso (Functor.LaxMonoidal.μ (obj' F) X Y)) :=
fun X Y => Action.isIso_of_hom_isIso ((μ F X Y).hom)
Functor.Monoidal.ofLaxMonoidal _
/-- The lift of a functor is braided. -/
instance obj'_braided : Functor.Braided (obj' F) := Functor.Braided.mk (fun X Y =>
Functor.LaxBraided.braided X Y)
variable {F F' : Discrete C ⥤ Rep k G} (η : F ⟶ F')
/-- The maps for a natural transformation between `obj' F` and `obj' F'`. -/
@ -680,10 +686,11 @@ lemma mapApp'_tensor (X Y : OverColor C) :
/-- Given a natural transformation between `F F' : Discrete C ⥤ Rep k G` the
monoidal natural transformation between `obj' F` and `obj' F'`. -/
def map' : (obj' F) ⟶ (obj' F') where
def map' : (obj' F) ⟶ (obj' F') where
app := mapApp' η
naturality _ _ f := mapApp'_naturality η f
/-- The lift of a natural transformation is monoidal. -/
instance map'_isMonoidal : NatTrans.IsMonoidal (map' η) where
unit := mapApp'_unit η
tensor := mapApp'_tensor η
@ -736,10 +743,13 @@ noncomputable def lift : (Discrete C ⥤ Rep k G) ⥤ LaxBraidedFunctor (OverCol
namespace lift
variable (F F' : Discrete C ⥤ Rep k G) (η : F ⟶ F')
/-- The lift of a functor is monoidal. -/
noncomputable instance : (lift.obj F).Monoidal := obj'_monoidalFunctor F
/-- The lift of a functor is lax-braided. -/
noncomputable instance : (lift.obj F).LaxBraided := obj'_laxBraidedFunctor F
/-- The lift of a functor is braided. -/
noncomputable instance : (lift.obj F).Braided := Functor.Braided.mk (fun X Y =>
Functor.LaxBraided.braided X Y)
@ -754,7 +764,8 @@ lemma map_tprod (F : Discrete C ⥤ Rep k G) {X Y : OverColor C} (f : X ⟶ Y)
lemma obj_μ_tprod_tmul (F : Discrete C ⥤ Rep k G) (X Y : OverColor C)
(p : (i : X.left) → (F.obj (Discrete.mk <| X.hom i)))
(q : (i : Y.left) → F.obj (Discrete.mk <| Y.hom i)) :
(Functor.LaxMonoidal.μ (lift.obj F).toFunctor X Y).hom (PiTensorProduct.tprod k p ⊗ₜ[k] PiTensorProduct.tprod k q) =
(Functor.LaxMonoidal.μ (lift.obj F).toFunctor X Y).hom
(PiTensorProduct.tprod k p ⊗ₜ[k] PiTensorProduct.tprod k q) =
(PiTensorProduct.tprod k) fun i =>
discreteSumEquiv F i (HepLean.PiTensorProduct.elimPureTensor p q i) := by
exact μ_tmul_tprod F p q
@ -764,12 +775,14 @@ lemma μIso_inv_tprod (F : Discrete C ⥤ Rep k G) (X Y : OverColor C)
(Functor.Monoidal.μIso (lift.obj F).toFunctor X Y).inv.hom (PiTensorProduct.tprod k p) =
(PiTensorProduct.tprod k (fun i => p (Sum.inl i))) ⊗ₜ[k]
(PiTensorProduct.tprod k (fun i => p (Sum.inr i))) := by
change ((Action.forget _ _).mapIso (Functor.Monoidal.μIso (lift.obj F).toFunctor X Y)).inv (PiTensorProduct.tprod k p) = _
trans ((Action.forget _ _).mapIso (Functor.Monoidal.μIso (lift.obj F).toFunctor X Y)).toLinearEquiv.symm
change ((Action.forget _ _).mapIso (Functor.Monoidal.μIso (lift.obj F).toFunctor X Y)).inv
(PiTensorProduct.tprod k p) = _
trans ((Action.forget _ _).mapIso
(Functor.Monoidal.μIso (lift.obj F).toFunctor X Y)).toLinearEquiv.symm
(PiTensorProduct.tprod k p)
· rfl
erw [← LinearEquiv.eq_symm_apply]
change _ = (Functor.LaxMonoidal.μ (lift.obj F).toFunctor X Y).hom _
change _ = (Functor.LaxMonoidal.μ (lift.obj F).toFunctor X Y).hom _
erw [obj_μ_tprod_tmul]
congr
funext i

10
HepLean/Tensors/TensorSpecies/Basic.lean
View file

@ -111,14 +111,18 @@ def F : Functor (OverColor S.C) (Rep S.k S.G) := ((OverColor.lift).obj S.FD).toF
/- The definition of `F` as a lemma. -/
lemma F_def : F S = ((OverColor.lift).obj S.FD).toFunctor := rfl
instance F_monoidal : Functor.Monoidal S.F := lift.instMonoidalRepObjFunctorDiscreteLaxBraidedFunctor S.FD
/-- The functor `F` is monoidal. -/
instance F_monoidal : Functor.Monoidal S.F :=
lift.instMonoidalRepObjFunctorDiscreteLaxBraidedFunctor S.FD
instance F_laxBraided : Functor.LaxBraided S.F := lift.instLaxBraidedRepObjFunctorDiscreteLaxBraidedFunctor S.FD
/-- The functor `F` is lax-braided. -/
instance F_laxBraided : Functor.LaxBraided S.F :=
lift.instLaxBraidedRepObjFunctorDiscreteLaxBraidedFunctor S.FD
/-- The functor `F` is braided. -/
instance F_braided : Functor.Braided S.F := Functor.Braided.mk
(fun X Y => Functor.LaxBraided.braided X Y)
lemma perm_contr_cond {n : ℕ} {c : Fin n.succ.succ → S.C} {c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ} {j : Fin n.succ}
(h : c1 (i.succAbove j) = S.τ (c1 i)) (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) :

7
HepLean/Tensors/TensorSpecies/Contractions/ContrMap.lean
View file

@ -152,7 +152,8 @@ lemma contrIso_hom_hom {n : ℕ} {c1 : Fin n.succ.succ → S.C}
(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 ≫
(Functor.Monoidal.μIso S.F (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
(Functor.Monoidal.μIso S.F
(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
@ -192,8 +193,8 @@ lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
(((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)
((Functor.Monoidal.μIso (lift.obj S.FD).toFunctor (OverColor.mk ((c ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm)
∘ Sum.inl))
((Functor.Monoidal.μIso (lift.obj S.FD).toFunctor
(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

7
HepLean/Tensors/Tree/NodeIdentities/Basic.lean
View file

@ -312,14 +312,15 @@ lemma prod_action {n n1 : ℕ} {c : Fin n → S.C} {c1 : Fin n1 → S.C} (g : S.
simp only [prod_tensor, action_tensor, map_tmul]
change _ = ((S.F.map (equivToIso finSumFinEquiv).hom).hom ≫
(S.F.obj (OverColor.mk (Sum.elim c c1 ∘ ⇑finSumFinEquiv.symm))).ρ g)
(((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).hom (t.tensor ⊗ₜ[S.k] t1.tensor)))
(((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).hom
(t.tensor ⊗ₜ[S.k] t1.tensor)))
erw [← (S.F.map (equivToIso finSumFinEquiv).hom).comm g]
simp only [Action.forget_obj, Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V,
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
Action.FunctorCategoryEquivalence.functor_obj_obj, ModuleCat.coe_comp, Function.comp_apply]
change _ = (S.F.map (equivToIso finSumFinEquiv).hom).hom
(((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).hom ≫ (S.F.obj (OverColor.mk (Sum.elim c c1))).ρ g)
(t.tensor ⊗ₜ[S.k] t1.tensor))
(((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).hom ≫
(S.F.obj (OverColor.mk (Sum.elim c c1))).ρ g) (t.tensor ⊗ₜ[S.k] t1.tensor))
erw [← (Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c1)).comm g]
rfl

9
HepLean/Tensors/Tree/NodeIdentities/PermContr.lean
View file

@ -117,14 +117,17 @@ lemma contrIso_comm_aux_2 {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
{i : Fin n.succ.succ} {j : Fin n.succ}
(σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) :
(S.F.map (extractTwoAux' i j σ ⊗ extractTwoAux i j σ)).hom ≫
(Functor.Monoidal.μIso S.F (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
(Functor.Monoidal.μIso S.F
(OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
(OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom =
(Functor.Monoidal.μIso S.F _ _).inv.hom ≫
(S.F.map (extractTwoAux' i j σ) ⊗ S.F.map (extractTwoAux i j σ)).hom := by
have h1 : (S.F.map (extractTwoAux' i j σ ⊗ extractTwoAux i j σ)) ≫
(Functor.Monoidal.μIso S.F (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
(Functor.Monoidal.μIso S.F
(OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inl))
(OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv =
(Functor.Monoidal.μIso S.F _ _).inv ≫ (S.F.map (extractTwoAux' i j σ) ⊗ S.F.map (extractTwoAux i j σ)) := by
(Functor.Monoidal.μIso S.F _ _).inv ≫
(S.F.map (extractTwoAux' i j σ) ⊗ S.F.map (extractTwoAux i j σ)) := by
erw [CategoryTheory.IsIso.comp_inv_eq, CategoryTheory.Category.assoc]
erw [CategoryTheory.IsIso.eq_inv_comp]
exact (Functor.LaxMonoidal.μ_natural S.F (extractTwoAux' i j σ) (extractTwoAux i j σ)).symm

6
HepLean/Tensors/Tree/NodeIdentities/PermProd.lean
View file

@ -54,7 +54,8 @@ theorem prod_perm_left (t : TensorTree S c) (t2 : TensorTree S c2) :
Action.FunctorCategoryEquivalence.functor_obj_obj, perm_tensor]
change (S.F.map (equivToIso finSumFinEquiv).hom).hom
(((S.F.map (σ) ▷ S.F.obj (OverColor.mk c2)) ≫
Functor.LaxMonoidal.μ S.F (OverColor.mk c') (OverColor.mk c2)).hom (t.tensor ⊗ₜ[S.k] t2.tensor)) = _
Functor.LaxMonoidal.μ S.F (OverColor.mk c') (OverColor.mk c2)).hom
(t.tensor ⊗ₜ[S.k] t2.tensor)) = _
rw [Functor.LaxMonoidal.μ_natural_left]
simp only [Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, Action.comp_hom,
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
@ -72,7 +73,8 @@ theorem prod_perm_right (t2 : TensorTree S c2) (t : TensorTree S c) :
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
Action.FunctorCategoryEquivalence.functor_obj_obj, perm_tensor]
change (S.F.map (equivToIso finSumFinEquiv).hom).hom
(((S.F.obj (OverColor.mk c2) ◁ S.F.map σ) ≫ Functor.LaxMonoidal.μ S.F (OverColor.mk c2) (OverColor.mk c')).hom
(((S.F.obj (OverColor.mk c2) ◁ S.F.map σ) ≫
Functor.LaxMonoidal.μ S.F (OverColor.mk c2) (OverColor.mk c')).hom
(t2.tensor ⊗ₜ[S.k] t.tensor)) = _
rw [Functor.LaxMonoidal.μ_natural_right]
simp only [Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V, Action.comp_hom,

17
HepLean/Tensors/Tree/NodeIdentities/ProdAssoc.lean
View file

@ -63,8 +63,8 @@ theorem prod_assoc (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree
rw [perm_tensor]
nth_rewrite 2 [prod_tensor]
change _ = ((S.F.map (equivToIso finSumFinEquiv).hom) ≫ S.F.map (assocPerm c c2 c3).hom).hom
(((Functor.LaxMonoidal.μ S.F (OverColor.mk (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm)) (OverColor.mk c3)).hom
((t.prod t2).tensor ⊗ₜ[S.k] t3.tensor)))
(((Functor.LaxMonoidal.μ S.F (OverColor.mk (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm))
(OverColor.mk c3)).hom ((t.prod t2).tensor ⊗ₜ[S.k] t3.tensor)))
rw [← S.F.map_comp, finSumFinEquiv_comp_assocPerm]
simp only [Functor.id_obj, mk_hom, whiskerRightIso_hom, Iso.symm_hom, whiskerLeftIso_hom,
Functor.map_comp, Action.comp_hom, Action.instMonoidalCategory_tensorObj_V,
@ -74,7 +74,8 @@ theorem prod_assoc (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree
apply congrArg
change _ = (S.F.map (OverColor.mk c ◁ (equivToIso finSumFinEquiv).hom)).hom
((S.F.map (α_ (OverColor.mk c) (OverColor.mk c2) (OverColor.mk c3)).hom).hom
((Functor.LaxMonoidal.μ S.F (OverColor.mk (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm)) (OverColor.mk c3)
((Functor.LaxMonoidal.μ S.F (OverColor.mk (Sum.elim c c2 ∘ ⇑finSumFinEquiv.symm))
(OverColor.mk c3)
≫ S.F.map ((equivToIso finSumFinEquiv).inv ▷ OverColor.mk c3)).hom
(((t.prod t2).tensor ⊗ₜ[S.k] t3.tensor))))
rw [← Functor.LaxMonoidal.μ_natural_left]
@ -91,8 +92,8 @@ theorem prod_assoc (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree
((S.F.map (α_ (OverColor.mk c) (OverColor.mk c2) (OverColor.mk c3)).hom).hom
((Functor.LaxMonoidal.μ S.F (OverColor.mk (Sum.elim c c2)) (OverColor.mk c3)).hom
((S.F.map (equivToIso finSumFinEquiv).hom ≫ S.F.map (equivToIso finSumFinEquiv).inv).hom
(((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c2)).hom (t.tensor ⊗ₜ[S.k] t2.tensor))) ⊗ₜ[S.k]
t3.tensor)))
(((Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk c2)).hom
(t.tensor ⊗ₜ[S.k] t2.tensor))) ⊗ₜ[S.k] t3.tensor)))
simp only [Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V,
Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
Action.FunctorCategoryEquivalence.functor_obj_obj, Iso.map_hom_inv_id, Action.id_hom,
@ -110,9 +111,11 @@ theorem prod_assoc (t : TensorTree S c) (t2 : TensorTree S c2) (t3 : TensorTree
ModuleCat.MonoidalCategory.associator_hom_apply]
rw [prod_tensor]
change ((_ ◁ (S.F.map (equivToIso finSumFinEquiv).hom)) ≫
Functor.LaxMonoidal.μ S.F (OverColor.mk c) (OverColor.mk (Sum.elim c2 c3 ∘ ⇑finSumFinEquiv.symm))).hom
Functor.LaxMonoidal.μ S.F (OverColor.mk c)
(OverColor.mk (Sum.elim c2 c3 ∘ ⇑finSumFinEquiv.symm))).hom
(t.tensor ⊗ₜ[S.k]
((Functor.LaxMonoidal.μ S.F (OverColor.mk c2) (OverColor.mk c3)).hom (t2.tensor ⊗ₜ[S.k] t3.tensor))) = _
((Functor.LaxMonoidal.μ S.F
(OverColor.mk c2) (OverColor.mk c3)).hom (t2.tensor ⊗ₜ[S.k] t3.tensor))) = _
rw [Functor.LaxMonoidal.μ_natural_right]
simp only [Action.instMonoidalCategory_tensorObj_V, Action.comp_hom, Equivalence.symm_inverse,
Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,

3
HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean
View file

@ -49,7 +49,8 @@ theorem prod_comm (t : TensorTree S c) (t2 : TensorTree S c2) :
rw [perm_tensor]
nth_rewrite 2 [prod_tensor]
change _ = (S.F.map (equivToIso finSumFinEquiv).hom ≫ S.F.map (braidPerm c c2)).hom
((Functor.LaxMonoidal.μ S.F (OverColor.mk c2) (OverColor.mk c)).hom (t2.tensor ⊗ₜ[S.k] t.tensor))
((Functor.LaxMonoidal.μ S.F (OverColor.mk c2) (OverColor.mk c)).hom
(t2.tensor ⊗ₜ[S.k] t.tensor))
rw [← S.F.map_comp]
rw [finSumFinEquiv_comp_braidPerm]
rw [S.F.map_comp]

12
HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean
View file

@ -172,7 +172,8 @@ lemma contrMap_prod_tprod (p : (i : (𝟭 Type).obj (OverColor.mk c).left) →
(q' : (i : (𝟭 Type).obj (OverColor.mk c1).left) →
CoeSort.coe (S.FD.obj { as := (OverColor.mk c1).hom i })) :
(S.F.map (equivToIso finSumFinEquiv).hom).hom
((Functor.LaxMonoidal.μ S.F (OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove)) (OverColor.mk c1)).hom
((Functor.LaxMonoidal.μ S.F
(OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove)) (OverColor.mk c1)).hom
((q.contrMap.hom (PiTensorProduct.tprod S.k p)) ⊗ₜ[S.k] (PiTensorProduct.tprod S.k) q'))
= (S.F.map (mkIso (by exact leftContr_map_eq q)).hom).hom
(q.leftContr.contrMap.hom
@ -288,7 +289,8 @@ lemma contr_prod
q.leftContr.h
(perm (OverColor.equivToIso ContrPair.leftContrEquivSuccSucc).hom (prod t t1)))).tensor) := by
simp only [contr_tensor, perm_tensor, prod_tensor]
change ((q.contrMap ▷ S.F.obj (OverColor.mk c1)) ≫ (Functor.LaxMonoidal.μ S.F _ ((OverColor.mk c1))) ≫
change ((q.contrMap ▷ S.F.obj (OverColor.mk c1)) ≫
(Functor.LaxMonoidal.μ S.F _ ((OverColor.mk c1))) ≫
S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom (t.tensor ⊗ₜ[S.k] t1.tensor) = _
rw [contrMap_prod]
simp only [Nat.succ_eq_add_one, Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V,
@ -405,7 +407,8 @@ lemma prod_contrMap_tprod (p : (i : (𝟭 Type).obj (OverColor.mk c1).left) →
(q' : (i : (𝟭 Type).obj (OverColor.mk c).left) →
CoeSort.coe (S.FD.obj { as := (OverColor.mk c).hom i })) :
(S.F.map (equivToIso finSumFinEquiv).hom).hom
((Functor.LaxMonoidal.μ S.F (OverColor.mk c1) (OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove))).hom
((Functor.LaxMonoidal.μ S.F (OverColor.mk c1)
(OverColor.mk (c ∘ q.i.succAbove ∘ q.j.succAbove))).hom
((PiTensorProduct.tprod S.k) p ⊗ₜ[S.k] (q.contrMap.hom (PiTensorProduct.tprod S.k q')))) =
(S.F.map (mkIso (by exact (rightContr_map_eq q))).hom).hom
(q.rightContr.contrMap.hom
@ -530,7 +533,8 @@ lemma prod_contr (t1 : TensorTree S c1) (t : TensorTree S c) :
(contr (q.rightContrI n1) (q.rightContrJ n1)
q.rightContr.h (prod t1 t))).tensor) := by
simp only [contr_tensor, perm_tensor, prod_tensor]
change ((S.F.obj (OverColor.mk c1) ◁ q.contrMap) ≫ (Functor.LaxMonoidal.μ S.F ((OverColor.mk c1)) _) ≫
change ((S.F.obj (OverColor.mk c1) ◁ q.contrMap) ≫
(Functor.LaxMonoidal.μ S.F ((OverColor.mk c1)) _) ≫
S.F.map (OverColor.equivToIso finSumFinEquiv).hom).hom (t1.tensor ⊗ₜ[S.k] t.tensor) = _
rw [prod_contrMap]
simp only [Nat.succ_eq_add_one, Functor.id_obj, mk_hom, Action.instMonoidalCategory_tensorObj_V,