Transferring "abelian-ness" across a functor #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

If C is an additive category, D is an abelian category, we have F : C ⥤ D G : D ⥤ C (both preserving zero morphisms), G is left exact (that is, preserves finite limits), and further we have adj : G ⊣ F and i : F ⋙ G ≅ 𝟭 C, then C is also abelian.

See https://stacks.math.columbia.edu/tag/03A3

Notes #

The hypotheses, following the statement from the Stacks project, may appear suprising: we don't ask that the counit of the adjunction is an isomorphism, but just that we have some potentially unrelated isomorphism i : F ⋙ G ≅ 𝟭 C.

However Lemma A1.1.1 from [Joh02] shows that in this situation the counit itself must be an isomorphism, and thus that C is a reflective subcategory of D.

Someone may like to formalize that lemma, and restate this theorem in terms of reflective. (That lemma has a nice string diagrammatic proof that holds in any bicategory.)

source

theorem category_theory.abelian_of_adjunction.has_kernels {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {D : Type u₂} [category_theory.category D] [category_theory.abelian D] (F : C ⥤ D) (G : D ⥤ C) [G.preserves_zero_morphisms] (i : F ⋙ G ≅ 𝟭 C) [category_theory.limits.preserves_finite_limits G] :

category_theory.limits.has_kernels C

No point making this an instance, as it requires i.

source

theorem category_theory.abelian_of_adjunction.has_cokernels {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {D : Type u₂} [category_theory.category D] [category_theory.abelian D] (F : C ⥤ D) (G : D ⥤ C) [G.preserves_zero_morphisms] (i : F ⋙ G ≅ 𝟭 C) (adj : G ⊣ F) :

category_theory.limits.has_cokernels C

No point making this an instance, as it requires i and adj.

source

noncomputable def category_theory.abelian_of_adjunction.cokernel_iso {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {D : Type u₂} [category_theory.category D] [category_theory.abelian D] (F : C ⥤ D) (G : D ⥤ C) [G.preserves_zero_morphisms] (i : F ⋙ G ≅ 𝟭 C) (adj : G ⊣ F) [category_theory.limits.has_cokernels C] {X Y : C} (f : X ⟶ Y) :

G.obj (category_theory.limits.cokernel (F.map f)) ≅ category_theory.limits.cokernel f

Auxiliary construction for coimage_iso_image

Equations

category_theory.abelian_of_adjunction.cokernel_iso F G i adj f = (((category_theory.as_iso (category_theory.limits.cokernel_comparison (F.map f) G)).symm ≪≫ category_theory.limits.cokernel_iso_of_eq _) ≪≫ category_theory.limits.cokernel_epi_comp (i.hom.app X) (f ≫ i.inv.app Y) _) ≪≫ category_theory.limits.cokernel_comp_is_iso f (i.inv.app Y) _

source

noncomputable def category_theory.abelian_of_adjunction.coimage_iso_image_aux {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {D : Type u₂} [category_theory.category D] [category_theory.abelian D] (F : C ⥤ D) (G : D ⥤ C) [G.preserves_zero_morphisms] (i : F ⋙ G ≅ 𝟭 C) (adj : G ⊣ F) [category_theory.limits.has_cokernels C] [category_theory.limits.has_kernels C] [category_theory.limits.preserves_finite_limits G] {X Y : C} (f : X ⟶ Y) :

category_theory.limits.kernel (G.map (category_theory.limits.cokernel.π (F.map f))) ≅ category_theory.limits.kernel (category_theory.limits.cokernel.π f)

Auxiliary construction for coimage_iso_image

Equations

category_theory.abelian_of_adjunction.coimage_iso_image_aux F G i adj f = (((((((category_theory.limits.kernel_iso_of_eq _ ≪≫ category_theory.limits.kernel_comp_mono (category_theory.limits.cokernel.π (G.map (F.map f))) (category_theory.limits.cokernel_comparison (F.map f) G) _) ≪≫ category_theory.limits.kernel_iso_of_eq _) ≪≫ category_theory.limits.kernel_comp_mono (category_theory.limits.cokernel.π (i.hom.app X ≫ f ≫ i.inv.app Y)) (category_theory.limits.cokernel_iso_of_eq _).hom _) ≪≫ category_theory.limits.kernel_iso_of_eq _) ≪≫ category_theory.limits.kernel_comp_mono (category_theory.limits.cokernel.π (f ≫ i.inv.app Y)) (category_theory.limits.cokernel_epi_comp (i.hom.app X) (f ≫ i.inv.app Y)).inv _) ≪≫ category_theory.limits.kernel_iso_of_eq _) ≪≫ category_theory.limits.kernel_is_iso_comp (category_theory.inv (i.inv.app Y)) (category_theory.limits.cokernel.π f ≫ (category_theory.limits.cokernel_comp_is_iso f (i.inv.app Y)).inv) _) ≪≫ category_theory.limits.kernel_comp_mono (category_theory.limits.cokernel.π f) (category_theory.limits.cokernel_comp_is_iso f (i.inv.app Y)).inv _

source

noncomputable def category_theory.abelian_of_adjunction.coimage_iso_image {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {D : Type u₂} [category_theory.category D] [category_theory.abelian D] (F : C ⥤ D) (G : D ⥤ C) [G.preserves_zero_morphisms] (i : F ⋙ G ≅ 𝟭 C) (adj : G ⊣ F) [category_theory.limits.has_cokernels C] [category_theory.limits.has_kernels C] [category_theory.limits.preserves_finite_limits G] [F.preserves_zero_morphisms] {X Y : C} (f : X ⟶ Y) :

category_theory.abelian.coimage f ≅ category_theory.abelian.image f

Auxiliary definition: the abelian coimage and abelian image agree. We still need to check that this agrees with the canonical morphism.

Equations

category_theory.abelian_of_adjunction.coimage_iso_image F G i adj f = ((((((((category_theory.iso.refl (category_theory.abelian.coimage f) ≪≫ (category_theory.abelian_of_adjunction.cokernel_iso F G i adj (category_theory.limits.kernel.ι f)).symm) ≪≫ G.map_iso (category_theory.limits.cokernel_iso_of_eq _)) ≪≫ G.map_iso (category_theory.limits.cokernel_epi_comp (category_theory.limits.kernel_comparison f F) (category_theory.limits.kernel.ι (F.map f)))) ≪≫ category_theory.iso.refl (G.obj (category_theory.limits.cokernel (category_theory.limits.kernel.ι (F.map f))))) ≪≫ G.map_iso (category_theory.abelian.coimage_iso_image (F.map f))) ≪≫ category_theory.iso.refl (G.obj (category_theory.abelian.image (F.map f)))) ≪≫ category_theory.limits.preserves_kernel.iso G (category_theory.limits.cokernel.π (F.map f)) category_theory.limits.preserves_limits_of_shape.preserves_limit) ≪≫ category_theory.abelian_of_adjunction.coimage_iso_image_aux F G i adj f) ≪≫ category_theory.iso.refl (category_theory.limits.kernel (category_theory.limits.cokernel.π f))

source

theorem category_theory.abelian_of_adjunction.coimage_iso_image_hom {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {D : Type u₂} [category_theory.category D] [category_theory.abelian D] (F : C ⥤ D) (G : D ⥤ C) [G.preserves_zero_morphisms] (i : F ⋙ G ≅ 𝟭 C) (adj : G ⊣ F) [category_theory.limits.has_cokernels C] [category_theory.limits.has_kernels C] [category_theory.limits.preserves_finite_limits G] [F.preserves_zero_morphisms] {X Y : C} (f : X ⟶ Y) :

(category_theory.abelian_of_adjunction.coimage_iso_image F G i adj f).hom = category_theory.abelian.coimage_image_comparison f

source

noncomputable def category_theory.abelian_of_adjunction {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_finite_products C] {D : Type u₂} [category_theory.category D] [category_theory.abelian D] (F : C ⥤ D) [F.preserves_zero_morphisms] (G : D ⥤ C) [G.preserves_zero_morphisms] [category_theory.limits.preserves_finite_limits G] (i : F ⋙ G ≅ 𝟭 C) (adj : G ⊣ F) :

category_theory.abelian C

See https://stacks.math.columbia.edu/tag/03A3

Equations

category_theory.abelian_of_adjunction F G i adj = category_theory.abelian.of_coimage_image_comparison_is_iso

source

noncomputable def category_theory.abelian_of_equivalence {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] [category_theory.limits.has_finite_products C] {D : Type u₂} [category_theory.category D] [category_theory.abelian D] (F : C ⥤ D) [F.preserves_zero_morphisms] [category_theory.is_equivalence F] :

category_theory.abelian C

If C is an additive category equivalent to an abelian category D via a functor that preserves zero morphisms, then C is also abelian.

Equations

category_theory.abelian_of_equivalence F = category_theory.abelian_of_adjunction F F.inv F.as_equivalence.unit_iso.symm F.as_equivalence.symm.to_adjunction