feat(category_theory/abelian): constructor in terms of coimage-image …

…comparison (#12972)

The "stacks constructor" for an abelian category, following https://stacks.math.columbia.edu/tag/0109.

I also factored out the canonical morphism from the abelian coimage to the abelian image (which exists whether or not the category is abelian), and reformulated `abelian.coimage_iso_image` in terms of an `is_iso` instance for this morphism.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/abelian/basic.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
+Authors: Markus Himmel, Johan Commelin, Scott Morrison
 -/
 
 import category_theory.limits.constructions.pullbacks
@@ -25,8 +25,8 @@ actually a consequence of the other properties, as we show in
 `non_preadditive_abelian.lean`. However, this fact is of little practical
 relevance, since essentially all interesting abelian categories come with a
 preadditive structure. In this way, by requiring preadditivity, we allow the
-user to pass in the preadditive structure the specific category they are
-working with has natively.
+user to pass in the "native" preadditive structure for the specific category they are
+working with.
 
 ## Main definitions
 
@@ -40,11 +40,13 @@ working with has natively.
 * If `f : X ⟶ Y`, then the map `factor_thru_image f : X ⟶ image f` is an epimorphism, and the map
   `factor_thru_coimage f : coimage f ⟶ Y` is a monomorphism.
 * Factoring through the image and coimage is a strong epi-mono factorisation. This means that
-  * every abelian category has images. We instantiated this in such a way that `abelian.image f` is
-    definitionally equal to `limits.image f`, and
-  * there is a canonical isomorphism `coimage_iso_image : coimage f ≅ image f` such that
-    `coimage.π f ≫ (coimage_iso_image f).hom ≫ image.ι f = f`. The lemma stating this is called
-    `full_image_factorisation`.
+  * every abelian category has images. We provide the isomorphism
+    `image_iso_image : abelian.image f ≅ limits.image f`.
+  * the canonical morphism `coimage_image_comparison : coimage f ⟶ image f`
+    is an isomorphism.
+* We provide the alternate characterisation of an abelian category as a category with
+  (co)kernels and finite products, and in which the canonical coimage-image comparison morphism
+  is always an isomorphism.
 * Every epimorphism is a cokernel of its kernel. Every monomorphism is a kernel of its cokernel.
 * The pullback of an epimorphism is an epimorphism. The pushout of a monomorphism is a monomorphism.
   (This is not to be confused with the fact that the pullback of a monomorphism is a monomorphism,
@@ -113,6 +115,141 @@ end category_theory
 
 open category_theory
 
+/-!
+We begin by providing an alternative constructor:
+a preadditive category with kernels, cokernels, and finite products,
+in which the coimage-image comparison morphism is always an isomorphism,
+is an abelian category.
+-/
+namespace category_theory.abelian
+
+variables {C : Type u} [category.{v} C] [preadditive C]
+variables [limits.has_kernels C] [limits.has_cokernels C]
+
+namespace of_coimage_image_comparison_is_iso
+
+/-- The factorisation of a morphism through its abelian image. -/
+@[simps]
+def image_mono_factorisation {X Y : C} (f : X ⟶ Y) : mono_factorisation f :=
+{ I := abelian.image f,
+  m := kernel.ι _,
+  m_mono := infer_instance,
+  e := kernel.lift _ f (cokernel.condition _),
+  fac' := kernel.lift_ι _ _ _ }
+
+lemma image_mono_factorisation_e' {X Y : C} (f : X ⟶ Y) :
+  (image_mono_factorisation f).e = cokernel.π _ ≫ abelian.coimage_image_comparison f :=
+begin
+  ext,
+  simp only [abelian.coimage_image_comparison, image_mono_factorisation_e,
+    category.assoc, cokernel.π_desc_assoc],
+end
+
+/-- If the coimage-image comparison morphism for a morphism `f` is an isomorphism,
+we obtain an image factorisation of `f`. -/
+def image_factorisation {X Y : C} (f : X ⟶ Y) [is_iso (abelian.coimage_image_comparison f)] :
+  image_factorisation f :=
+{ F := image_mono_factorisation f,
+  is_image :=
+  { lift := λ F, inv (abelian.coimage_image_comparison f) ≫ cokernel.desc _ F.e F.kernel_ι_comp,
+    lift_fac' := λ F, begin
+      simp only [image_mono_factorisation_m, is_iso.inv_comp_eq, category.assoc,
+        abelian.coimage_image_comparison],
+      ext,
+      rw [limits.coequalizer.π_desc_assoc, limits.coequalizer.π_desc_assoc, F.fac, kernel.lift_ι]
+    end } }
+
+instance [has_zero_object C] {X Y : C} (f : X ⟶ Y) [mono f]
+  [is_iso (abelian.coimage_image_comparison f)] :
+  is_iso (image_mono_factorisation f).e :=
+by { rw image_mono_factorisation_e', exact is_iso.comp_is_iso }
+
+instance [has_zero_object C] {X Y : C} (f : X ⟶ Y) [epi f] :
+  is_iso (image_mono_factorisation f).m :=
+by { dsimp, apply_instance }
+
+variables [∀ {X Y : C} (f : X ⟶ Y), is_iso (abelian.coimage_image_comparison f)]
+
+/-- A category in which coimage-image comparisons are all isomorphisms has images. -/
+lemma has_images : has_images C :=
+{ has_image := λ X Y f,
+  { exists_image := ⟨image_factorisation f⟩ } }
+
+variables [limits.has_finite_products C]
+local attribute [instance] limits.has_finite_biproducts.of_has_finite_products
+
+/--
+A category with finite products in which coimage-image comparisons are all isomorphisms
+is a normal mono category.
+-/
+def normal_mono_category : normal_mono_category C :=
+{ normal_mono_of_mono := λ X Y f m,
+  { Z := _,
+    g := cokernel.π f,
+    w := by simp,
+    is_limit := begin
+      haveI : limits.has_images C := has_images,
+      haveI : has_equalizers C := preadditive.has_equalizers_of_has_kernels,
+      letI : has_zero_object C := has_zero_object_of_has_finite_biproducts _,
+      have aux : _ := _,
+      refine is_limit_aux _ (λ A, limit.lift _ _ ≫ inv (image_mono_factorisation f).e) aux _,
+      { intros A g hg,
+        rw [kernel_fork.ι_of_ι] at hg,
+        rw [← cancel_mono f, hg, ← aux, kernel_fork.ι_of_ι], },
+      { intro A,
+        simp only [kernel_fork.ι_of_ι, category.assoc],
+        convert limit.lift_π _ _ using 2,
+        rw [is_iso.inv_comp_eq, eq_comm],
+        exact (image_mono_factorisation f).fac, },
+    end }, }
+
+/--
+A category with finite products in which coimage-image comparisons are all isomorphisms
+is a normal epi category.
+-/
+def normal_epi_category : normal_epi_category C :=
+{ normal_epi_of_epi := λ X Y f m,
+  { W := kernel f,
+    g := kernel.ι _,
+    w := kernel.condition _,
+    is_colimit := begin
+      haveI : limits.has_images C := has_images,
+      haveI : has_equalizers C := preadditive.has_equalizers_of_has_kernels,
+      letI : has_zero_object C := has_zero_object_of_has_finite_biproducts _,
+      have aux : _ := _,
+      refine is_colimit_aux _
+        (λ A, inv (image_mono_factorisation f).m ≫
+          inv (abelian.coimage_image_comparison f) ≫ colimit.desc _ _)
+        aux _,
+      { intros A g hg,
+        rw [cokernel_cofork.π_of_π] at hg,
+        rw [← cancel_epi f, hg, ← aux, cokernel_cofork.π_of_π], },
+      { intro A,
+        simp only [cokernel_cofork.π_of_π, ← category.assoc],
+        convert colimit.ι_desc _ _ using 2,
+        rw [is_iso.comp_inv_eq, is_iso.comp_inv_eq, eq_comm, ←image_mono_factorisation_e'],
+        exact (image_mono_factorisation f).fac, }
+    end }, }
+
+end of_coimage_image_comparison_is_iso
+
+variables [∀ {X Y : C} (f : X ⟶ Y), is_iso (abelian.coimage_image_comparison f)]
+  [limits.has_finite_products C]
+local attribute [instance] of_coimage_image_comparison_is_iso.normal_mono_category
+local attribute [instance] of_coimage_image_comparison_is_iso.normal_epi_category
+
+/--
+A preadditive category with kernels, cokernels, and finite products,
+in which the coimage-image comparison morphism is always an isomorphism,
+is an abelian category.
+
+The Stacks project uses this characterisation at the definition of an abelian category.
+See https://stacks.math.columbia.edu/tag/0109.
+-/
+def of_coimage_image_comparison_is_iso : abelian C := {}
+
+end category_theory.abelian
+
 namespace category_theory.abelian
 variables {C : Type u} [category.{v} C] [abelian C]
 
@@ -220,27 +357,34 @@ end has_strong_epi_mono_factorisations
 section images
 variables {X Y : C} (f : X ⟶ Y)
 
-/-- There is a canonical isomorphism between the coimage and the image of a morphism. -/
-abbreviation coimage_iso_image : abelian.coimage f ≅ abelian.image f :=
-is_image.iso_ext (coimage_strong_epi_mono_factorisation f).to_mono_is_image
-  (image_strong_epi_mono_factorisation f).to_mono_is_image
+/--
+The coimage-image comparison morphism is always an isomorphism in an abelian category.
+See `category_theory.abelian.of_coimage_image_comparison_is_iso` for the converse.
+-/
+instance : is_iso (coimage_image_comparison f) :=
+begin
+  convert is_iso.of_iso (is_image.iso_ext (coimage_strong_epi_mono_factorisation f).to_mono_is_image
+    (image_strong_epi_mono_factorisation f).to_mono_is_image),
+  ext,
+  change _ = _ ≫ (image_strong_epi_mono_factorisation f).m,
+  simp [-image_strong_epi_mono_factorisation_to_mono_factorisation_m]
+end
 
-/-- There is a canonical isomorphism between the abelian image and the categorical image of a
+/-- There is a canonical isomorphism between the abelian coimage and the abelian image of a
     morphism. -/
-abbreviation image_iso_image : abelian.image f ≅ image f :=
-is_image.iso_ext (image_strong_epi_mono_factorisation f).to_mono_is_image (image.is_image f)
+abbreviation coimage_iso_image : abelian.coimage f ≅ abelian.image f :=
+as_iso (coimage_image_comparison f)
 
 /-- There is a canonical isomorphism between the abelian coimage and the categorical image of a
     morphism. -/
 abbreviation coimage_iso_image' : abelian.coimage f ≅ image f :=
 is_image.iso_ext (coimage_strong_epi_mono_factorisation f).to_mono_is_image
   (image.is_image f)
 
-lemma full_image_factorisation : abelian.coimage.π f ≫ (coimage_iso_image f).hom ≫
-  abelian.image.ι f = f :=
-by rw [limits.is_image.iso_ext_hom,
-  ←image_strong_epi_mono_factorisation_to_mono_factorisation_m, is_image.lift_fac,
-  coimage_strong_epi_mono_factorisation_to_mono_factorisation_m, abelian.coimage.fac]
+/-- There is a canonical isomorphism between the abelian image and the categorical image of a
+    morphism. -/
+abbreviation image_iso_image : abelian.image f ≅ image f :=
+is_image.iso_ext (image_strong_epi_mono_factorisation f).to_mono_is_image (image.is_image f)
 
 end images
 

src/category_theory/abelian/exact.lean

@@ -83,7 +83,8 @@ begin
         kernel.lift (cokernel.π f) u _ ≫ (image_iso_image f).hom ≫ (image_subobject_iso _).inv,
       rw [←kernel.lift_ι g u hu, category.assoc, h.2, has_zero_morphisms.comp_zero] },
     { tidy },
-    { intros, rw [←cancel_mono (image_subobject f).arrow, w], simp, } }
+    { intros, rw [←cancel_mono (image_subobject f).arrow, w],
+      simp, } }
 end
 
 theorem exact_iff' {cg : kernel_fork g} (hg : is_limit cg)

src/category_theory/abelian/images.lean

@@ -14,6 +14,11 @@ In an abelian category we usually want the image of a morphism `f` to be defined
 We make these definitions here, as `abelian.image f` and `abelian.coimage f`
 (without assuming the category is actually abelian),
 and later relate these to the usual categorical notions when in an abelian category.
+
+There is a canonical morphism `coimage_image_comparison : abelian.coimage f ⟶ abelian.image f`.
+Later we show that this is always an isomorphism in an abelian category,
+and conversely a category with (co)kernels and finite products in which this morphism
+is always an isomorphism is an abelian category.
 -/
 
 noncomputable theory
@@ -73,4 +78,31 @@ epi_of_epi_fac $ coimage.fac f
 
 end coimage
 
+/--
+The canonical map from the abelian coimage to the abelian image.
+In any abelian category this is an isomorphism.
+
+Conversely, any additive category with kernels and cokernels and
+in which this is always an isomorphism, is abelian.
+
+See https://stacks.math.columbia.edu/tag/0107
+-/
+def coimage_image_comparison : abelian.coimage f ⟶ abelian.image f :=
+cokernel.desc (kernel.ι f) (kernel.lift (cokernel.π f) f (by simp)) $ (by { ext, simp, })
+
+/--
+An alternative formulation of the canonical map from the abelian coimage to the abelian image.
+-/
+def coimage_image_comparison' : abelian.coimage f ⟶ abelian.image f :=
+kernel.lift (cokernel.π f) (cokernel.desc (kernel.ι f) f (by simp)) (by { ext, simp, })
+
+lemma coimage_image_comparison_eq_coimage_image_comparison' :
+  coimage_image_comparison f = coimage_image_comparison' f :=
+by { ext, simp [coimage_image_comparison, coimage_image_comparison'], }
+
+@[simp, reassoc]
+lemma coimage_image_factorisation :
+  coimage.π f ≫ coimage_image_comparison f ≫ image.ι f = f :=
+by simp [coimage_image_comparison]
+
 end category_theory.abelian

src/category_theory/limits/shapes/biproducts.lean

@@ -590,6 +590,17 @@ def biproduct.unique_up_to_iso (f : J → C) [has_biproduct f] {b : bicone f} (h
   inv_hom_id' := by rw [← biproduct.cone_point_unique_up_to_iso_hom f hb,
     ← biproduct.cone_point_unique_up_to_iso_inv f hb, iso.inv_hom_id] }
 
+section
+variables (C)
+
+/-- A category with finite biproducts has a zero object. -/
+def has_zero_object_of_has_finite_biproducts [has_finite_biproducts C] : has_zero_object C :=
+{ zero := biproduct pempty.elim,
+  unique_to := λ X, ⟨⟨0⟩, by tidy⟩,
+  unique_from := λ X, ⟨⟨0⟩, by tidy⟩, }
+
+end
+
 /--
 A binary bicone for a pair of objects `P Q : C` consists of the cone point `X`,
 maps from `X` to both `P` and `Q`, and maps from both `P` and `Q` to `X`,

src/category_theory/limits/shapes/kernels.lean

@@ -458,7 +458,7 @@ cofork.is_colimit.mk' _ $ λ s,
   let s' : cokernel_cofork f := cofork.of_π s.π
     (by apply hg.left_cancellation; simp [←category.assoc, s.condition]) in
   let l := cokernel_cofork.is_colimit.desc' i s'.π s'.condition in
-  ⟨l.1, l.2, 
+  ⟨l.1, l.2,
     λ m hm, by apply cofork.is_colimit.hom_ext i; rw cofork.π_of_π at hm; rw hm; exact l.2.symm⟩
 
 end
@@ -668,6 +668,15 @@ zero_of_target_iso_zero _ (cokernel.of_epi f)
 
 end has_zero_object
 
+section mono_factorisation
+variables {f}
+
+@[simp] lemma mono_factorisation.kernel_ι_comp [has_kernel f] (F : mono_factorisation f) :
+  kernel.ι f ≫ F.e = 0 :=
+by rw [← cancel_mono F.m, zero_comp, category.assoc, F.fac, kernel.condition]
+
+end mono_factorisation
+
 section has_image
 
 /--

src/data/fin/basic.lean

@@ -94,6 +94,10 @@ localized "attribute [instance] fact.bit1.pos" in fin_fact
 localized "attribute [instance] fact.pow.pos" in fin_fact
 
 namespace fin
+
+/-- A non-dependent variant of `elim0`. -/
+def elim0' {α : Sort*} (x : fin 0) : α := x.elim0
+
 variables {n m : ℕ} {a b : fin n}
 
 instance fin_to_nat (n : ℕ) : has_coe (fin n) nat := ⟨subtype.val⟩