feat(Algebra/Category/GroupCat/Abelian): prove AddCommGroupCat is AB5 (#5597)

This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed.

Co-authored-by: Moritz Firsching <moritz.firsching@gmail.com>
Co-authored-by: Nikolas Kuhn <nikolaskuhn@gmx.de>
Co-authored-by: Amelia Livingston <101damnations@github.com>



Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: adamtopaz <github@adamtopaz.com>
Co-authored-by: nick-kuhn <nikolaskuhn@gmx.de>

Author: 5 people

Mathlib.lean

@@ -47,6 +47,7 @@ import Mathlib.Algebra.Category.GroupCat.EquivalenceGroupAddGroup
 import Mathlib.Algebra.Category.GroupCat.FilteredColimits
 import Mathlib.Algebra.Category.GroupCat.Images
 import Mathlib.Algebra.Category.GroupCat.Injective
+import Mathlib.Algebra.Category.GroupCat.Kernels
 import Mathlib.Algebra.Category.GroupCat.Limits
 import Mathlib.Algebra.Category.GroupCat.Preadditive
 import Mathlib.Algebra.Category.GroupCat.Subobject

Mathlib/Algebra/Category/GroupCat/Abelian.lean

@@ -3,32 +3,30 @@ Copyright (c) 2020 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-import Mathlib.Algebra.Category.GroupCat.ZModuleEquivalence
-import Mathlib.Algebra.Category.GroupCat.Limits
 import Mathlib.Algebra.Category.GroupCat.Colimits
+import Mathlib.Algebra.Category.GroupCat.FilteredColimits
+import Mathlib.Algebra.Category.GroupCat.Kernels
+import Mathlib.Algebra.Category.GroupCat.Limits
+import Mathlib.Algebra.Category.GroupCat.ZModuleEquivalence
 import Mathlib.Algebra.Category.ModuleCat.Abelian
-import Mathlib.CategoryTheory.Abelian.Basic
+import Mathlib.CategoryTheory.Abelian.FunctorCategory
+import Mathlib.CategoryTheory.Limits.ConcreteCategory
 
 #align_import algebra.category.Group.abelian from "leanprover-community/mathlib"@"f7baecbb54bd0f24f228576f97b1752fc3c9b318"
 
 /-!
 # The category of abelian groups is abelian
 -/
 
-
-open CategoryTheory
-
-open CategoryTheory.Limits
+open CategoryTheory Limits
 
 universe u
 
 noncomputable section
 
 namespace AddCommGroupCat
 
-section
-
-variable {X Y : AddCommGroupCat.{u}} (f : X ⟶ Y)
+variable {X Y Z : AddCommGroupCat.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
 
 /-- In the category of abelian groups, every monomorphism is normal. -/
 def normalMono (_ : Mono f) : NormalMono f :=
@@ -44,18 +42,38 @@ def normalEpi (_ : Epi f) : NormalEpi f :=
 set_option linter.uppercaseLean3 false in
 #align AddCommGroup.normal_epi AddCommGroupCat.normalEpi
 
-end
-
 /-- The category of abelian groups is abelian. -/
 instance : Abelian AddCommGroupCat.{u} where
-  has_finite_products := ⟨by infer_instance⟩
+  has_finite_products := ⟨HasFiniteProducts.out⟩
   normalMonoOfMono := normalMono
   normalEpiOfEpi := normalEpi
-  add_comp := by
-    intros
-    simp only [Preadditive.add_comp]
-  comp_add := by
-    intros
-    simp only [Preadditive.comp_add]
+
+theorem exact_iff : Exact f g ↔ f.range = g.ker := by
+  rw [Abelian.exact_iff' f g (kernelIsLimit _) (cokernelIsColimit _)]
+  exact
+    ⟨fun h => ((AddMonoidHom.range_le_ker_iff _ _).mpr h.left).antisymm
+        ((QuotientAddGroup.ker_le_range_iff _ _).mpr h.right),
+      fun h => ⟨(AddMonoidHom.range_le_ker_iff _ _).mp h.le,
+          (QuotientAddGroup.ker_le_range_iff _ _).mp h.symm.le⟩⟩
+
+/-- The category of abelian groups satisfies Grothedieck's Axiom AB5. -/
+instance {J : Type u} [SmallCategory J] [IsFiltered J] :
+    PreservesFiniteLimits <| colim (J := J) (C := AddCommGroupCat.{u}) := by
+  refine Functor.preservesFiniteLimitsOfMapExact _
+    fun F G H η γ h => (exact_iff _ _).mpr (le_antisymm ?_ ?_)
+  all_goals replace h : ∀ j : J, Exact (η.app j) (γ.app j) :=
+    fun j => Functor.map_exact ((evaluation _ _).obj j) η γ h
+  · rw [AddMonoidHom.range_le_ker_iff, ← comp_def]
+    exact colimit.hom_ext fun j => by simp [reassoc_of% (h j).w]
+  · intro x (hx : _ = _)
+    rcases Concrete.colimit_exists_rep G x with ⟨j, y, rfl⟩
+    erw [← comp_apply, colimit.ι_map, comp_apply,
+      ← map_zero (by exact colimit.ι H j : H.obj j →+ ↑(colimit H))] at hx
+    rcases Concrete.colimit_exists_of_rep_eq H _ _ hx with ⟨k, e₁, e₂, hk : _ = H.map e₂ 0⟩
+    rw [map_zero, ← comp_apply, ← NatTrans.naturality, comp_apply] at hk
+    rcases ((exact_iff _ _).mp <| h k).ge hk with ⟨t, ht⟩
+    use colimit.ι F k t
+    erw [← comp_apply, colimit.ι_map, comp_apply, ht]
+    exact colimit.w_apply G e₁ y
 
 end AddCommGroupCat

Mathlib/Algebra/Category/GroupCat/Basic.lean

@@ -74,6 +74,9 @@ lemma coe_id {X : GroupCat} : (𝟙 X : X → X) = id := rfl
 @[to_additive (attr := simp)]
 lemma coe_comp {X Y Z : GroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
+@[to_additive]
+lemma comp_def {X Y Z : GroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : f ≫ g = g.comp f := rfl
+
 -- porting note: added
 @[simp] lemma forget_map (f : X ⟶ Y) : (forget GroupCat).map f = (f : X → Y) := rfl
 
@@ -220,6 +223,9 @@ lemma coe_id {X : CommGroupCat} : (𝟙 X : X → X) = id := rfl
 @[to_additive (attr := simp)]
 lemma coe_comp {X Y Z : CommGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
+@[to_additive]
+lemma comp_def {X Y Z : CommGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : f ≫ g = g.comp f := rfl
+
 -- porting note: added
 @[to_additive (attr := simp)]
 lemma forget_map {X Y : CommGroupCat} (f : X ⟶ Y) :

Mathlib/Algebra/Category/GroupCat/Kernels.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2023 Moritz Firsching. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Kurniadi Angdinata, Moritz Firsching, Nikolas Kuhn
+-/
+import Mathlib.Algebra.Category.GroupCat.EpiMono
+import Mathlib.Algebra.Category.GroupCat.Preadditive
+import Mathlib.CategoryTheory.Limits.Shapes.Kernels
+
+/-!
+# The concrete (co)kernels in the category of abelian groups are categorical (co)kernels.
+-/
+
+namespace AddCommGroupCat
+
+open AddMonoidHom CategoryTheory Limits QuotientAddGroup
+
+universe u
+
+variable {G H : AddCommGroupCat.{u}} (f : G ⟶ H)
+
+/-- The kernel cone induced by the concrete kernel. -/
+def kernelCone : KernelFork f :=
+  KernelFork.ofι (Z := of f.ker) f.ker.subtype <| ext fun x => x.casesOn fun _ hx => hx
+
+/-- The kernel of a group homomorphism is a kernel in the categorical sense. -/
+def kernelIsLimit : IsLimit <| kernelCone f :=
+  Fork.IsLimit.mk _
+    (fun s => (by exact Fork.ι s : _ →+ G).codRestrict _ <| fun c => f.mem_ker.mpr <|
+      by exact FunLike.congr_fun s.condition c)
+    (fun _ => by rfl)
+    (fun _ _ h => ext fun x => Subtype.ext_iff_val.mpr <| by exact FunLike.congr_fun h x)
+
+/-- The cokernel cocone induced by the projection onto the quotient. -/
+def cokernelCocone : CokernelCofork f :=
+  CokernelCofork.ofπ (Z := of <| H ⧸ f.range) (mk' f.range) <| ext fun x =>
+    (eq_zero_iff _).mpr ⟨x, rfl⟩
+
+/-- The projection onto the quotient is a cokernel in the categorical sense. -/
+def cokernelIsColimit : IsColimit <| cokernelCocone f :=
+  Cofork.IsColimit.mk _
+    (fun s => lift _ _ <| (range_le_ker_iff _ _).mpr <| CokernelCofork.condition s)
+    (fun _ => rfl)
+    (fun _ _ h => have : Epi (cokernelCocone f).π := (epi_iff_surjective _).mpr <| mk'_surjective _
+      (cancel_epi _).mp <| by simpa only [parallelPair_obj_one] using h)
+
+end AddCommGroupCat

Mathlib/GroupTheory/QuotientGroup.lean

@@ -44,7 +44,7 @@ isomorphism theorems, quotient groups
 
 open Function
 
-universe u v
+universe u v w
 
 namespace QuotientGroup
 
@@ -122,6 +122,12 @@ theorem eq_one_iff {N : Subgroup G} [nN : N.Normal] (x : G) : (x : G ⧸ N) = 1
 #align quotient_group.eq_one_iff QuotientGroup.eq_one_iff
 #align quotient_add_group.eq_zero_iff QuotientAddGroup.eq_zero_iff
 
+@[to_additive]
+theorem ker_le_range_iff {I : Type w} [Group I] (f : G →* H) [f.range.Normal] (g : H →* I) :
+    g.ker ≤ f.range ↔ (mk' f.range).comp g.ker.subtype = 1 :=
+  ⟨fun h => MonoidHom.ext fun ⟨_, hx⟩ => (eq_one_iff _).mpr <| h hx,
+    fun h x hx => (eq_one_iff _).mp <| by exact FunLike.congr_fun h ⟨x, hx⟩⟩
+
 @[to_additive (attr := simp)]
 theorem ker_mk' : MonoidHom.ker (QuotientGroup.mk' N : G →* G ⧸ N) = N :=
   Subgroup.ext eq_one_iff

Mathlib/GroupTheory/Subgroup/Basic.lean

@@ -89,7 +89,7 @@ subgroup, subgroups
 open Function
 open Int
 
-variable {G G' : Type _} [Group G] [Group G']
+variable {G G' G'' : Type _} [Group G] [Group G'] [Group G'']
 
 variable {A : Type _} [AddGroup A]
 
@@ -2869,6 +2869,10 @@ theorem ker_prodMap {G' : Type _} {N' : Type _} [Group G'] [Group N'] (f : G →
 #align monoid_hom.ker_prod_map MonoidHom.ker_prodMap
 #align add_monoid_hom.ker_sum_map AddMonoidHom.ker_sumMap
 
+@[to_additive]
+theorem range_le_ker_iff (f : G →* G') (g : G' →* G'') : f.range ≤ g.ker ↔ g.comp f = 1 :=
+  ⟨fun h => ext fun x => h ⟨x, rfl⟩, by rintro h _ ⟨y, rfl⟩; exact FunLike.congr_fun h y⟩
+
 @[to_additive]
 instance (priority := 100) normal_ker (f : G →* M) : f.ker.Normal :=
   ⟨fun x hx y => by