From 57ecf7e1090522f6f814b702b53c98b7cff20cac Mon Sep 17 00:00:00 2001 From: Yuma Mizuno Date: Thu, 7 Mar 2024 18:39:26 +0000 Subject: [PATCH] =?UTF-8?q?chore(CategoryTheory/Monoidal):=20replace=20`?= =?UTF-8?q?=F0=9D=9F=99=20X=20=E2=8A=97=20f`=20with=20`X=20=E2=97=81=20f`?= =?UTF-8?q?=20(#11223)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Extracted from #6307 --- .../Algebra/Category/FGModuleCat/Basic.lean | 6 ++--- .../Category/ModuleCat/Monoidal/Basic.lean | 24 +++++++++---------- .../ModuleCat/Monoidal/Symmetric.lean | 4 ++-- .../Monoidal/Braided/Basic.lean | 2 -- .../CategoryTheory/Monoidal/Preadditive.lean | 2 +- Mathlib/Tactic/CategoryTheory/Coherence.lean | 3 ++- .../Tactic/CategoryTheory/MonoidalComp.lean | 8 +++---- 7 files changed, 24 insertions(+), 25 deletions(-) diff --git a/Mathlib/Algebra/Category/FGModuleCat/Basic.lean b/Mathlib/Algebra/Category/FGModuleCat/Basic.lean index 9c83f276980cf..c5d33993fb9d0 100644 --- a/Mathlib/Algebra/Category/FGModuleCat/Basic.lean +++ b/Mathlib/Algebra/Category/FGModuleCat/Basic.lean @@ -269,13 +269,13 @@ theorem FGModuleCatEvaluation_apply (f : FGModuleCatDual K V) (x : V) : private theorem coevaluation_evaluation : letI V' : FGModuleCat K := FGModuleCatDual K V - (𝟙 V' ⊗ FGModuleCatCoevaluation K V) ≫ (α_ V' V V').inv ≫ (FGModuleCatEvaluation K V ⊗ 𝟙 V') = + V' ◁ FGModuleCatCoevaluation K V ≫ (α_ V' V V').inv ≫ FGModuleCatEvaluation K V ▷ V' = (ρ_ V').hom ≫ (λ_ V').inv := by apply contractLeft_assoc_coevaluation K V private theorem evaluation_coevaluation : - (FGModuleCatCoevaluation K V ⊗ 𝟙 V) ≫ - (α_ V (FGModuleCatDual K V) V).hom ≫ (𝟙 V ⊗ FGModuleCatEvaluation K V) = + FGModuleCatCoevaluation K V ▷ V ≫ + (α_ V (FGModuleCatDual K V) V).hom ≫ V ◁ FGModuleCatEvaluation K V = (λ_ V).hom ≫ (ρ_ V).inv := by apply contractLeft_assoc_coevaluation' K V diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean index fbd4cb999a6c3..88549728edaed 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean @@ -136,9 +136,9 @@ variable (R) private theorem pentagon_aux (W X Y Z : Type*) [AddCommMonoid W] [AddCommMonoid X] [AddCommMonoid Y] [AddCommMonoid Z] [Module R W] [Module R X] [Module R Y] [Module R Z] : - ((map (1 : W →ₗ[R] W) (assoc R X Y Z).toLinearMap).comp + (((assoc R X Y Z).toLinearMap.lTensor W).comp (assoc R W (X ⊗[R] Y) Z).toLinearMap).comp - (map ↑(assoc R W X Y) (1 : Z →ₗ[R] Z)) = + ((assoc R W X Y).rTensor Z) = (assoc R W X (Y ⊗[R] Z)).toLinearMap.comp (assoc R (W ⊗[R] X) Y Z).toLinearMap := by apply TensorProduct.ext_fourfold intro w x y z @@ -156,8 +156,8 @@ theorem associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : ModuleCat R} (f #align Module.monoidal_category.associator_naturality ModuleCat.MonoidalCategory.associator_naturality theorem pentagon (W X Y Z : ModuleCat R) : - tensorHom (associator W X Y).hom (𝟙 Z) ≫ - (associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom = + whiskerRight (associator W X Y).hom Z ≫ + (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom = (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom := by convert pentagon_aux R W X Y Z using 1 #align Module.monoidal_category.pentagon ModuleCat.MonoidalCategory.pentagon @@ -288,30 +288,30 @@ instance : MonoidalPreadditive (ModuleCat.{u} R) := by simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply] rw [LinearMap.zero_apply] -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [MonoidalCategory.hom_apply] + erw [MonoidalCategory.whiskerLeft_apply] rw [LinearMap.zero_apply, TensorProduct.tmul_zero] · dsimp only [autoParam]; intros refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _) simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply] rw [LinearMap.zero_apply] -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [MonoidalCategory.hom_apply] + erw [MonoidalCategory.whiskerRight_apply] rw [LinearMap.zero_apply, TensorProduct.zero_tmul] · dsimp only [autoParam]; intros refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _) simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply] rw [LinearMap.add_apply] -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [MonoidalCategory.hom_apply, MonoidalCategory.hom_apply] - erw [MonoidalCategory.hom_apply] + erw [MonoidalCategory.whiskerLeft_apply, MonoidalCategory.whiskerLeft_apply] + erw [MonoidalCategory.whiskerLeft_apply] rw [LinearMap.add_apply, TensorProduct.tmul_add] · dsimp only [autoParam]; intros refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _) simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply] rw [LinearMap.add_apply] -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [MonoidalCategory.hom_apply, MonoidalCategory.hom_apply] - erw [MonoidalCategory.hom_apply] + erw [MonoidalCategory.whiskerRight_apply, MonoidalCategory.whiskerRight_apply] + erw [MonoidalCategory.whiskerRight_apply] rw [LinearMap.add_apply, TensorProduct.add_tmul] -- Porting note: simp wasn't firing but rw was, annoying @@ -322,14 +322,14 @@ instance : MonoidalLinear R (ModuleCat.{u} R) := by simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply] rw [LinearMap.smul_apply] -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [MonoidalCategory.hom_apply, MonoidalCategory.hom_apply] + erw [MonoidalCategory.whiskerLeft_apply, MonoidalCategory.whiskerLeft_apply] rw [LinearMap.smul_apply, TensorProduct.tmul_smul] · dsimp only [autoParam]; intros refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _) simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply] rw [LinearMap.smul_apply] -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644 - erw [MonoidalCategory.hom_apply, MonoidalCategory.hom_apply] + erw [MonoidalCategory.whiskerRight_apply, MonoidalCategory.whiskerRight_apply] rw [LinearMap.smul_apply, TensorProduct.smul_tmul, TensorProduct.tmul_smul] end ModuleCat diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean index a8569e1313bd7..bb2468a4d14a8 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean @@ -54,7 +54,7 @@ theorem braiding_naturality_right (X : ModuleCat R) {Y Z : ModuleCat R} (f : Y @[simp] theorem hexagon_forward (X Y Z : ModuleCat.{u} R) : (α_ X Y Z).hom ≫ (braiding X _).hom ≫ (α_ Y Z X).hom = - ((braiding X Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ (braiding X Z).hom) := by + (braiding X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (braiding X Z).hom := by apply TensorProduct.ext_threefold intro x y z rfl @@ -64,7 +64,7 @@ set_option linter.uppercaseLean3 false in @[simp] theorem hexagon_reverse (X Y Z : ModuleCat.{u} R) : (α_ X Y Z).inv ≫ (braiding _ Z).hom ≫ (α_ Z X Y).inv = - (𝟙 X ⊗ (Y.braiding Z).hom) ≫ (α_ X Z Y).inv ≫ ((X.braiding Z).hom ⊗ 𝟙 Y) := by + X ◁ (Y.braiding Z).hom ≫ (α_ X Z Y).inv ≫ (X.braiding Z).hom ▷ Y := by apply (cancel_epi (α_ X Y Z).hom).1 apply TensorProduct.ext_threefold intro x y z diff --git a/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean index 6c78ad50cccbb..1a4c9a8cee547 100644 --- a/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean +++ b/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean @@ -291,7 +291,6 @@ theorem braiding_leftUnitor_aux₂ (X : C) : by (slice_lhs 2 3 => rw [← braiding_naturality_right]); simp only [assoc] _ = (α_ _ _ _).hom ≫ (_ ◁ (λ_ _).hom) := by rw [Iso.hom_inv_id, comp_id] _ = (ρ_ X).hom ▷ 𝟙_ C := by rw [triangle] - #align category_theory.braiding_left_unitor_aux₂ CategoryTheory.braiding_leftUnitor_aux₂ @[reassoc] @@ -324,7 +323,6 @@ theorem braiding_rightUnitor_aux₂ (X : C) : by (slice_lhs 2 3 => rw [← braiding_naturality_left]); simp only [assoc] _ = (α_ _ _ _).inv ≫ ((ρ_ _).hom ▷ _) := by rw [Iso.hom_inv_id, comp_id] _ = 𝟙_ C ◁ (λ_ X).hom := by rw [triangle_assoc_comp_right] - #align category_theory.braiding_right_unitor_aux₂ CategoryTheory.braiding_rightUnitor_aux₂ @[reassoc] diff --git a/Mathlib/CategoryTheory/Monoidal/Preadditive.lean b/Mathlib/CategoryTheory/Monoidal/Preadditive.lean index 4ced695752758..4fb557ff645db 100644 --- a/Mathlib/CategoryTheory/Monoidal/Preadditive.lean +++ b/Mathlib/CategoryTheory/Monoidal/Preadditive.lean @@ -202,7 +202,7 @@ theorem leftDistributor_assoc {J : Type} [Fintype J] (X Y : C) (f : J → C) : simp_rw [← id_tensorHom] simp only [← id_tensor_comp, biproduct.ι_π] simp only [id_tensor_comp, tensor_dite, comp_dite] - simp [id_tensorHom] + simp #align category_theory.left_distributor_assoc CategoryTheory.leftDistributor_assoc /-- The isomorphism showing how tensor product on the right distributes over direct sums. -/ diff --git a/Mathlib/Tactic/CategoryTheory/Coherence.lean b/Mathlib/Tactic/CategoryTheory/Coherence.lean index 4efcc6f2ecaf2..b08a2335840fa 100644 --- a/Mathlib/Tactic/CategoryTheory/Coherence.lean +++ b/Mathlib/Tactic/CategoryTheory/Coherence.lean @@ -262,7 +262,8 @@ elab_rules : tactic MonoidalCategory.whiskerRight_tensor, MonoidalCategory.whiskerRight_id, MonoidalCategory.whiskerLeft_comp, MonoidalCategory.whiskerLeft_id, MonoidalCategory.comp_whiskerRight, MonoidalCategory.id_whiskerRight, - MonoidalCategory.whisker_assoc]; + MonoidalCategory.whisker_assoc, + MonoidalCategory.id_tensorHom, MonoidalCategory.tensorHom_id]; -- I'm not sure if `tensorHom` should be expanded. try simp only [MonoidalCategory.tensorHom_def] )) diff --git a/Mathlib/Tactic/CategoryTheory/MonoidalComp.lean b/Mathlib/Tactic/CategoryTheory/MonoidalComp.lean index 4acfa6699d1f1..998bb02ec7870 100644 --- a/Mathlib/Tactic/CategoryTheory/MonoidalComp.lean +++ b/Mathlib/Tactic/CategoryTheory/MonoidalComp.lean @@ -90,22 +90,22 @@ instance refl (X : C) : MonoidalCoherence X X := ⟨𝟙 _⟩ @[simps] instance whiskerLeft (X Y Z : C) [MonoidalCoherence Y Z] : MonoidalCoherence (X ⊗ Y) (X ⊗ Z) := - ⟨𝟙 X ⊗ ⊗𝟙⟩ + ⟨X ◁ ⊗𝟙⟩ @[simps] instance whiskerRight (X Y Z : C) [MonoidalCoherence X Y] : MonoidalCoherence (X ⊗ Z) (Y ⊗ Z) := - ⟨⊗𝟙 ⊗ 𝟙 Z⟩ + ⟨⊗𝟙 ▷ Z⟩ @[simps] instance tensor_right (X Y : C) [MonoidalCoherence (𝟙_ C) Y] : MonoidalCoherence X (X ⊗ Y) := - ⟨(ρ_ X).inv ≫ (𝟙 X ⊗ ⊗𝟙)⟩ + ⟨(ρ_ X).inv ≫ X ◁ ⊗𝟙⟩ @[simps] instance tensor_right' (X Y : C) [MonoidalCoherence Y (𝟙_ C)] : MonoidalCoherence (X ⊗ Y) X := - ⟨(𝟙 X ⊗ ⊗𝟙) ≫ (ρ_ X).hom⟩ + ⟨X ◁ ⊗𝟙 ≫ (ρ_ X).hom⟩ @[simps] instance left (X Y : C) [MonoidalCoherence X Y] :