feat(CategoryTheory/Abelian): AB4 and AB5 axioms (#6504)

Joint work with @IsaacHernando and Coleton Kotch.



Co-authored-by: Adam Topaz <[email protected]>
Co-authored-by: Jakob von Raumer <[email protected]>

Mathlib.lean

@@ -1359,6 +1359,7 @@ import Mathlib.CategoryTheory.Abelian.Exact
 import Mathlib.CategoryTheory.Abelian.Ext
 import Mathlib.CategoryTheory.Abelian.FunctorCategory
 import Mathlib.CategoryTheory.Abelian.Generator
+import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms
 import Mathlib.CategoryTheory.Abelian.Images
 import Mathlib.CategoryTheory.Abelian.Injective
 import Mathlib.CategoryTheory.Abelian.InjectiveResolution

Mathlib/Algebra/Category/Grp/AB5.lean

@@ -9,6 +9,7 @@ import Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
 import Mathlib.CategoryTheory.Abelian.Exact
 import Mathlib.Algebra.Category.Grp.FilteredColimits
 import Mathlib.CategoryTheory.Abelian.FunctorCategory
+import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms
 
 /-!
 # The category of abelian groups satisfies Grothendieck's axiom AB5
@@ -45,3 +46,9 @@ noncomputable instance :
 noncomputable instance :
     PreservesFiniteLimits <| colim (J := J) (C := AddCommGrp.{u}) := by
   apply Functor.preservesFiniteLimitsOfPreservesHomology
+
+instance : HasFilteredColimits (AddCommGrp.{u}) where
+  HasColimitsOfShape := inferInstance
+
+noncomputable instance : AB5 (AddCommGrp.{u}) where
+  preservesFiniteLimits := fun _ => inferInstance

Mathlib/CategoryTheory/Abelian/GrothendieckAxioms.lean

@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2023 Adam Topaz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Isaac Hernando, Coleton Kotch, Adam Topaz
+-/
+
+import Mathlib.CategoryTheory.Limits.Filtered
+import Mathlib.CategoryTheory.Limits.Preserves.Finite
+
+/-!
+
+# Grothendieck Axioms
+
+This file defines some of the Grothendieck Axioms for abelian categories, and proves
+basic facts about them.
+
+## Definitions
+
+- `AB4` -- an abelian category satisfies `AB4` provided that coproducts are exact.
+- `AB5` -- an abelian category satisfies `AB5` provided that filtered colimits are exact.
+- The duals of the above definitions, called `AB4Star` and `AB5Star`.
+
+## Remarks
+
+For `AB4` and `AB5`, we only require left exactness as right exactness is automatic.
+A comparison with Grothendieck's original formulation of the properties can be found in the
+comments of the linked Stacks page.
+Exactness as the preservation of short exact sequences is introduced in
+`CategoryTheory.Abelian.Exact`.
+
+## Projects
+
+- Add additional axioms, especially define Grothendieck categories.
+- Prove that `AB5` implies `AB4`.
+
+## References
+* [Stacks: Grothendieck's AB conditions](https://stacks.math.columbia.edu/tag/079A)
+
+-/
+
+namespace CategoryTheory
+
+open Limits
+
+universe v v' u u'
+
+variable (C : Type u) [Category.{v} C]
+
+/--
+A category `C` which has coproducts is said to have `AB4` provided that
+coproducts are exact.
+-/
+class AB4 [HasCoproducts C] where
+  /-- Exactness of coproducts stated as `colim : (Discrete α ⥤ C) ⥤ C` preserving limits. -/
+  preservesFiniteLimits (α : Type v) :
+    PreservesFiniteLimits (colim (J := Discrete α) (C := C))
+
+attribute [instance] AB4.preservesFiniteLimits
+
+/-- A category `C` which has products is said to have `AB4Star` (in literature `AB4*`)
+provided that products are exact. -/
+class AB4Star [HasProducts C] where
+  /-- Exactness of products stated as `lim : (Discrete α ⥤ C) ⥤ C` preserving colimits. -/
+  preservesFiniteColimits (α : Type v) :
+    PreservesFiniteColimits (lim (J := Discrete α) (C := C))
+
+attribute [instance] AB4Star.preservesFiniteColimits
+
+/--
+A category `C` which has filtered colimits is said to have `AB5` provided that
+filtered colimits are exact.
+-/
+class AB5 [HasFilteredColimits C] where
+  /-- Exactness of filtered colimits stated as `colim : (J ⥤ C) ⥤ C` on filtered `J`
+  preserving limits. -/
+  preservesFiniteLimits (J : Type v) [SmallCategory J] [IsFiltered J] :
+    PreservesFiniteLimits (colim (J := J) (C := C))
+
+attribute [instance] AB5.preservesFiniteLimits
+
+/--
+A category `C` which has cofiltered limits is said to have `AB5Star` (in literature `AB5*`)
+provided that cofiltered limits are exact.
+-/
+class AB5Star [HasCofilteredLimits C] where
+  /-- Exactness of cofiltered limits stated as `lim : (J ⥤ C) ⥤ C` on cofiltered `J`
+  preserving colimits. -/
+  preservesFiniteColimits (J : Type v) [SmallCategory J] [IsCofiltered J] :
+    PreservesFiniteColimits (lim (J := J) (C := C))
+
+attribute [instance] AB5Star.preservesFiniteColimits
+
+end CategoryTheory

Mathlib/CategoryTheory/Adjunction/Limits.lean

@@ -90,6 +90,11 @@ def leftAdjointPreservesColimits : PreservesColimitsOfSize.{v, u} F where
               @Equiv.unique _ _ (IsColimit.isoUniqueCoconeMorphism.hom hc _)
                 ((adj.functorialityAdjunction _).homEquiv _ _) } }
 
+noncomputable
+instance colimPreservesColimits [HasColimitsOfShape J C] :
+    PreservesColimits (colim (J := J) (C := C)) :=
+  colimConstAdj.leftAdjointPreservesColimits
+
 -- see Note [lower instance priority]
 noncomputable instance (priority := 100) isEquivalencePreservesColimits
     (E : C ⥤ D) [E.IsEquivalence] :
@@ -193,6 +198,11 @@ def rightAdjointPreservesLimits : PreservesLimitsOfSize.{v, u} G where
               @Equiv.unique _ _ (IsLimit.isoUniqueConeMorphism.hom hc _)
                 ((adj.functorialityAdjunction' _).homEquiv _ _).symm } }
 
+noncomputable
+instance limPreservesLimits [HasLimitsOfShape J C] :
+    PreservesLimits (lim (J := J) (C := C)) :=
+  constLimAdj.rightAdjointPreservesLimits
+
 -- see Note [lower instance priority]
 noncomputable instance (priority := 100) isEquivalencePreservesLimits
     (E : D ⥤ C) [E.IsEquivalence] :

Mathlib/CategoryTheory/Limits/Filtered.lean

@@ -77,6 +77,12 @@ class HasFilteredColimitsOfSize : Prop where
   /-- For all filtered types of a size `w`, we have colimits -/
   HasColimitsOfShape : ∀ (I : Type w) [Category.{w'} I] [IsFiltered I], HasColimitsOfShape I C
 
+/-- Class for having cofiltered limits. -/
+abbrev HasCofilteredLimits := HasCofilteredLimitsOfSize.{v, v} C
+
+/-- Class for having filtered colimits. -/
+abbrev HasFilteredColimits := HasFilteredColimitsOfSize.{v, v} C
+
 end
 
 instance (priority := 100) hasLimitsOfShape_of_has_cofiltered_limits