From dc9ef57eb7d8ab4fa05742c84f3ea69789957fec Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 12 Sep 2023 23:07:38 +0000 Subject: [PATCH] feat(CategoryTheory/Limits/Shapes/Biproducts): add associator --- .../Limits/Shapes/Biproducts.lean | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean index 520e0a6bd9332..54f34b82aeeb7 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean @@ -1960,6 +1960,26 @@ theorem biprod.symmetry (P Q : C) : (biprod.braiding P Q).hom ≫ (biprod.braidi by simp #align category_theory.limits.biprod.symmetry CategoryTheory.Limits.biprod.symmetry +/-- The associator isomorphism which associates a binary biproduct. -/ +@[simps] +def biprod.associator (P Q R : C) : (P ⊞ Q) ⊞ R ≅ P ⊞ (Q ⊞ R) where + hom := biprod.lift (biprod.fst ≫ biprod.fst) (biprod.lift (biprod.fst ≫ biprod.snd) biprod.snd) + inv := biprod.lift (biprod.lift biprod.fst (biprod.snd ≫ biprod.fst)) (biprod.snd ≫ biprod.snd) + +/-- The associator isomorphism can be passed through a map by swapping the order. -/ +@[reassoc] +theorem biprod.associator_natural {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (g : W ⟶ Z) : + biprod.map (biprod.map f g) h ≫ (biprod.associator _ _ _).hom + = (biprod.associator _ _ _).hom ≫ biprod.map f (biprod.map g h) := by + aesop_cat + +/-- The associator isomorphism can be passed through a map by swapping the order. -/ +@[reassoc] +theorem biprod.associator_inv_natural {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (g : W ⟶ Z) : + biprod.map f (biprod.map g h) ≫ (biprod.associator _ _ _).inv + = (biprod.associator _ _ _).inv ≫ biprod.map (biprod.map f g) h := by + aesop_cat + end end Limits