Documentation

Mathlib.CategoryTheory.Preadditive.OfBiproducts

Constructing a semiadditive structure from binary biproducts #

We show that any category with zero morphisms and binary biproducts is enriched over the category of commutative monoids.

source
def CategoryTheory.SemiadditiveOfBinaryBiproducts.leftAdd {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproducts C] (X Y : C) (f g : X ⟶ Y) :
X ⟶ Y

f +ₗ g is the composite X ⟶ Y ⊞ Y ⟶ Y, where the first map is (f, g) and the second map is (𝟙 𝟙).

Equations
    Instances For
      source
      def CategoryTheory.SemiadditiveOfBinaryBiproducts.rightAdd {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproducts C] (X Y : C) (f g : X ⟶ Y) :
      X ⟶ Y

      f +ᵣ g is the composite X ⟶ X ⊞ X ⟶ Y, where the first map is (𝟙, 𝟙) and the second map is (f g).

      Equations
        Instances For
          source
          theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.isUnital_leftAdd {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproducts C] (X Y : C) :
          EckmannHilton.IsUnital (fun (x1 x2 : X ⟶ Y) => leftAdd X Y x1 x2) 0
          source
          theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.isUnital_rightAdd {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproducts C] (X Y : C) :
          EckmannHilton.IsUnital (fun (x1 x2 : X ⟶ Y) => rightAdd X Y x1 x2) 0
          source
          theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.distrib {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproducts C] (X Y : C) (f g h k : X ⟶ Y) :
          leftAdd X Y (rightAdd X Y f g) (rightAdd X Y h k) = rightAdd X Y (leftAdd X Y f h) (leftAdd X Y g k)
          source
          def CategoryTheory.SemiadditiveOfBinaryBiproducts.addCommMonoidHomOfHasBinaryBiproducts {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproducts C] (X Y : C) :
          AddCommMonoid (X ⟶ Y)

          In a category with binary biproducts, the morphisms form a commutative monoid.

          Equations
            Instances For
              source
              theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.add_eq_right_addition {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproducts C] {X Y : C} (f g : X ⟶ Y) :
              f + g = CategoryStruct.comp (Limits.biprod.lift (CategoryStruct.id X) (CategoryStruct.id X)) (Limits.biprod.desc f g)
              source
              theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.add_eq_left_addition {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproducts C] {X Y : C} (f g : X ⟶ Y) :
              f + g = CategoryStruct.comp (Limits.biprod.lift f g) (Limits.biprod.desc (CategoryStruct.id Y) (CategoryStruct.id Y))
              source
              theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.add_comp {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproducts C] {X Y Z : C} (f g : X ⟶ Y) (h : Y ⟶ Z) :
              CategoryStruct.comp (f + g) h = CategoryStruct.comp f h + CategoryStruct.comp g h
              source
              theorem CategoryTheory.SemiadditiveOfBinaryBiproducts.comp_add {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] [Limits.HasBinaryBiproducts C] {X Y Z : C} (f : X ⟶ Y) (g h : Y ⟶ Z) :
              CategoryStruct.comp f (g + h) = CategoryStruct.comp f g + CategoryStruct.comp f h