chore: cleanup API for distributors in preadditive monoidal categories (

#6257) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Aug 1, 2023 · 881c646 · 881c646
1 parent c8214aa
commit 881c646
Showing 1 changed file with 143 additions and 15 deletions.
diff --git a/Mathlib/CategoryTheory/Monoidal/Preadditive.lean b/Mathlib/CategoryTheory/Monoidal/Preadditive.lean
@@ -138,7 +138,6 @@ def leftDistributor {J : Type} [Fintype J] (X : C) (f : J → C) : X ⊗ ⨁ f
   (tensorLeft X).mapBiproduct f
 #align category_theory.left_distributor CategoryTheory.leftDistributor
 
-@[simp]
 theorem leftDistributor_hom {J : Type} [Fintype J] (X : C) (f : J → C) :
     (leftDistributor X f).hom =
       ∑ j : J, (𝟙 X ⊗ biproduct.π f j) ≫ biproduct.ι (fun j => X ⊗ f j) j := by
@@ -149,7 +148,6 @@ theorem leftDistributor_hom {J : Type} [Fintype J] (X : C) (f : J → C) :
     Finset.sum_dite_eq', Finset.mem_univ, ite_true, eqToHom_refl, Category.comp_id]
 #align category_theory.left_distributor_hom CategoryTheory.leftDistributor_hom
 
-@[simp]
 theorem leftDistributor_inv {J : Type} [Fintype J] (X : C) (f : J → C) :
     (leftDistributor X f).inv = ∑ j : J, biproduct.π _ j ≫ (𝟙 X ⊗ biproduct.ι f j) := by
   ext
@@ -159,6 +157,28 @@ theorem leftDistributor_inv {J : Type} [Fintype J] (X : C) (f : J → C) :
     biproduct.ι_desc]
 #align category_theory.left_distributor_inv CategoryTheory.leftDistributor_inv
 
+@[reassoc (attr := simp)]
+theorem leftDistributor_hom_comp_biproduct_π {J : Type} [Fintype J] (X : C) (f : J → C) (j : J) :
+    (leftDistributor X f).hom ≫ biproduct.π _ j = 𝟙 X ⊗ biproduct.π _ j := by
+  simp [leftDistributor_hom, Preadditive.sum_comp, biproduct.ι_π, comp_dite]
+
+@[reassoc (attr := simp)]
+theorem biproduct_ι_comp_leftDistributor_hom {J : Type} [Fintype J] (X : C) (f : J → C) (j : J) :
+    (𝟙 X ⊗ biproduct.ι _ j) ≫ (leftDistributor X f).hom = biproduct.ι (fun j => X ⊗ f j) j := by
+  simp [leftDistributor_hom, Preadditive.comp_sum, ← id_tensor_comp_assoc, biproduct.ι_π,
+    tensor_dite, dite_comp]
+
+@[reassoc (attr := simp)]
+theorem leftDistributor_inv_comp_biproduct_π {J : Type} [Fintype J] (X : C) (f : J → C) (j : J) :
+    (leftDistributor X f).inv ≫ (𝟙 X ⊗ biproduct.π _ j) = biproduct.π _ j := by
+  simp [leftDistributor_inv, Preadditive.sum_comp, ← id_tensor_comp, biproduct.ι_π, tensor_dite,
+    comp_dite]
+
+@[reassoc (attr := simp)]
+theorem biproduct_ι_comp_leftDistributor_inv {J : Type} [Fintype J] (X : C) (f : J → C) (j : J) :
+    biproduct.ι _ j ≫ (leftDistributor X f).inv = 𝟙 X ⊗ biproduct.ι _ j := by
+  simp [leftDistributor_inv, Preadditive.comp_sum, ← id_tensor_comp, biproduct.ι_π_assoc, dite_comp]
+
 theorem leftDistributor_assoc {J : Type} [Fintype J] (X Y : C) (f : J → C) :
     (asIso (𝟙 X) ⊗ leftDistributor Y f) ≪≫ leftDistributor X _ =
       (α_ X Y (⨁ f)).symm ≪≫ leftDistributor (X ⊗ Y) f ≪≫ biproduct.mapIso fun j => α_ X Y _ := by
