category_theory.preadditive.left_exact

source

def category_theory.functor.is_limit_map_cone_binary_fan_of_preserves_kernels {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {D : Type u₂} [category_theory.category D] [category_theory.preadditive D] (F : C ⥤ D) [F.preserves_zero_morphisms] {X Y Z : C} (π₁ : Z ⟶ X) (π₂ : Z ⟶ Y) [category_theory.limits.preserves_limit (category_theory.limits.parallel_pair π₂ 0) F] (i : category_theory.limits.is_limit (category_theory.limits.binary_fan.mk π₁ π₂)) :

category_theory.limits.is_limit (F.map_cone (category_theory.limits.binary_fan.mk π₁ π₂))

A functor between preadditive categories which preserves kernels preserves that an arbitrary binary fan is a limit.

Equations

F.is_limit_map_cone_binary_fan_of_preserves_kernels π₁ π₂ i = let bc : category_theory.limits.binary_bicone X Y := category_theory.limits.binary_bicone.of_limit_cone i, presf : category_theory.limits.preserves_limit (category_theory.limits.parallel_pair bc.snd 0) F := _.mpr _inst_6, hf : category_theory.limits.is_limit bc.snd_kernel_fork := category_theory.limits.binary_bicone.is_limit_snd_kernel_fork i in (category_theory.limits.is_limit_map_cone_binary_fan_equiv F π₁ π₂).inv_fun ((F.map_binary_bicone bc).is_bilimit_of_kernel_inl (⇑(category_theory.limits.is_limit_map_cone_fork_equiv' F _) (category_theory.limits.is_limit_of_preserves F hf))).is_limit

source

def category_theory.functor.preserves_binary_product_of_preserves_kernels {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {D : Type u₂} [category_theory.category D] [category_theory.preadditive D] (F : C ⥤ D) [F.preserves_zero_morphisms] [Π {X Y : C} (f : X ⟶ Y), category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f 0) F] {X Y : C} :

category_theory.limits.preserves_limit (category_theory.limits.pair X Y) F

A kernel preserving functor between preadditive categories preserves any pair being a limit.

Equations

F.preserves_binary_product_of_preserves_kernels = {preserves := λ (c : category_theory.limits.cone (category_theory.limits.pair X Y)) (hc : category_theory.limits.is_limit c), (F.is_limit_map_cone_binary_fan_of_preserves_kernels (category_theory.limits.binary_fan.fst c) (category_theory.limits.binary_fan.snd c) (hc.of_iso_limit (category_theory.limits.iso_binary_fan_mk c))).of_iso_limit ((category_theory.limits.cones.functoriality (category_theory.limits.pair X Y) F).map_iso (category_theory.limits.iso_binary_fan_mk c).symm)}

source

def category_theory.functor.preserves_binary_products_of_preserves_kernels {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {D : Type u₂} [category_theory.category D] [category_theory.preadditive D] (F : C ⥤ D) [F.preserves_zero_morphisms] [Π {X Y : C} (f : X ⟶ Y), category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f 0) F] :

category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F

A kernel preserving functor between preadditive categories preserves binary products.

Equations

F.preserves_binary_products_of_preserves_kernels = {preserves_limit := λ (p : category_theory.discrete category_theory.limits.walking_pair ⥤ C), category_theory.limits.preserves_limit_of_iso_diagram F (category_theory.limits.diagram_iso_pair p).symm}

source

def category_theory.functor.preserves_equalizer_of_preserves_kernels {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {D : Type u₂} [category_theory.category D] [category_theory.preadditive D] (F : C ⥤ D) [F.preserves_zero_morphisms] [category_theory.limits.has_binary_biproducts C] [Π {X Y : C} (f : X ⟶ Y), category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f 0) F] {X Y : C} (f g : X ⟶ Y) :

category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f g) F

A functor between preadditive categories preserves the equalizer of two morphisms if it preserves all kernels.

Equations

F.preserves_equalizer_of_preserves_kernels f g = let _inst : category_theory.limits.preserves_binary_biproducts F := category_theory.limits.preserves_binary_biproducts_of_preserves_binary_products F in {preserves := λ (c : category_theory.limits.cone (category_theory.limits.parallel_pair f g)) (i : category_theory.limits.is_limit c), let c' : category_theory.limits.is_limit (category_theory.preadditive.kernel_fork_of_fork (category_theory.limits.fork.of_ι (category_theory.limits.fork.ι c) _)) := category_theory.preadditive.is_limit_kernel_fork_of_fork (i.of_iso_limit (category_theory.limits.fork.iso_fork_of_ι c)) in id (let c' : category_theory.limits.is_limit (category_theory.limits.kernel_fork.of_ι (category_theory.limits.fork.ι c) _) := category_theory.preadditive.is_limit_kernel_fork_of_fork (i.of_iso_limit (category_theory.limits.fork.iso_fork_of_ι c)), iFc : category_theory.limits.is_limit (category_theory.limits.kernel_fork.of_ι (F.map (category_theory.limits.fork.ι c)) _) := category_theory.limits.is_limit_fork_map_of_is_limit' F _ c' in ((category_theory.limits.is_limit_map_cone_fork_equiv F _).inv_fun (let p : category_theory.limits.parallel_pair (F.map (f - g)) 0 ≅ category_theory.limits.parallel_pair (F.map f - F.map g) 0 := category_theory.limits.parallel_pair.eq_of_hom_eq _ _ in (category_theory.preadditive.is_limit_fork_of_kernel_fork (⇑((category_theory.limits.is_limit.postcompose_hom_equiv p (category_theory.limits.kernel_fork.of_ι (F.map (category_theory.limits.fork.ι c)) _)).symm) iFc)).of_iso_limit (_.mpr (category_theory.preadditive.fork_of_kernel_fork ((category_theory.limits.cones.postcompose p.hom).obj (category_theory.limits.kernel_fork.of_ι (F.map (category_theory.limits.fork.ι c)) _))).iso_fork_of_ι))).of_iso_limit ((category_theory.limits.cones.functoriality (category_theory.limits.parallel_pair f g) F).map_iso (category_theory.limits.fork.iso_fork_of_ι c).symm))}

source

def category_theory.functor.preserves_equalizers_of_preserves_kernels {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {D : Type u₂} [category_theory.category D] [category_theory.preadditive D] (F : C ⥤ D) [F.preserves_zero_morphisms] [category_theory.limits.has_binary_biproducts C] [Π {X Y : C} (f : X ⟶ Y), category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f 0) F] :

category_theory.limits.preserves_limits_of_shape category_theory.limits.walking_parallel_pair F

A functor between preadditive categories preserves all equalizers if it preserves all kernels.

Equations

source

noncomputable def category_theory.functor.preserves_finite_limits_of_preserves_kernels {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {D : Type u₂} [category_theory.category D] [category_theory.preadditive D] (F : C ⥤ D) [F.preserves_zero_morphisms] [category_theory.limits.has_binary_biproducts C] [category_theory.limits.has_finite_products C] [category_theory.limits.has_equalizers C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_object D] [Π {X Y : C} (f : X ⟶ Y), category_theory.limits.preserves_limit (category_theory.limits.parallel_pair f 0) F] :

category_theory.limits.preserves_finite_limits F

A functor between preadditive categories which preserves kernels preserves all finite limits.

Equations

F.preserves_finite_limits_of_preserves_kernels = let _inst : category_theory.limits.preserves_limits_of_shape category_theory.limits.walking_parallel_pair F := F.preserves_equalizers_of_preserves_kernels, _inst_12 : category_theory.limits.preserves_limit (category_theory.functor.empty C) F := F.preserves_terminal_object_of_preserves_zero_morphisms, _inst_13 : category_theory.limits.preserves_limits_of_shape (category_theory.discrete pempty) F := category_theory.limits.preserves_limits_of_shape_pempty_of_preserves_terminal F, p_prod : Π (J : Type) [_inst_7 : fintype J], category_theory.limits.preserves_limits_of_shape (category_theory.discrete J) F := category_theory.preserves_finite_products_of_preserves_binary_and_terminal F in category_theory.limits.preserves_finite_limits_of_preserves_equalizers_and_finite_products F

source

def category_theory.functor.is_colimit_map_cocone_binary_cofan_of_preserves_cokernels {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {D : Type u₂} [category_theory.category D] [category_theory.preadditive D] (F : C ⥤ D) [F.preserves_zero_morphisms] {X Y Z : C} (ι₁ : X ⟶ Z) (ι₂ : Y ⟶ Z) [category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair ι₂ 0) F] (i : category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk ι₁ ι₂)) :

category_theory.limits.is_colimit (F.map_cocone (category_theory.limits.binary_cofan.mk ι₁ ι₂))

A functor between preadditive categories which preserves cokernels preserves finite coproducts.

Equations

F.is_colimit_map_cocone_binary_cofan_of_preserves_cokernels ι₁ ι₂ i = let bc : category_theory.limits.binary_bicone X Y := category_theory.limits.binary_bicone.of_colimit_cocone i, presf : category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair bc.inr 0) F := _.mpr _inst_6, hf : category_theory.limits.is_colimit bc.inr_cokernel_cofork := category_theory.limits.binary_bicone.is_colimit_inr_cokernel_cofork i in (category_theory.limits.is_colimit_map_cocone_binary_cofan_equiv F ι₁ ι₂).inv_fun ((F.map_binary_bicone bc).is_bilimit_of_cokernel_fst (⇑(category_theory.limits.is_colimit_map_cocone_cofork_equiv' F _) (category_theory.limits.is_colimit_of_preserves F hf))).is_colimit

source

def category_theory.functor.preserves_coproduct_of_preserves_cokernels {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {D : Type u₂} [category_theory.category D] [category_theory.preadditive D] (F : C ⥤ D) [F.preserves_zero_morphisms] [Π {X Y : C} (f : X ⟶ Y), category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f 0) F] {X Y : C} :

category_theory.limits.preserves_colimit (category_theory.limits.pair X Y) F

A cokernel preserving functor between preadditive categories preserves any pair being a colimit.

Equations

F.preserves_coproduct_of_preserves_cokernels = {preserves := λ (c : category_theory.limits.cocone (category_theory.limits.pair X Y)) (hc : category_theory.limits.is_colimit c), (F.is_colimit_map_cocone_binary_cofan_of_preserves_cokernels (category_theory.limits.binary_cofan.inl c) (category_theory.limits.binary_cofan.inr c) (hc.of_iso_colimit (category_theory.limits.iso_binary_cofan_mk c))).of_iso_colimit ((category_theory.limits.cocones.functoriality (category_theory.limits.pair X Y) F).map_iso (category_theory.limits.iso_binary_cofan_mk c).symm)}

source

def category_theory.functor.preserves_binary_coproducts_of_preserves_cokernels {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {D : Type u₂} [category_theory.category D] [category_theory.preadditive D] (F : C ⥤ D) [F.preserves_zero_morphisms] [Π {X Y : C} (f : X ⟶ Y), category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f 0) F] :

category_theory.limits.preserves_colimits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F

A cokernel preserving functor between preadditive categories preserves binary coproducts.

Equations

F.preserves_binary_coproducts_of_preserves_cokernels = {preserves_colimit := λ (p : category_theory.discrete category_theory.limits.walking_pair ⥤ C), category_theory.limits.preserves_colimit_of_iso_diagram F (category_theory.limits.diagram_iso_pair p).symm}

source

def category_theory.functor.preserves_coequalizer_of_preserves_cokernels {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {D : Type u₂} [category_theory.category D] [category_theory.preadditive D] (F : C ⥤ D) [F.preserves_zero_morphisms] [category_theory.limits.has_binary_biproducts C] [Π {X Y : C} (f : X ⟶ Y), category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f 0) F] {X Y : C} (f g : X ⟶ Y) :

category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f g) F

A functor between preadditive categoris preserves the coequalizer of two morphisms if it preserves all cokernels.

Equations

F.preserves_coequalizer_of_preserves_cokernels f g = let _inst : category_theory.limits.preserves_binary_biproducts F := category_theory.limits.preserves_binary_biproducts_of_preserves_binary_coproducts F in {preserves := λ (c : category_theory.limits.cocone (category_theory.limits.parallel_pair f g)) (i : category_theory.limits.is_colimit c), let c' : category_theory.limits.is_colimit (category_theory.preadditive.cokernel_cofork_of_cofork (category_theory.limits.cofork.of_π (category_theory.limits.cofork.π c) _)) := category_theory.preadditive.is_colimit_cokernel_cofork_of_cofork (i.of_iso_colimit (category_theory.limits.cofork.iso_cofork_of_π c)) in id (let c' : category_theory.limits.is_colimit (category_theory.limits.cokernel_cofork.of_π (category_theory.limits.cofork.π c) _) := category_theory.preadditive.is_colimit_cokernel_cofork_of_cofork (i.of_iso_colimit (category_theory.limits.cofork.iso_cofork_of_π c)), iFc : category_theory.limits.is_colimit (category_theory.limits.cokernel_cofork.of_π (F.map (category_theory.limits.cofork.π c)) _) := category_theory.limits.is_colimit_cofork_map_of_is_colimit' F _ c' in ((category_theory.limits.is_colimit_map_cocone_cofork_equiv F _).inv_fun (let p : category_theory.limits.parallel_pair (F.map (f - g)) 0 ≅ category_theory.limits.parallel_pair (F.map f - F.map g) 0 := category_theory.limits.parallel_pair.ext (category_theory.iso.refl ((category_theory.limits.parallel_pair (F.map (f - g)) 0).obj category_theory.limits.walking_parallel_pair.zero)) (category_theory.iso.refl ((category_theory.limits.parallel_pair (F.map (f - g)) 0).obj category_theory.limits.walking_parallel_pair.one)) _ _ in (category_theory.preadditive.is_colimit_cofork_of_cokernel_cofork (⇑((category_theory.limits.is_colimit.precompose_hom_equiv p.symm (category_theory.limits.cokernel_cofork.of_π (F.map (category_theory.limits.cofork.π c)) _)).symm) iFc)).of_iso_colimit (_.mpr (category_theory.preadditive.cofork_of_cokernel_cofork ((category_theory.limits.cocones.precompose p.symm.hom).obj (category_theory.limits.cokernel_cofork.of_π (F.map (category_theory.limits.cofork.π c)) _))).iso_cofork_of_π))).of_iso_colimit ((category_theory.limits.cocones.functoriality (category_theory.limits.parallel_pair f g) F).map_iso (category_theory.limits.cofork.iso_cofork_of_π c).symm))}

source

def category_theory.functor.preserves_coequalizers_of_preserves_cokernels {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {D : Type u₂} [category_theory.category D] [category_theory.preadditive D] (F : C ⥤ D) [F.preserves_zero_morphisms] [category_theory.limits.has_binary_biproducts C] [Π {X Y : C} (f : X ⟶ Y), category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f 0) F] :

category_theory.limits.preserves_colimits_of_shape category_theory.limits.walking_parallel_pair F

A functor between preadditive categories preserves all coequalizers if it preserves all kernels.

Equations

source

noncomputable def category_theory.functor.preserves_finite_colimits_of_preserves_cokernels {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {D : Type u₂} [category_theory.category D] [category_theory.preadditive D] (F : C ⥤ D) [F.preserves_zero_morphisms] [category_theory.limits.has_binary_biproducts C] [category_theory.limits.has_finite_coproducts C] [category_theory.limits.has_coequalizers C] [category_theory.limits.has_zero_object C] [category_theory.limits.has_zero_object D] [Π {X Y : C} (f : X ⟶ Y), category_theory.limits.preserves_colimit (category_theory.limits.parallel_pair f 0) F] :

category_theory.limits.preserves_finite_colimits F

A functor between preadditive categories which preserves kernels preserves all finite limits.

Equations

F.preserves_finite_colimits_of_preserves_cokernels = let _inst : category_theory.limits.preserves_colimits_of_shape category_theory.limits.walking_parallel_pair F := F.preserves_coequalizers_of_preserves_cokernels, _inst_12 : category_theory.limits.preserves_colimit (category_theory.functor.empty C) F := F.preserves_initial_object_of_preserves_zero_morphisms, _inst_13 : category_theory.limits.preserves_colimits_of_shape (category_theory.discrete pempty) F := category_theory.limits.preserves_colimits_of_shape_pempty_of_preserves_initial F, p_prod : Π (J : Type) [_inst_7 : fintype J], category_theory.limits.preserves_colimits_of_shape (category_theory.discrete J) F := category_theory.preserves_finite_coproducts_of_preserves_binary_and_initial F in category_theory.limits.preserves_finite_colimits_of_preserves_coequalizers_and_finite_coproducts F

mathlib3 documentation

Left exactness of functors between preadditive categories #

Main results #