Preservation of biproducts #
We define the image of a (binary) bicone under a functor that preserves zero morphisms and define
classes preserves_biproduct and preserves_binary_biproduct. We then
- show that a functor that preserves biproducts of a two-element type preserves binary biproducts,
- give the canonical isomorphism between the image of a biproduct and the biproduct of the images,
- show that in a preadditive category, a functor preserves a biproduct if and only if it preserves the corresponding product if and only if it preserves the corresponding coproduct.
@[simp]
theorem
category_theory.functor.map_bicone_X
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type v}
{f : J → C}
(b : category_theory.limits.bicone f) :
(F.map_bicone b).X = F.obj b.X
@[simp]
theorem
category_theory.functor.map_bicone_π
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type v}
{f : J → C}
(b : category_theory.limits.bicone f)
(j : J) :
(F.map_bicone b).π j = F.map (b.π j)
def
category_theory.functor.map_bicone
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type v}
{f : J → C}
(b : category_theory.limits.bicone f) :
The image of a bicone under a functor.
@[simp]
theorem
category_theory.functor.map_bicone_ι
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type v}
{f : J → C}
(b : category_theory.limits.bicone f)
(j : J) :
(F.map_bicone b).ι j = F.map (b.ι j)
@[simp]
theorem
category_theory.functor.map_binary_bicone_X
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{X Y : C}
(b : category_theory.limits.binary_bicone X Y) :
(F.map_binary_bicone b).X = F.obj b.X
@[simp]
theorem
category_theory.functor.map_binary_bicone_inl
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{X Y : C}
(b : category_theory.limits.binary_bicone X Y) :
(F.map_binary_bicone b).inl = F.map b.inl
@[simp]
theorem
category_theory.functor.map_binary_bicone_snd
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{X Y : C}
(b : category_theory.limits.binary_bicone X Y) :
(F.map_binary_bicone b).snd = F.map b.snd
@[simp]
theorem
category_theory.functor.map_binary_bicone_fst
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{X Y : C}
(b : category_theory.limits.binary_bicone X Y) :
(F.map_binary_bicone b).fst = F.map b.fst
def
category_theory.functor.map_binary_bicone
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{X Y : C}
(b : category_theory.limits.binary_bicone X Y) :
category_theory.limits.binary_bicone (F.obj X) (F.obj Y)
The image of a binary bicone under a functor.
@[simp]
theorem
category_theory.functor.map_binary_bicone_inr
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{X Y : C}
(b : category_theory.limits.binary_bicone X Y) :
(F.map_binary_bicone b).inr = F.map b.inr
@[class]
structure
category_theory.limits.preserves_biproduct
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
{J : Type v}
(f : J → C)
(F : C ⥤ D)
[F.preserves_zero_morphisms] :
Type (max u u₂ v)
- preserves : Π {b : category_theory.limits.bicone f}, b.is_bilimit → (F.map_bicone b).is_bilimit
A functor F preserves biproducts of f if F maps every bilimit bicone over f to a
bilimit bicone over F.obj ∘ f.
Instances of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_biproduct
- category_theory.limits.preserves_biproduct.has_sizeof_inst
def
category_theory.limits.is_bilimit_of_preserves
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
{J : Type v}
{f : J → C}
(F : C ⥤ D)
[F.preserves_zero_morphisms]
[category_theory.limits.preserves_biproduct f F]
{b : category_theory.limits.bicone f}
(hb : b.is_bilimit) :
(F.map_bicone b).is_bilimit
A functor F preserves biproducts of f if F maps every bilimit bicone over f to a
bilimit bicone over F.obj ∘ f.
@[class]
structure
category_theory.limits.preserves_biproducts_of_shape
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(J : Type v)
(F : C ⥤ D)
[F.preserves_zero_morphisms] :
Type (max u u₂ v)
- preserves : Π {f : J → C}, category_theory.limits.preserves_biproduct f F
A functor F preserves biproducts of shape J if it preserves biproducts of f for every
f : J → C.
Instances of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_biproducts_of_shape
- category_theory.limits.preserves_biproducts_of_shape.has_sizeof_inst
@[class]
structure
category_theory.limits.preserves_finite_biproducts
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms] :
Type (max u u₂ (v+1))
- preserves : Π {J : Type ?} [_inst_5_1 : fintype J], category_theory.limits.preserves_biproducts_of_shape J F
A functor F preserves finite biproducts if it preserves biproducts of shape J whenever
J is a fintype.
Instances of this typeclass
- category_theory.limits.preserves_finite_biproducts_of_preserves_biproducts
- category_theory.functor.preserves_finite_biproducts_of_additive
- category_theory.monoidal_category.tensor_left.limits.preserves_finite_biproducts
- category_theory.monoidal_category.tensor_right.limits.preserves_finite_biproducts
Instances of other typeclasses for category_theory.limits.preserves_finite_biproducts
- category_theory.limits.preserves_finite_biproducts.has_sizeof_inst
@[class]
structure
category_theory.limits.preserves_biproducts
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms] :
Type (max u u₂ (v+1))
- preserves : Π {J : Type ?}, category_theory.limits.preserves_biproducts_of_shape J F
A functor F preserves biproducts if it preserves biproducts of any (small) shape J.
Instances for category_theory.limits.preserves_biproducts
- category_theory.limits.preserves_biproducts.has_sizeof_inst
@[protected, instance]
def
category_theory.limits.preserves_finite_biproducts_of_preserves_biproducts
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
[category_theory.limits.preserves_biproducts F] :
Equations
- category_theory.limits.preserves_finite_biproducts_of_preserves_biproducts F = {preserves := λ (J : Type v) (_x : fintype J), infer_instance}
@[class]
structure
category_theory.limits.preserves_binary_biproduct
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(X Y : C)
(F : C ⥤ D)
[F.preserves_zero_morphisms] :
Type (max u u₂ v)
- preserves : Π {b : category_theory.limits.binary_bicone X Y}, b.is_bilimit → (F.map_binary_bicone b).is_bilimit
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 of this typeclass
Instances of other typeclasses for category_theory.limits.preserves_binary_biproduct
- category_theory.limits.preserves_binary_biproduct.has_sizeof_inst
def
category_theory.limits.is_binary_bilimit_of_preserves
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
{X Y : C}
(F : C ⥤ D)
[F.preserves_zero_morphisms]
[category_theory.limits.preserves_binary_biproduct X Y F]
{b : category_theory.limits.binary_bicone X Y}
(hb : b.is_bilimit) :
(F.map_binary_bicone b).is_bilimit
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.
@[class]
structure
category_theory.limits.preserves_binary_biproducts
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms] :
Type (max u u₂ v)
- preserves : (Π {X Y : C}, category_theory.limits.preserves_binary_biproduct X Y F) . "apply_instance"
A functor F preserves binary biproducts if it preserves the binary biproduct of X and Y
for all X and Y.
Instances for category_theory.limits.preserves_binary_biproducts
- category_theory.limits.preserves_binary_biproducts.has_sizeof_inst
def
category_theory.limits.preserves_binary_biproduct_of_preserves_biproduct
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
(X Y : C)
[category_theory.limits.preserves_biproduct (category_theory.limits.pair_function X Y) F] :
A functor that preserves biproducts of a pair preserves binary biproducts.
Equations
- category_theory.limits.preserves_binary_biproduct_of_preserves_biproduct F X Y = {preserves := λ (b : category_theory.limits.binary_bicone X Y) (hb : b.is_bilimit), {is_limit := (⇑((category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.limits.diagram_iso_pair (category_theory.discrete.functor (F.obj ∘ category_theory.limits.pair_function X Y))) (F.map_bicone b.to_bicone).to_cone).symm) (category_theory.limits.is_bilimit_of_preserves F (⇑(b.to_bicone_is_bilimit.symm) hb)).is_limit).of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose (category_theory.limits.diagram_iso_pair (category_theory.discrete.functor (F.obj ∘ category_theory.limits.pair_function X Y))).hom).obj (F.map_bicone b.to_bicone).to_cone).X) _), is_colimit := (⇑((category_theory.limits.is_colimit.precompose_inv_equiv (category_theory.limits.diagram_iso_pair (category_theory.discrete.functor (F.obj ∘ category_theory.limits.pair_function X Y))) (F.map_bicone b.to_bicone).to_cocone).symm) (category_theory.limits.is_bilimit_of_preserves F (⇑(b.to_bicone_is_bilimit.symm) hb)).is_colimit).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose (category_theory.limits.diagram_iso_pair (category_theory.discrete.functor (F.obj ∘ category_theory.limits.pair_function X Y))).inv).obj (F.map_bicone b.to_bicone).to_cocone).X) _)}}
def
category_theory.limits.preserves_binary_biproducts_of_preserves_biproducts
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
[category_theory.limits.preserves_biproducts_of_shape category_theory.limits.walking_pair F] :
A functor that preserves biproducts of a pair preserves binary biproducts.
@[protected, instance]
def
category_theory.functor.has_biproduct_of_preserves
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
{J : Type v}
(F : C ⥤ D)
[F.preserves_zero_morphisms]
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.preserves_biproduct f F] :
@[simp]
noncomputable
def
category_theory.functor.map_biproduct
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
{J : Type v}
(F : C ⥤ D)
[F.preserves_zero_morphisms]
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.preserves_biproduct f F] :
If F preserves a biproduct, we get a definitionally nice isomorphism
F.obj (⨁ f) ≅ ⨁ (F.obj ∘ f).
theorem
category_theory.functor.map_biproduct_hom
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
{J : Type v}
(F : C ⥤ D)
[F.preserves_zero_morphisms]
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.preserves_biproduct f F] :
(F.map_biproduct f).hom = category_theory.limits.biproduct.lift (λ (j : J), F.map (category_theory.limits.biproduct.π f j))
theorem
category_theory.functor.map_biproduct_inv
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
{J : Type v}
(F : C ⥤ D)
[F.preserves_zero_morphisms]
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.preserves_biproduct f F] :
(F.map_biproduct f).inv = category_theory.limits.biproduct.desc (λ (j : J), F.map (category_theory.limits.biproduct.ι f j))
@[protected, instance]
def
category_theory.functor.has_binary_biproduct_of_preserves
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.preserves_binary_biproduct X Y F] :
category_theory.limits.has_binary_biproduct (F.obj X) (F.obj Y)
@[simp]
noncomputable
def
category_theory.functor.map_biprod
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.preserves_binary_biproduct X Y F] :
If F preserves a binary biproduct, we get a definitionally nice isomorphism
F.obj (X ⊞ Y) ≅ F.obj X ⊞ F.obj Y.
theorem
category_theory.functor.map_biprod_hom
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.preserves_binary_biproduct X Y F] :
theorem
category_theory.functor.map_biprod_inv
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.preserves_binary_biproduct X Y F] :
theorem
category_theory.limits.biproduct.map_lift_map_biprod
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type v}
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.preserves_biproduct f F]
{W : C}
(g : Π (j : J), W ⟶ f j) :
F.map (category_theory.limits.biproduct.lift g) ≫ (F.map_biproduct f).hom = category_theory.limits.biproduct.lift (λ (j : J), F.map (g j))
theorem
category_theory.limits.biproduct.map_biproduct_inv_map_desc
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type v}
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.preserves_biproduct f F]
{W : C}
(g : Π (j : J), f j ⟶ W) :
(F.map_biproduct f).inv ≫ F.map (category_theory.limits.biproduct.desc g) = category_theory.limits.biproduct.desc (λ (j : J), F.map (g j))
theorem
category_theory.limits.biproduct.map_biproduct_hom_desc
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type v}
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.preserves_biproduct f F]
{W : C}
(g : Π (j : J), f j ⟶ W) :
(F.map_biproduct f).hom ≫ category_theory.limits.biproduct.desc (λ (j : J), F.map (g j)) = F.map (category_theory.limits.biproduct.desc g)
theorem
category_theory.limits.biprod.map_lift_map_biprod
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.preserves_binary_biproduct X Y F]
{W : C}
(f : W ⟶ X)
(g : W ⟶ Y) :
F.map (category_theory.limits.biprod.lift f g) ≫ (F.map_biprod X Y).hom = category_theory.limits.biprod.lift (F.map f) (F.map g)
theorem
category_theory.limits.biprod.lift_map_biprod
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.preserves_binary_biproduct X Y F]
{W : C}
(f : W ⟶ X)
(g : W ⟶ Y) :
category_theory.limits.biprod.lift (F.map f) (F.map g) ≫ (F.map_biprod X Y).inv = F.map (category_theory.limits.biprod.lift f g)
theorem
category_theory.limits.biprod.map_biprod_inv_map_desc
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.preserves_binary_biproduct X Y F]
{W : C}
(f : X ⟶ W)
(g : Y ⟶ W) :
(F.map_biprod X Y).inv ≫ F.map (category_theory.limits.biprod.desc f g) = category_theory.limits.biprod.desc (F.map f) (F.map g)
theorem
category_theory.limits.biprod.map_biprod_hom_desc
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.preserves_binary_biproduct X Y F]
{W : C}
(f : X ⟶ W)
(g : Y ⟶ W) :
(F.map_biprod X Y).hom ≫ category_theory.limits.biprod.desc (F.map f) (F.map g) = F.map (category_theory.limits.biprod.desc f g)
noncomputable
def
category_theory.limits.preserves_product_of_preserves_biproduct
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type v}
[fintype J]
{f : J → C}
[category_theory.limits.preserves_biproduct f F] :
A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite products.
Equations
- category_theory.limits.preserves_product_of_preserves_biproduct F = {preserves := λ (c : category_theory.limits.cone (category_theory.discrete.functor f)) (hc : category_theory.limits.is_limit c), (⇑((category_theory.limits.is_limit.postcompose_inv_equiv (category_theory.discrete.comp_nat_iso_discrete f F) (F.map_bicone (category_theory.limits.bicone.of_limit_cone hc)).to_cone).symm) (category_theory.limits.is_bilimit_of_preserves F (category_theory.limits.bicone_is_bilimit_of_limit_cone_of_is_limit hc)).is_limit).of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose (category_theory.discrete.comp_nat_iso_discrete f F).inv).obj (F.map_bicone (category_theory.limits.bicone.of_limit_cone hc)).to_cone).X) _)}
noncomputable
def
category_theory.limits.preserves_products_of_shape_of_preserves_biproducts_of_shape
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type v}
[fintype J]
[category_theory.limits.preserves_biproducts_of_shape J F] :
A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite products.
def
category_theory.limits.preserves_biproduct_of_preserves_product
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type v}
[fintype J]
{f : J → C}
[category_theory.limits.preserves_limit (category_theory.discrete.functor f) F] :
A functor between preadditive categories that preserves (zero morphisms and) finite products preserves finite biproducts.
Equations
- category_theory.limits.preserves_biproduct_of_preserves_product F = {preserves := λ (b : category_theory.limits.bicone f) (hb : b.is_bilimit), category_theory.limits.is_bilimit_of_is_limit (F.map_bicone b) ((⇑((category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.discrete.comp_nat_iso_discrete f F) (F.map_cone b.to_cone)).symm) (category_theory.limits.is_limit_of_preserves F hb.is_limit)).of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose (category_theory.discrete.comp_nat_iso_discrete f F).hom).obj (F.map_cone b.to_cone)).X) _))}
def
category_theory.limits.preserves_biproducts_of_shape_of_preserves_products_of_shape
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type v}
[fintype J]
[category_theory.limits.preserves_limits_of_shape (category_theory.discrete J) F] :
A functor between preadditive categories that preserves (zero morphisms and) finite products preserves finite biproducts.
noncomputable
def
category_theory.limits.preserves_coproduct_of_preserves_biproduct
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type v}
[fintype J]
{f : J → C}
[category_theory.limits.preserves_biproduct f F] :
A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite coproducts.
Equations
- category_theory.limits.preserves_coproduct_of_preserves_biproduct F = {preserves := λ (c : category_theory.limits.cocone (category_theory.discrete.functor f)) (hc : category_theory.limits.is_colimit c), (⇑((category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.discrete.comp_nat_iso_discrete f F) (F.map_bicone (category_theory.limits.bicone.of_colimit_cocone hc)).to_cocone).symm) (category_theory.limits.is_bilimit_of_preserves F (category_theory.limits.bicone_is_bilimit_of_colimit_cocone_of_is_colimit hc)).is_colimit).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose (category_theory.discrete.comp_nat_iso_discrete f F).hom).obj (F.map_bicone (category_theory.limits.bicone.of_colimit_cocone hc)).to_cocone).X) _)}
noncomputable
def
category_theory.limits.preserves_coproducts_of_shape_of_preserves_biproducts_of_shape
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type v}
[fintype J]
[category_theory.limits.preserves_biproducts_of_shape J F] :
A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite coproducts.
def
category_theory.limits.preserves_biproduct_of_preserves_coproduct
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type v}
[fintype J]
{f : J → C}
[category_theory.limits.preserves_colimit (category_theory.discrete.functor f) F] :
A functor between preadditive categories that preserves (zero morphisms and) finite coproducts preserves finite biproducts.
Equations
- category_theory.limits.preserves_biproduct_of_preserves_coproduct F = {preserves := λ (b : category_theory.limits.bicone f) (hb : b.is_bilimit), category_theory.limits.is_bilimit_of_is_colimit (F.map_bicone b) ((⇑((category_theory.limits.is_colimit.precompose_inv_equiv (category_theory.discrete.comp_nat_iso_discrete f F) (F.map_cocone b.to_cocone)).symm) (category_theory.limits.is_colimit_of_preserves F hb.is_colimit)).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose (category_theory.discrete.comp_nat_iso_discrete f F).inv).obj (F.map_cocone b.to_cocone)).X) _))}
def
category_theory.limits.preserves_biproducts_of_shape_of_preserves_coproducts_of_shape
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{J : Type v}
[fintype J]
[category_theory.limits.preserves_colimits_of_shape (category_theory.discrete J) F] :
A functor between preadditive categories that preserves (zero morphisms and) finite coproducts preserves finite biproducts.
def
category_theory.limits.preserves_binary_product_of_preserves_binary_biproduct
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{X Y : C}
[category_theory.limits.preserves_binary_biproduct X Y F] :
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary products.
Equations
- category_theory.limits.preserves_binary_product_of_preserves_binary_biproduct F = {preserves := λ (c : category_theory.limits.cone (category_theory.limits.pair X Y)) (hc : category_theory.limits.is_limit c), (⇑((category_theory.limits.is_limit.postcompose_inv_equiv (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)) (F.map_binary_bicone (category_theory.limits.binary_bicone.of_limit_cone hc)).to_cone).symm) (category_theory.limits.is_binary_bilimit_of_preserves F (category_theory.limits.binary_bicone_is_bilimit_of_limit_cone_of_is_limit hc)).is_limit).of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)).inv).obj (F.map_binary_bicone (category_theory.limits.binary_bicone.of_limit_cone hc)).to_cone).X) _)}
def
category_theory.limits.preserves_binary_products_of_preserves_binary_biproducts
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
[category_theory.limits.preserves_binary_biproducts F] :
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary products.
def
category_theory.limits.preserves_binary_biproduct_of_preserves_binary_product
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{X Y : C}
[category_theory.limits.preserves_limit (category_theory.limits.pair X Y) F] :
A functor between preadditive categories that preserves (zero morphisms and) binary products preserves binary biproducts.
Equations
- category_theory.limits.preserves_binary_biproduct_of_preserves_binary_product F = {preserves := λ (b : category_theory.limits.binary_bicone X Y) (hb : b.is_bilimit), category_theory.limits.is_binary_bilimit_of_is_limit (F.map_binary_bicone b) ((⇑((category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)) (F.map_cone b.to_cone)).symm) (category_theory.limits.is_limit_of_preserves F hb.is_limit)).of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)).hom).obj (F.map_cone b.to_cone)).X) _))}
def
category_theory.limits.preserves_binary_biproducts_of_preserves_binary_products
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
[category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F] :
A functor between preadditive categories that preserves (zero morphisms and) binary products preserves binary biproducts.
def
category_theory.limits.preserves_binary_coproduct_of_preserves_binary_biproduct
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{X Y : C}
[category_theory.limits.preserves_binary_biproduct X Y F] :
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary coproducts.
Equations
- category_theory.limits.preserves_binary_coproduct_of_preserves_binary_biproduct F = {preserves := λ (c : category_theory.limits.cocone (category_theory.limits.pair X Y)) (hc : category_theory.limits.is_colimit c), (⇑((category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)) (F.map_binary_bicone (category_theory.limits.binary_bicone.of_colimit_cocone hc)).to_cocone).symm) (category_theory.limits.is_binary_bilimit_of_preserves F (category_theory.limits.binary_bicone_is_bilimit_of_colimit_cocone_of_is_colimit hc)).is_colimit).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)).hom).obj (F.map_binary_bicone (category_theory.limits.binary_bicone.of_colimit_cocone hc)).to_cocone).X) _)}
def
category_theory.limits.preserves_binary_coproducts_of_preserves_binary_biproducts
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
[category_theory.limits.preserves_binary_biproducts F] :
A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary coproducts.
def
category_theory.limits.preserves_binary_biproduct_of_preserves_binary_coproduct
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
{X Y : C}
[category_theory.limits.preserves_colimit (category_theory.limits.pair X Y) F] :
A functor between preadditive categories that preserves (zero morphisms and) binary coproducts preserves binary biproducts.
Equations
- category_theory.limits.preserves_binary_biproduct_of_preserves_binary_coproduct F = {preserves := λ (b : category_theory.limits.binary_bicone X Y) (hb : b.is_bilimit), category_theory.limits.is_binary_bilimit_of_is_colimit (F.map_binary_bicone b) ((⇑((category_theory.limits.is_colimit.precompose_inv_equiv (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)) (F.map_cocone b.to_cocone)).symm) (category_theory.limits.is_colimit_of_preserves F hb.is_colimit)).of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose (category_theory.limits.diagram_iso_pair (category_theory.limits.pair X Y ⋙ F)).inv).obj (F.map_cocone b.to_cocone)).X) _))}
def
category_theory.limits.preserves_binary_biproducts_of_preserves_binary_coproducts
{C : Type u}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.preserves_zero_morphisms]
[category_theory.limits.preserves_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F] :
A functor between preadditive categories that preserves (zero morphisms and) binary coproducts preserves binary biproducts.