@@ -175,13 +195,12 @@ theorem leftDistributor_assoc {J : Type} [Fintype J] (X Y : C) (f : J → C) :
 #align category_theory.left_distributor_assoc CategoryTheory.leftDistributor_assoc
 
 /-- The isomorphism showing how tensor product on the right distributes over direct sums. -/
-def rightDistributor {J : Type} [Fintype J] (X : C) (f : J → C) : (⨁ f) ⊗ X ≅ ⨁ fun j => f j ⊗ X :=
+def rightDistributor {J : Type} [Fintype J] (f : J → C) (X : C) : (⨁ f) ⊗ X ≅ ⨁ fun j => f j ⊗ X :=
   (tensorRight X).mapBiproduct f
 #align category_theory.right_distributor CategoryTheory.rightDistributor
 
-@[simp]
-theorem rightDistributor_hom {J : Type} [Fintype J] (X : C) (f : J → C) :
-    (rightDistributor X f).hom =
+theorem rightDistributor_hom {J : Type} [Fintype J] (f : J → C) (X : C) :
+    (rightDistributor f X).hom =
       ∑ j : J, (biproduct.π f j ⊗ 𝟙 X) ≫ biproduct.ι (fun j => f j ⊗ X) j := by
   ext
   dsimp [rightDistributor, Functor.mapBiproduct, Functor.mapBicone]
@@ -190,18 +209,40 @@ theorem rightDistributor_hom {J : Type} [Fintype J] (X : C) (f : J → C) :
     Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, ite_true]
 #align category_theory.right_distributor_hom CategoryTheory.rightDistributor_hom
 
-@[simp]
-theorem rightDistributor_inv {J : Type} [Fintype J] (X : C) (f : J → C) :
-    (rightDistributor X f).inv = ∑ j : J, biproduct.π _ j ≫ (biproduct.ι f j ⊗ 𝟙 X) := by
+theorem rightDistributor_inv {J : Type} [Fintype J] (f : J → C) (X : C) :
+    (rightDistributor f X).inv = ∑ j : J, biproduct.π _ j ≫ (biproduct.ι f j ⊗ 𝟙 X) := by
   ext
   dsimp [rightDistributor, Functor.mapBiproduct, Functor.mapBicone]
   simp only [biproduct.ι_desc, Preadditive.comp_sum, ne_eq, biproduct.ι_π_assoc, dite_comp,
     zero_comp, Finset.sum_dite_eq, Finset.mem_univ, eqToHom_refl, Category.id_comp, ite_true]
 #align category_theory.right_distributor_inv CategoryTheory.rightDistributor_inv
 
