Preservation of biproducts #

We define the image of a (binary) bicone under a functor that preserves zero morphisms and define classes PreservesBiproduct and PreservesBinaryBiproduct. We then

show that a functor that preserves biproducts of a two-element type preserves binary biproducts,
construct the comparison morphisms between the image of a biproduct and the biproduct of the images and show that the biproduct is preserved if one of them is an isomorphism,
give the canonical isomorphism between the image of a biproduct and the biproduct of the images in case that the biproduct is preserved.

source

def CategoryTheory.Functor.mapBicone {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} {f : J → C} (b : Limits.Bicone f) :

Limits.Bicone (F.obj ∘ f)

The image of a bicone under a functor.

Equations

F.mapBicone b = { pt := F.obj b.pt, π := fun (j : J) => F.map (b.π j), ι := fun (j : J) => F.map (b.ι j), ι_π := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.Functor.mapBicone_ι {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} {f : J → C} (b : Limits.Bicone f) (j : J) :

(F.mapBicone b).ι j = F.map (b.ι j)

source

@[simp]

theorem CategoryTheory.Functor.mapBicone_pt {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} {f : J → C} (b : Limits.Bicone f) :

(F.mapBicone b).pt = F.obj b.pt

source

@[simp]

theorem CategoryTheory.Functor.mapBicone_π {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} {f : J → C} (b : Limits.Bicone f) (j : J) :

(F.mapBicone b).π j = F.map (b.π j)

source

theorem CategoryTheory.Functor.mapBicone_whisker {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} {K : Type w₂} {g : K ≃ J} {f : J → C} (c : Limits.Bicone f) :

F.mapBicone (c.whisker g) = (F.mapBicone c).whisker g

source

def CategoryTheory.Functor.mapBinaryBicone {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (b : Limits.BinaryBicone X Y) :

Limits.BinaryBicone (F.obj X) (F.obj Y)

The image of a binary bicone under a functor.

Equations

F.mapBinaryBicone b = (CategoryTheory.Limits.BinaryBicones.functoriality X Y F).obj b

Instances For

source

@[simp]

theorem CategoryTheory.Functor.mapBinaryBicone_inl {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (b : Limits.BinaryBicone X Y) :

(F.mapBinaryBicone b).inl = F.map b.inl

source

@[simp]

theorem CategoryTheory.Functor.mapBinaryBicone_snd {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (b : Limits.BinaryBicone X Y) :

(F.mapBinaryBicone b).snd = F.map b.snd

source

@[simp]

theorem CategoryTheory.Functor.mapBinaryBicone_inr {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (b : Limits.BinaryBicone X Y) :

(F.mapBinaryBicone b).inr = F.map b.inr

source

@[simp]

theorem CategoryTheory.Functor.mapBinaryBicone_pt {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (b : Limits.BinaryBicone X Y) :

(F.mapBinaryBicone b).pt = F.obj b.pt

source

@[simp]

theorem CategoryTheory.Functor.mapBinaryBicone_fst {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {X Y : C} (b : Limits.BinaryBicone X Y) :

(F.mapBinaryBicone b).fst = F.map b.fst

source

class CategoryTheory.Limits.PreservesBiproduct {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] {J : Type w₁} (f : J → C) (F : Functor C D) [F.PreservesZeroMorphisms] :

Prop

A functor F preserves biproducts of f if F maps every bilimit bicone over f to a bilimit bicone over F.obj ∘ f.

preserves {b : Bicone f} : ∀ (a : b.IsBilimit), Nonempty (F.mapBicone b).IsBilimit
A functor F preserves biproducts of f if F maps every bilimit bicone over f to a bilimit bicone over F.obj ∘ f.

Instances

source

def CategoryTheory.Limits.isBilimitOfPreserves {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] {J : Type w₁} {f : J → C} (F : Functor C D) [F.PreservesZeroMorphisms] [PreservesBiproduct f F] {b : Bicone f} (hb : b.IsBilimit) :

(F.mapBicone b).IsBilimit

A functor F preserves biproducts of f if F maps every bilimit bicone over f to a bilimit bicone over F.obj ∘ f.

Equations

CategoryTheory.Limits.isBilimitOfPreserves F hb = ⋯.some

Instances For

source

class CategoryTheory.Limits.PreservesBiproductsOfShape {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (J : Type w₁) (F : Functor C D) [F.PreservesZeroMorphisms] :

Prop

A functor F preserves biproducts of shape J if it preserves biproducts of f for every f : J → C.

preserves {f : J → C} : PreservesBiproduct f F
A functor F preserves biproducts of shape J if it preserves biproducts of f for every f : J → C.

Instances

source

class CategoryTheory.Limits.PreservesFiniteBiproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] :

Prop

A functor F preserves finite biproducts if it preserves biproducts of shape J whenever J is a finite type.

preserves {J : Type} [Finite J] : PreservesBiproductsOfShape J F
A functor F preserves finite biproducts if it preserves biproducts of shape J whenever J is a finite type.

Instances

source

class CategoryTheory.Limits.PreservesBiproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] :

Prop

A functor F preserves biproducts if it preserves biproducts of any shape J of size w. The usual notion of preservation of biproducts is recovered by choosing w to be the universe of the morphisms of C.

preserves {J : Type w₁} : PreservesBiproductsOfShape J F
A functor F preserves biproducts if it preserves biproducts of any shape J of size w. The usual notion of preservation of biproducts is recovered by choosing w to be the universe of the morphisms of C.

Instances

source

theorem CategoryTheory.Limits.preservesBiproducts_shrink {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] [PreservesBiproducts F] :

PreservesBiproducts F

Preserving biproducts at a bigger universe level implies preserving biproducts at a smaller universe level.

source

@[instance 100]

instance CategoryTheory.Limits.preservesFiniteBiproductsOfPreservesBiproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] [PreservesBiproducts F] :

PreservesFiniteBiproducts F

source

class CategoryTheory.Limits.PreservesBinaryBiproduct {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (X Y : C) (F : Functor C D) [F.PreservesZeroMorphisms] :

Prop

A functor F preserves binary biproducts of X and Y if F maps every bilimit bicone over X and Y to a bilimit bicone over F.obj X and F.obj Y.

preserves {b : BinaryBicone X Y} : ∀ (a : b.IsBilimit), Nonempty (F.mapBinaryBicone b).IsBilimit
A functor F preserves binary biproducts of X and Y if F maps every bilimit bicone over X and Y to a bilimit bicone over F.obj X and F.obj Y.

Instances

source

def CategoryTheory.Limits.isBinaryBilimitOfPreserves {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] {X Y : C} (F : Functor C D) [F.PreservesZeroMorphisms] [PreservesBinaryBiproduct X Y F] {b : BinaryBicone X Y} (hb : b.IsBilimit) :

(F.mapBinaryBicone b).IsBilimit

A functor F preserves binary biproducts of X and Y if F maps every bilimit bicone over X and Y to a bilimit bicone over F.obj X and F.obj Y.

Equations

CategoryTheory.Limits.isBinaryBilimitOfPreserves F hb = ⋯.some

Instances For

source

class CategoryTheory.Limits.PreservesBinaryBiproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] :

Prop

A functor F preserves binary biproducts if it preserves the binary biproduct of X and Y for all X and Y.

preserves {X Y : C} : PreservesBinaryBiproduct X Y F
A functor F preserves binary biproducts if it preserves the binary biproduct of X and Y for all X and Y.

Instances

source

theorem CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBiproduct {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] (X Y : C) [PreservesBiproduct (pairFunction X Y) F] :

PreservesBinaryBiproduct X Y F

A functor that preserves biproducts of a pair preserves binary biproducts.

source

theorem CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBiproducts {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] [PreservesBiproductsOfShape WalkingPair F] :

PreservesBinaryBiproducts F

A functor that preserves biproducts of a pair preserves binary biproducts.

source

def CategoryTheory.Functor.biproductComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] :

F.obj (⨁ f) ⟶ ⨁ F.obj ∘ f

As for products, any functor between categories with biproducts gives rise to a morphism F.obj (⨁ f) ⟶ ⨁ (F.obj ∘ f).

Equations

F.biproductComparison f = CategoryTheory.Limits.biproduct.lift fun (j : J) => F.map (CategoryTheory.Limits.biproduct.π f j)

Instances For

source

@[simp]

theorem CategoryTheory.Functor.biproductComparison_π {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] (j : J) :

CategoryStruct.comp (F.biproductComparison f) (Limits.biproduct.π (F.obj ∘ f) j) = F.map (Limits.biproduct.π f j)

source

@[simp]

theorem CategoryTheory.Functor.biproductComparison_π_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] (j : J) {Z : D} (h : (F.obj ∘ f) j ⟶ Z) :

CategoryStruct.comp (F.biproductComparison f) (CategoryStruct.comp (Limits.biproduct.π (F.obj ∘ f) j) h) = CategoryStruct.comp (F.map (Limits.biproduct.π f j)) h

source

def CategoryTheory.Functor.biproductComparison' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] :

⨁ F.obj ∘ f ⟶ F.obj (⨁ f)

As for coproducts, any functor between categories with biproducts gives rise to a morphism ⨁ (F.obj ∘ f) ⟶ F.obj (⨁ f)

Equations

F.biproductComparison' f = CategoryTheory.Limits.biproduct.desc fun (j : J) => F.map (CategoryTheory.Limits.biproduct.ι f j)

Instances For

source

@[simp]

theorem CategoryTheory.Functor.ι_biproductComparison' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] (j : J) :

CategoryStruct.comp (Limits.biproduct.ι (F.obj ∘ f) j) (F.biproductComparison' f) = F.map (Limits.biproduct.ι f j)

source

@[simp]

theorem CategoryTheory.Functor.ι_biproductComparison'_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] (j : J) {Z : D} (h : F.obj (⨁ f) ⟶ Z) :

CategoryStruct.comp (Limits.biproduct.ι (F.obj ∘ f) j) (CategoryStruct.comp (F.biproductComparison' f) h) = CategoryStruct.comp (F.map (Limits.biproduct.ι f j)) h

source

@[simp]

theorem CategoryTheory.Functor.biproductComparison'_comp_biproductComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms] :

CategoryStruct.comp (F.biproductComparison' f) (F.biproductComparison f) = CategoryStruct.id (⨁ F.obj ∘ f)

The composition in the opposite direction is equal to the identity if and only if F preserves the biproduct, see preservesBiproduct_of_monoBiproductComparison.

source

@[simp]

theorem CategoryTheory.Functor.biproductComparison'_comp_biproductComparison_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms] {Z : D} (h : ⨁ F.obj ∘ f ⟶ Z) :

CategoryStruct.comp (F.biproductComparison' f) (CategoryStruct.comp (F.biproductComparison f) h) = h

The composition in the opposite direction is equal to the identity if and only if F preserves the biproduct, see preservesBiproduct_of_monoBiproductComparison.

source

def CategoryTheory.Functor.splitEpiBiproductComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms] :

SplitEpi (F.biproductComparison f)

biproduct_comparison F f is a split epimorphism.

Equations

F.splitEpiBiproductComparison f = { section_ := F.biproductComparison' f, id := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.Functor.splitEpiBiproductComparison_section_ {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms] :

(F.splitEpiBiproductComparison f).section_ = F.biproductComparison' f

source

instance CategoryTheory.Functor.instIsSplitEpiBiproductComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms] :

IsSplitEpi (F.biproductComparison f)

source

def CategoryTheory.Functor.splitMonoBiproductComparison' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms] :

SplitMono (F.biproductComparison' f)

biproduct_comparison' F f is a split monomorphism.

Equations

F.splitMonoBiproductComparison' f = { retraction := F.biproductComparison f, id := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.Functor.splitMonoBiproductComparison'_retraction {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms] :

(F.splitMonoBiproductComparison' f).retraction = F.biproductComparison f

source

instance CategoryTheory.Functor.instIsSplitMonoBiproductComparison' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms] :

IsSplitMono (F.biproductComparison' f)

source

instance CategoryTheory.Functor.hasBiproduct_of_preserves {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [F.PreservesZeroMorphisms] [Limits.PreservesBiproduct f F] :

Limits.HasBiproduct (F.obj ∘ f)

source

@[instance 100]

instance CategoryTheory.Functor.hasBiproduct_of_preserves' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [F.PreservesZeroMorphisms] [Limits.PreservesBiproduct f F] :

Limits.HasBiproduct fun (i : J) => F.obj (f i)

This instance applies more often than hasBiproduct_of_preserves, but the discrimination tree key matches a lot more (since it does not look through lambdas).

source

@[reducible, inline]

abbrev CategoryTheory.Functor.mapBiproduct {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [F.PreservesZeroMorphisms] [Limits.PreservesBiproduct f F] :

F.obj (⨁ f) ≅ ⨁ F.obj ∘ f

If F preserves a biproduct, we get a definitionally nice isomorphism F.obj (⨁ f) ≅ ⨁ (F.obj ∘ f).

Equations

F.mapBiproduct f = CategoryTheory.Limits.biproduct.uniqueUpToIso (F.obj ∘ f) (CategoryTheory.Limits.isBilimitOfPreserves F (CategoryTheory.Limits.biproduct.isBilimit f))

Instances For

source

theorem CategoryTheory.Functor.mapBiproduct_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [F.PreservesZeroMorphisms] [Limits.PreservesBiproduct f F] :

(F.mapBiproduct f).hom = Limits.biproduct.lift fun (j : J) => F.map (Limits.biproduct.π f j)

source

theorem CategoryTheory.Functor.mapBiproduct_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {J : Type w₁} (F : Functor C D) (f : J → C) [Limits.HasBiproduct f] [F.PreservesZeroMorphisms] [Limits.PreservesBiproduct f F] :

(F.mapBiproduct f).inv = Limits.biproduct.desc fun (j : J) => F.map (Limits.biproduct.ι f j)

source

def CategoryTheory.Functor.biprodComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] :

F.obj (X ⊞ Y) ⟶ F.obj X ⊞ F.obj Y

As for products, any functor between categories with binary biproducts gives rise to a morphism F.obj (X ⊞ Y) ⟶ F.obj X ⊞ F.obj Y.

Equations

F.biprodComparison X Y = CategoryTheory.Limits.biprod.lift (F.map CategoryTheory.Limits.biprod.fst) (F.map CategoryTheory.Limits.biprod.snd)

Instances For

source

@[simp]

theorem CategoryTheory.Functor.biprodComparison_fst {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] :

CategoryStruct.comp (F.biprodComparison X Y) Limits.biprod.fst = F.map Limits.biprod.fst

source

@[simp]

theorem CategoryTheory.Functor.biprodComparison_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] {Z : D} (h : F.obj X ⟶ Z) :

CategoryStruct.comp (F.biprodComparison X Y) (CategoryStruct.comp Limits.biprod.fst h) = CategoryStruct.comp (F.map Limits.biprod.fst) h

source

@[simp]

theorem CategoryTheory.Functor.biprodComparison_snd {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] :

CategoryStruct.comp (F.biprodComparison X Y) Limits.biprod.snd = F.map Limits.biprod.snd

source

@[simp]

theorem CategoryTheory.Functor.biprodComparison_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] {Z : D} (h : F.obj Y ⟶ Z) :

CategoryStruct.comp (F.biprodComparison X Y) (CategoryStruct.comp Limits.biprod.snd h) = CategoryStruct.comp (F.map Limits.biprod.snd) h

source

def CategoryTheory.Functor.biprodComparison' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] :

F.obj X ⊞ F.obj Y ⟶ F.obj (X ⊞ Y)

As for coproducts, any functor between categories with binary biproducts gives rise to a morphism F.obj X ⊞ F.obj Y ⟶ F.obj (X ⊞ Y).

Equations

F.biprodComparison' X Y = CategoryTheory.Limits.biprod.desc (F.map CategoryTheory.Limits.biprod.inl) (F.map CategoryTheory.Limits.biprod.inr)

Instances For

source

@[simp]

theorem CategoryTheory.Functor.inl_biprodComparison' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] :

CategoryStruct.comp Limits.biprod.inl (F.biprodComparison' X Y) = F.map Limits.biprod.inl

source

@[simp]

theorem CategoryTheory.Functor.inl_biprodComparison'_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] {Z : D} (h : F.obj (X ⊞ Y) ⟶ Z) :

CategoryStruct.comp Limits.biprod.inl (CategoryStruct.comp (F.biprodComparison' X Y) h) = CategoryStruct.comp (F.map Limits.biprod.inl) h

source

@[simp]

theorem CategoryTheory.Functor.inr_biprodComparison' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] :

CategoryStruct.comp Limits.biprod.inr (F.biprodComparison' X Y) = F.map Limits.biprod.inr

source

@[simp]

theorem CategoryTheory.Functor.inr_biprodComparison'_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] {Z : D} (h : F.obj (X ⊞ Y) ⟶ Z) :

CategoryStruct.comp Limits.biprod.inr (CategoryStruct.comp (F.biprodComparison' X Y) h) = CategoryStruct.comp (F.map Limits.biprod.inr) h

source

@[simp]

theorem CategoryTheory.Functor.biprodComparison'_comp_biprodComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms] :

CategoryStruct.comp (F.biprodComparison' X Y) (F.biprodComparison X Y) = CategoryStruct.id (F.obj X ⊞ F.obj Y)

The composition in the opposite direction is equal to the identity if and only if F preserves the biproduct, see preservesBinaryBiproduct_of_monoBiprodComparison.

source

@[simp]

theorem CategoryTheory.Functor.biprodComparison'_comp_biprodComparison_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms] {Z : D} (h : F.obj X ⊞ F.obj Y ⟶ Z) :

CategoryStruct.comp (F.biprodComparison' X Y) (CategoryStruct.comp (F.biprodComparison X Y) h) = h

The composition in the opposite direction is equal to the identity if and only if F preserves the biproduct, see preservesBinaryBiproduct_of_monoBiprodComparison.

source

def CategoryTheory.Functor.splitEpiBiprodComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms] :

SplitEpi (F.biprodComparison X Y)

biprodComparison F X Y is a split epi.

Equations

F.splitEpiBiprodComparison X Y = { section_ := F.biprodComparison' X Y, id := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.Functor.splitEpiBiprodComparison_section_ {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms] :

(F.splitEpiBiprodComparison X Y).section_ = F.biprodComparison' X Y

source

instance CategoryTheory.Functor.instIsSplitEpiBiprodComparison {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms] :

IsSplitEpi (F.biprodComparison X Y)

source

def CategoryTheory.Functor.splitMonoBiprodComparison' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms] :

SplitMono (F.biprodComparison' X Y)

biprodComparison' F X Y is a split mono.

Equations

F.splitMonoBiprodComparison' X Y = { retraction := F.biprodComparison X Y, id := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.Functor.splitMonoBiprodComparison'_retraction {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms] :

(F.splitMonoBiprodComparison' X Y).retraction = F.biprodComparison X Y

source

instance CategoryTheory.Functor.instIsSplitMonoBiprodComparison' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms] :

IsSplitMono (F.biprodComparison' X Y)

source

instance CategoryTheory.Functor.hasBinaryBiproduct_of_preserves {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [F.PreservesZeroMorphisms] [Limits.PreservesBinaryBiproduct X Y F] :

Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)

source

@[reducible, inline]

abbrev CategoryTheory.Functor.mapBiprod {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [F.PreservesZeroMorphisms] [Limits.PreservesBinaryBiproduct X Y F] :

F.obj (X ⊞ Y) ≅ F.obj X ⊞ F.obj Y

If F preserves a binary biproduct, we get a definitionally nice isomorphism F.obj (X ⊞ Y) ≅ F.obj X ⊞ F.obj Y.

Equations

F.mapBiprod X Y = CategoryTheory.Limits.biprod.uniqueUpToIso (F.obj X) (F.obj Y) (CategoryTheory.Limits.isBinaryBilimitOfPreserves F (CategoryTheory.Limits.BinaryBiproduct.isBilimit X Y))

Instances For

source

theorem CategoryTheory.Functor.mapBiprod_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [F.PreservesZeroMorphisms] [Limits.PreservesBinaryBiproduct X Y F] :

(F.mapBiprod X Y).hom = Limits.biprod.lift (F.map Limits.biprod.fst) (F.map Limits.biprod.snd)

source

theorem CategoryTheory.Functor.mapBiprod_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (F : Functor C D) (X Y : C) [Limits.HasBinaryBiproduct X Y] [F.PreservesZeroMorphisms] [Limits.PreservesBinaryBiproduct X Y F] :

(F.mapBiprod X Y).inv = Limits.biprod.desc (F.map Limits.biprod.inl) (F.map Limits.biprod.inr)

source

theorem CategoryTheory.Limits.biproduct.map_lift_mapBiprod {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} (f : J → C) [HasBiproduct f] [PreservesBiproduct f F] {W : C} (g : (j : J) → W ⟶ f j) :

CategoryStruct.comp (F.map (lift g)) (F.mapBiproduct f).hom = lift fun (j : J) => F.map (g j)

source

theorem CategoryTheory.Limits.biproduct.mapBiproduct_inv_map_desc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} (f : J → C) [HasBiproduct f] [PreservesBiproduct f F] {W : C} (g : (j : J) → f j ⟶ W) :

CategoryStruct.comp (F.mapBiproduct f).inv (F.map (desc g)) = desc fun (j : J) => F.map (g j)

source

theorem CategoryTheory.Limits.biproduct.mapBiproduct_hom_desc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] {J : Type w₁} (f : J → C) [HasBiproduct f] [PreservesBiproduct f F] {W : C} (g : (j : J) → f j ⟶ W) :

CategoryStruct.comp (F.mapBiproduct f).hom (desc fun (j : J) => F.map (g j)) = F.map (desc g)

source

theorem CategoryTheory.Limits.biprod.map_lift_mapBiprod {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] (X Y : C) [HasBinaryBiproduct X Y] [PreservesBinaryBiproduct X Y F] {W : C} (f : W ⟶ X) (g : W ⟶ Y) :

CategoryStruct.comp (F.map (lift f g)) (F.mapBiprod X Y).hom = lift (F.map f) (F.map g)

source

theorem CategoryTheory.Limits.biprod.lift_mapBiprod {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] (X Y : C) [HasBinaryBiproduct X Y] [PreservesBinaryBiproduct X Y F] {W : C} (f : W ⟶ X) (g : W ⟶ Y) :

CategoryStruct.comp (lift (F.map f) (F.map g)) (F.mapBiprod X Y).inv = F.map (lift f g)

source

theorem CategoryTheory.Limits.biprod.mapBiprod_inv_map_desc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] (X Y : C) [HasBinaryBiproduct X Y] [PreservesBinaryBiproduct X Y F] {W : C} (f : X ⟶ W) (g : Y ⟶ W) :

CategoryStruct.comp (F.mapBiprod X Y).inv (F.map (desc f g)) = desc (F.map f) (F.map g)

source

theorem CategoryTheory.Limits.biprod.mapBiprod_hom_desc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : Functor C D) [F.PreservesZeroMorphisms] (X Y : C) [HasBinaryBiproduct X Y] [PreservesBinaryBiproduct X Y F] {W : C} (f : X ⟶ W) (g : Y ⟶ W) :

CategoryStruct.comp (F.mapBiprod X Y).hom (desc (F.map f) (F.map g)) = F.map (desc f g)

Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

Preservation of biproducts #