[Merged by Bors] - feat(Algebra/Category/GroupCat/Abelian): prove AddCommGroupCat is AB5

Mathlib.lean

@@ -42,6 +42,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

@@ -8,30 +8,28 @@ Authors: Markus Himmel
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-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
 
 /-!
 # 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 :=
@@ -47,18 +45,44 @@ 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]
+  add_comp := by exact Preadditive.add_comp
+  comp_add := by exact 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⟩⟩
+
+theorem exact_iff' : Exact f g ↔ f ≫ g = 0 ∧ g.ker ≤ f.range := by
+  rw [exact_iff, le_antisymm_iff]
+  exact and_congr ⟨fun h => ext fun x => h (AddMonoidHom.mem_range.mpr ⟨x, rfl⟩),
+    by rintro h _ ⟨x, rfl⟩; exact FunLike.congr_fun h x⟩ Iff.rfl
+
+/-- 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 ?_
+  replace h : ∀ j : J, Exact (η.app j) (γ.app j) :=
+    fun j => Functor.map_exact ((evaluation _ _).obj j) η γ h
+  constructor
+  · 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).right 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/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

@@ -47,7 +47,7 @@ isomorphism theorems, quotient groups
 
 open Function
 
-universe u v
+universe u v w
 
 namespace QuotientGroup
 
@@ -125,6 +125,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

@@ -92,7 +92,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]
 
@@ -2873,6 +2873,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