Preservation of biproducts #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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,
- 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.
@[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 w₁}
{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 w₁}
{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 w₁}
{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 w₁}
{f : J → C}
(b : category_theory.limits.bicone f)
(j : J) :
(F.map_bicone b).ι j = F.map (b.ι j)
theorem
category_theory.functor.map_bicone_whisker
{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 w₁}
{K : Type w₂}
{g : K ≃ J}
{f : J → C}
(c : category_theory.limits.bicone f) :
F.map_bicone (c.whisker g) = (F.map_bicone c).whisker g
@[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 w₁}
(f : J → C)
(F : C ⥤ D)
[F.preserves_zero_morphisms] :
Type (max u₁ u₂ v₁ v₂ w₁)
- 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 w₁}
{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 w₁)
(F : C ⥤ D)
[F.preserves_zero_morphisms] :
Type (max u₁ u₂ v₁ v₂ w₁)
- 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 1 u₁ u₂ v₁ v₂)
- 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₁ v₂ (w₁+1))
- preserves : Π {J : Type ?}, category_theory.limits.preserves_biproducts_of_shape 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 for category_theory.limits.preserves_biproducts
- category_theory.limits.preserves_biproducts.has_sizeof_inst
def
category_theory.limits.preserves_biproducts_shrink
{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]
[hp : category_theory.limits.preserves_biproducts F] :
Preserving biproducts at a bigger universe level implies preserving biproducts at a smaller universe level.
Equations
- category_theory.limits.preserves_biproducts_shrink F = {preserves := λ (J : Type w₁), {preserves := λ (f : J → C), {preserves := λ (b : category_theory.limits.bicone f) (ib : b.is_bilimit), ((F.map_bicone b).whisker_is_bilimit_iff equiv.ulift).to_fun (category_theory.limits.is_bilimit_of_preserves F ((b.whisker_is_bilimit_iff equiv.ulift).inv_fun ib))}}}
@[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
@[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₁ 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₁ 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.
noncomputable
def
category_theory.functor.biproduct_comparison
{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 w₁}
(F : C ⥤ D)
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (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.biproduct_comparison f = category_theory.limits.biproduct.lift (λ (j : J), F.map (category_theory.limits.biproduct.π f j))
Instances for category_theory.functor.biproduct_comparison
@[simp]
theorem
category_theory.functor.biproduct_comparison_π
{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 w₁}
(F : C ⥤ D)
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (F.obj ∘ f)]
(j : J) :
F.biproduct_comparison f ≫ category_theory.limits.biproduct.π (F.obj ∘ f) j = F.map (category_theory.limits.biproduct.π f j)
@[simp]
theorem
category_theory.functor.biproduct_comparison_π_assoc
{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 w₁}
(F : C ⥤ D)
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (F.obj ∘ f)]
(j : J)
{X' : D}
(f' : (F.obj ∘ f) j ⟶ X') :
F.biproduct_comparison f ≫ category_theory.limits.biproduct.π (F.obj ∘ f) j ≫ f' = F.map (category_theory.limits.biproduct.π f j) ≫ f'
noncomputable
def
category_theory.functor.biproduct_comparison'
{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 w₁}
(F : C ⥤ D)
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (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.biproduct_comparison' f = category_theory.limits.biproduct.desc (λ (j : J), F.map (category_theory.limits.biproduct.ι f j))
Instances for category_theory.functor.biproduct_comparison'
@[simp]
theorem
category_theory.functor.ι_biproduct_comparison'
{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 w₁}
(F : C ⥤ D)
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (F.obj ∘ f)]
(j : J) :
category_theory.limits.biproduct.ι (F.obj ∘ f) j ≫ F.biproduct_comparison' f = F.map (category_theory.limits.biproduct.ι f j)
@[simp]
theorem
category_theory.functor.ι_biproduct_comparison'_assoc
{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 w₁}
(F : C ⥤ D)
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (F.obj ∘ f)]
(j : J)
{X' : D}
(f' : F.obj (⨁ f) ⟶ X') :
category_theory.limits.biproduct.ι (F.obj ∘ f) j ≫ F.biproduct_comparison' f ≫ f' = F.map (category_theory.limits.biproduct.ι f j) ≫ f'
@[simp]
theorem
category_theory.functor.biproduct_comparison'_comp_biproduct_comparison_assoc
{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 w₁}
(F : C ⥤ D)
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (F.obj ∘ f)]
[F.preserves_zero_morphisms]
{X' : D}
(f' : ⨁ F.obj ∘ f ⟶ X') :
F.biproduct_comparison' f ≫ F.biproduct_comparison f ≫ f' = f'
@[simp]
theorem
category_theory.functor.biproduct_comparison'_comp_biproduct_comparison
{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 w₁}
(F : C ⥤ D)
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (F.obj ∘ f)]
[F.preserves_zero_morphisms] :
F.biproduct_comparison' f ≫ F.biproduct_comparison f = 𝟙 (⨁ F.obj ∘ f)
The composition in the opposite direction is equal to the identity if and only if F preserves
the biproduct, see preserves_biproduct_of_mono_biproduct_comparison.
noncomputable
def
category_theory.functor.split_epi_biproduct_comparison
{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 w₁}
(F : C ⥤ D)
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (F.obj ∘ f)]
[F.preserves_zero_morphisms] :
biproduct_comparison F f is a split epimorphism.
Equations
- F.split_epi_biproduct_comparison f = {section_ := F.biproduct_comparison' f _inst_6, id' := _}
@[simp]
theorem
category_theory.functor.split_epi_biproduct_comparison_section_
{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 w₁}
(F : C ⥤ D)
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (F.obj ∘ f)]
[F.preserves_zero_morphisms] :
@[protected, instance]
def
category_theory.functor.biproduct_comparison.category_theory.is_split_epi
{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 w₁}
(F : C ⥤ D)
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (F.obj ∘ f)]
[F.preserves_zero_morphisms] :
noncomputable
def
category_theory.functor.split_mono_biproduct_comparison'
{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 w₁}
(F : C ⥤ D)
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (F.obj ∘ f)]
[F.preserves_zero_morphisms] :
biproduct_comparison' F f is a split monomorphism.
Equations
- F.split_mono_biproduct_comparison' f = {retraction := F.biproduct_comparison f _inst_6, id' := _}
@[simp]
theorem
category_theory.functor.split_mono_biproduct_comparison'_retraction
{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 w₁}
(F : C ⥤ D)
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (F.obj ∘ f)]
[F.preserves_zero_morphisms] :
@[protected, instance]
def
category_theory.functor.biproduct_comparison'.category_theory.is_split_mono
{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 w₁}
(F : C ⥤ D)
(f : J → C)
[category_theory.limits.has_biproduct f]
[category_theory.limits.has_biproduct (F.obj ∘ f)]
[F.preserves_zero_morphisms] :
@[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 w₁}
(F : C ⥤ D)
(f : J → C)
[category_theory.limits.has_biproduct f]
[F.preserves_zero_morphisms]
[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 w₁}
(F : C ⥤ D)
(f : J → C)
[category_theory.limits.has_biproduct f]
[F.preserves_zero_morphisms]
[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 w₁}
(F : C ⥤ D)
(f : J → C)
[category_theory.limits.has_biproduct f]
[F.preserves_zero_morphisms]
[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 w₁}
(F : C ⥤ D)
(f : J → C)
[category_theory.limits.has_biproduct f]
[F.preserves_zero_morphisms]
[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))
noncomputable
def
category_theory.functor.biprod_comparison
{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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (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
Instances for category_theory.functor.biprod_comparison
@[simp]
theorem
category_theory.functor.biprod_comparison_fst_assoc
{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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (F.obj X) (F.obj Y)]
{X' : D}
(f' : F.obj X ⟶ X') :
@[simp]
theorem
category_theory.functor.biprod_comparison_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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (F.obj X) (F.obj Y)] :
@[simp]
theorem
category_theory.functor.biprod_comparison_snd_assoc
{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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (F.obj X) (F.obj Y)]
{X' : D}
(f' : F.obj Y ⟶ X') :
@[simp]
theorem
category_theory.functor.biprod_comparison_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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (F.obj X) (F.obj Y)] :
noncomputable
def
category_theory.functor.biprod_comparison'
{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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (F.obj X) (F.obj 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
Instances for category_theory.functor.biprod_comparison'
@[simp]
theorem
category_theory.functor.inl_biprod_comparison'_assoc
{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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (F.obj X) (F.obj Y)]
{X' : D}
(f' : F.obj (X ⊞ Y) ⟶ X') :
@[simp]
theorem
category_theory.functor.inl_biprod_comparison'
{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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (F.obj X) (F.obj Y)] :
@[simp]
theorem
category_theory.functor.inr_biprod_comparison'
{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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (F.obj X) (F.obj Y)] :
@[simp]
theorem
category_theory.functor.inr_biprod_comparison'_assoc
{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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (F.obj X) (F.obj Y)]
{X' : D}
(f' : F.obj (X ⊞ Y) ⟶ X') :
@[simp]
theorem
category_theory.functor.biprod_comparison'_comp_biprod_comparison
{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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (F.obj X) (F.obj Y)]
[F.preserves_zero_morphisms] :
F.biprod_comparison' X Y ≫ F.biprod_comparison X Y = 𝟙 (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 preserves_binary_biproduct_of_mono_biprod_comparison.
@[simp]
theorem
category_theory.functor.biprod_comparison'_comp_biprod_comparison_assoc
{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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (F.obj X) (F.obj Y)]
[F.preserves_zero_morphisms]
{X' : D}
(f' : F.obj X ⊞ F.obj Y ⟶ X') :
F.biprod_comparison' X Y ≫ F.biprod_comparison X Y ≫ f' = f'
@[simp]
theorem
category_theory.functor.split_epi_biprod_comparison_section_
{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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (F.obj X) (F.obj Y)]
[F.preserves_zero_morphisms] :
(F.split_epi_biprod_comparison X Y).section_ = F.biprod_comparison' X Y
noncomputable
def
category_theory.functor.split_epi_biprod_comparison
{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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (F.obj X) (F.obj Y)]
[F.preserves_zero_morphisms] :
biprod_comparison F X Y is a split epi.
Equations
- F.split_epi_biprod_comparison X Y = {section_ := F.biprod_comparison' X Y _inst_6, id' := _}
@[protected, instance]
def
category_theory.functor.biprod_comparison.category_theory.is_split_epi
{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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (F.obj X) (F.obj Y)]
[F.preserves_zero_morphisms] :
@[simp]
theorem
category_theory.functor.split_mono_biprod_comparison'_retraction
{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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (F.obj X) (F.obj Y)]
[F.preserves_zero_morphisms] :
(F.split_mono_biprod_comparison' X Y).retraction = F.biprod_comparison X Y
noncomputable
def
category_theory.functor.split_mono_biprod_comparison'
{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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (F.obj X) (F.obj Y)]
[F.preserves_zero_morphisms] :
biprod_comparison' F X Y is a split mono.
Equations
- F.split_mono_biprod_comparison' X Y = {retraction := F.biprod_comparison X Y _inst_6, id' := _}
@[protected, instance]
def
category_theory.functor.biprod_comparison'.category_theory.is_split_mono
{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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[category_theory.limits.has_binary_biproduct (F.obj X) (F.obj Y)]
[F.preserves_zero_morphisms] :
@[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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[F.preserves_zero_morphisms]
[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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[F.preserves_zero_morphisms]
[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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[F.preserves_zero_morphisms]
[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)
(X Y : C)
[category_theory.limits.has_binary_biproduct X Y]
[F.preserves_zero_morphisms]
[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 w₁}
(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 w₁}
(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 w₁}
(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)