From d3684bc372116d10c47e064c11e409280f3b35e8 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 29 Mar 2022 18:32:04 +0000 Subject: [PATCH] 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 --- src/category_theory/abelian/basic.lean | 184 ++++++++++++++++-- src/category_theory/abelian/exact.lean | 3 +- src/category_theory/abelian/images.lean | 32 +++ .../limits/shapes/biproducts.lean | 11 ++ .../limits/shapes/kernels.lean | 11 +- src/data/fin/basic.lean | 4 + 6 files changed, 223 insertions(+), 22 deletions(-) diff --git a/src/category_theory/abelian/basic.lean b/src/category_theory/abelian/basic.lean index eaed4d272707f..3bff58debf47f 100644 --- a/src/category_theory/abelian/basic.lean +++ b/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,15 +357,23 @@ 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. -/ @@ -236,11 +381,10 @@ 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 diff --git a/src/category_theory/abelian/exact.lean b/src/category_theory/abelian/exact.lean index 6acb0c2b72c3d..7e25cd93eec8a 100644 --- a/src/category_theory/abelian/exact.lean +++ b/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) diff --git a/src/category_theory/abelian/images.lean b/src/category_theory/abelian/images.lean index 3ad00811d190c..5c840a792222a 100644 --- a/src/category_theory/abelian/images.lean +++ b/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 diff --git a/src/category_theory/limits/shapes/biproducts.lean b/src/category_theory/limits/shapes/biproducts.lean index dd0d2f7c21d31..00121c67478bd 100644 --- a/src/category_theory/limits/shapes/biproducts.lean +++ b/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`, diff --git a/src/category_theory/limits/shapes/kernels.lean b/src/category_theory/limits/shapes/kernels.lean index a021c301ba3fc..40d00bc14718f 100644 --- a/src/category_theory/limits/shapes/kernels.lean +++ b/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 /-- diff --git a/src/data/fin/basic.lean b/src/data/fin/basic.lean index da2b79f9ab320..a1f7e51161ecb 100644 --- a/src/data/fin/basic.lean +++ b/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⟩