-theorem rightDistributor_assoc {J : Type} [Fintype J] (X Y : C) (f : J → C) :
-    (rightDistributor X f ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor Y _ =
-      α_ (⨁ f) X Y ≪≫ rightDistributor (X ⊗ Y) f ≪≫ biproduct.mapIso fun j => (α_ _ X Y).symm := by
+@[reassoc (attr := simp)]
+theorem rightDistributor_hom_comp_biproduct_π {J : Type} [Fintype J] (f : J → C) (X : C) (j : J) :
+    (rightDistributor f X).hom ≫ biproduct.π _ j = biproduct.π _ j ⊗ 𝟙 X := by
+  simp [rightDistributor_hom, Preadditive.sum_comp, biproduct.ι_π, comp_dite]
+
+@[reassoc (attr := simp)]
+theorem biproduct_ι_comp_rightDistributor_hom {J : Type} [Fintype J] (f : J → C) (X : C) (j : J) :
+    (biproduct.ι _ j ⊗ 𝟙 X) ≫ (rightDistributor f X).hom = biproduct.ι (fun j => f j ⊗ X) j := by
+  simp [rightDistributor_hom, Preadditive.comp_sum, ← comp_tensor_id_assoc, biproduct.ι_π,
+    dite_tensor, dite_comp]
+
+@[reassoc (attr := simp)]
+theorem rightDistributor_inv_comp_biproduct_π {J : Type} [Fintype J] (f : J → C) (X : C) (j : J) :
+    (rightDistributor f X).inv ≫ (biproduct.π _ j ⊗ 𝟙 X) = biproduct.π _ j := by
+  simp [rightDistributor_inv, Preadditive.sum_comp, ← comp_tensor_id, biproduct.ι_π, dite_tensor,
+    comp_dite]
+
+@[reassoc (attr := simp)]
+theorem biproduct_ι_comp_rightDistributor_inv {J : Type} [Fintype J] (f : J → C) (X : C) (j : J) :
+    biproduct.ι _ j ≫ (rightDistributor f X).inv = biproduct.ι _ j ⊗ 𝟙 X := by
+  simp [rightDistributor_inv, Preadditive.comp_sum, ← id_tensor_comp, biproduct.ι_π_assoc,
+    dite_comp]
+
+theorem rightDistributor_assoc {J : Type} [Fintype J] (f : J → C) (X Y : C) :
+    (rightDistributor f X ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor _ Y =
+      α_ (⨁ f) X Y ≪≫ rightDistributor f (X ⊗ Y) ≪≫ biproduct.mapIso fun j => (α_ _ X Y).symm := by
   ext
   simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.symm_hom, Iso.trans_hom,
     asIso_hom, comp_zero, comp_dite, Preadditive.sum_comp, Preadditive.comp_sum, sum_tensor,
@@ -215,10 +256,11 @@ theorem rightDistributor_assoc {J : Type} [Fintype J] (X Y : C) (f : J → C) :
   simp only [← tensor_id, associator_inv_naturality, Iso.hom_inv_id_assoc]
 #align category_theory.right_distributor_assoc CategoryTheory.rightDistributor_assoc
 
-theorem leftDistributor_rightDistributor_assoc {J : Type _} [Fintype J] (X Y : C) (f : J → C) :
-    (leftDistributor X f ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor Y _ =
+theorem leftDistributor_rightDistributor_assoc {J : Type _} [Fintype J]
+    (X : C) (f : J → C) (Y : C) :
+    (leftDistributor X f ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor _ Y =
       α_ X (⨁ f) Y ≪≫
-        (asIso (𝟙 X) ⊗ rightDistributor Y _) ≪≫
+        (asIso (𝟙 X) ⊗ rightDistributor _ Y) ≪≫
           leftDistributor X _ ≪≫ biproduct.mapIso fun j => (α_ _ _ _).symm := by
   ext
   simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.symm_hom, Iso.trans_hom,
@@ -235,4 +277,90 @@ theorem leftDistributor_rightDistributor_assoc {J : Type _} [Fintype J] (X Y : C
   simp only [associator_inv_naturality, Iso.hom_inv_id_assoc]
 #align category_theory.left_distributor_right_distributor_assoc CategoryTheory.leftDistributor_rightDistributor_assoc
 
+@[ext]
+theorem leftDistributor_ext_left {J : Type} [Fintype J] {X Y : C} {f : J → C} {g h : X ⊗ ⨁ f ⟶ Y}
+    (w : ∀ j, (𝟙 X ⊗ biproduct.ι f j) ≫ g = (𝟙 X ⊗ biproduct.ι f j) ≫ h) : g = h := by
+  apply (cancel_epi (leftDistributor X f).inv).mp
+  ext
+  simp? [leftDistributor_inv, Preadditive.comp_sum_assoc, biproduct.ι_π_assoc, dite_comp] says
+    simp only [leftDistributor_inv, Preadditive.comp_sum_assoc, ne_eq, biproduct.ι_π_assoc,
+      dite_comp, zero_comp, Finset.sum_dite_eq, Finset.mem_univ, eqToHom_refl, Category.id_comp,
+      ite_true]
+  apply w
+
+@[ext]
+theorem leftDistributor_ext_right {J : Type} [Fintype J] {X Y : C} {f : J → C} {g h : X ⟶ Y ⊗ ⨁ f}
+    (w : ∀ j, g ≫ (𝟙 Y ⊗ biproduct.π f j) = h ≫ (𝟙 Y ⊗ biproduct.π f j)) : g = h := by
+  apply (cancel_mono (leftDistributor Y f).hom).mp
+  ext
+  simp? [leftDistributor_hom, Preadditive.sum_comp, Preadditive.comp_sum_assoc, biproduct.ι_π,
+    comp_dite] says
+    simp only [leftDistributor_hom, Category.assoc, Preadditive.sum_comp, ne_eq, biproduct.ι_π,
+      comp_dite, comp_zero, Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id,
+      ite_true]
+  apply w
+
+-- One might wonder how many iterated tensor products we need simp lemmas for.
+-- The answer is two: this lemma is needed to verify the pentagon identity.
+@[ext]
+theorem leftDistributor_ext₂_left {J : Type} [Fintype J]
+    {X Y Z : C} {f : J → C} {g h : X ⊗ (Y ⊗ ⨁ f) ⟶ Z}
+    (w : ∀ j, (𝟙 X ⊗ (𝟙 Y ⊗ biproduct.ι f j)) ≫ g = (𝟙 X ⊗ (𝟙 Y ⊗ biproduct.ι f j)) ≫ h) :
+    g = h := by
+  apply (cancel_epi (α_ _ _ _).hom).mp
+  ext
+  simp_rw [← tensor_id, associator_naturality_assoc, w]
+
+@[ext]
+theorem leftDistributor_ext₂_right {J : Type} [Fintype J]
+    {X Y Z : C} {f : J → C} {g h : X ⟶ Y ⊗ (Z ⊗ ⨁ f)}
+    (w : ∀ j, g ≫ (𝟙 Y ⊗ (𝟙 Z ⊗ biproduct.π f j)) = h ≫ (𝟙 Y ⊗ (𝟙 Z ⊗ biproduct.π f j))) :
+    g = h := by
+  apply (cancel_mono (α_ _ _ _).inv).mp
+  ext
+  simp_rw [← tensor_id, Category.assoc, ← associator_inv_naturality, ← Category.assoc, w]
+
+@[ext]
+theorem rightDistributor_ext_left {J : Type} [Fintype J]
+    {f : J → C} {X Y : C} {g h : (⨁ f) ⊗ X ⟶ Y}
+    (w : ∀ j, (biproduct.ι f j ⊗ 𝟙 X) ≫ g = (biproduct.ι f j ⊗ 𝟙 X) ≫ h) : g = h := by
+  apply (cancel_epi (rightDistributor f X).inv).mp
+  ext
+  simp? [rightDistributor_inv, Preadditive.comp_sum_assoc, biproduct.ι_π_assoc, dite_comp] says
+    simp only [rightDistributor_inv, Preadditive.comp_sum_assoc, ne_eq, biproduct.ι_π_assoc,
+      dite_comp, zero_comp, Finset.sum_dite_eq, Finset.mem_univ, eqToHom_refl, Category.id_comp,
+      ite_true]
+  apply w
+
+@[ext]
+theorem rightDistributor_ext_right {J : Type} [Fintype J]
+    {f : J → C} {X Y : C} {g h : X ⟶ (⨁ f) ⊗ Y}
+    (w : ∀ j, g ≫ (biproduct.π f j ⊗ 𝟙 Y) = h ≫ (biproduct.π f j ⊗ 𝟙 Y)) : g = h := by
+  apply (cancel_mono (rightDistributor f Y).hom).mp
+  ext
+  simp? [rightDistributor_hom, Preadditive.sum_comp, Preadditive.comp_sum_assoc, biproduct.ι_π,
+    comp_dite] says
+    simp only [rightDistributor_hom, Category.assoc, Preadditive.sum_comp, ne_eq, biproduct.ι_π,
+      comp_dite, comp_zero, Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id,
+      ite_true]
+  apply w
+
+@[ext]
+theorem rightDistributor_ext₂_left {J : Type} [Fintype J]
+    {f : J → C} {X Y Z : C} {g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z}
+    (w : ∀ j, ((biproduct.ι f j ⊗ 𝟙 X) ⊗ 𝟙 Y) ≫ g = ((biproduct.ι f j ⊗ 𝟙 X) ⊗ 𝟙 Y) ≫ h) :
+    g = h := by
+  apply (cancel_epi (α_ _ _ _).inv).mp
+  ext
+  simp_rw [← tensor_id, associator_inv_naturality_assoc, w]
+
+@[ext]
+theorem rightDistributor_ext₂_right {J : Type} [Fintype J]
+    {f : J → C} {X Y Z : C} {g h : X ⟶ ((⨁ f) ⊗ Y) ⊗ Z}
+    (w : ∀ j, g ≫ ((biproduct.π f j ⊗ 𝟙 Y) ⊗ 𝟙 Z) = h ≫ ((biproduct.π f j ⊗ 𝟙 Y) ⊗ 𝟙 Z)) :
+    g = h := by
+  apply (cancel_mono (α_ _ _ _).hom).mp
+  ext
+  simp_rw [← tensor_id, Category.assoc, ← associator_naturality, ← Category.assoc, w]
+
 end CategoryTheory