From 3c87dcb1d31cd54d8796ec7795de25b6f88470b4 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sun, 26 Jan 2025 11:32:25 +0100
Subject: [PATCH 01/57] Bad start

---
 .../Category/Grp/LeftExactFunctor.lean        | 64 +++++++++++++++++++
 1 file changed, 64 insertions(+)
 create mode 100644 Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean

diff --git a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
new file mode 100644
index 00000000000000..59afb36b8c2b51
--- /dev/null
+++ b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.Limits.ExactFunctor
+import Mathlib.CategoryTheory.Preadditive.Basic
+import Mathlib.CategoryTheory.Limits.Shapes.Biproducts
+import Mathlib.Algebra.Category.Grp.Limits
+
+/-!
+# The functor `(C ⥤ₗ AddCommGroup) ⥤ (C ⥤ₗ Type v)` is an equivalence
+-/
+
+open CategoryTheory Limits
+
+universe v u
+
+section
+
+variable {C : Type u} [Category.{v} C] [Preadditive C] [HasFiniteBiproducts C]
+
+variable (F : C ⥤ Type v) [PreservesFiniteLimits F]
+
+section
+
+variable (X : C)
+
+attribute [local instance] hasBinaryBiproducts_of_finite_biproducts
+
+#check F.map <| Limits.biprod.desc (𝟙 X) (𝟙 X)
+
+def addCommGroup : AddCommGroup (F.obj X) := sorry
+
+end
+
+def lift (F : C ⥤ Type v) : C ⥤ AddCommGrp.{v} := sorry
+
+instance : PreservesFiniteLimits (lift F) := sorry
+
+def liftIso :
+    ((LeftExactFunctor.whiskeringRight _ _ _).obj ⟨forget AddCommGrp.{v}, inferInstance⟩).obj ⟨lift F, inferInstance⟩ ≅ (⟨F, inferInstance⟩ : C ⥤ₗ Type v) := sorry
+
+end
+
+section
+
+variable {C : Type u} [Category.{v} C] [Preadditive C] [HasFiniteBiproducts C]
+
+section
+
+variable (F : C ⥤ AddCommGrp.{v}) [PreservesFiniteLimits F] (X : C)
+
+def q : F.obj X ≅ @AddCommGrp.of ((F ⋙ forget _).obj X) (addCommGroup (F ⋙ forget _) X) := sorry
+
+end
+
+instance : Functor.IsEquivalence <|
+    (LeftExactFunctor.whiskeringRight C _ _).obj ⟨forget AddCommGrp.{v}, inferInstance⟩ where
+  full := sorry
+  faithful := sorry
+  essSurj := ⟨(⟨_, ⟨liftIso ·.1⟩⟩)⟩
+
+end

From f4a3c794a137906a2a5699706bd728a4203fa76e Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sun, 26 Jan 2025 17:46:10 +0100
Subject: [PATCH 02/57] WIP

---
 .../Category/Grp/LeftExactFunctor.lean        | 121 +++++++++++++++++-
 1 file changed, 119 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
index 59afb36b8c2b51..7d450dc491d8eb 100644
--- a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
+++ b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
@@ -7,6 +7,8 @@ import Mathlib.CategoryTheory.Limits.ExactFunctor
 import Mathlib.CategoryTheory.Preadditive.Basic
 import Mathlib.CategoryTheory.Limits.Shapes.Biproducts
 import Mathlib.Algebra.Category.Grp.Limits
+import Mathlib.CategoryTheory.Limits.Shapes.Types
+import Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
 
 /-!
 # The functor `(C ⥤ₗ AddCommGroup) ⥤ (C ⥤ₗ Type v)` is an equivalence
@@ -14,7 +16,118 @@ import Mathlib.Algebra.Category.Grp.Limits
 
 open CategoryTheory Limits
 
-universe v u
+universe v v' u u'
+
+section
+
+variable {C : Type u} [Category.{v} C] [HasFiniteProducts C]
+
+structure AbelianGroupObject (X : C) where
+  m : X ⨯ X ⟶ X
+  e : ⊤_ C ⟶ X
+  inv : X ⟶ X
+  assoc : (prod.associator X X X).hom ≫ prod.map (𝟙 X) m ≫ m = prod.map m (𝟙 X) ≫ m
+  comm : (prod.braiding X X).hom ≫ m = m
+  left_id : prod.lift (terminal.from X ≫ e) (𝟙 X) ≫ m = 𝟙 X
+  right_id : prod.lift (𝟙 X) (terminal.from X ≫ e) ≫ m = 𝟙 X
+  left_inv : prod.lift inv (𝟙 X) ≫ m = terminal.from _ ≫ e
+  right_inv : prod.lift (𝟙 X) inv ≫ m = terminal.from _ ≫ e
+
+  -- -- assoc : m ≫ m = (prod.fst ≫ m) ≫ m ≫ m
+  -- comm : m = m ≫ (prod.snd ≫ prod.fst)
+  -- left_id : (e ≫ prod.fst) ≫ m = prod.snd
+  -- right_id : (prod.fst ≫ e) ≫ m = prod.fst
+  -- left_inv : (inv ≫ prod.fst) ≫ m = e
+  -- right_inv : (prod.fst ≫ inv) ≫ m = e
+
+-- structure InternalAddCommGrp (X : C) where
+--   presheaf : Cᵒᵖ ⥤ AddCommGrp.{v}
+--   iso : presheaf ⋙ forget _ ≅ yoneda.obj X
+
+-- def add {X : Type v} (G : InternalAddCommGrp X) : X × X → X :=
+--   fun x y => _
+
+-- variable {D : Type u} [Category.{v} D] (F : C ⥤ D) [PreservesFiniteLimits F]
+
+-- def InternalAddCommGrp.map {X : C} (G : InternalAddCommGrp X) : InternalAddCommGrp (F.obj X) where
+--   presheaf := sorry
+--   iso := sorry
+
+end
+
+section
+
+variable {C : Type u} [Category.{v} C] [Preadditive C] [HasFiniteBiproducts C]
+
+attribute [local instance] hasBinaryBiproducts_of_finite_biproducts
+
+noncomputable def Preadditive.abelianGroupObject (X : C) : AbelianGroupObject X where
+  m := prod.fst + prod.snd
+  e := IsZero.to_ (IsZero.of_mono_zero (⊤_ C) X) _
+  inv := -𝟙 X
+  assoc := by
+    rw [← cancel_epi (biprod.isoProd _ _).hom]
+    simp [add_assoc]
+  comm := by
+    rw [← cancel_epi (biprod.isoProd _ _).hom]
+    simp [add_comm]
+  left_id := by simp [IsZero.to_eq _ 0]
+  right_id := by simp [IsZero.to_eq _ 0]
+  left_inv := by simp [IsZero.to_eq _ 0]
+  right_inv := by simp [IsZero.to_eq _ 0]
+
+end
+
+section
+
+variable {C : Type u} [Category.{v} C] [HasFiniteProducts C]
+variable {D : Type u'} [Category.{v'} D] [HasFiniteProducts D]
+variable (F : C ⥤ D) [PreservesFiniteProducts F]
+
+noncomputable def Functor.mapAbelianGroupObject {X : C} (G : AbelianGroupObject X) :
+    AbelianGroupObject (F.obj X) where
+  m := (PreservesLimitPair.iso F X X).inv ≫ F.map G.m
+  e := (PreservesTerminal.iso F).inv ≫ F.map G.e
+  inv := sorry
+  assoc := sorry
+  comm := sorry
+  left_id := sorry
+  right_id := sorry
+  left_inv := sorry
+  right_inv := sorry
+
+end
+
+namespace AbelianGroupObject.Types
+
+section
+
+noncomputable def add {X : Type v} (G : AbelianGroupObject X) : Add X where
+  add x y := G.m ((Types.binaryProductIso _ _).inv (x, y))
+
+noncomputable def neg {X : Type v} (G : AbelianGroupObject X) : Neg X where
+  neg x := G.inv x
+
+noncomputable def zero {X : Type v} (G : AbelianGroupObject X) : Zero X where
+  zero := G.e default
+
+protected theorem add_comm {X : Type v} (G : AbelianGroupObject X) (x y : X) :
+    letI : Add X := add G
+    x + y = y + x := by
+  dsimp only [(· + ·)]
+  rw [Add.add, add]
+  simp only
+  conv_lhs => rw [← G.comm]
+  simp
+  apply congr_arg G.m
+  apply (Types.binaryProductIso _ _).toEquiv.injective
+  ext
+  · simp [elementwise_of% (prod.lift_fst (prod.snd : X ⨯ X ⟶ X) prod.fst)]
+  · simp [elementwise_of% (prod.lift_snd (prod.snd : X ⨯ X ⟶ X) prod.fst)]
+
+end
+
+end AbelianGroupObject.Types
 
 section
 
@@ -36,10 +149,14 @@ end
 
 def lift (F : C ⥤ Type v) : C ⥤ AddCommGrp.{v} := sorry
 
+def liftCompForget (F : C ⥤ Type v) : lift F ⋙ forget _ ≅ F := sorry
+
 instance : PreservesFiniteLimits (lift F) := sorry
 
 def liftIso :
-    ((LeftExactFunctor.whiskeringRight _ _ _).obj ⟨forget AddCommGrp.{v}, inferInstance⟩).obj ⟨lift F, inferInstance⟩ ≅ (⟨F, inferInstance⟩ : C ⥤ₗ Type v) := sorry
+    ((LeftExactFunctor.whiskeringRight _ _ _).obj (LeftExactFunctor.of (forget AddCommGrp))).obj
+      (LeftExactFunctor.of (lift F)) ≅ LeftExactFunctor.of F :=
+  InducedCategory.isoMk (liftCompForget F)
 
 end
 

From 2d7126dc6bde5512401bd31a8fff523f4c0eff6e Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sun, 2 Feb 2025 09:15:16 +0100
Subject: [PATCH 03/57] nothing

---
 Mathlib/CategoryTheory/Monoidal/CommGrp_.lean | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/Monoidal/CommGrp_.lean

diff --git a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
new file mode 100644
index 00000000000000..b45cc6fc755bc0
--- /dev/null
+++ b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.Monoidal.CommMon_
+
+/-!
+# The category of commutative groups in a braided monoidal category
+-/
+
+universe v₁ v₂ u₁ u₂ u
+
+open CategoryTheory MonoidalCategory
+
+variable (C : Type u₁) [Category.{v₁} C] [MonoidalCategory.{v₁} C] [BraidedCategory.{v₁} C]
+
+structure CommGrp_ extends CommMon_ C where
+  

From b2d6f6bda76824194dabbdc8869c8bbfb4be8243 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sun, 2 Feb 2025 16:41:06 +0100
Subject: [PATCH 04/57] feat: group objects

---
 Mathlib.lean                                  |   3 +
 .../CategoryTheory/ChosenFiniteProducts.lean  |  83 +++++++
 .../Monoidal/Cartesian/Mon_.lean              |  38 +++
 Mathlib/CategoryTheory/Monoidal/Grp_.lean     | 228 ++++++++++++++++++
 4 files changed, 352 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean
 create mode 100644 Mathlib/CategoryTheory/Monoidal/Grp_.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 03b67d0a6f8e58..93ac5b72463903 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2083,9 +2083,11 @@ import Mathlib.CategoryTheory.Monoidal.Braided.Basic
 import Mathlib.CategoryTheory.Monoidal.Braided.Opposite
 import Mathlib.CategoryTheory.Monoidal.Braided.Reflection
 import Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_
+import Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_
 import Mathlib.CategoryTheory.Monoidal.Category
 import Mathlib.CategoryTheory.Monoidal.Center
 import Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
+import Mathlib.CategoryTheory.Monoidal.CommGrp_
 import Mathlib.CategoryTheory.Monoidal.CommMon_
 import Mathlib.CategoryTheory.Monoidal.Comon_
 import Mathlib.CategoryTheory.Monoidal.Conv
@@ -2095,6 +2097,7 @@ import Mathlib.CategoryTheory.Monoidal.Free.Basic
 import Mathlib.CategoryTheory.Monoidal.Free.Coherence
 import Mathlib.CategoryTheory.Monoidal.Functor
 import Mathlib.CategoryTheory.Monoidal.FunctorCategory
+import Mathlib.CategoryTheory.Monoidal.Grp_
 import Mathlib.CategoryTheory.Monoidal.Hopf_
 import Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
 import Mathlib.CategoryTheory.Monoidal.Internal.Limits
diff --git a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
index 0172d99e2112c4..f186a198c15495 100644
--- a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
+++ b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@@ -128,6 +128,11 @@ lemma comp_lift {V W X Y : C} (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) :
 @[simp]
 lemma lift_fst_snd {X Y : C} : lift (fst X Y) (snd X Y) = 𝟙 (X ⊗ Y) := by ext <;> simp
 
+@[simp]
+lemma lift_comp_fst_snd {X Y Z : C} (f : X ⟶ Y ⊗ Z) :
+    lift (f ≫ fst _ _) (f ≫ snd _ _) = f := by
+  aesop_cat
+
 @[reassoc (attr := simp)]
 lemma tensorHom_fst {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) :
     (f ⊗ g) ≫ fst _ _ = fst _ _ ≫ f := lift_fst _ _
@@ -164,6 +169,16 @@ lemma whiskerRight_snd {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :
     (f ▷ Y) ≫ snd _ _ = snd _ _ :=
   (tensorHom_snd _ _).trans (by simp)
 
+@[reassoc (attr := simp)]
+lemma lift_whiskerRight {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : Y ⟶ W) :
+    lift f g ≫ (h ▷ Z) = lift (f ≫ h) g := by
+  aesop_cat
+
+@[reassoc (attr := simp)]
+lemma lift_whiskerLeft {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : Z ⟶ W) :
+    lift f g ≫ (Y ◁ h) = lift f (g ≫ h) := by
+  aesop_cat
+
 @[reassoc (attr := simp)]
 lemma associator_hom_fst (X Y Z : C) :
     (α_ X Y Z).hom ≫ fst _ _ = fst _ _ ≫ fst _ _ := lift_fst _ _
@@ -196,6 +211,16 @@ lemma associator_inv_fst_snd (X Y Z : C) :
 lemma associator_inv_snd (X Y Z : C) :
     (α_ X Y Z).inv ≫ snd _ _ = snd _ _ ≫ snd _ _ := lift_snd _ _
 
+@[reassoc (attr := simp)]
+lemma lift_lift_associator_hom {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) :
+    lift (lift f g) h ≫ (α_ Y Z W).hom = lift f (lift g h) := by
+  aesop_cat
+
+@[reassoc (attr := simp)]
+lemma lift_lift_associator_inv {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W) :
+    lift f (lift g h) ≫ (α_ Y Z W).inv = lift (lift f g) h := by
+  aesop_cat
+
 @[reassoc (attr := simp)]
 lemma leftUnitor_inv_fst (X : C) :
     (λ_ X).inv ≫ fst _ _ = toUnit _ := toUnit_unique _ _
@@ -212,6 +237,18 @@ lemma rightUnitor_inv_fst (X : C) :
 lemma rightUnitor_inv_snd (X : C) :
     (ρ_ X).inv ≫ snd _ _ = toUnit _ := toUnit_unique _ _
 
+@[reassoc (attr := simp)]
+lemma lift_leftUnitor_hom {X Y : C} (f : X ⟶ 𝟙_ C) (g : X ⟶ Y) :
+    lift f g ≫ (λ_ Y).hom = g := by
+  rw [← Iso.eq_comp_inv]
+  aesop_cat
+
+@[reassoc (attr := simp)]
+lemma lift_rightUnitor_hom {X Y : C} (f : X ⟶ Y) (g : X ⟶ 𝟙_ C) :
+    lift f g ≫ (ρ_ Y).hom = f := by
+  rw [← Iso.eq_comp_inv]
+  aesop_cat
+
 /--
 Construct an instance of `ChosenFiniteProducts C` given an instance of `HasFiniteProducts C`.
 -/
@@ -547,4 +584,50 @@ noncomputable def monoidalOfChosenFiniteProducts : F.Monoidal :=
 
 end Functor
 
+namespace Functor.Monoidal
+
+variable {C : Type u} [Category.{v} C] [ChosenFiniteProducts C]
+  {D : Type u₁} [Category.{v₁} D] [ChosenFiniteProducts D] (F : C ⥤ D)
+
+section
+
+attribute [local instance] oplaxMonoidalOfChosenFiniteProducts
+
+@[reassoc (attr := simp)]
+lemma δ_fst {X Y : C} : OplaxMonoidal.δ F X Y ≫ fst _ _ = F.map (fst _ _) := by
+  simp [δ_of_chosenFiniteProducts]
+
+@[reassoc (attr := simp)]
+lemma δ_snd {X Y : C} : OplaxMonoidal.δ F X Y ≫ snd _ _ = F.map (snd _ _) := by
+  simp [δ_of_chosenFiniteProducts]
+
+@[reassoc (attr := simp)]
+lemma lift_δ {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) :
+    F.map (lift f g) ≫ OplaxMonoidal.δ F _ _ = lift (F.map f) (F.map g) := by
+  apply hom_ext <;> simp [← F.map_comp]
+
+end
+
+section
+
+open Limits
+
+variable [PreservesLimit (Functor.empty.{0} C) F]
+  [PreservesLimitsOfShape (Discrete WalkingPair) F]
+
+attribute [local instance] monoidalOfChosenFiniteProducts
+
+@[reassoc]
+lemma toUnit_ε {X : C} : toUnit (F.obj X) ≫ LaxMonoidal.ε F = F.map (toUnit X) :=
+  (cancel_mono (εIso _).inv).1 (toUnit_unique _ _)
+
+@[reassoc]
+lemma lift_μ {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) :
+    lift (F.map f) (F.map g) ≫ LaxMonoidal.μ F _ _ = F.map (lift f g) :=
+  (cancel_mono (μIso _ _ _).inv).1 (by simp)
+
+end
+
+end Functor.Monoidal
+
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean b/Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean
new file mode 100644
index 00000000000000..6237d4751385c6
--- /dev/null
+++ b/Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean
@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.ChosenFiniteProducts
+import Mathlib.CategoryTheory.Monoidal.Mon_
+
+/-!
+# Additional results about monoid objects in cartesian monoidal categories
+-/
+
+universe v₁ u₁
+
+open CategoryTheory MonoidalCategory ChosenFiniteProducts
+
+variable {C : Type u₁} [Category.{v₁} C] [ChosenFiniteProducts.{v₁} C]
+
+namespace Mon_
+
+theorem lift_lift_assoc {A : C} {B : Mon_ C} (f g h : A ⟶ B.X) :
+    lift (lift f g ≫ B.mul) h ≫ B.mul = lift f (lift g h ≫ B.mul) ≫ B.mul := by
+  have := lift (lift f g) h ≫= B.mul_assoc
+  rwa [lift_whiskerRight_assoc, lift_lift_associator_hom_assoc, lift_whiskerLeft_assoc] at this
+
+@[reassoc (attr := simp)]
+theorem lift_comp_one_left {A : C} {B : Mon_ C} (f : A ⟶ 𝟙_ C) (g : A ⟶ B.X) :
+    lift (f ≫ B.one) g ≫ B.mul = g := by
+  have := lift f g ≫= B.one_mul
+  rwa [lift_whiskerRight_assoc, lift_leftUnitor_hom] at this
+
+@[reassoc (attr := simp)]
+theorem lift_comp_one_right {A : C} {B : Mon_ C} (f : A ⟶ B.X) (g : A ⟶ 𝟙_ C) :
+    lift f (g ≫ B.one) ≫ B.mul = f := by
+  have := lift f g ≫= B.mul_one
+  rwa [lift_whiskerLeft_assoc, lift_rightUnitor_hom] at this
+
+end Mon_
diff --git a/Mathlib/CategoryTheory/Monoidal/Grp_.lean b/Mathlib/CategoryTheory/Monoidal/Grp_.lean
new file mode 100644
index 00000000000000..06d74080bbe31e
--- /dev/null
+++ b/Mathlib/CategoryTheory/Monoidal/Grp_.lean
@@ -0,0 +1,228 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_
+import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
+
+/-!
+# The category of groups in a cartesian monoidal category
+
+We define group objects in cartesian monoidal categories.
+
+We show that the associativity diagram of a group object is always cartesian and deduce that
+morphisms of group objects commute with taking inverses.
+
+We show that a finite-product-preserving functor takes group objects to group objects.
+-/
+
+universe v₁ v₂ u₁ u₂ u
+
+open CategoryTheory Category Limits MonoidalCategory ChosenFiniteProducts Mon_
+
+variable (C : Type u₁) [Category.{v₁} C] [ChosenFiniteProducts.{v₁} C]
+
+/-- A group object in a cartesian monoidal category. -/
+structure Grp_ extends Mon_ C where
+  /-- The inversion operation -/
+  inv : X ⟶ X
+  left_inv : lift inv (𝟙 X) ≫ mul = toUnit _ ≫ one := by aesop_cat
+  right_inv : lift (𝟙 X) inv ≫ mul = toUnit _ ≫ one := by aesop_cat
+
+attribute [reassoc (attr := simp)] Grp_.left_inv
+attribute [reassoc (attr := simp)] Grp_.right_inv
+
+namespace Grp_
+
+/-- The trivial group object. -/
+def trivial : Grp_ C :=
+  { Mon_.trivial C with inv := 𝟙 _ }
+
+instance : Inhabited (Grp_ C) where
+  default := trivial C
+
+variable {C}
+
+instance : Category (Grp_ C) :=
+  InducedCategory.category Grp_.toMon_
+
+@[simp]
+theorem id_hom (A : Grp_ C) : Mon_.Hom.hom (𝟙 A) = 𝟙 A.X :=
+  rfl
+
+@[simp]
+theorem comp_hom {R S T : Grp_ C} (f : R ⟶ S) (g : S ⟶ T) :
+    Mon_.Hom.hom (f ≫ g) = f.hom ≫ g.hom :=
+  rfl
+
+@[ext]
+theorem hom_ext {A B : Grp_ C} (f g : A ⟶ B) (h : f.hom = g.hom) : f = g :=
+  Mon_.Hom.ext h
+
+@[simp]
+lemma id' (A : Grp_ C) : (𝟙 A : A.toMon_ ⟶ A.toMon_) = 𝟙 (A.toMon_) := rfl
+
+@[simp]
+lemma comp' {A₁ A₂ A₃ : Grp_ C} (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) :
+    ((f ≫ g : A₁ ⟶ A₃) : A₁.toMon_ ⟶ A₃.toMon_) = @CategoryStruct.comp (Mon_ C) _ _ _ _ f g := rfl
+
+@[reassoc (attr := simp)]
+theorem lift_comp_inv_right {A : C} {B : Grp_ C} (f : A ⟶ B.X) :
+    lift f (f ≫ B.inv) ≫ B.mul = toUnit _ ≫ B.one := by
+  have := f ≫= B.right_inv
+  rwa [comp_lift_assoc, comp_id, reassoc_of% toUnit_unique (f ≫ toUnit B.X) (toUnit A)] at this
+
+@[reassoc]
+theorem lift_inv_comp_right {A B : Grp_ C} (f : A ⟶ B) :
+    lift f.hom (A.inv ≫ f.hom) ≫ B.mul = toUnit _ ≫ B.one := by
+  have := A.right_inv =≫ f.hom
+  rwa [assoc, f.mul_hom, assoc, f.one_hom, lift_map_assoc, id_comp] at this
+
+@[reassoc (attr := simp)]
+theorem lift_comp_inv_left {A : C} {B : Grp_ C} (f : A ⟶ B.X) :
+    lift (f ≫ B.inv) f ≫ B.mul = toUnit _ ≫ B.one := by
+  have := f ≫= B.left_inv
+  rwa [comp_lift_assoc, comp_id, reassoc_of% toUnit_unique (f ≫ toUnit B.X) (toUnit A)] at this
+
+@[reassoc]
+theorem lift_inv_comp_left {A B : Grp_ C} (f : A ⟶ B) :
+    lift (A.inv ≫ f.hom) f.hom ≫ B.mul = toUnit _ ≫ B.one := by
+  have := A.left_inv =≫ f.hom
+  rwa [assoc, f.mul_hom, assoc, f.one_hom, lift_map_assoc, id_comp] at this
+
+theorem eq_lift_inv_left {A : C} {B : Grp_ C} (f g h : A ⟶ B.X) :
+    f = lift (g ≫ B.inv) h ≫ B.mul ↔ lift g f ≫ B.mul = h := by
+  refine ⟨?_, ?_⟩ <;> (rintro rfl; simp [← lift_lift_assoc])
+
+theorem lift_inv_left_eq {A : C} {B : Grp_ C} (f g h : A ⟶ B.X) :
+    lift (f ≫ B.inv) g ≫ B.mul = h ↔ g = lift f h ≫ B.mul := by
+  rw [eq_comm, eq_lift_inv_left, eq_comm]
+
+theorem eq_lift_inv_right {A : C} {B : Grp_ C} (f g h : A ⟶ B.X) :
+    f = lift g (h ≫ B.inv) ≫ B.mul ↔ lift f h ≫ B.mul = g := by
+  refine ⟨?_, ?_⟩ <;> (rintro rfl; simp [lift_lift_assoc])
+
+theorem lift_inv_right_eq {A : C} {B : Grp_ C} (f g h : A ⟶ B.X) :
+    lift f (g ≫ B.inv) ≫ B.mul = h ↔ f = lift h g ≫ B.mul := by
+  rw [eq_comm, eq_lift_inv_right, eq_comm]
+
+/-- The associativity diagram of a group object is cartesian.
+
+In fact, any monoid object whose associativity diagram is cartesian can be made into a group object
+(we do not prove this in this file), so we should expect that many properties of group objects
+follow from this result. -/
+theorem isPullback (A : Grp_ C) :
+    IsPullback (A.mul ▷ A.X) ((α_ A.X A.X A.X).hom ≫ (A.X ◁ A.mul)) A.mul A.mul where
+  w := by simp
+  isLimit' := Nonempty.intro <| PullbackCone.IsLimit.mk _
+    (fun s => lift
+      (lift
+        (s.snd ≫ fst _ _)
+        (lift (s.snd ≫ fst _ _ ≫ A.inv) (s.fst ≫ fst _ _) ≫ A.mul))
+      (s.fst ≫ snd _ _))
+    (by
+      refine fun s => ChosenFiniteProducts.hom_ext _ _ ?_ (by simp)
+      simp only [lift_whiskerRight, lift_fst]
+      rw [← lift_lift_assoc, ← assoc, lift_comp_inv_right, lift_comp_one_left])
+    (by
+      refine fun s => ChosenFiniteProducts.hom_ext _ _ (by simp) ?_
+      simp only [lift_lift_associator_hom_assoc, lift_whiskerLeft, lift_snd]
+      have : lift (s.snd ≫ fst _ _ ≫ A.inv) (s.fst ≫ fst _ _) ≫ A.mul =
+          lift (s.snd ≫ snd _ _) (s.fst ≫ snd _ _ ≫ A.inv) ≫ A.mul := by
+        rw [← assoc s.fst, eq_lift_inv_right, lift_lift_assoc, ← assoc s.snd, lift_inv_left_eq,
+          lift_comp_fst_snd, lift_comp_fst_snd, s.condition]
+      rw [this, lift_lift_assoc, ← assoc, lift_comp_inv_left, lift_comp_one_right])
+    (by
+      intro s m hm₁ hm₂
+      refine ChosenFiniteProducts.hom_ext _ _ (ChosenFiniteProducts.hom_ext _ _ ?_ ?_) ?_
+      · simpa using hm₂ =≫ fst _ _
+      · have h : m ≫ fst _ _ ≫ fst _ _ = s.snd ≫ fst _ _ := by simpa using hm₂ =≫ fst _ _
+        have := hm₁ =≫ fst _ _
+        simp only [assoc, whiskerRight_fst, lift_fst, lift_snd] at this ⊢
+        rw [← assoc, ← lift_comp_fst_snd (m ≫ _), assoc, assoc, h] at this
+        rwa [← assoc s.snd, eq_lift_inv_left]
+      · simpa using hm₁ =≫ snd _ _)
+
+/-- Morphisms of group objects preserve inverses. -/
+@[reassoc (attr := simp)]
+theorem inv_hom {A B : Grp_ C} (f : A ⟶ B) : A.inv ≫ f.hom = f.hom ≫ B.inv := by
+  suffices lift (lift f.hom (A.inv ≫ f.hom)) f.hom =
+      lift (lift f.hom (f.hom ≫ B.inv)) f.hom by simpa using (this =≫ fst _ _) =≫ snd _ _
+  apply B.isPullback.hom_ext <;> apply ChosenFiniteProducts.hom_ext <;>
+    simp [lift_inv_comp_right, lift_inv_comp_left]
+
+section
+
+variable (C)
+
+/-- The forgetful functor from group objects to monoid objects. -/
+def forget₂Mon_ : Grp_ C ⥤ Mon_ C :=
+  inducedFunctor Grp_.toMon_
+
+/-- The forgetful functor from group objects to monoid objects is fully faithful. -/
+def fullyFaithfulForget₂Mon_ : (forget₂Mon_ C).FullyFaithful :=
+  fullyFaithfulInducedFunctor _
+
+instance : (forget₂Mon_ C).Full := InducedCategory.full _
+instance : (forget₂Mon_ C).Faithful := InducedCategory.faithful _
+
+@[simp]
+theorem forget₂Mon_obj_one (A : Grp_ C) : ((forget₂Mon_ C).obj A).one = A.one :=
+  rfl
+
+@[simp]
+theorem forget₂Mon_obj_mul (A : Grp_ C) : ((forget₂Mon_ C).obj A).mul = A.mul :=
+  rfl
+
+@[simp]
+theorem forget₂Mon_map_hom {A B : Grp_ C} (f : A ⟶ B) : ((forget₂Mon_ C).map f).hom = f.hom :=
+  rfl
+
+end
+
+section
+
+variable {M N : Grp_ C} (f : M.X ≅ N.X) (one_f : M.one ≫ f.hom = N.one := by aesop_cat)
+  (mul_f : M.mul ≫ f.hom = (f.hom ⊗ f.hom) ≫ N.mul := by aesop_cat)
+
+/-- Constructor for isomorphisms in the category `Grp_ C`. -/
+def mkIso : M ≅ N :=
+  (fullyFaithfulForget₂Mon_ C).preimageIso (Mon_.mkIso f one_f mul_f)
+
+@[simp] lemma mkIso_hom_hom : (mkIso f one_f mul_f).hom.hom = f.hom := rfl
+@[simp] lemma mkIso_inv_hom : (mkIso f one_f mul_f).inv.hom = f.inv := rfl
+
+end
+
+instance uniqueHomFromTrivial (A : Grp_ C) : Unique (trivial C ⟶ A) :=
+  Mon_.uniqueHomFromTrivial A.toMon_
+
+instance : HasInitial (Grp_ C) :=
+  hasInitial_of_unique (trivial C)
+
+end Grp_
+
+namespace CategoryTheory.Functor
+
+variable {D : Type u₂} [Category.{v₂} D] [ChosenFiniteProducts.{v₂} D] (F : C ⥤ D)
+variable [PreservesLimit (Functor.empty.{0} C) F]
+  [PreservesLimitsOfShape (Discrete WalkingPair) F]
+
+attribute [local instance] monoidalOfChosenFiniteProducts
+
+/-- A finite-product-preserving functor takes group objects to group objects. -/
+@[simps!]
+noncomputable def mapGrp : Grp_ C ⥤ Grp_ D where
+  obj A :=
+    { F.mapMon.obj A.toMon_ with
+      inv := F.map A.inv
+      left_inv := by
+        simp [← Functor.map_id, Functor.Monoidal.lift_μ_assoc,
+          Functor.Monoidal.toUnit_ε_assoc, ← Functor.map_comp]
+      right_inv := by
+        simp [← Functor.map_id, Functor.Monoidal.lift_μ_assoc,
+          Functor.Monoidal.toUnit_ε_assoc, ← Functor.map_comp] }
+  map f := F.mapMon.map f
+
+end CategoryTheory.Functor

From 6ad4df4dfadd99dd71ee5bae1abc59653959967f Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sun, 2 Feb 2025 16:41:52 +0100
Subject: [PATCH 05/57] Revert "nothing"

This reverts commit 2d7126dc6bde5512401bd31a8fff523f4c0eff6e.
---
 Mathlib/CategoryTheory/Monoidal/CommGrp_.lean | 19 -------------------
 1 file changed, 19 deletions(-)
 delete mode 100644 Mathlib/CategoryTheory/Monoidal/CommGrp_.lean

diff --git a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
deleted file mode 100644
index b45cc6fc755bc0..00000000000000
--- a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2025 Markus Himmel. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-import Mathlib.CategoryTheory.Monoidal.CommMon_
-
-/-!
-# The category of commutative groups in a braided monoidal category
--/
-
-universe v₁ v₂ u₁ u₂ u
-
-open CategoryTheory MonoidalCategory
-
-variable (C : Type u₁) [Category.{v₁} C] [MonoidalCategory.{v₁} C] [BraidedCategory.{v₁} C]
-
-structure CommGrp_ extends CommMon_ C where
-  

From a79005572fd4f4362079ccb39229205d338e471e Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sun, 2 Feb 2025 16:42:08 +0100
Subject: [PATCH 06/57] Mathlib.lean

---
 Mathlib.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 93ac5b72463903..1a5de436e40955 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2087,7 +2087,6 @@ import Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_
 import Mathlib.CategoryTheory.Monoidal.Category
 import Mathlib.CategoryTheory.Monoidal.Center
 import Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
-import Mathlib.CategoryTheory.Monoidal.CommGrp_
 import Mathlib.CategoryTheory.Monoidal.CommMon_
 import Mathlib.CategoryTheory.Monoidal.Comon_
 import Mathlib.CategoryTheory.Monoidal.Conv

From f36a814ab89b9d1a43e70f7cd649938fbf234f70 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Mon, 3 Feb 2025 16:52:58 +0100
Subject: [PATCH 07/57] Switch to PreservesFiniteProducts

---
 Mathlib/CategoryTheory/ChosenFiniteProducts.lean | 10 ++++------
 Mathlib/CategoryTheory/Monoidal/Grp_.lean        |  3 +--
 2 files changed, 5 insertions(+), 8 deletions(-)

diff --git a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
index f186a198c15495..0dffc1370bf50a 100644
--- a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
+++ b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@@ -3,9 +3,9 @@ Copyright (c) 2024 Adam Topaz. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adam Topaz, Robin Carlier
 -/
-import Mathlib.CategoryTheory.Monoidal.OfChosenFiniteProducts.Symmetric
 import Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
-import Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
+import Mathlib.CategoryTheory.Limits.Preserves.Finite
+import Mathlib.CategoryTheory.Monoidal.OfChosenFiniteProducts.Symmetric
 
 /-!
 # Categories with chosen finite products
@@ -568,8 +568,7 @@ lemma δ_of_chosenFiniteProducts (X Y : C) : δ F X Y = prodComparison F X Y :=
 
 open Limits
 
-variable [PreservesLimit (Functor.empty.{0} C) F]
-  [PreservesLimitsOfShape (Discrete WalkingPair) F]
+variable [PreservesFiniteProducts F]
 
 instance : IsIso (η F) :=
   terminalComparison_isIso_of_preservesLimits F
@@ -612,8 +611,7 @@ section
 
 open Limits
 
-variable [PreservesLimit (Functor.empty.{0} C) F]
-  [PreservesLimitsOfShape (Discrete WalkingPair) F]
+variable [PreservesFiniteProducts F]
 
 attribute [local instance] monoidalOfChosenFiniteProducts
 
diff --git a/Mathlib/CategoryTheory/Monoidal/Grp_.lean b/Mathlib/CategoryTheory/Monoidal/Grp_.lean
index 06d74080bbe31e..ac1102b078534d 100644
--- a/Mathlib/CategoryTheory/Monoidal/Grp_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Grp_.lean
@@ -206,8 +206,7 @@ end Grp_
 namespace CategoryTheory.Functor
 
 variable {D : Type u₂} [Category.{v₂} D] [ChosenFiniteProducts.{v₂} D] (F : C ⥤ D)
-variable [PreservesLimit (Functor.empty.{0} C) F]
-  [PreservesLimitsOfShape (Discrete WalkingPair) F]
+variable [PreservesFiniteProducts F]
 
 attribute [local instance] monoidalOfChosenFiniteProducts
 

From d121ea81db2eb0a80afb1a3c993fb6224446b123 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Wed, 5 Feb 2025 18:36:52 +0100
Subject: [PATCH 08/57] Additional group stuff

---
 .../CategoryTheory/ChosenFiniteProducts.lean  | 20 +++++++++++++++++++
 Mathlib/CategoryTheory/Monoidal/Grp_.lean     |  9 +++++++++
 2 files changed, 29 insertions(+)

diff --git a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
index 0dffc1370bf50a..e4cfd50124f636 100644
--- a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
+++ b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@@ -626,6 +626,26 @@ lemma lift_μ {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) :
 
 end
 
+
 end Functor.Monoidal
 
+-- open CategoryTheory.Functor
+
+namespace NatTrans
+
+variable {C : Type u} [Category.{v} C] [ChosenFiniteProducts C]
+  {D : Type u₁} [Category.{v₁} D] [ChosenFiniteProducts D] (F G : C ⥤ D)
+  [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteLimits G]
+
+attribute [local instance] Functor.monoidalOfChosenFiniteProducts in
+theorem monoidal_of_preservesFiniteLimits (α : F ⟶ G) :
+    NatTrans.IsMonoidal α where
+  unit := (cancel_mono (Functor.Monoidal.εIso _).inv).1 (toUnit_unique _ _)
+  tensor {X Y} := by
+    rw [← cancel_mono (Functor.Monoidal.μIso _ _ _).inv]
+    rw [← cancel_epi (Functor.Monoidal.μIso _ _ _).inv]
+    apply ChosenFiniteProducts.hom_ext <;> simp
+
+end NatTrans
+
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Monoidal/Grp_.lean b/Mathlib/CategoryTheory/Monoidal/Grp_.lean
index ac1102b078534d..eaacebb77c124f 100644
--- a/Mathlib/CategoryTheory/Monoidal/Grp_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Grp_.lean
@@ -5,6 +5,7 @@ Authors: Markus Himmel
 -/
 import Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_
 import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
+import Mathlib.CategoryTheory.Limits.ExactFunctor
 
 /-!
 # The category of groups in a cartesian monoidal category
@@ -36,6 +37,7 @@ attribute [reassoc (attr := simp)] Grp_.right_inv
 namespace Grp_
 
 /-- The trivial group object. -/
+@[simps!]
 def trivial : Grp_ C :=
   { Mon_.trivial C with inv := 𝟙 _ }
 
@@ -224,4 +226,11 @@ noncomputable def mapGrp : Grp_ C ⥤ Grp_ D where
           Functor.Monoidal.toUnit_ε_assoc, ← Functor.map_comp] }
   map f := F.mapMon.map f
 
+attribute [local instance] NatTrans.monoidal_of_preservesFiniteLimits in
+/-- `mapGrp` is functorial in the left-exact functor. -/
+@[simps]
+noncomputable def mapGrpFunctor : (C ⥤ₗ D) ⥤ Grp_ C ⥤ Grp_ D where
+  obj F := F.1.mapGrp
+  map {F G} α := { app := fun A => { hom := α.app A.X } }
+
 end CategoryTheory.Functor

From 4ddcb9df52d60c0d0ab51cd98c530b9c73cbe50e Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Wed, 5 Feb 2025 18:37:16 +0100
Subject: [PATCH 09/57] CommGrp

---
 Mathlib.lean                                  |   1 +
 Mathlib/CategoryTheory/Monoidal/CommGrp_.lean | 133 ++++++++++++++++++
 2 files changed, 134 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/Monoidal/CommGrp_.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 1a5de436e40955..93ac5b72463903 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2087,6 +2087,7 @@ import Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_
 import Mathlib.CategoryTheory.Monoidal.Category
 import Mathlib.CategoryTheory.Monoidal.Center
 import Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
+import Mathlib.CategoryTheory.Monoidal.CommGrp_
 import Mathlib.CategoryTheory.Monoidal.CommMon_
 import Mathlib.CategoryTheory.Monoidal.Comon_
 import Mathlib.CategoryTheory.Monoidal.Conv
diff --git a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
new file mode 100644
index 00000000000000..763fe3abd24809
--- /dev/null
+++ b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.Monoidal.Grp_
+import Mathlib.CategoryTheory.Monoidal.CommMon_
+
+/-!
+# The category of commutative groups in a cartesian monoidal category
+-/
+
+universe v₁ v₂ u₁ u₂ u
+
+open CategoryTheory Category Limits MonoidalCategory ChosenFiniteProducts Mon_ Grp_ CommMon_
+
+variable (C : Type u₁) [Category.{v₁} C] [ChosenFiniteProducts.{v₁} C]
+
+/-- A commutative group object internal to a cartesian monoidal category. -/
+structure CommGrp_ extends Grp_ C, CommMon_ C where
+
+attribute [reassoc (attr := simp)] CommGrp_.mul_comm
+
+namespace CommGrp_
+
+/-- The trivial commutative group object. -/
+@[simps!]
+def trivial : CommGrp_ C :=
+  { Grp_.trivial C with mul_comm := by simpa using unitors_equal.symm }
+
+instance : Inhabited (CommGrp_ C) where
+  default := trivial C
+
+variable {C}
+
+instance : Category (CommGrp_ C) :=
+  InducedCategory.category CommGrp_.toGrp_
+
+@[simp]
+theorem id_hom (A : Grp_ C) : Mon_.Hom.hom (𝟙 A) = 𝟙 A.X :=
+  rfl
+
+@[simp]
+theorem comp_hom {R S T : CommGrp_ C} (f : R ⟶ S) (g : S ⟶ T) :
+    Mon_.Hom.hom (f ≫ g) = f.hom ≫ g.hom :=
+  rfl
+
+@[ext]
+theorem hom_ext {A B : CommGrp_ C} (f g : A ⟶ B) (h : f.hom = g.hom) : f = g :=
+  Mon_.Hom.ext h
+
+@[simp]
+lemma id' (A : CommGrp_ C) : (𝟙 A : A.toMon_ ⟶ A.toMon_) = 𝟙 (A.toMon_) := rfl
+
+@[simp]
+lemma comp' {A₁ A₂ A₃ : CommGrp_ C} (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) :
+    ((f ≫ g : A₁ ⟶ A₃) : A₁.toMon_ ⟶ A₃.toMon_) = @CategoryStruct.comp (Mon_ C) _ _ _ _ f g := rfl
+
+section
+
+variable (C)
+
+/-- The forgetful functor from commutative group objects to group objects. -/
+def forget₂Grp_ : CommGrp_ C ⥤ Grp_ C :=
+  inducedFunctor CommGrp_.toGrp_
+
+/-- The forgetful functor from commutative group objects to group objects is fully faithful. -/
+def fullyFaithfulForget₂Grp_ : (forget₂Grp_ C).FullyFaithful :=
+    fullyFaithfulInducedFunctor _
+
+instance : (forget₂Grp_ C).Full := InducedCategory.full _
+instance : (forget₂Grp_ C).Faithful := InducedCategory.faithful _
+
+@[simp]
+theorem forget₂Grp_obj_one (A : CommGrp_ C) : ((forget₂Grp_ C).obj A).one = A.one :=
+  rfl
+
+@[simp]
+theorem forget₂Grp_obj_mul (A : CommGrp_ C) : ((forget₂Grp_ C).obj A).mul = A.mul :=
+  rfl
+
+@[simp]
+theorem forget₂Grp_map_hom {A B : CommGrp_ C} (f : A ⟶ B) : ((forget₂Grp_ C).map f).hom = f.hom :=
+  rfl
+
+/-- The forgetful functor from commutative group objects to commutative monoid objects. -/
+def forget₂CommMon_ : CommGrp_ C ⥤ CommMon_ C :=
+  inducedFunctor CommGrp_.toCommMon_
+
+/-- The forgetful functor from commutative group objects to commutative monoid objects is fully
+faithful. -/
+def fullyFaithfulForget₂CommMon_ : (forget₂CommMon_ C).FullyFaithful :=
+    fullyFaithfulInducedFunctor _
+
+instance : (forget₂CommMon_ C).Full := InducedCategory.full _
+instance : (forget₂CommMon_ C).Faithful := InducedCategory.faithful _
+
+@[simp]
+theorem forget₂CommMon_obj_one (A : CommGrp_ C) : ((forget₂CommMon_ C).obj A).one = A.one :=
+  rfl
+
+@[simp]
+theorem forget₂CommMon_obj_mul (A : CommGrp_ C) : ((forget₂CommMon_ C).obj A).mul = A.mul :=
+  rfl
+
+@[simp]
+theorem forget₂CommMon_map_hom {A B : CommGrp_ C} (f : A ⟶ B) :
+    ((forget₂CommMon_ C).map f).hom = f.hom :=
+  rfl
+
+end
+
+section
+
+variable {M N : CommGrp_ C} (f : M.X ≅ N.X) (one_f : M.one ≫ f.hom = N.one := by aesop_cat)
+  (mul_f : M.mul ≫ f.hom = (f.hom ⊗ f.hom) ≫ N.mul := by aesop_cat)
+
+/-- Constructor for isomorphisms in the category `Grp_ C`. -/
+def mkIso : M ≅ N :=
+  (fullyFaithfulForget₂Grp_ C).preimageIso (Grp_.mkIso f one_f mul_f)
+
+@[simp] lemma mkIso_hom_hom : (mkIso f one_f mul_f).hom.hom = f.hom := rfl
+@[simp] lemma mkIso_inv_hom : (mkIso f one_f mul_f).inv.hom = f.inv := rfl
+
+end
+
+instance uniqueHomFromTrivial (A : CommGrp_ C) : Unique (trivial C ⟶ A) :=
+  Mon_.uniqueHomFromTrivial A.toMon_
+
+instance : HasInitial (CommGrp_ C) :=
+  hasInitial_of_unique (trivial C)
+
+end CommGrp_

From ef5a5d6be6f0d2e30c2d4dbfb16712ebbb9786c5 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Wed, 5 Feb 2025 18:36:52 +0100
Subject: [PATCH 10/57] Additional group stuff

---
 .../CategoryTheory/ChosenFiniteProducts.lean  | 20 +++++++++++++++++++
 Mathlib/CategoryTheory/Monoidal/Grp_.lean     |  9 +++++++++
 2 files changed, 29 insertions(+)

diff --git a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
index 0dffc1370bf50a..e4cfd50124f636 100644
--- a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
+++ b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@@ -626,6 +626,26 @@ lemma lift_μ {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) :
 
 end
 
+
 end Functor.Monoidal
 
+-- open CategoryTheory.Functor
+
+namespace NatTrans
+
+variable {C : Type u} [Category.{v} C] [ChosenFiniteProducts C]
+  {D : Type u₁} [Category.{v₁} D] [ChosenFiniteProducts D] (F G : C ⥤ D)
+  [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteLimits G]
+
+attribute [local instance] Functor.monoidalOfChosenFiniteProducts in
+theorem monoidal_of_preservesFiniteLimits (α : F ⟶ G) :
+    NatTrans.IsMonoidal α where
+  unit := (cancel_mono (Functor.Monoidal.εIso _).inv).1 (toUnit_unique _ _)
+  tensor {X Y} := by
+    rw [← cancel_mono (Functor.Monoidal.μIso _ _ _).inv]
+    rw [← cancel_epi (Functor.Monoidal.μIso _ _ _).inv]
+    apply ChosenFiniteProducts.hom_ext <;> simp
+
+end NatTrans
+
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Monoidal/Grp_.lean b/Mathlib/CategoryTheory/Monoidal/Grp_.lean
index ac1102b078534d..eaacebb77c124f 100644
--- a/Mathlib/CategoryTheory/Monoidal/Grp_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Grp_.lean
@@ -5,6 +5,7 @@ Authors: Markus Himmel
 -/
 import Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_
 import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
+import Mathlib.CategoryTheory.Limits.ExactFunctor
 
 /-!
 # The category of groups in a cartesian monoidal category
@@ -36,6 +37,7 @@ attribute [reassoc (attr := simp)] Grp_.right_inv
 namespace Grp_
 
 /-- The trivial group object. -/
+@[simps!]
 def trivial : Grp_ C :=
   { Mon_.trivial C with inv := 𝟙 _ }
 
@@ -224,4 +226,11 @@ noncomputable def mapGrp : Grp_ C ⥤ Grp_ D where
           Functor.Monoidal.toUnit_ε_assoc, ← Functor.map_comp] }
   map f := F.mapMon.map f
 
+attribute [local instance] NatTrans.monoidal_of_preservesFiniteLimits in
+/-- `mapGrp` is functorial in the left-exact functor. -/
+@[simps]
+noncomputable def mapGrpFunctor : (C ⥤ₗ D) ⥤ Grp_ C ⥤ Grp_ D where
+  obj F := F.1.mapGrp
+  map {F G} α := { app := fun A => { hom := α.app A.X } }
+
 end CategoryTheory.Functor

From f8fe6886c3494cf4417fe01ca50c665df606efdd Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Wed, 5 Feb 2025 18:38:16 +0100
Subject: [PATCH 11/57] Cleanup

---
 Mathlib/CategoryTheory/ChosenFiniteProducts.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
index e4cfd50124f636..278c03a91f05cb 100644
--- a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
+++ b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@@ -629,8 +629,6 @@ end
 
 end Functor.Monoidal
 
--- open CategoryTheory.Functor
-
 namespace NatTrans
 
 variable {C : Type u} [Category.{v} C] [ChosenFiniteProducts C]

From eab57ef2cc7e52458ae774c8212c41459883a98b Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Wed, 5 Feb 2025 18:57:50 +0100
Subject: [PATCH 12/57] WIP

---
 .../CategoryTheory/ChosenFiniteProducts.lean  | 15 ++++++++++
 Mathlib/CategoryTheory/Monoidal/CommGrp_.lean | 29 +++++++++++++++++++
 Mathlib/CategoryTheory/Monoidal/Grp_.lean     |  2 +-
 3 files changed, 45 insertions(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
index e4cfd50124f636..2867d228e514d4 100644
--- a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
+++ b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@@ -249,6 +249,9 @@ lemma lift_rightUnitor_hom {X Y : C} (f : X ⟶ Y) (g : X ⟶ 𝟙_ C) :
   rw [← Iso.eq_comp_inv]
   aesop_cat
 
+theorem braiding_fst {X Y : C} : (β_ X Y).hom ≫ fst _ _ = snd _ _ := by
+  simp [BraidedCategory.braiding, fst]
+
 /--
 Construct an instance of `ChosenFiniteProducts C` given an instance of `HasFiniteProducts C`.
 -/
@@ -581,6 +584,18 @@ that preserves finite products, then it is a monoidal functor. -/
 noncomputable def monoidalOfChosenFiniteProducts : F.Monoidal :=
   Functor.Monoidal.ofOplaxMonoidal F
 
+noncomputable def braidedOfChosenFiniteProducts : F.Braided :=
+  { monoidalOfChosenFiniteProducts F with
+    braided X Y := by
+      let _ := monoidalOfChosenFiniteProducts F
+      rw [← cancel_mono (Monoidal.μIso _ _ _).inv]
+      simp
+      apply ChosenFiniteProducts.hom_ext
+      simp
+
+
+     }
+
 end Functor
 
 namespace Functor.Monoidal
diff --git a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
index 763fe3abd24809..8f50268f504095 100644
--- a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
@@ -131,3 +131,32 @@ instance : HasInitial (CommGrp_ C) :=
   hasInitial_of_unique (trivial C)
 
 end CommGrp_
+
+namespace CategoryTheory.Functor
+
+variable {D : Type u₂} [Category.{v₂} D] [ChosenFiniteProducts.{v₂} D] (F : C ⥤ D)
+variable [PreservesFiniteProducts F]
+
+attribute [local instance] monoidalOfChosenFiniteProducts
+
+/-- A finite-product-preserving functor takes commutative group objects to commutative group objects. -/
+@[simps!]
+noncomputable def mapCommGrp : CommGrp_ C ⥤ CommGrp_ D where
+  obj A :=
+    { F.mapGrp.obj A.toGrp_ with
+      mul_comm := by
+        dsimp
+        rw [← Functor.LaxBraided.braided_assoc (F := F) A.X A.X, ← Functor.map_comp]
+          }
+  map f := F.mapMon.map f
+  map_id := sorry
+  map_comp := sorry
+
+attribute [local instance] NatTrans.monoidal_of_preservesFiniteLimits in
+/-- `mapGrp` is functorial in the left-exact functor. -/
+@[simps]
+noncomputable def mapCommGrpFunctor : (C ⥤ₗ D) ⥤ Grp_ C ⥤ Grp_ D where
+  obj F := F.1.mapGrp
+  map {F G} α := { app := fun A => { hom := α.app A.X } }
+
+end CategoryTheory.Functor
diff --git a/Mathlib/CategoryTheory/Monoidal/Grp_.lean b/Mathlib/CategoryTheory/Monoidal/Grp_.lean
index eaacebb77c124f..1264f544af2c98 100644
--- a/Mathlib/CategoryTheory/Monoidal/Grp_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Grp_.lean
@@ -207,7 +207,7 @@ end Grp_
 
 namespace CategoryTheory.Functor
 
-variable {D : Type u₂} [Category.{v₂} D] [ChosenFiniteProducts.{v₂} D] (F : C ⥤ D)
+variable {C} {D : Type u₂} [Category.{v₂} D] [ChosenFiniteProducts.{v₂} D] (F : C ⥤ D)
 variable [PreservesFiniteProducts F]
 
 attribute [local instance] monoidalOfChosenFiniteProducts

From 56828363466c2dc37a9396c6fe3d432693652f36 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Thu, 6 Feb 2025 16:09:05 +0100
Subject: [PATCH 13/57] Okay

---
 .../CategoryTheory/ChosenFiniteProducts.lean  | 51 +++++++++++++------
 Mathlib/CategoryTheory/Monoidal/CommGrp_.lean | 14 +++--
 .../OfChosenFiniteProducts/Basic.lean         | 22 ++++++++
 3 files changed, 63 insertions(+), 24 deletions(-)

diff --git a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
index 2867d228e514d4..4c18a4c3ef8e0b 100644
--- a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
+++ b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@@ -58,6 +58,9 @@ variable {C : Type u} [Category.{v} C] [ChosenFiniteProducts C]
 
 open MonoidalCategory
 
+theorem braiding_eq_braiding (X Y : C) :
+  (β_ X Y) = Limits.BinaryFan.braiding (product X Y).isLimit (product Y X).isLimit := rfl
+
 /--
 The unique map to the terminal object.
 -/
@@ -249,8 +252,13 @@ lemma lift_rightUnitor_hom {X Y : C} (f : X ⟶ Y) (g : X ⟶ 𝟙_ C) :
   rw [← Iso.eq_comp_inv]
   aesop_cat
 
-theorem braiding_fst {X Y : C} : (β_ X Y).hom ≫ fst _ _ = snd _ _ := by
-  simp [BraidedCategory.braiding, fst]
+@[reassoc (attr := simp)]
+theorem braiding_hom_fst {X Y : C} : (β_ X Y).hom ≫ fst _ _ = snd _ _ := by
+  simp [braiding_eq_braiding, fst, snd]
+
+@[reassoc (attr := simp)]
+theorem braiding_hom_snd {X Y : C} : (β_ X Y).hom ≫ snd _ _ = fst _ _ := by
+  simp [braiding_eq_braiding, fst, snd]
 
 /--
 Construct an instance of `ChosenFiniteProducts C` given an instance of `HasFiniteProducts C`.
@@ -584,18 +592,6 @@ that preserves finite products, then it is a monoidal functor. -/
 noncomputable def monoidalOfChosenFiniteProducts : F.Monoidal :=
   Functor.Monoidal.ofOplaxMonoidal F
 
-noncomputable def braidedOfChosenFiniteProducts : F.Braided :=
-  { monoidalOfChosenFiniteProducts F with
-    braided X Y := by
-      let _ := monoidalOfChosenFiniteProducts F
-      rw [← cancel_mono (Monoidal.μIso _ _ _).inv]
-      simp
-      apply ChosenFiniteProducts.hom_ext
-      simp
-
-
-     }
-
 end Functor
 
 namespace Functor.Monoidal
@@ -639,12 +635,35 @@ lemma lift_μ {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) :
     lift (F.map f) (F.map g) ≫ LaxMonoidal.μ F _ _ = F.map (lift f g) :=
   (cancel_mono (μIso _ _ _).inv).1 (by simp)
 
-end
+@[reassoc (attr := simp)]
+lemma μ_fst {X Y : C} : LaxMonoidal.μ F X Y ≫ F.map (fst X Y) = fst (F.obj X) (F.obj Y) :=
+  (cancel_epi (μIso _ _ _).inv).1 (by simp)
+
+@[reassoc (attr := simp)]
+lemma μ_snd {X Y : C} : LaxMonoidal.μ F X Y ≫ F.map (snd X Y) = snd (F.obj X) (F.obj Y) :=
+  (cancel_epi (μIso _ _ _).inv).1 (by simp)
 
 
+end
+
 end Functor.Monoidal
 
--- open CategoryTheory.Functor
+namespace Functor
+
+variable {C : Type u} [Category.{v} C] [ChosenFiniteProducts C]
+  {D : Type u₁} [Category.{v₁} D] [ChosenFiniteProducts D] (F : C ⥤ D)
+
+attribute [local instance] monoidalOfChosenFiniteProducts
+
+/-- A finite-product-preserving functor between categories with chosen finite products is
+braided. -/
+noncomputable def braidedOfChosenFiniteProducts [Limits.PreservesFiniteProducts F] : F.Braided :=
+  { monoidalOfChosenFiniteProducts F with
+    braided X Y := by
+      rw [← cancel_mono (Monoidal.μIso _ _ _).inv]
+      apply ChosenFiniteProducts.hom_ext <;> simp [← Functor.map_comp] }
+
+end Functor
 
 namespace NatTrans
 
diff --git a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
index 8f50268f504095..45154cb5435ba9 100644
--- a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
@@ -137,26 +137,24 @@ namespace CategoryTheory.Functor
 variable {D : Type u₂} [Category.{v₂} D] [ChosenFiniteProducts.{v₂} D] (F : C ⥤ D)
 variable [PreservesFiniteProducts F]
 
-attribute [local instance] monoidalOfChosenFiniteProducts
+attribute [local instance] braidedOfChosenFiniteProducts
 
-/-- A finite-product-preserving functor takes commutative group objects to commutative group objects. -/
+/-- A finite-product-preserving functor takes commutative group objects to commutative group
+    objects. -/
 @[simps!]
 noncomputable def mapCommGrp : CommGrp_ C ⥤ CommGrp_ D where
   obj A :=
     { F.mapGrp.obj A.toGrp_ with
       mul_comm := by
         dsimp
-        rw [← Functor.LaxBraided.braided_assoc (F := F) A.X A.X, ← Functor.map_comp]
-          }
+        rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, A.mul_comm] }
   map f := F.mapMon.map f
-  map_id := sorry
-  map_comp := sorry
 
 attribute [local instance] NatTrans.monoidal_of_preservesFiniteLimits in
 /-- `mapGrp` is functorial in the left-exact functor. -/
 @[simps]
-noncomputable def mapCommGrpFunctor : (C ⥤ₗ D) ⥤ Grp_ C ⥤ Grp_ D where
-  obj F := F.1.mapGrp
+noncomputable def mapCommGrpFunctor : (C ⥤ₗ D) ⥤ CommGrp_ C ⥤ CommGrp_ D where
+  obj F := F.1.mapCommGrp
   map {F G} α := { app := fun A => { hom := α.app A.X } }
 
 end CategoryTheory.Functor
diff --git a/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean b/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean
index 045a1d884c4b36..d4cbae1f3c6ed0 100644
--- a/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean
+++ b/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean
@@ -78,6 +78,28 @@ def BinaryFan.braiding {X Y : C} {s : BinaryFan X Y} (P : IsLimit s) {t : Binary
     (Q : IsLimit t) : s.pt ≅ t.pt :=
   IsLimit.conePointUniqueUpToIso P Q.swapBinaryFan
 
+section
+
+variable {X Y : C} {s : BinaryFan X Y} (P : IsLimit s) {t : BinaryFan Y X} (Q : IsLimit t)
+
+@[reassoc (attr := simp)]
+theorem BinaryFan.braiding_hom_fst : (braiding P Q).hom ≫ t.fst = s.snd :=
+  IsLimit.conePointUniqueUpToIso_hom_comp P _ ⟨WalkingPair.right⟩
+
+@[reassoc (attr := simp)]
+theorem BinaryFan.braiding_hom_snd : (braiding P Q).hom ≫ t.snd = s.fst :=
+  IsLimit.conePointUniqueUpToIso_hom_comp P _ ⟨WalkingPair.left⟩
+
+@[reassoc (attr := simp)]
+theorem BinaryFan.braiding_inv_fst : (braiding P Q).inv ≫ s.fst = t.snd :=
+  IsLimit.conePointUniqueUpToIso_inv_comp P _ ⟨WalkingPair.left⟩
+
+@[reassoc (attr := simp)]
+theorem BinaryFan.braiding_inv_snd : (braiding P Q).inv ≫ s.snd = t.fst :=
+  IsLimit.conePointUniqueUpToIso_inv_comp P _ ⟨WalkingPair.right⟩
+
+end
+
 /-- Given binary fans `sXY` over `X Y`, and `sYZ` over `Y Z`, and `s` over `sXY.X Z`,
 if `sYZ` is a limit cone we can construct a binary fan over `X sYZ.X`.
 

From c1b92deeb2b38571199a03c9cb9817faec4a38cb Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Thu, 6 Feb 2025 19:03:30 +0100
Subject: [PATCH 14/57] WIP

---
 Mathlib.lean                                  |  1 +
 .../CategoryTheory/Preadditive/CommGrp_.lean  | 51 +++++++++++++++++++
 2 files changed, 52 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/Preadditive/CommGrp_.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 93ac5b72463903..8d7ecdca0483e6 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2148,6 +2148,7 @@ import Mathlib.CategoryTheory.Pi.Basic
 import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
 import Mathlib.CategoryTheory.Preadditive.Basic
 import Mathlib.CategoryTheory.Preadditive.Biproducts
+import Mathlib.CategoryTheory.Preadditive.CommGrp_
 import Mathlib.CategoryTheory.Preadditive.EilenbergMoore
 import Mathlib.CategoryTheory.Preadditive.EndoFunctor
 import Mathlib.CategoryTheory.Preadditive.FunctorCategory
diff --git a/Mathlib/CategoryTheory/Preadditive/CommGrp_.lean b/Mathlib/CategoryTheory/Preadditive/CommGrp_.lean
new file mode 100644
index 00000000000000..0a4ca8ccc34f7b
--- /dev/null
+++ b/Mathlib/CategoryTheory/Preadditive/CommGrp_.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.Monoidal.CommGrp_
+import Mathlib.CategoryTheory.Preadditive.Biproducts
+
+/-!
+#
+-/
+
+universe v u
+
+namespace CategoryTheory.Preadditive
+
+open CategoryTheory MonoidalCategory ChosenFiniteProducts
+
+variable {C : Type u} [Category.{v} C] [Preadditive C] [ChosenFiniteProducts C]
+
+variable (C) in
+/-- The canonical functor from an additive category into its commutative group objects. -/
+@[simps]
+def toCommGrp_ : C ⥤ CommGrp_ C where
+  obj X :=
+    { X := X
+      one := 0
+      mul := fst _ _ + snd _ _
+      inv := -𝟙 X
+      mul_assoc := by simp [add_assoc]
+      mul_comm := by simp [add_comm] }
+  map {X Y} f := { hom := f }
+
+def oneDirection :
+    toCommGrp_ C ⋙ CommGrp_.forget₂Grp_ _ ⋙ Grp_.forget₂Mon_ _ ⋙ Mon_.forget _ ≅ 𝟭 C :=
+  Iso.refl _
+
+def otherDirection :
+    CommGrp_.forget₂Grp_ _ ⋙ Grp_.forget₂Mon_ _ ⋙ Mon_.forget _ ⋙ toCommGrp_ C ≅ 𝟭 (CommGrp_ C) := by
+  refine NatIso.ofComponents ?_ ?_
+  · intro X
+    refine CommGrp_.mkIso (Iso.refl _) ?_ ?_
+    · simp
+      
+      sorry
+    · simp
+      sorry
+  · aesop_cat
+
+
+end CategoryTheory.Preadditive

From 97bdbcac2815403ef620a8781448f0109ce1ef9c Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Thu, 6 Feb 2025 20:08:16 +0100
Subject: [PATCH 15/57] Done

---
 .../CategoryTheory/Preadditive/CommGrp_.lean  | 62 +++++++++++++------
 1 file changed, 44 insertions(+), 18 deletions(-)

diff --git a/Mathlib/CategoryTheory/Preadditive/CommGrp_.lean b/Mathlib/CategoryTheory/Preadditive/CommGrp_.lean
index 0a4ca8ccc34f7b..3515b9d2d928ff 100644
--- a/Mathlib/CategoryTheory/Preadditive/CommGrp_.lean
+++ b/Mathlib/CategoryTheory/Preadditive/CommGrp_.lean
@@ -7,21 +7,27 @@ import Mathlib.CategoryTheory.Monoidal.CommGrp_
 import Mathlib.CategoryTheory.Preadditive.Biproducts
 
 /-!
-#
+# Internal commutative group objects in additive categories.
+
+We construct an inverse of the forgetful functor `CommGrp_ C ⥤ C` if `C` is an additive category.
+
+This looks slightly strange because the additive structure of `C` maps to the multiplicative
+structure of the commutative group objects.
 -/
 
 universe v u
 
 namespace CategoryTheory.Preadditive
 
-open CategoryTheory MonoidalCategory ChosenFiniteProducts
+open CategoryTheory Limits MonoidalCategory ChosenFiniteProducts
 
 variable {C : Type u} [Category.{v} C] [Preadditive C] [ChosenFiniteProducts C]
 
 variable (C) in
-/-- The canonical functor from an additive category into its commutative group objects. -/
+/-- The canonical functor from an additive category into its commutative group objects. This is
+always an equivalence, see `commGrpEquivalence`. -/
 @[simps]
-def toCommGrp_ : C ⥤ CommGrp_ C where
+def toCommGrp : C ⥤ CommGrp_ C where
   obj X :=
     { X := X
       one := 0
@@ -31,21 +37,41 @@ def toCommGrp_ : C ⥤ CommGrp_ C where
       mul_comm := by simp [add_comm] }
   map {X Y} f := { hom := f }
 
-def oneDirection :
-    toCommGrp_ C ⋙ CommGrp_.forget₂Grp_ _ ⋙ Grp_.forget₂Mon_ _ ⋙ Mon_.forget _ ≅ 𝟭 C :=
-  Iso.refl _
-
-def otherDirection :
-    CommGrp_.forget₂Grp_ _ ⋙ Grp_.forget₂Mon_ _ ⋙ Mon_.forget _ ⋙ toCommGrp_ C ≅ 𝟭 (CommGrp_ C) := by
-  refine NatIso.ofComponents ?_ ?_
-  · intro X
-    refine CommGrp_.mkIso (Iso.refl _) ?_ ?_
-    · simp
-      
-      sorry
-    · simp
-      sorry
+-- PROJECT: develop `ChosenFiniteCoproducts`, and construct `ChosenFiniteCoproducts` from
+-- `ChosenFiniteProducts` in preadditive categories, to give this lemma a proper home.
+private theorem monoidal_hom_ext {X Y Z : C} {f g : X ⊗ Y ⟶ Z}
+    (h₁ : lift (𝟙 X) 0 ≫ f = lift (𝟙 X) 0 ≫ g) (h₂ : lift 0 (𝟙 Y) ≫ f = lift 0 (𝟙 Y) ≫ g) :
+    f = g :=
+  BinaryCofan.IsColimit.hom_ext
+    (binaryBiconeIsBilimitOfLimitConeOfIsLimit (product X Y).isLimit).isColimit h₁ h₂
+
+/-- Auxiliary definition for `commGrpEquivalence`. -/
+@[simps!]
+def commGrpEquivalenceAux :
+    CommGrp_.forget₂Grp_ _ ⋙ Grp_.forget₂Mon_ _ ⋙ Mon_.forget _ ⋙ toCommGrp C ≅
+      𝟭 (CommGrp_ C) := by
+  refine NatIso.ofComponents (fun _ => CommGrp_.mkIso (Iso.refl _) ?_ ?_) ?_
+  · exact ((IsZero.iff_id_eq_zero _).2 (Subsingleton.elim _ _)).eq_of_src _ _
+  · simp only [Functor.comp_obj, Mon_.forget_obj, toCommGrp_obj_X, Functor.id_obj,
+      toCommGrp_obj_mul, Iso.refl_hom, Category.comp_id, tensorHom_id, id_whiskerRight,
+      Category.id_comp]
+    apply monoidal_hom_ext
+    · simp only [comp_add, lift_fst, lift_snd, add_zero]
+      convert (Mon_.lift_comp_one_right _ 0).symm
+      · simp
+      · infer_instance
+    · simp only [comp_add, lift_fst, lift_snd, zero_add]
+      convert (Mon_.lift_comp_one_left 0 _).symm
+      · simp
+      · infer_instance
   · aesop_cat
 
+/-- An additive category is equivalent to its category of commutative group objects. -/
+@[simps!]
+def commGrpEquivalence : C ≌ CommGrp_ C where
+  functor := toCommGrp C
+  inverse := CommGrp_.forget₂Grp_ _ ⋙ Grp_.forget₂Mon_ _ ⋙ Mon_.forget _
+  unitIso := Iso.refl _
+  counitIso := commGrpEquivalenceAux
 
 end CategoryTheory.Preadditive

From 1cf5d22fc43e80e38ff750d738b4eaac0c9348a2 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Thu, 6 Feb 2025 20:09:07 +0100
Subject: [PATCH 16/57] Fix

---
 Mathlib/CategoryTheory/Preadditive/CommGrp_.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Preadditive/CommGrp_.lean b/Mathlib/CategoryTheory/Preadditive/CommGrp_.lean
index 3515b9d2d928ff..45b35454267e3c 100644
--- a/Mathlib/CategoryTheory/Preadditive/CommGrp_.lean
+++ b/Mathlib/CategoryTheory/Preadditive/CommGrp_.lean
@@ -7,7 +7,7 @@ import Mathlib.CategoryTheory.Monoidal.CommGrp_
 import Mathlib.CategoryTheory.Preadditive.Biproducts
 
 /-!
-# Internal commutative group objects in additive categories.
+# Commutative group objects in additive categories.
 
 We construct an inverse of the forgetful functor `CommGrp_ C ⥤ C` if `C` is an additive category.
 

From 93b6633e4712f19299f0fffcc49951df7cddb55a Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 8 Feb 2025 10:24:29 +0100
Subject: [PATCH 17/57] Add forgetful functor

---
 Mathlib/CategoryTheory/Monoidal/Grp_.lean | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Monoidal/Grp_.lean b/Mathlib/CategoryTheory/Monoidal/Grp_.lean
index eaacebb77c124f..496bb6bb815a91 100644
--- a/Mathlib/CategoryTheory/Monoidal/Grp_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Grp_.lean
@@ -181,6 +181,16 @@ theorem forget₂Mon_obj_mul (A : Grp_ C) : ((forget₂Mon_ C).obj A).mul = A.mu
 theorem forget₂Mon_map_hom {A B : Grp_ C} (f : A ⟶ B) : ((forget₂Mon_ C).map f).hom = f.hom :=
   rfl
 
+/-- The forgetful functor from group objects to the ambient category. -/
+@[simps!]
+def forget : Grp_ C ⥤ C :=
+  forget₂Mon_ C ⋙ Mon_.forget C
+
+instance : (forget C).Faithful where
+
+@[simp]
+theorem forget₂Mon_comp_forget : forget₂Mon_ C ⋙ Mon_.forget C = forget C := rfl
+
 end
 
 section
@@ -226,7 +236,7 @@ noncomputable def mapGrp : Grp_ C ⥤ Grp_ D where
           Functor.Monoidal.toUnit_ε_assoc, ← Functor.map_comp] }
   map f := F.mapMon.map f
 
-attribute [local instance] NatTrans.monoidal_of_preservesFiniteLimits in
+attribute [local instance] NatTrans.monoidal_of_preservesFiniteProducts in
 /-- `mapGrp` is functorial in the left-exact functor. -/
 @[simps]
 noncomputable def mapGrpFunctor : (C ⥤ₗ D) ⥤ Grp_ C ⥤ Grp_ D where

From 10f6445f4dd9c864220a9c4910e77446141cb2f1 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 8 Feb 2025 16:13:11 +0100
Subject: [PATCH 18/57] Import

---
 .../Monoidal/Internal/Types.lean              | 52 +++++++++++++++++++
 .../CategoryTheory/Monoidal/Types/Basic.lean  |  7 ++-
 2 files changed, 58 insertions(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Monoidal/Internal/Types.lean b/Mathlib/CategoryTheory/Monoidal/Internal/Types.lean
index 6b12e1e0abe4d2..4feb445d62a0f6 100644
--- a/Mathlib/CategoryTheory/Monoidal/Internal/Types.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Internal/Types.lean
@@ -5,6 +5,8 @@ Authors: Kim Morrison
 -/
 import Mathlib.Algebra.Category.MonCat.Basic
 import Mathlib.CategoryTheory.Monoidal.CommMon_
+import Mathlib.CategoryTheory.Monoidal.Grp_
+import Mathlib.Algebra.Category.Grp.Basic
 import Mathlib.CategoryTheory.Monoidal.Types.Basic
 
 /-!
@@ -141,6 +143,56 @@ noncomputable def commMonTypeEquivalenceCommMon : CommMon_ (Type u) ≌ CommMonC
               map_mul' := fun _ _ => rfl } })
       (by aesop_cat)
 
+namespace GrpTypeEquivalenceGrp
+
+instance grpGroup (A : Grp_ (Type u)) : Group A.X :=
+  { MonTypeEquivalenceMon.monMonoid A.toMon_ with
+    inv := A.inv
+    inv_mul_cancel a := congr_fun A.left_inv a }
+
+/-- Converting a group object in `Type u` into a group. -/
+noncomputable def functor : Grp_ (Type u) ⥤ Grp.{u} where
+  obj A := Grp.of A.X
+  map f := Grp.ofHom (MonTypeEquivalenceMon.functor.map f).hom
+
+/-- Converting a group into a group object in `Type u`. -/
+noncomputable def inverse : Grp.{u} ⥤ Grp_ (Type u) where
+  obj A :=
+    { MonTypeEquivalenceMon.inverse.obj ((forget₂ Grp MonCat).obj A) with
+      inv := ((·⁻¹) : A → A)
+      left_inv := by
+        ext x
+        exact inv_mul_cancel (G := A) x
+      right_inv := by
+        ext x
+        exact mul_inv_cancel (G := A) x }
+  map f := MonTypeEquivalenceMon.inverse.map ((forget₂ Grp MonCat).map f)
+
+end GrpTypeEquivalenceGrp
+
+/-- The category of group objects in `Type u` is equivalent to the category of groups. -/
+noncomputable def grpTypeEquivalenceGrp : Grp_ (Type u) ≌ Grp.{u} where
+  functor := GrpTypeEquivalenceGrp.functor
+  inverse := GrpTypeEquivalenceGrp.inverse
+  unitIso :=
+    NatIso.ofComponents
+      (fun A =>
+        { hom := { hom := 𝟙 _ }
+          inv := { hom := 𝟙 _ } })
+      (by aesop_cat)
+  counitIso :=
+    NatIso.ofComponents
+      (fun A =>
+        { hom := Grp.ofHom
+            { toFun := id
+              map_one' := rfl
+              map_mul' := fun _ _ => rfl }
+          inv := Grp.ofHom
+            { toFun := id
+              map_one' := rfl
+              map_mul' := fun _ _ => rfl } })
+      (by aesop_cat)
+
 /-- The equivalences `Mon_ (Type u) ≌ MonCat.{u}` and `CommMon_ (Type u) ≌ CommMonCat.{u}`
 are naturally compatible with the forgetful functors to `MonCat` and `Mon_ (Type u)`.
 -/
diff --git a/Mathlib/CategoryTheory/Monoidal/Types/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Types/Basic.lean
index 340b2b39e0d013..d92384f78e2205 100644
--- a/Mathlib/CategoryTheory/Monoidal/Types/Basic.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Types/Basic.lean
@@ -12,7 +12,7 @@ import Mathlib.CategoryTheory.Limits.Shapes.Types
 -/
 
 
-open CategoryTheory Limits MonoidalCategory
+open CategoryTheory Limits MonoidalCategory ChosenFiniteProducts
 
 open Tactic
 
@@ -103,6 +103,11 @@ theorem braiding_inv_apply {X Y : Type u} {x : X} {y : Y} :
     ((β_ X Y).inv : Y ⊗ X → X ⊗ Y) (y, x) = (x, y) :=
   rfl
 
+@[simp]
+theorem lift_apply {X Y Z : Type u} {f : X ⟶ Y} {g : X ⟶ Z} {x : X} :
+    lift f g x = (f x, g x) :=
+  rfl
+
 -- We don't yet have an API for tensor products indexed by finite ordered types,
 -- but it would be nice to state how monoidal functors preserve these.
 /-- If `F` is a monoidal functor out of `Type`, it takes the (n+1)st cartesian power

From 0d20720342ca78d7b9304361f9d0794a17a43900 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 8 Feb 2025 16:16:33 +0100
Subject: [PATCH 19/57] Compatibility

---
 Mathlib/CategoryTheory/Monoidal/Internal/Types.lean | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/Mathlib/CategoryTheory/Monoidal/Internal/Types.lean b/Mathlib/CategoryTheory/Monoidal/Internal/Types.lean
index 4feb445d62a0f6..2a47358d8302cb 100644
--- a/Mathlib/CategoryTheory/Monoidal/Internal/Types.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Internal/Types.lean
@@ -199,7 +199,12 @@ are naturally compatible with the forgetful functors to `MonCat` and `Mon_ (Type
 noncomputable def commMonTypeEquivalenceCommMonForget :
     CommMonTypeEquivalenceCommMon.functor ⋙ forget₂ CommMonCat MonCat ≅
       CommMon_.forget₂Mon_ (Type u) ⋙ MonTypeEquivalenceMon.functor :=
-  NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat)
+  Iso.refl _
 
-noncomputable instance commMonTypeInhabited : Inhabited (CommMon_ (Type u)) :=
-  ⟨CommMonTypeEquivalenceCommMon.inverse.obj (CommMonCat.of PUnit)⟩
+/-- The equivalences `Mon_ (Type u) ≌ MonCat.{u}` and `Grp_ (Type u) ≌ Grp.{u}`
+are naturally compatible with the forgetful functors to `MonCat` and `Mon_ (Type u)`.
+-/
+noncomputable def grpTypeEquivalenceGrpForget :
+    GrpTypeEquivalenceGrp.functor ⋙ forget₂ Grp MonCat ≅
+      Grp_.forget₂Mon_ (Type u) ⋙ MonTypeEquivalenceMon.functor :=
+  Iso.refl _

From b1c3eee8b122e6795c7fa0e3d14bb1843d1c96f0 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 8 Feb 2025 16:23:09 +0100
Subject: [PATCH 20/57] Fix namespace

---
 Mathlib/CategoryTheory/Monoidal/Types/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Monoidal/Types/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Types/Basic.lean
index d92384f78e2205..337706c117c548 100644
--- a/Mathlib/CategoryTheory/Monoidal/Types/Basic.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Types/Basic.lean
@@ -12,7 +12,7 @@ import Mathlib.CategoryTheory.Limits.Shapes.Types
 -/
 
 
-open CategoryTheory Limits MonoidalCategory ChosenFiniteProducts
+open CategoryTheory Limits MonoidalCategory
 
 open Tactic
 
@@ -104,7 +104,7 @@ theorem braiding_inv_apply {X Y : Type u} {x : X} {y : Y} :
   rfl
 
 @[simp]
-theorem lift_apply {X Y Z : Type u} {f : X ⟶ Y} {g : X ⟶ Z} {x : X} :
+theorem ChosenFiniteProducts.lift_apply {X Y Z : Type u} {f : X ⟶ Y} {g : X ⟶ Z} {x : X} :
     lift f g x = (f x, g x) :=
   rfl
 

From 2fe34b5a6991c9a425cc6677e5c47e627885cea2 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 8 Feb 2025 16:26:55 +0100
Subject: [PATCH 21/57] Move to separate file

---
 Mathlib.lean                                  |  3 +-
 .../Internal/{Types.lean => Types/Basic.lean} | 60 --------------
 .../Monoidal/Internal/Types/Grp_.lean         | 79 +++++++++++++++++++
 3 files changed, 81 insertions(+), 61 deletions(-)
 rename Mathlib/CategoryTheory/Monoidal/Internal/{Types.lean => Types/Basic.lean} (70%)
 create mode 100644 Mathlib/CategoryTheory/Monoidal/Internal/Types/Grp_.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 173981b9fd64c8..7d11ccef09598e 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2119,7 +2119,8 @@ import Mathlib.CategoryTheory.Monoidal.Hopf_
 import Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
 import Mathlib.CategoryTheory.Monoidal.Internal.Limits
 import Mathlib.CategoryTheory.Monoidal.Internal.Module
-import Mathlib.CategoryTheory.Monoidal.Internal.Types
+import Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
+import Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp_
 import Mathlib.CategoryTheory.Monoidal.Limits
 import Mathlib.CategoryTheory.Monoidal.Linear
 import Mathlib.CategoryTheory.Monoidal.Mod_
diff --git a/Mathlib/CategoryTheory/Monoidal/Internal/Types.lean b/Mathlib/CategoryTheory/Monoidal/Internal/Types/Basic.lean
similarity index 70%
rename from Mathlib/CategoryTheory/Monoidal/Internal/Types.lean
rename to Mathlib/CategoryTheory/Monoidal/Internal/Types/Basic.lean
index 2a47358d8302cb..9a07c628326d3d 100644
--- a/Mathlib/CategoryTheory/Monoidal/Internal/Types.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Internal/Types/Basic.lean
@@ -5,8 +5,6 @@ Authors: Kim Morrison
 -/
 import Mathlib.Algebra.Category.MonCat.Basic
 import Mathlib.CategoryTheory.Monoidal.CommMon_
-import Mathlib.CategoryTheory.Monoidal.Grp_
-import Mathlib.Algebra.Category.Grp.Basic
 import Mathlib.CategoryTheory.Monoidal.Types.Basic
 
 /-!
@@ -143,56 +141,6 @@ noncomputable def commMonTypeEquivalenceCommMon : CommMon_ (Type u) ≌ CommMonC
               map_mul' := fun _ _ => rfl } })
       (by aesop_cat)
 
-namespace GrpTypeEquivalenceGrp
-
-instance grpGroup (A : Grp_ (Type u)) : Group A.X :=
-  { MonTypeEquivalenceMon.monMonoid A.toMon_ with
-    inv := A.inv
-    inv_mul_cancel a := congr_fun A.left_inv a }
-
-/-- Converting a group object in `Type u` into a group. -/
-noncomputable def functor : Grp_ (Type u) ⥤ Grp.{u} where
-  obj A := Grp.of A.X
-  map f := Grp.ofHom (MonTypeEquivalenceMon.functor.map f).hom
-
-/-- Converting a group into a group object in `Type u`. -/
-noncomputable def inverse : Grp.{u} ⥤ Grp_ (Type u) where
-  obj A :=
-    { MonTypeEquivalenceMon.inverse.obj ((forget₂ Grp MonCat).obj A) with
-      inv := ((·⁻¹) : A → A)
-      left_inv := by
-        ext x
-        exact inv_mul_cancel (G := A) x
-      right_inv := by
-        ext x
-        exact mul_inv_cancel (G := A) x }
-  map f := MonTypeEquivalenceMon.inverse.map ((forget₂ Grp MonCat).map f)
-
-end GrpTypeEquivalenceGrp
-
-/-- The category of group objects in `Type u` is equivalent to the category of groups. -/
-noncomputable def grpTypeEquivalenceGrp : Grp_ (Type u) ≌ Grp.{u} where
-  functor := GrpTypeEquivalenceGrp.functor
-  inverse := GrpTypeEquivalenceGrp.inverse
-  unitIso :=
-    NatIso.ofComponents
-      (fun A =>
-        { hom := { hom := 𝟙 _ }
-          inv := { hom := 𝟙 _ } })
-      (by aesop_cat)
-  counitIso :=
-    NatIso.ofComponents
-      (fun A =>
-        { hom := Grp.ofHom
-            { toFun := id
-              map_one' := rfl
-              map_mul' := fun _ _ => rfl }
-          inv := Grp.ofHom
-            { toFun := id
-              map_one' := rfl
-              map_mul' := fun _ _ => rfl } })
-      (by aesop_cat)
-
 /-- The equivalences `Mon_ (Type u) ≌ MonCat.{u}` and `CommMon_ (Type u) ≌ CommMonCat.{u}`
 are naturally compatible with the forgetful functors to `MonCat` and `Mon_ (Type u)`.
 -/
@@ -200,11 +148,3 @@ noncomputable def commMonTypeEquivalenceCommMonForget :
     CommMonTypeEquivalenceCommMon.functor ⋙ forget₂ CommMonCat MonCat ≅
       CommMon_.forget₂Mon_ (Type u) ⋙ MonTypeEquivalenceMon.functor :=
   Iso.refl _
-
-/-- The equivalences `Mon_ (Type u) ≌ MonCat.{u}` and `Grp_ (Type u) ≌ Grp.{u}`
-are naturally compatible with the forgetful functors to `MonCat` and `Mon_ (Type u)`.
--/
-noncomputable def grpTypeEquivalenceGrpForget :
-    GrpTypeEquivalenceGrp.functor ⋙ forget₂ Grp MonCat ≅
-      Grp_.forget₂Mon_ (Type u) ⋙ MonTypeEquivalenceMon.functor :=
-  Iso.refl _
diff --git a/Mathlib/CategoryTheory/Monoidal/Internal/Types/Grp_.lean b/Mathlib/CategoryTheory/Monoidal/Internal/Types/Grp_.lean
new file mode 100644
index 00000000000000..b368fef518d611
--- /dev/null
+++ b/Mathlib/CategoryTheory/Monoidal/Internal/Types/Grp_.lean
@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
+import Mathlib.CategoryTheory.Monoidal.Grp_
+import Mathlib.Algebra.Category.Grp.Basic
+
+/-!
+# `Grp_ (Type u) ≌ Grp.{u}`
+
+The category of internal group objects in `Type`
+is equivalent to the category of "native" bundled groups.
+
+Moreover, this equivalence is compatible with the forgetful functors to `Type`.
+-/
+
+universe v u
+
+open CategoryTheory
+
+namespace GrpTypeEquivalenceGrp
+
+instance grpGroup (A : Grp_ (Type u)) : Group A.X :=
+  { MonTypeEquivalenceMon.monMonoid A.toMon_ with
+    inv := A.inv
+    inv_mul_cancel a := congr_fun A.left_inv a }
+
+/-- Converting a group object in `Type u` into a group. -/
+noncomputable def functor : Grp_ (Type u) ⥤ Grp.{u} where
+  obj A := Grp.of A.X
+  map f := Grp.ofHom (MonTypeEquivalenceMon.functor.map f).hom
+
+/-- Converting a group into a group object in `Type u`. -/
+noncomputable def inverse : Grp.{u} ⥤ Grp_ (Type u) where
+  obj A :=
+    { MonTypeEquivalenceMon.inverse.obj ((forget₂ Grp MonCat).obj A) with
+      inv := ((·⁻¹) : A → A)
+      left_inv := by
+        ext x
+        exact inv_mul_cancel (G := A) x
+      right_inv := by
+        ext x
+        exact mul_inv_cancel (G := A) x }
+  map f := MonTypeEquivalenceMon.inverse.map ((forget₂ Grp MonCat).map f)
+
+end GrpTypeEquivalenceGrp
+
+/-- The category of group objects in `Type u` is equivalent to the category of groups. -/
+noncomputable def grpTypeEquivalenceGrp : Grp_ (Type u) ≌ Grp.{u} where
+  functor := GrpTypeEquivalenceGrp.functor
+  inverse := GrpTypeEquivalenceGrp.inverse
+  unitIso :=
+    NatIso.ofComponents
+      (fun A =>
+        { hom := { hom := 𝟙 _ }
+          inv := { hom := 𝟙 _ } })
+      (by aesop_cat)
+  counitIso :=
+    NatIso.ofComponents
+      (fun A =>
+        { hom := Grp.ofHom
+            { toFun := id
+              map_one' := rfl
+              map_mul' := fun _ _ => rfl }
+          inv := Grp.ofHom
+            { toFun := id
+              map_one' := rfl
+              map_mul' := fun _ _ => rfl } })
+      (by aesop_cat)
+
+/-- The equivalences `Mon_ (Type u) ≌ MonCat.{u}` and `Grp_ (Type u) ≌ Grp.{u}`
+are naturally compatible with the forgetful functors to `MonCat` and `Mon_ (Type u)`.
+-/
+noncomputable def grpTypeEquivalenceGrpForget :
+    GrpTypeEquivalenceGrp.functor ⋙ forget₂ Grp MonCat ≅
+      Grp_.forget₂Mon_ (Type u) ⋙ MonTypeEquivalenceMon.functor :=
+  Iso.refl _

From 6da6e17d230e9b34bf1c449e291fc267613bc7cc Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 8 Feb 2025 17:03:27 +0100
Subject: [PATCH 22/57] Fix

---
 Mathlib/CategoryTheory/Monoidal/Grp_.lean | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Monoidal/Grp_.lean b/Mathlib/CategoryTheory/Monoidal/Grp_.lean
index 1264f544af2c98..496bb6bb815a91 100644
--- a/Mathlib/CategoryTheory/Monoidal/Grp_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Grp_.lean
@@ -181,6 +181,16 @@ theorem forget₂Mon_obj_mul (A : Grp_ C) : ((forget₂Mon_ C).obj A).mul = A.mu
 theorem forget₂Mon_map_hom {A B : Grp_ C} (f : A ⟶ B) : ((forget₂Mon_ C).map f).hom = f.hom :=
   rfl
 
+/-- The forgetful functor from group objects to the ambient category. -/
+@[simps!]
+def forget : Grp_ C ⥤ C :=
+  forget₂Mon_ C ⋙ Mon_.forget C
+
+instance : (forget C).Faithful where
+
+@[simp]
+theorem forget₂Mon_comp_forget : forget₂Mon_ C ⋙ Mon_.forget C = forget C := rfl
+
 end
 
 section
@@ -207,7 +217,7 @@ end Grp_
 
 namespace CategoryTheory.Functor
 
-variable {C} {D : Type u₂} [Category.{v₂} D] [ChosenFiniteProducts.{v₂} D] (F : C ⥤ D)
+variable {D : Type u₂} [Category.{v₂} D] [ChosenFiniteProducts.{v₂} D] (F : C ⥤ D)
 variable [PreservesFiniteProducts F]
 
 attribute [local instance] monoidalOfChosenFiniteProducts
@@ -226,7 +236,7 @@ noncomputable def mapGrp : Grp_ C ⥤ Grp_ D where
           Functor.Monoidal.toUnit_ε_assoc, ← Functor.map_comp] }
   map f := F.mapMon.map f
 
-attribute [local instance] NatTrans.monoidal_of_preservesFiniteLimits in
+attribute [local instance] NatTrans.monoidal_of_preservesFiniteProducts in
 /-- `mapGrp` is functorial in the left-exact functor. -/
 @[simps]
 noncomputable def mapGrpFunctor : (C ⥤ₗ D) ⥤ Grp_ C ⥤ Grp_ D where

From 527b8c9ed3f48eb9d23eae72a88aa340a9dd7140 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 8 Feb 2025 17:04:42 +0100
Subject: [PATCH 23/57] Add forgetful functor

---
 Mathlib/CategoryTheory/Monoidal/CommGrp_.lean | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
index 45154cb5435ba9..129279fbc5f9bb 100644
--- a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
@@ -108,6 +108,20 @@ theorem forget₂CommMon_map_hom {A B : CommGrp_ C} (f : A ⟶ B) :
     ((forget₂CommMon_ C).map f).hom = f.hom :=
   rfl
 
+
+/-- The forgetful functor from group objects to the ambient category. -/
+@[simps!]
+def forget : CommGrp_ C ⥤ C :=
+  forget₂Grp_ C ⋙ Grp_.forget C
+
+instance : (forget C).Faithful where
+
+@[simp]
+theorem forget₂Grp_comp_forget : forget₂Grp_ C ⋙ Grp_.forget C = forget C := rfl
+
+@[simp]
+theorem forget₂CommMon_comp_forget : forget₂CommMon_ C ⋙ CommMon_.forget C = forget C := rfl
+
 end
 
 section

From 4e118dde583ee30c09e1695ef359e3879c805f6a Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 8 Feb 2025 17:04:56 +0100
Subject: [PATCH 24/57] Fix

---
 Mathlib/CategoryTheory/Monoidal/CommGrp_.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
index 129279fbc5f9bb..daca4542991ac1 100644
--- a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
@@ -108,8 +108,7 @@ theorem forget₂CommMon_map_hom {A B : CommGrp_ C} (f : A ⟶ B) :
     ((forget₂CommMon_ C).map f).hom = f.hom :=
   rfl
 
-
-/-- The forgetful functor from group objects to the ambient category. -/
+/-- The forgetful functor from commutative group objects to the ambient category. -/
 @[simps!]
 def forget : CommGrp_ C ⥤ C :=
   forget₂Grp_ C ⋙ Grp_.forget C

From 22b12d29254d2919818b0f1cf430afc09b37b212 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 8 Feb 2025 17:15:10 +0100
Subject: [PATCH 25/57] Cleanup

---
 Mathlib/CategoryTheory/Monoidal/CommGrp_.lean    | 4 ++--
 Mathlib/CategoryTheory/Monoidal/Grp_.lean        | 2 +-
 Mathlib/CategoryTheory/Preadditive/CommGrp_.lean | 5 ++---
 3 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
index daca4542991ac1..10b4040494b14d 100644
--- a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
@@ -147,7 +147,7 @@ end CommGrp_
 
 namespace CategoryTheory.Functor
 
-variable {D : Type u₂} [Category.{v₂} D] [ChosenFiniteProducts.{v₂} D] (F : C ⥤ D)
+variable {C} {D : Type u₂} [Category.{v₂} D] [ChosenFiniteProducts.{v₂} D] (F : C ⥤ D)
 variable [PreservesFiniteProducts F]
 
 attribute [local instance] braidedOfChosenFiniteProducts
@@ -163,7 +163,7 @@ noncomputable def mapCommGrp : CommGrp_ C ⥤ CommGrp_ D where
         rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, A.mul_comm] }
   map f := F.mapMon.map f
 
-attribute [local instance] NatTrans.monoidal_of_preservesFiniteLimits in
+attribute [local instance] NatTrans.monoidal_of_preservesFiniteProducts in
 /-- `mapGrp` is functorial in the left-exact functor. -/
 @[simps]
 noncomputable def mapCommGrpFunctor : (C ⥤ₗ D) ⥤ CommGrp_ C ⥤ CommGrp_ D where
diff --git a/Mathlib/CategoryTheory/Monoidal/Grp_.lean b/Mathlib/CategoryTheory/Monoidal/Grp_.lean
index 496bb6bb815a91..aec113eb2f30dc 100644
--- a/Mathlib/CategoryTheory/Monoidal/Grp_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Grp_.lean
@@ -217,7 +217,7 @@ end Grp_
 
 namespace CategoryTheory.Functor
 
-variable {D : Type u₂} [Category.{v₂} D] [ChosenFiniteProducts.{v₂} D] (F : C ⥤ D)
+variable {C} {D : Type u₂} [Category.{v₂} D] [ChosenFiniteProducts.{v₂} D] (F : C ⥤ D)
 variable [PreservesFiniteProducts F]
 
 attribute [local instance] monoidalOfChosenFiniteProducts
diff --git a/Mathlib/CategoryTheory/Preadditive/CommGrp_.lean b/Mathlib/CategoryTheory/Preadditive/CommGrp_.lean
index 45b35454267e3c..bd43b2eeca5fb2 100644
--- a/Mathlib/CategoryTheory/Preadditive/CommGrp_.lean
+++ b/Mathlib/CategoryTheory/Preadditive/CommGrp_.lean
@@ -47,8 +47,7 @@ private theorem monoidal_hom_ext {X Y Z : C} {f g : X ⊗ Y ⟶ Z}
 
 /-- Auxiliary definition for `commGrpEquivalence`. -/
 @[simps!]
-def commGrpEquivalenceAux :
-    CommGrp_.forget₂Grp_ _ ⋙ Grp_.forget₂Mon_ _ ⋙ Mon_.forget _ ⋙ toCommGrp C ≅
+def commGrpEquivalenceAux : CommGrp_.forget C ⋙ toCommGrp C ≅
       𝟭 (CommGrp_ C) := by
   refine NatIso.ofComponents (fun _ => CommGrp_.mkIso (Iso.refl _) ?_ ?_) ?_
   · exact ((IsZero.iff_id_eq_zero _).2 (Subsingleton.elim _ _)).eq_of_src _ _
@@ -70,7 +69,7 @@ def commGrpEquivalenceAux :
 @[simps!]
 def commGrpEquivalence : C ≌ CommGrp_ C where
   functor := toCommGrp C
-  inverse := CommGrp_.forget₂Grp_ _ ⋙ Grp_.forget₂Mon_ _ ⋙ Mon_.forget _
+  inverse := CommGrp_.forget C
   unitIso := Iso.refl _
   counitIso := commGrpEquivalenceAux
 

From d575b258af7b279bc5cdac365a617bb4714b5e85 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 8 Feb 2025 17:15:38 +0100
Subject: [PATCH 26/57] Fix implicitness

---
 Mathlib/CategoryTheory/Monoidal/Grp_.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Monoidal/Grp_.lean b/Mathlib/CategoryTheory/Monoidal/Grp_.lean
index 496bb6bb815a91..aec113eb2f30dc 100644
--- a/Mathlib/CategoryTheory/Monoidal/Grp_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Grp_.lean
@@ -217,7 +217,7 @@ end Grp_
 
 namespace CategoryTheory.Functor
 
-variable {D : Type u₂} [Category.{v₂} D] [ChosenFiniteProducts.{v₂} D] (F : C ⥤ D)
+variable {C} {D : Type u₂} [Category.{v₂} D] [ChosenFiniteProducts.{v₂} D] (F : C ⥤ D)
 variable [PreservesFiniteProducts F]
 
 attribute [local instance] monoidalOfChosenFiniteProducts

From e53b99f3f43e23f24ee55fcee164b11f74032c18 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 8 Feb 2025 17:16:08 +0100
Subject: [PATCH 27/57] Fix implicitness

---
 Mathlib/CategoryTheory/Monoidal/CommGrp_.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
index daca4542991ac1..6a659cfd20ab15 100644
--- a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
@@ -147,7 +147,7 @@ end CommGrp_
 
 namespace CategoryTheory.Functor
 
-variable {D : Type u₂} [Category.{v₂} D] [ChosenFiniteProducts.{v₂} D] (F : C ⥤ D)
+variable {C} {D : Type u₂} [Category.{v₂} D] [ChosenFiniteProducts.{v₂} D] (F : C ⥤ D)
 variable [PreservesFiniteProducts F]
 
 attribute [local instance] braidedOfChosenFiniteProducts

From 9837c6788d9793da615e2ccc86395c6c14157bd0 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 8 Feb 2025 17:44:28 +0100
Subject: [PATCH 28/57] Oops

---
 Mathlib/CategoryTheory/Monoidal/CommGrp_.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
index 6a659cfd20ab15..10b4040494b14d 100644
--- a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
@@ -163,7 +163,7 @@ noncomputable def mapCommGrp : CommGrp_ C ⥤ CommGrp_ D where
         rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, A.mul_comm] }
   map f := F.mapMon.map f
 
-attribute [local instance] NatTrans.monoidal_of_preservesFiniteLimits in
+attribute [local instance] NatTrans.monoidal_of_preservesFiniteProducts in
 /-- `mapGrp` is functorial in the left-exact functor. -/
 @[simps]
 noncomputable def mapCommGrpFunctor : (C ⥤ₗ D) ⥤ CommGrp_ C ⥤ CommGrp_ D where

From a8d8b86d9d77856742fa2f2db1cfba73962337c6 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 8 Feb 2025 17:46:21 +0100
Subject: [PATCH 29/57] Lint?!

---
 Mathlib/CategoryTheory/Monoidal/CommGrp_.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
index 10b4040494b14d..7507afa91688ce 100644
--- a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
@@ -19,6 +19,9 @@ variable (C : Type u₁) [Category.{v₁} C] [ChosenFiniteProducts.{v₁} C]
 /-- A commutative group object internal to a cartesian monoidal category. -/
 structure CommGrp_ extends Grp_ C, CommMon_ C where
 
+/-- Turn a commutative group object into a commutative monoid object. -/
+add_decl_doc CommGrp_.toCommMon_
+
 attribute [reassoc (attr := simp)] CommGrp_.mul_comm
 
 namespace CommGrp_

From 015fdedfa0a0956d9172d08d0d74cb253bd0d3c4 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 8 Feb 2025 17:58:11 +0100
Subject: [PATCH 30/57] Add code

---
 Mathlib.lean                                  |  1 +
 .../Monoidal/Internal/Types/CommGrp_.lean     | 82 +++++++++++++++++++
 2 files changed, 83 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/Monoidal/Internal/Types/CommGrp_.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index d10643deb6adae..5926b4be7a58b0 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2121,6 +2121,7 @@ import Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
 import Mathlib.CategoryTheory.Monoidal.Internal.Limits
 import Mathlib.CategoryTheory.Monoidal.Internal.Module
 import Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
+import Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_
 import Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp_
 import Mathlib.CategoryTheory.Monoidal.Limits
 import Mathlib.CategoryTheory.Monoidal.Linear
diff --git a/Mathlib/CategoryTheory/Monoidal/Internal/Types/CommGrp_.lean b/Mathlib/CategoryTheory/Monoidal/Internal/Types/CommGrp_.lean
new file mode 100644
index 00000000000000..8ea54ddc19b889
--- /dev/null
+++ b/Mathlib/CategoryTheory/Monoidal/Internal/Types/CommGrp_.lean
@@ -0,0 +1,82 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp_
+import Mathlib.CategoryTheory.Monoidal.CommGrp_
+
+/-!
+# `CommGrp_ (Type u) ≌ CommGrp.{u}`
+
+The category of internal commutative group objects in `Type`
+is equivalent to the category of "native" bundled commutative groups.
+
+Moreover, this equivalence is compatible with the forgetful functors to `Type`.
+-/
+
+universe v u
+
+open CategoryTheory
+
+namespace CommGrpTypeEquivalenceCommGrp
+
+instance commGrpCommGroup (A : CommGrp_ (Type u)) : CommGroup A.X :=
+  { GrpTypeEquivalenceGrp.grpGroup A.toGrp_ with
+    mul_comm := fun x y => by convert congr_fun A.mul_comm (y, x) }
+
+/-- Converting a commutative group object in `Type u` into a group. -/
+noncomputable def functor : CommGrp_ (Type u) ⥤ CommGrp.{u} where
+  obj A := CommGrp.of A.X
+  map f := CommGrp.ofHom (GrpTypeEquivalenceGrp.functor.map f).hom
+
+/-- Converting a group into a group object in `Type u`. -/
+noncomputable def inverse : CommGrp.{u} ⥤ CommGrp_ (Type u) where
+  obj A :=
+    { grpTypeEquivalenceGrp.inverse.obj ((forget₂ CommGrp Grp).obj A) with
+      mul_comm := by
+        ext ⟨x : A, y : A⟩
+        exact CommMonoid.mul_comm y x }
+  map f := GrpTypeEquivalenceGrp.inverse.map ((forget₂ CommGrp Grp).map f)
+
+end CommGrpTypeEquivalenceCommGrp
+
+/-- The category of commutative group objects in `Type u` is equivalent to the category of
+commutative groups. -/
+noncomputable def commGrpTypeEquivalenceCommGrp : CommGrp_ (Type u) ≌ CommGrp.{u} where
+  functor := CommGrpTypeEquivalenceCommGrp.functor
+  inverse := CommGrpTypeEquivalenceCommGrp.inverse
+  unitIso :=
+    NatIso.ofComponents
+      (fun A =>
+        { hom := { hom := 𝟙 _ }
+          inv := { hom := 𝟙 _ } })
+      (by aesop_cat)
+  counitIso :=
+    NatIso.ofComponents
+      (fun A =>
+        { hom := CommGrp.ofHom
+            { toFun := id
+              map_one' := rfl
+              map_mul' := fun _ _ => rfl }
+          inv := CommGrp.ofHom
+            { toFun := id
+              map_one' := rfl
+              map_mul' := fun _ _ => rfl } })
+      (by aesop_cat)
+
+/-- The equivalences `Grp_ (Type u) ≌ Grp.{u}` and `CommGrp_ (Type u) ≌ CommGrp.{u}`
+are naturally compatible with the forgetful functors to `Grp` and `Grp_ (Type u)`.
+-/
+noncomputable def commGrpTypeEquivalenceCommGrpForgetGrp :
+    CommGrpTypeEquivalenceCommGrp.functor ⋙ forget₂ CommGrp Grp ≅
+      CommGrp_.forget₂Grp_ (Type u) ⋙ GrpTypeEquivalenceGrp.functor :=
+  Iso.refl _
+
+/-- The equivalences `CommMon_ (Type u) ≌ CommMonCat.{u}` and `CommGrp_ (Type u) ≌ CommGrp.{u}`
+are naturally compatible with the forgetful functors to `Grp` and `Grp_ (Type u)`.
+-/
+noncomputable def commGrpTypeEquivalenceCommGrpForgetCommMon :
+    CommGrpTypeEquivalenceCommGrp.functor ⋙ forget₂ CommGrp CommMonCat ≅
+      CommGrp_.forget₂CommMon_ (Type u) ⋙ CommMonTypeEquivalenceCommMon.functor :=
+  Iso.refl _

From ec1677caa3faac6b017ba3b6a7e6a48c1c721eca Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sun, 9 Feb 2025 08:37:45 +0100
Subject: [PATCH 31/57] Tricky sorry

---
 .../Category/Grp/LeftExactFunctor.lean        | 204 ++++--------------
 1 file changed, 45 insertions(+), 159 deletions(-)

diff --git a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
index 7d450dc491d8eb..d227de1e586168 100644
--- a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
+++ b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
@@ -4,178 +4,64 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
 import Mathlib.CategoryTheory.Limits.ExactFunctor
-import Mathlib.CategoryTheory.Preadditive.Basic
-import Mathlib.CategoryTheory.Limits.Shapes.Biproducts
+import Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_
+import Mathlib.CategoryTheory.Preadditive.CommGrp_
 import Mathlib.Algebra.Category.Grp.Limits
-import Mathlib.CategoryTheory.Limits.Shapes.Types
-import Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
+import Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
 
 /-!
-# The functor `(C ⥤ₗ AddCommGroup) ⥤ (C ⥤ₗ Type v)` is an equivalence
+# The forgetful functor `(C ⥤ₗ AddCommGroup) ⥤ (C ⥤ₗ Type v)` is an equivalence
 -/
 
 open CategoryTheory Limits
 
 universe v v' u u'
 
-section
-
-variable {C : Type u} [Category.{v} C] [HasFiniteProducts C]
-
-structure AbelianGroupObject (X : C) where
-  m : X ⨯ X ⟶ X
-  e : ⊤_ C ⟶ X
-  inv : X ⟶ X
-  assoc : (prod.associator X X X).hom ≫ prod.map (𝟙 X) m ≫ m = prod.map m (𝟙 X) ≫ m
-  comm : (prod.braiding X X).hom ≫ m = m
-  left_id : prod.lift (terminal.from X ≫ e) (𝟙 X) ≫ m = 𝟙 X
-  right_id : prod.lift (𝟙 X) (terminal.from X ≫ e) ≫ m = 𝟙 X
-  left_inv : prod.lift inv (𝟙 X) ≫ m = terminal.from _ ≫ e
-  right_inv : prod.lift (𝟙 X) inv ≫ m = terminal.from _ ≫ e
-
-  -- -- assoc : m ≫ m = (prod.fst ≫ m) ≫ m ≫ m
-  -- comm : m = m ≫ (prod.snd ≫ prod.fst)
-  -- left_id : (e ≫ prod.fst) ≫ m = prod.snd
-  -- right_id : (prod.fst ≫ e) ≫ m = prod.fst
-  -- left_inv : (inv ≫ prod.fst) ≫ m = e
-  -- right_inv : (prod.fst ≫ inv) ≫ m = e
-
--- structure InternalAddCommGrp (X : C) where
---   presheaf : Cᵒᵖ ⥤ AddCommGrp.{v}
---   iso : presheaf ⋙ forget _ ≅ yoneda.obj X
-
--- def add {X : Type v} (G : InternalAddCommGrp X) : X × X → X :=
---   fun x y => _
-
--- variable {D : Type u} [Category.{v} D] (F : C ⥤ D) [PreservesFiniteLimits F]
-
--- def InternalAddCommGrp.map {X : C} (G : InternalAddCommGrp X) : InternalAddCommGrp (F.obj X) where
---   presheaf := sorry
---   iso := sorry
-
-end
-
-section
-
-variable {C : Type u} [Category.{v} C] [Preadditive C] [HasFiniteBiproducts C]
-
-attribute [local instance] hasBinaryBiproducts_of_finite_biproducts
-
-noncomputable def Preadditive.abelianGroupObject (X : C) : AbelianGroupObject X where
-  m := prod.fst + prod.snd
-  e := IsZero.to_ (IsZero.of_mono_zero (⊤_ C) X) _
-  inv := -𝟙 X
-  assoc := by
-    rw [← cancel_epi (biprod.isoProd _ _).hom]
-    simp [add_assoc]
-  comm := by
-    rw [← cancel_epi (biprod.isoProd _ _).hom]
-    simp [add_comm]
-  left_id := by simp [IsZero.to_eq _ 0]
-  right_id := by simp [IsZero.to_eq _ 0]
-  left_inv := by simp [IsZero.to_eq _ 0]
-  right_inv := by simp [IsZero.to_eq _ 0]
-
-end
-
-section
-
-variable {C : Type u} [Category.{v} C] [HasFiniteProducts C]
-variable {D : Type u'} [Category.{v'} D] [HasFiniteProducts D]
-variable (F : C ⥤ D) [PreservesFiniteProducts F]
-
-noncomputable def Functor.mapAbelianGroupObject {X : C} (G : AbelianGroupObject X) :
-    AbelianGroupObject (F.obj X) where
-  m := (PreservesLimitPair.iso F X X).inv ≫ F.map G.m
-  e := (PreservesTerminal.iso F).inv ≫ F.map G.e
-  inv := sorry
-  assoc := sorry
-  comm := sorry
-  left_id := sorry
-  right_id := sorry
-  left_inv := sorry
-  right_inv := sorry
-
-end
-
-namespace AbelianGroupObject.Types
-
-section
-
-noncomputable def add {X : Type v} (G : AbelianGroupObject X) : Add X where
-  add x y := G.m ((Types.binaryProductIso _ _).inv (x, y))
-
-noncomputable def neg {X : Type v} (G : AbelianGroupObject X) : Neg X where
-  neg x := G.inv x
-
-noncomputable def zero {X : Type v} (G : AbelianGroupObject X) : Zero X where
-  zero := G.e default
-
-protected theorem add_comm {X : Type v} (G : AbelianGroupObject X) (x y : X) :
-    letI : Add X := add G
-    x + y = y + x := by
-  dsimp only [(· + ·)]
-  rw [Add.add, add]
-  simp only
-  conv_lhs => rw [← G.comm]
-  simp
-  apply congr_arg G.m
-  apply (Types.binaryProductIso _ _).toEquiv.injective
-  ext
-  · simp [elementwise_of% (prod.lift_fst (prod.snd : X ⨯ X ⟶ X) prod.fst)]
-  · simp [elementwise_of% (prod.lift_snd (prod.snd : X ⨯ X ⟶ X) prod.fst)]
-
-end
-
-end AbelianGroupObject.Types
 
 section
 
 variable {C : Type u} [Category.{v} C] [Preadditive C] [HasFiniteBiproducts C]
 
-variable (F : C ⥤ Type v) [PreservesFiniteLimits F]
-
-section
-
-variable (X : C)
-
-attribute [local instance] hasBinaryBiproducts_of_finite_biproducts
-
-#check F.map <| Limits.biprod.desc (𝟙 X) (𝟙 X)
-
-def addCommGroup : AddCommGroup (F.obj X) := sorry
-
-end
-
-def lift (F : C ⥤ Type v) : C ⥤ AddCommGrp.{v} := sorry
-
-def liftCompForget (F : C ⥤ Type v) : lift F ⋙ forget _ ≅ F := sorry
-
-instance : PreservesFiniteLimits (lift F) := sorry
-
-def liftIso :
-    ((LeftExactFunctor.whiskeringRight _ _ _).obj (LeftExactFunctor.of (forget AddCommGrp))).obj
-      (LeftExactFunctor.of (lift F)) ≅ LeftExactFunctor.of F :=
-  InducedCategory.isoMk (liftCompForget F)
-
-end
-
-section
-
-variable {C : Type u} [Category.{v} C] [Preadditive C] [HasFiniteBiproducts C]
-
-section
-
-variable (F : C ⥤ AddCommGrp.{v}) [PreservesFiniteLimits F] (X : C)
-
-def q : F.obj X ≅ @AddCommGrp.of ((F ⋙ forget _).obj X) (addCommGroup (F ⋙ forget _) X) := sorry
-
-end
-
-instance : Functor.IsEquivalence <|
-    (LeftExactFunctor.whiskeringRight C _ _).obj ⟨forget AddCommGrp.{v}, inferInstance⟩ where
-  full := sorry
-  faithful := sorry
-  essSurj := ⟨(⟨_, ⟨liftIso ·.1⟩⟩)⟩
+attribute [local instance] hasFiniteProducts_of_hasFiniteBiproducts
+attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
+
+@[simps!]
+noncomputable def inverseAux : (C ⥤ₗ Type v) ⥤ C ⥤ AddCommGrp.{v} :=
+  Functor.mapCommGrpFunctor ⋙ (whiskeringLeft _ _ _).obj Preadditive.commGrpEquivalence.functor ⋙
+    (whiskeringRight _ _ _).obj
+      (commGrpTypeEquivalenceCommGrp.functor ⋙ commGroupAddCommGroupEquivalence.functor)
+
+instance (F : C ⥤ₗ Type v) : PreservesFiniteLimits (inverseAux.obj F) where
+  preservesFiniteLimits J _ _ :=
+    have : PreservesLimitsOfShape J (inverseAux.obj F ⋙ forget AddCommGrp) :=
+      inferInstanceAs (PreservesLimitsOfShape J F.1)
+    preservesLimitsOfShape_of_reflects_of_preserves _ (forget AddCommGrp)
+
+@[simps!]
+noncomputable def inverse : (C ⥤ₗ Type v) ⥤ (C ⥤ₗ AddCommGrp.{v}) :=
+  FullSubcategory.lift _ inverseAux inferInstance
+
+noncomputable def unitIso : 𝟭 (C ⥤ₗ AddCommGrp) ≅
+    (LeftExactFunctor.whiskeringRight _ _ _).obj (LeftExactFunctor.of (forget _)) ⋙ inverse := by
+  refine NatIso.ofComponents
+    (fun F => InducedCategory.isoMk (NatIso.ofComponents (fun X => ?_) ?_)) ?_
+  · dsimp [inverse, inverseAux]
+    
+    refine AddEquiv.toAddCommGrpIso { Equiv.refl _ with map_add' := ?_ }
+    simp
+    intro x y
+    sorry
+  · aesop_cat
+  · aesop_cat
+
+
+
+
+noncomputable def forgetEquivalence : (C ⥤ₗ AddCommGrp.{v}) ≌ (C ⥤ₗ Type v) where
+  functor := (LeftExactFunctor.whiskeringRight _ _ _).obj (LeftExactFunctor.of (forget _))
+  inverse := inverse
+  unitIso := unitIso
+  counitIso := Iso.refl _
+  functor_unitIso_comp := by aesop_cat
 
 end

From 384a483920a6cbd1139fcb8ef44833c123a48a73 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sun, 9 Feb 2025 08:44:38 +0100
Subject: [PATCH 32/57] WIP

---
 Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean |  4 ++--
 Mathlib/CategoryTheory/Limits/ExactFunctor.lean    | 12 ++++++------
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
index d227de1e586168..af1f079fd88944 100644
--- a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
+++ b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
@@ -51,8 +51,8 @@ noncomputable def unitIso : 𝟭 (C ⥤ₗ AddCommGrp) ≅
     simp
     intro x y
     sorry
-  · aesop_cat
-  · aesop_cat
+  · sorry
+  · sorry
 
 
 
diff --git a/Mathlib/CategoryTheory/Limits/ExactFunctor.lean b/Mathlib/CategoryTheory/Limits/ExactFunctor.lean
index c39bc0d0cfc333..abe9465ffd4660 100644
--- a/Mathlib/CategoryTheory/Limits/ExactFunctor.lean
+++ b/Mathlib/CategoryTheory/Limits/ExactFunctor.lean
@@ -215,7 +215,7 @@ section
 variable (C D E)
 
 /-- Whiskering a left exact functor by a left exact functor yields a left exact functor. -/
-@[simps!]
+@[simps! obj_obj obj_map map_app_app]
 def LeftExactFunctor.whiskeringLeft : (C ⥤ₗ D) ⥤ (D ⥤ₗ E) ⥤ (C ⥤ₗ E) where
   obj F := FullSubcategory.lift _ (forget _ _ ⋙ (CategoryTheory.whiskeringLeft C D E).obj F.obj)
     (fun G => by dsimp; exact comp_preservesFiniteLimits _ _)
@@ -230,7 +230,7 @@ def LeftExactFunctor.whiskeringLeft : (C ⥤ₗ D) ⥤ (D ⥤ₗ E) ⥤ (C ⥤
     aesop_cat
 
 /-- Whiskering a left exact functor by a left exact functor yields a left exact functor. -/
-@[simps!]
+@[simps! obj_obj obj_map map_app_app]
 def LeftExactFunctor.whiskeringRight : (D ⥤ₗ E) ⥤ (C ⥤ₗ D) ⥤ (C ⥤ₗ E) where
   obj F := FullSubcategory.lift _ (forget _ _ ⋙ (CategoryTheory.whiskeringRight C D E).obj F.obj)
     (fun G => by dsimp; exact comp_preservesFiniteLimits _ _)
@@ -245,7 +245,7 @@ def LeftExactFunctor.whiskeringRight : (D ⥤ₗ E) ⥤ (C ⥤ₗ D) ⥤ (C ⥤
     aesop_cat
 
 /-- Whiskering a right exact functor by a right exact functor yields a right exact functor. -/
-@[simps!]
+@[simps! obj_obj obj_map map_app_app]
 def RightExactFunctor.whiskeringLeft : (C ⥤ᵣ D) ⥤ (D ⥤ᵣ E) ⥤ (C ⥤ᵣ E) where
   obj F := FullSubcategory.lift _ (forget _ _ ⋙ (CategoryTheory.whiskeringLeft C D E).obj F.obj)
     (fun G => by dsimp; exact comp_preservesFiniteColimits _ _)
@@ -260,7 +260,7 @@ def RightExactFunctor.whiskeringLeft : (C ⥤ᵣ D) ⥤ (D ⥤ᵣ E) ⥤ (C ⥤
     aesop_cat
 
 /-- Whiskering a right exact functor by a right exact functor yields a right exact functor. -/
-@[simps!]
+@[simps! obj_obj obj_map map_app_app]
 def RightExactFunctor.whiskeringRight : (D ⥤ᵣ E) ⥤ (C ⥤ᵣ D) ⥤ (C ⥤ᵣ E) where
   obj F := FullSubcategory.lift _ (forget _ _ ⋙ (CategoryTheory.whiskeringRight C D E).obj F.obj)
     (fun G => by dsimp; exact comp_preservesFiniteColimits _ _)
@@ -275,7 +275,7 @@ def RightExactFunctor.whiskeringRight : (D ⥤ᵣ E) ⥤ (C ⥤ᵣ D) ⥤ (C ⥤
     aesop_cat
 
 /-- Whiskering an exact functor by an exact functor yields an exact functor. -/
-@[simps!]
+@[simps! obj_obj obj_map map_app_app]
 def ExactFunctor.whiskeringLeft : (C ⥤ₑ D) ⥤ (D ⥤ₑ E) ⥤ (C ⥤ₑ E) where
   obj F := FullSubcategory.lift _ (forget _ _ ⋙ (CategoryTheory.whiskeringLeft C D E).obj F.obj)
     (fun G => ⟨by dsimp; exact comp_preservesFiniteLimits _ _,
@@ -291,7 +291,7 @@ def ExactFunctor.whiskeringLeft : (C ⥤ₑ D) ⥤ (D ⥤ₑ E) ⥤ (C ⥤ₑ E)
     aesop_cat
 
 /-- Whiskering an exact functor by an exact functor yields an exact functor. -/
-@[simps!]
+@[simps! obj_obj obj_map map_app_app]
 def ExactFunctor.whiskeringRight : (D ⥤ₑ E) ⥤ (C ⥤ₑ D) ⥤ (C ⥤ₑ E) where
   obj F := FullSubcategory.lift _ (forget _ _ ⋙ (CategoryTheory.whiskeringRight C D E).obj F.obj)
     (fun G => ⟨by dsimp; exact comp_preservesFiniteLimits _ _,

From 284fdf7669201943ab57f3906f930054c080fdd2 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sun, 9 Feb 2025 16:43:06 +0100
Subject: [PATCH 33/57] sorry-free?!

---
 Mathlib.lean                                  |  2 +
 .../Category/Grp/ChosenFiniteProducts.lean    | 36 +++++++++++++
 .../Category/Grp/LeftExactFunctor.lean        | 54 +++++++++++++------
 .../CategoryTheory/ChosenFiniteProducts.lean  | 14 +++++
 .../Monoidal/Internal/Types/CommGrp_.lean     | 12 +++++
 5 files changed, 103 insertions(+), 15 deletions(-)
 create mode 100644 Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index ddd44db7e4cfbc..c89fb1315ba271 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -84,6 +84,7 @@ import Mathlib.Algebra.Category.Grp.Abelian
 import Mathlib.Algebra.Category.Grp.Adjunctions
 import Mathlib.Algebra.Category.Grp.Basic
 import Mathlib.Algebra.Category.Grp.Biproducts
+import Mathlib.Algebra.Category.Grp.ChosenFiniteProducts
 import Mathlib.Algebra.Category.Grp.Colimits
 import Mathlib.Algebra.Category.Grp.EnoughInjectives
 import Mathlib.Algebra.Category.Grp.EpiMono
@@ -95,6 +96,7 @@ import Mathlib.Algebra.Category.Grp.Images
 import Mathlib.Algebra.Category.Grp.Injective
 import Mathlib.Algebra.Category.Grp.Kernels
 import Mathlib.Algebra.Category.Grp.LargeColimits
+import Mathlib.Algebra.Category.Grp.LeftExactFunctor
 import Mathlib.Algebra.Category.Grp.Limits
 import Mathlib.Algebra.Category.Grp.Preadditive
 import Mathlib.Algebra.Category.Grp.Subobject
diff --git a/Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean b/Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean
new file mode 100644
index 00000000000000..ff3a117ed15a62
--- /dev/null
+++ b/Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean
@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.ChosenFiniteProducts
+import Mathlib.Algebra.Category.Grp.Biproducts
+import Mathlib.Algebra.Category.Grp.Zero
+import Mathlib.CategoryTheory.Monoidal.Types.Basic
+
+/-!
+# Chosen finite products for `AddCommGrp.{u}`.
+-/
+
+universe u
+
+open CategoryTheory MonoidalCategory
+
+namespace AddCommGrp
+
+/-- We choose `AddCommGrp.of (X × Y)` as the product of `X` and `Y` and `AddCommGrp.of PUnit` as
+the terminal object. -/
+noncomputable instance : ChosenFiniteProducts AddCommGrp.{u} where
+  product X Y := binaryProductLimitCone X Y
+  terminal := ⟨_, (isZero_of_subsingleton (AddCommGrp.of PUnit.{u + 1})).isTerminal⟩
+
+attribute [local instance] Functor.monoidalOfChosenFiniteProducts
+
+-- TODO: is this evil??
+theorem μ_forget_apply {X Y : AddCommGrp.{u}} (p : X) (q : Y) :
+    Functor.LaxMonoidal.μ (forget AddCommGrp.{u}) X Y (p, q) = (p, q) := by
+  apply Prod.ext
+  · exact congrFun (Functor.Monoidal.μ_fst (forget AddCommGrp.{u}) (X := X) (Y := Y)) (p, q)
+  · exact congrFun (Functor.Monoidal.μ_snd (forget AddCommGrp.{u}) (X := X) (Y := Y)) (p, q)
+
+end AddCommGrp
diff --git a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
index af1f079fd88944..90a9757e3128fb 100644
--- a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
+++ b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
@@ -6,26 +6,30 @@ Authors: Markus Himmel
 import Mathlib.CategoryTheory.Limits.ExactFunctor
 import Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_
 import Mathlib.CategoryTheory.Preadditive.CommGrp_
+import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
 import Mathlib.Algebra.Category.Grp.Limits
 import Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
+import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
+import Mathlib.Algebra.Category.Grp.ChosenFiniteProducts
 
 /-!
 # The forgetful functor `(C ⥤ₗ AddCommGroup) ⥤ (C ⥤ₗ Type v)` is an equivalence
 -/
 
-open CategoryTheory Limits
+open CategoryTheory MonoidalCategory Limits
 
 universe v v' u u'
 
-
 section
 
 variable {C : Type u} [Category.{v} C] [Preadditive C] [HasFiniteBiproducts C]
 
 attribute [local instance] hasFiniteProducts_of_hasFiniteBiproducts
-attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
+-- attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
+
+noncomputable local instance : ChosenFiniteProducts C :=
+  ChosenFiniteProducts.ofFiniteProducts _
 
-@[simps!]
 noncomputable def inverseAux : (C ⥤ₗ Type v) ⥤ C ⥤ AddCommGrp.{v} :=
   Functor.mapCommGrpFunctor ⋙ (whiskeringLeft _ _ _).obj Preadditive.commGrpEquivalence.functor ⋙
     (whiskeringRight _ _ _).obj
@@ -37,25 +41,45 @@ instance (F : C ⥤ₗ Type v) : PreservesFiniteLimits (inverseAux.obj F) where
       inferInstanceAs (PreservesLimitsOfShape J F.1)
     preservesLimitsOfShape_of_reflects_of_preserves _ (forget AddCommGrp)
 
-@[simps!]
 noncomputable def inverse : (C ⥤ₗ Type v) ⥤ (C ⥤ₗ AddCommGrp.{v}) :=
   FullSubcategory.lift _ inverseAux inferInstance
 
+noncomputable def preIso (F : C ⥤ AddCommGrp.{v}) [PreservesFiniteLimits F] (X : C) :
+    commGrpTypeEquivalenceCommGrp.inverse.obj (AddCommGrp.toCommGrp.obj (F.obj X)) ≅
+      (F ⋙ forget AddCommGrp).mapCommGrp.obj (Preadditive.commGrpEquivalence.functor.obj X) := by
+  refine CommGrp_.mkIso ?_ ?_ ?_
+  · dsimp
+    exact Multiplicative.toAdd.toIso
+  · dsimp
+    ext x
+    simp
+    erw [toAdd_one]
+  · dsimp [-ConcreteCategory.forget_map_eq_coe, -AddCommGrp.forget_map, -Functor.comp_map]
+    have : HasZeroObject AddCommGrp.{v} := hasZeroObject_of_hasTerminal_object
+    have : F.Additive := Functor.additive_of_preserves_binary_products _
+    rw [Functor.comp_map, F.map_add,
+      Functor.Monoidal.μ_comp F (forget AddCommGrp.{v}) (X := X) (Y := X),
+      Category.assoc, ← Functor.map_comp, Preadditive.comp_add, Functor.Monoidal.μ_fst,
+      Functor.Monoidal.μ_snd]
+    ext ⟨p, q⟩
+    simp
+    erw [toAdd_mul]
+    simp only [AddCommGrp.μ_forget_apply]
+    rfl
+
 noncomputable def unitIso : 𝟭 (C ⥤ₗ AddCommGrp) ≅
     (LeftExactFunctor.whiskeringRight _ _ _).obj (LeftExactFunctor.of (forget _)) ⋙ inverse := by
   refine NatIso.ofComponents
     (fun F => InducedCategory.isoMk (NatIso.ofComponents (fun X => ?_) ?_)) ?_
   · dsimp [inverse, inverseAux]
-    
-    refine AddEquiv.toAddCommGrpIso { Equiv.refl _ with map_add' := ?_ }
-    simp
-    intro x y
-    sorry
-  · sorry
-  · sorry
-
-
-
+    let q :=
+      CommGrp.toAddCommGrp.mapIso (CommGrpTypeEquivalenceCommGrp.functor.mapIso (preIso F.obj X))
+    refine ?_ ≪≫ q
+    refine ?_ ≪≫ (CommGrp.toAddCommGrp.mapIso
+      (commGrpTypeEquivalenceCommGrp.counitIso.app (AddCommGrp.toCommGrp.obj (F.obj.obj X)))).symm
+    exact commGroupAddCommGroupEquivalence.counitIso.app _
+  · aesop_cat
+  · aesop_cat
 
 noncomputable def forgetEquivalence : (C ⥤ₗ AddCommGrp.{v}) ≌ (C ⥤ₗ Type v) where
   functor := (LeftExactFunctor.whiskeringRight _ _ _).obj (LeftExactFunctor.of (forget _))
diff --git a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
index 3de3eb0ec737c3..41f226aacbf372 100644
--- a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
+++ b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@@ -651,6 +651,20 @@ lemma μ_fst {X Y : C} : LaxMonoidal.μ F X Y ≫ F.map (fst X Y) = fst (F.obj X
 lemma μ_snd {X Y : C} : LaxMonoidal.μ F X Y ≫ F.map (snd X Y) = snd (F.obj X) (F.obj Y) :=
   (cancel_epi (μIso _ _ _).inv).1 (by simp)
 
+section
+
+variable {E : Type u₂} [Category.{v₂} E] [ChosenFiniteProducts E] (G : D ⥤ E)
+  [PreservesFiniteProducts G]
+
+attribute [-instance] Functor.LaxMonoidal.comp Functor.Monoidal.instComp
+
+@[reassoc (attr := simp)]
+lemma μ_comp {X Y : C} :
+    LaxMonoidal.μ (F ⋙ G) X Y = LaxMonoidal.μ G _ _ ≫ G.map (LaxMonoidal.μ F X Y) := by
+  apply (cancel_mono (μIso _ _ _).inv).1
+  apply ChosenFiniteProducts.hom_ext <;> simp [← Functor.comp_obj, ← Functor.map_comp]
+
+end
 
 end
 
diff --git a/Mathlib/CategoryTheory/Monoidal/Internal/Types/CommGrp_.lean b/Mathlib/CategoryTheory/Monoidal/Internal/Types/CommGrp_.lean
index 8ea54ddc19b889..27c0e9ea274a8b 100644
--- a/Mathlib/CategoryTheory/Monoidal/Internal/Types/CommGrp_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Internal/Types/CommGrp_.lean
@@ -31,6 +31,7 @@ noncomputable def functor : CommGrp_ (Type u) ⥤ CommGrp.{u} where
   map f := CommGrp.ofHom (GrpTypeEquivalenceGrp.functor.map f).hom
 
 /-- Converting a group into a group object in `Type u`. -/
+--@[simps!?]
 noncomputable def inverse : CommGrp.{u} ⥤ CommGrp_ (Type u) where
   obj A :=
     { grpTypeEquivalenceGrp.inverse.obj ((forget₂ CommGrp Grp).obj A) with
@@ -39,10 +40,21 @@ noncomputable def inverse : CommGrp.{u} ⥤ CommGrp_ (Type u) where
         exact CommMonoid.mul_comm y x }
   map f := GrpTypeEquivalenceGrp.inverse.map ((forget₂ CommGrp Grp).map f)
 
+@[simp]
+theorem inverse_obj_X {A : CommGrp.{u}} : (inverse.obj A).X = A := rfl
+@[simp]
+theorem inverse_obj_one {A : CommGrp.{u}} {x} : (inverse.obj A).one x = (1 : A) := rfl
+@[simp]
+theorem inverse_obj_mul {A : CommGrp.{u}} {p} : (inverse.obj A).mul p = (p.1 : A) * p.2 := rfl
+@[simp]
+theorem inverse_obj_inv {A : CommGrp.{u}} {x} : (inverse.obj A).inv x = (x : A)⁻¹ := rfl
+
+
 end CommGrpTypeEquivalenceCommGrp
 
 /-- The category of commutative group objects in `Type u` is equivalent to the category of
 commutative groups. -/
+@[simps]
 noncomputable def commGrpTypeEquivalenceCommGrp : CommGrp_ (Type u) ≌ CommGrp.{u} where
   functor := CommGrpTypeEquivalenceCommGrp.functor
   inverse := CommGrpTypeEquivalenceCommGrp.inverse

From 75256b265660d546c4b5c934372ce6c5c28e4cd4 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sun, 9 Feb 2025 16:52:14 +0100
Subject: [PATCH 34/57] Going to try the multiplicative version now

---
 Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
index 90a9757e3128fb..1d5d4ed85c03e2 100644
--- a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
+++ b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
@@ -25,11 +25,11 @@ section
 variable {C : Type u} [Category.{v} C] [Preadditive C] [HasFiniteBiproducts C]
 
 attribute [local instance] hasFiniteProducts_of_hasFiniteBiproducts
--- attribute [local instance] ChosenFiniteProducts.ofFiniteProducts
 
 noncomputable local instance : ChosenFiniteProducts C :=
   ChosenFiniteProducts.ofFiniteProducts _
 
+/-- Implementation, see `forgetEquivalence`. -/
 noncomputable def inverseAux : (C ⥤ₗ Type v) ⥤ C ⥤ AddCommGrp.{v} :=
   Functor.mapCommGrpFunctor ⋙ (whiskeringLeft _ _ _).obj Preadditive.commGrpEquivalence.functor ⋙
     (whiskeringRight _ _ _).obj
@@ -41,9 +41,11 @@ instance (F : C ⥤ₗ Type v) : PreservesFiniteLimits (inverseAux.obj F) where
       inferInstanceAs (PreservesLimitsOfShape J F.1)
     preservesLimitsOfShape_of_reflects_of_preserves _ (forget AddCommGrp)
 
+/-- Implementation, see `forgetEquivalence`. -/
 noncomputable def inverse : (C ⥤ₗ Type v) ⥤ (C ⥤ₗ AddCommGrp.{v}) :=
   FullSubcategory.lift _ inverseAux inferInstance
 
+/-- Implementation, see `forgetEquivalence`. -/
 noncomputable def preIso (F : C ⥤ AddCommGrp.{v}) [PreservesFiniteLimits F] (X : C) :
     commGrpTypeEquivalenceCommGrp.inverse.obj (AddCommGrp.toCommGrp.obj (F.obj X)) ≅
       (F ⋙ forget AddCommGrp).mapCommGrp.obj (Preadditive.commGrpEquivalence.functor.obj X) := by
@@ -67,6 +69,7 @@ noncomputable def preIso (F : C ⥤ AddCommGrp.{v}) [PreservesFiniteLimits F] (X
     simp only [AddCommGrp.μ_forget_apply]
     rfl
 
+/-- Implementation, see `forgetEquivalence`. -/
 noncomputable def unitIso : 𝟭 (C ⥤ₗ AddCommGrp) ≅
     (LeftExactFunctor.whiskeringRight _ _ _).obj (LeftExactFunctor.of (forget _)) ⋙ inverse := by
   refine NatIso.ofComponents
@@ -81,11 +84,18 @@ noncomputable def unitIso : 𝟭 (C ⥤ₗ AddCommGrp) ≅
   · aesop_cat
   · aesop_cat
 
+/-- To construct a functor from `C ⥤ₗ Type v` to `C ⥤ₗ AddCommGrp.{v}`, notice that a left-exact
+functor `F : C ⥤ Type v` induces a functor `CommGrp_ C ⥤ CommGrp_ (Type v)`. But `CommGrp_ C` is
+equivalent to `C`, and `CommGrp_ (Type v)` is equivalent to `AddCommGrp.{v}`, so we turn this
+into a functor `C ⥤ AddCommGrp.{v}`. By construction, composing with with the forgetful
+functor recovers the functor we started with, so since the forgetful functor reflects finite
+limits and `F` preserves finite limits, our constructed functor also preserves finite limits. It
+can be shown that this construction gives a quasi-inverse to the whiskering operation
+`(C ⥤ₗ AddCommGrp.{v}) ⥤ (C ⥤ₗ Type v)`. -/
 noncomputable def forgetEquivalence : (C ⥤ₗ AddCommGrp.{v}) ≌ (C ⥤ₗ Type v) where
   functor := (LeftExactFunctor.whiskeringRight _ _ _).obj (LeftExactFunctor.of (forget _))
   inverse := inverse
   unitIso := unitIso
   counitIso := Iso.refl _
-  functor_unitIso_comp := by aesop_cat
 
 end

From 4799598ecc04dcc592d9635d6f1dcb3abc77b80c Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sun, 9 Feb 2025 17:05:47 +0100
Subject: [PATCH 35/57] Cleanup

---
 .../Category/Grp/ChosenFiniteProducts.lean    |  2 +-
 .../Category/Grp/LeftExactFunctor.lean        | 65 +++++++------------
 2 files changed, 26 insertions(+), 41 deletions(-)

diff --git a/Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean b/Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean
index ff3a117ed15a62..9f869480a2cb19 100644
--- a/Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean
+++ b/Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean
@@ -26,7 +26,7 @@ noncomputable instance : ChosenFiniteProducts AddCommGrp.{u} where
 
 attribute [local instance] Functor.monoidalOfChosenFiniteProducts
 
--- TODO: is this evil??
+@[simp]
 theorem μ_forget_apply {X Y : AddCommGrp.{u}} (p : X) (q : Y) :
     Functor.LaxMonoidal.μ (forget AddCommGrp.{u}) X Y (p, q) = (p, q) := by
   apply Prod.ext
diff --git a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
index 1d5d4ed85c03e2..c09c6446da3d87 100644
--- a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
+++ b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
@@ -3,17 +3,16 @@ Copyright (c) 2025 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-import Mathlib.CategoryTheory.Limits.ExactFunctor
+import Mathlib.Algebra.Category.Grp.ChosenFiniteProducts
+import Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
 import Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_
-import Mathlib.CategoryTheory.Preadditive.CommGrp_
 import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
-import Mathlib.Algebra.Category.Grp.Limits
-import Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
-import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
-import Mathlib.Algebra.Category.Grp.ChosenFiniteProducts
+import Mathlib.CategoryTheory.Preadditive.CommGrp_
 
 /-!
 # The forgetful functor `(C ⥤ₗ AddCommGroup) ⥤ (C ⥤ₗ Type v)` is an equivalence
+
+We construct a quasi-inverse for the 
 -/
 
 open CategoryTheory MonoidalCategory Limits
@@ -26,7 +25,7 @@ variable {C : Type u} [Category.{v} C] [Preadditive C] [HasFiniteBiproducts C]
 
 attribute [local instance] hasFiniteProducts_of_hasFiniteBiproducts
 
-noncomputable local instance : ChosenFiniteProducts C :=
+private noncomputable local instance : ChosenFiniteProducts C :=
   ChosenFiniteProducts.ofFiniteProducts _
 
 /-- Implementation, see `forgetEquivalence`. -/
@@ -45,44 +44,30 @@ instance (F : C ⥤ₗ Type v) : PreservesFiniteLimits (inverseAux.obj F) where
 noncomputable def inverse : (C ⥤ₗ Type v) ⥤ (C ⥤ₗ AddCommGrp.{v}) :=
   FullSubcategory.lift _ inverseAux inferInstance
 
-/-- Implementation, see `forgetEquivalence`. -/
-noncomputable def preIso (F : C ⥤ AddCommGrp.{v}) [PreservesFiniteLimits F] (X : C) :
+/-- Implementation, see `forgetEquivalence`.
+This is the complicated bit, where we show that forgetting the group structure in the image of
+`F` and then reconstructing it recovers the group structure we started with. -/
+noncomputable def unitIsoAux (F : C ⥤ AddCommGrp.{v}) [PreservesFiniteLimits F] (X : C) :
     commGrpTypeEquivalenceCommGrp.inverse.obj (AddCommGrp.toCommGrp.obj (F.obj X)) ≅
       (F ⋙ forget AddCommGrp).mapCommGrp.obj (Preadditive.commGrpEquivalence.functor.obj X) := by
-  refine CommGrp_.mkIso ?_ ?_ ?_
-  · dsimp
-    exact Multiplicative.toAdd.toIso
-  · dsimp
-    ext x
-    simp
-    erw [toAdd_one]
-  · dsimp [-ConcreteCategory.forget_map_eq_coe, -AddCommGrp.forget_map, -Functor.comp_map]
-    have : HasZeroObject AddCommGrp.{v} := hasZeroObject_of_hasTerminal_object
-    have : F.Additive := Functor.additive_of_preserves_binary_products _
-    rw [Functor.comp_map, F.map_add,
-      Functor.Monoidal.μ_comp F (forget AddCommGrp.{v}) (X := X) (Y := X),
-      Category.assoc, ← Functor.map_comp, Preadditive.comp_add, Functor.Monoidal.μ_fst,
-      Functor.Monoidal.μ_snd]
-    ext ⟨p, q⟩
-    simp
-    erw [toAdd_mul]
-    simp only [AddCommGrp.μ_forget_apply]
-    rfl
+  refine CommGrp_.mkIso Multiplicative.toAdd.toIso (by aesop_cat) ?_
+  dsimp [-Functor.comp_map]
+  have : F.Additive := Functor.additive_of_preserves_binary_products _
+  rw [Functor.comp_map, F.map_add,
+    Functor.Monoidal.μ_comp F (forget AddCommGrp.{v}) (X := X) (Y := X),
+    Category.assoc, ← Functor.map_comp, Preadditive.comp_add, Functor.Monoidal.μ_fst,
+    Functor.Monoidal.μ_snd]
+  aesop_cat
 
 /-- Implementation, see `forgetEquivalence`. -/
 noncomputable def unitIso : 𝟭 (C ⥤ₗ AddCommGrp) ≅
-    (LeftExactFunctor.whiskeringRight _ _ _).obj (LeftExactFunctor.of (forget _)) ⋙ inverse := by
-  refine NatIso.ofComponents
-    (fun F => InducedCategory.isoMk (NatIso.ofComponents (fun X => ?_) ?_)) ?_
-  · dsimp [inverse, inverseAux]
-    let q :=
-      CommGrp.toAddCommGrp.mapIso (CommGrpTypeEquivalenceCommGrp.functor.mapIso (preIso F.obj X))
-    refine ?_ ≪≫ q
-    refine ?_ ≪≫ (CommGrp.toAddCommGrp.mapIso
-      (commGrpTypeEquivalenceCommGrp.counitIso.app (AddCommGrp.toCommGrp.obj (F.obj.obj X)))).symm
-    exact commGroupAddCommGroupEquivalence.counitIso.app _
-  · aesop_cat
-  · aesop_cat
+    (LeftExactFunctor.whiskeringRight _ _ _).obj (LeftExactFunctor.of (forget _)) ⋙ inverse :=
+  NatIso.ofComponents (fun F => InducedCategory.isoMk (NatIso.ofComponents (fun X =>
+    commGroupAddCommGroupEquivalence.counitIso.app _ ≪≫
+      (CommGrp.toAddCommGrp.mapIso (commGrpTypeEquivalenceCommGrp.counitIso.app
+        (AddCommGrp.toCommGrp.obj (F.obj.obj X)))).symm ≪≫
+      CommGrp.toAddCommGrp.mapIso
+        (CommGrpTypeEquivalenceCommGrp.functor.mapIso (unitIsoAux F.obj X)))))
 
 /-- To construct a functor from `C ⥤ₗ Type v` to `C ⥤ₗ AddCommGrp.{v}`, notice that a left-exact
 functor `F : C ⥤ Type v` induces a functor `CommGrp_ C ⥤ CommGrp_ (Type v)`. But `CommGrp_ C` is

From 09788fa9e685cbc2f6c27d7b67208ff19be4c1de Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sun, 9 Feb 2025 17:37:03 +0100
Subject: [PATCH 36/57] Done?!?!

---
 Mathlib.lean                                  |  2 +
 .../Category/Grp/LeftExactFunctor.lean        |  7 +++-
 .../GrothendieckAxioms/Indization.lean        | 16 ++++++++
 .../CategoryTheory/Abelian/Indization.lean    | 39 +++++++++++++++++++
 .../CategoryTheory/Generator/Indization.lean  | 10 +++++
 .../Preadditive/Indization.lean               | 30 ++++++++++++++
 6 files changed, 103 insertions(+), 1 deletion(-)
 create mode 100644 Mathlib/CategoryTheory/Abelian/Indization.lean
 create mode 100644 Mathlib/CategoryTheory/Preadditive/Indization.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index c89fb1315ba271..659ed9ef660677 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1674,6 +1674,7 @@ import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf
 import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types
 import Mathlib.CategoryTheory.Abelian.GrothendieckCategory
 import Mathlib.CategoryTheory.Abelian.Images
+import Mathlib.CategoryTheory.Abelian.Indization
 import Mathlib.CategoryTheory.Abelian.Injective
 import Mathlib.CategoryTheory.Abelian.InjectiveResolution
 import Mathlib.CategoryTheory.Abelian.LeftDerived
@@ -2175,6 +2176,7 @@ import Mathlib.CategoryTheory.Preadditive.EilenbergMoore
 import Mathlib.CategoryTheory.Preadditive.EndoFunctor
 import Mathlib.CategoryTheory.Preadditive.FunctorCategory
 import Mathlib.CategoryTheory.Preadditive.HomOrthogonal
+import Mathlib.CategoryTheory.Preadditive.Indization
 import Mathlib.CategoryTheory.Preadditive.Injective
 import Mathlib.CategoryTheory.Preadditive.InjectiveResolution
 import Mathlib.CategoryTheory.Preadditive.LeftExact
diff --git a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
index c09c6446da3d87..a71f7cdbf4f795 100644
--- a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
+++ b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
@@ -12,13 +12,16 @@ import Mathlib.CategoryTheory.Preadditive.CommGrp_
 /-!
 # The forgetful functor `(C ⥤ₗ AddCommGroup) ⥤ (C ⥤ₗ Type v)` is an equivalence
 
-We construct a quasi-inverse for the 
+We construct a quasi-inverse for the
 -/
 
 open CategoryTheory MonoidalCategory Limits
 
+
 universe v v' u u'
 
+namespace AddCommGrp
+
 section
 
 variable {C : Type u} [Category.{v} C] [Preadditive C] [HasFiniteBiproducts C]
@@ -84,3 +87,5 @@ noncomputable def forgetEquivalence : (C ⥤ₗ AddCommGrp.{v}) ≌ (C ⥤ₗ Ty
   counitIso := Iso.refl _
 
 end
+
+end AddCommGrp
diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean
index 660fbca91cfe69..0472fd97b1127e 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean
@@ -5,7 +5,10 @@ Authors: Markus Himmel
 -/
 import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory
 import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types
+import Mathlib.CategoryTheory.Abelian.Indization
 import Mathlib.CategoryTheory.Limits.Indization.Category
+import Mathlib.CategoryTheory.Generator.Indization
+import Mathlib.CategoryTheory.Abelian.GrothendieckCategory
 
 /-!
 # AB axioms in the category of ind-objects
@@ -17,6 +20,8 @@ universe v u
 
 namespace CategoryTheory.Limits
 
+section
+
 variable {C : Type u} [Category.{v} C]
 
 instance {J : Type v} [SmallCategory J] [IsFiltered J] [HasFiniteLimits C] :
@@ -26,4 +31,15 @@ instance {J : Type v} [SmallCategory J] [IsFiltered J] [HasFiniteLimits C] :
 instance [HasFiniteLimits C] : AB5 (Ind C) where
   ofShape _ _ _ := inferInstance
 
+end
+
+section
+
+variable {C : Type u} [SmallCategory C] [Abelian C]
+
+instance isGrothendieckAbelian_ind : IsGrothendieckAbelian.{u} (Ind C) where
+  hasSeparator := ⟨⟨_, Ind.isSeparator_range_yoneda⟩⟩
+
+end
+
 end CategoryTheory.Limits
diff --git a/Mathlib/CategoryTheory/Abelian/Indization.lean b/Mathlib/CategoryTheory/Abelian/Indization.lean
new file mode 100644
index 00000000000000..67c9ce26579891
--- /dev/null
+++ b/Mathlib/CategoryTheory/Abelian/Indization.lean
@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.Preadditive.Indization
+import Mathlib.CategoryTheory.Abelian.FunctorCategory
+import Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
+
+/-!
+# The category of ind-objects is abelian
+-/
+
+universe v
+
+open CategoryTheory.Abelian
+
+namespace CategoryTheory
+
+variable {C : Type v} [SmallCategory C] [Abelian C]
+
+instance {X Y : Ind C} (f : X ⟶ Y) : IsIso (Abelian.coimageImageComparison f) := by
+  obtain ⟨I, _, _, F, G, ϕ, ⟨i⟩⟩ := Ind.exists_nonempty_arrow_mk_iso_ind_lim (f := f)
+  let i' := coimageImageComparisonFunctor.mapIso i
+  dsimp at i'
+  rw [Arrow.isIso_iff_isIso_of_isIso i'.hom]
+  have : Limits.HasFiniteBiproducts (Ind C) :=
+    Limits.HasFiniteBiproducts.of_hasFiniteCoproducts
+  have : Limits.HasZeroObject (Ind C) :=
+    Limits.hasZeroObject_of_hasFiniteBiproducts _
+  have : (Ind.lim I (C := C)).PreservesZeroMorphisms :=
+    Functor.preservesZeroMorphisms_of_preserves_terminal_object
+  rw [Arrow.isIso_iff_isIso_of_isIso (PreservesCoimageImageComparison.iso (Ind.lim I) ϕ).inv]
+  infer_instance
+
+noncomputable instance : Abelian (Ind C) :=
+  .ofCoimageImageComparisonIsIso
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Generator/Indization.lean b/Mathlib/CategoryTheory/Generator/Indization.lean
index 4c79e7d781802e..20ca172a335cc2 100644
--- a/Mathlib/CategoryTheory/Generator/Indization.lean
+++ b/Mathlib/CategoryTheory/Generator/Indization.lean
@@ -5,6 +5,7 @@ Authors: Markus Himmel
 -/
 import Mathlib.CategoryTheory.Generator.Basic
 import Mathlib.CategoryTheory.Limits.Indization.Category
+import Mathlib.CategoryTheory.Preadditive.Indization
 
 /-!
 # Separating set in the category of ind-objects
@@ -34,4 +35,13 @@ theorem Ind.isSeparating_range_yoneda : IsSeparating (Set.range (Ind.yoneda : C
 
 end
 
+section
+
+variable {C : Type u} [SmallCategory C] [Preadditive C] [HasFiniteColimits C]
+
+theorem Ind.isSeparator_range_yoneda : IsSeparator (∐ (Ind.yoneda : C ⥤ _).obj) :=
+  Ind.isSeparating_range_yoneda.isSeparator_coproduct
+
+end
+
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Preadditive/Indization.lean b/Mathlib/CategoryTheory/Preadditive/Indization.lean
new file mode 100644
index 00000000000000..53673046d5d92b
--- /dev/null
+++ b/Mathlib/CategoryTheory/Preadditive/Indization.lean
@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.Limits.Indization.Category
+import Mathlib.CategoryTheory.Preadditive.Transfer
+import Mathlib.CategoryTheory.Preadditive.Opposite
+import Mathlib.Algebra.Category.Grp.LeftExactFunctor
+
+/-!
+# The category of ind-objects is preadditive
+-/
+
+universe v u
+
+open CategoryTheory Limits
+
+namespace CategoryTheory
+
+variable {C : Type u} [SmallCategory C] [Preadditive C] [HasFiniteColimits C]
+
+attribute [local instance] HasFiniteBiproducts.of_hasFiniteCoproducts
+
+noncomputable instance : Preadditive (Ind C) :=
+  .ofFullyFaithful (((Ind.leftExactFunctorEquivalence C).trans
+    AddCommGrp.forgetEquivalence.symm).fullyFaithfulFunctor.comp
+      (fullyFaithfulFullSubcategoryInclusion _))
+
+end CategoryTheory

From 1c6cd7041109a80c976d60e4d27e8e9455165c83 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Mon, 17 Feb 2025 06:48:07 +0100
Subject: [PATCH 37/57] Import

---
 Mathlib.lean                                  |  1 +
 .../Category/Grp/LeftExactFunctor.lean        | 91 +++++++++++++++++++
 2 files changed, 92 insertions(+)
 create mode 100644 Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 64ecbeeab2c99b..1e90eff2703c73 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -97,6 +97,7 @@ import Mathlib.Algebra.Category.Grp.Images
 import Mathlib.Algebra.Category.Grp.Injective
 import Mathlib.Algebra.Category.Grp.Kernels
 import Mathlib.Algebra.Category.Grp.LargeColimits
+import Mathlib.Algebra.Category.Grp.LeftExactFunctor
 import Mathlib.Algebra.Category.Grp.Limits
 import Mathlib.Algebra.Category.Grp.Preadditive
 import Mathlib.Algebra.Category.Grp.Subobject
diff --git a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
new file mode 100644
index 00000000000000..a71f7cdbf4f795
--- /dev/null
+++ b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
@@ -0,0 +1,91 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.Algebra.Category.Grp.ChosenFiniteProducts
+import Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
+import Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_
+import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
+import Mathlib.CategoryTheory.Preadditive.CommGrp_
+
+/-!
+# The forgetful functor `(C ⥤ₗ AddCommGroup) ⥤ (C ⥤ₗ Type v)` is an equivalence
+
+We construct a quasi-inverse for the
+-/
+
+open CategoryTheory MonoidalCategory Limits
+
+
+universe v v' u u'
+
+namespace AddCommGrp
+
+section
+
+variable {C : Type u} [Category.{v} C] [Preadditive C] [HasFiniteBiproducts C]
+
+attribute [local instance] hasFiniteProducts_of_hasFiniteBiproducts
+
+private noncomputable local instance : ChosenFiniteProducts C :=
+  ChosenFiniteProducts.ofFiniteProducts _
+
+/-- Implementation, see `forgetEquivalence`. -/
+noncomputable def inverseAux : (C ⥤ₗ Type v) ⥤ C ⥤ AddCommGrp.{v} :=
+  Functor.mapCommGrpFunctor ⋙ (whiskeringLeft _ _ _).obj Preadditive.commGrpEquivalence.functor ⋙
+    (whiskeringRight _ _ _).obj
+      (commGrpTypeEquivalenceCommGrp.functor ⋙ commGroupAddCommGroupEquivalence.functor)
+
+instance (F : C ⥤ₗ Type v) : PreservesFiniteLimits (inverseAux.obj F) where
+  preservesFiniteLimits J _ _ :=
+    have : PreservesLimitsOfShape J (inverseAux.obj F ⋙ forget AddCommGrp) :=
+      inferInstanceAs (PreservesLimitsOfShape J F.1)
+    preservesLimitsOfShape_of_reflects_of_preserves _ (forget AddCommGrp)
+
+/-- Implementation, see `forgetEquivalence`. -/
+noncomputable def inverse : (C ⥤ₗ Type v) ⥤ (C ⥤ₗ AddCommGrp.{v}) :=
+  FullSubcategory.lift _ inverseAux inferInstance
+
+/-- Implementation, see `forgetEquivalence`.
+This is the complicated bit, where we show that forgetting the group structure in the image of
+`F` and then reconstructing it recovers the group structure we started with. -/
+noncomputable def unitIsoAux (F : C ⥤ AddCommGrp.{v}) [PreservesFiniteLimits F] (X : C) :
+    commGrpTypeEquivalenceCommGrp.inverse.obj (AddCommGrp.toCommGrp.obj (F.obj X)) ≅
+      (F ⋙ forget AddCommGrp).mapCommGrp.obj (Preadditive.commGrpEquivalence.functor.obj X) := by
+  refine CommGrp_.mkIso Multiplicative.toAdd.toIso (by aesop_cat) ?_
+  dsimp [-Functor.comp_map]
+  have : F.Additive := Functor.additive_of_preserves_binary_products _
+  rw [Functor.comp_map, F.map_add,
+    Functor.Monoidal.μ_comp F (forget AddCommGrp.{v}) (X := X) (Y := X),
+    Category.assoc, ← Functor.map_comp, Preadditive.comp_add, Functor.Monoidal.μ_fst,
+    Functor.Monoidal.μ_snd]
+  aesop_cat
+
+/-- Implementation, see `forgetEquivalence`. -/
+noncomputable def unitIso : 𝟭 (C ⥤ₗ AddCommGrp) ≅
+    (LeftExactFunctor.whiskeringRight _ _ _).obj (LeftExactFunctor.of (forget _)) ⋙ inverse :=
+  NatIso.ofComponents (fun F => InducedCategory.isoMk (NatIso.ofComponents (fun X =>
+    commGroupAddCommGroupEquivalence.counitIso.app _ ≪≫
+      (CommGrp.toAddCommGrp.mapIso (commGrpTypeEquivalenceCommGrp.counitIso.app
+        (AddCommGrp.toCommGrp.obj (F.obj.obj X)))).symm ≪≫
+      CommGrp.toAddCommGrp.mapIso
+        (CommGrpTypeEquivalenceCommGrp.functor.mapIso (unitIsoAux F.obj X)))))
+
+/-- To construct a functor from `C ⥤ₗ Type v` to `C ⥤ₗ AddCommGrp.{v}`, notice that a left-exact
+functor `F : C ⥤ Type v` induces a functor `CommGrp_ C ⥤ CommGrp_ (Type v)`. But `CommGrp_ C` is
+equivalent to `C`, and `CommGrp_ (Type v)` is equivalent to `AddCommGrp.{v}`, so we turn this
+into a functor `C ⥤ AddCommGrp.{v}`. By construction, composing with with the forgetful
+functor recovers the functor we started with, so since the forgetful functor reflects finite
+limits and `F` preserves finite limits, our constructed functor also preserves finite limits. It
+can be shown that this construction gives a quasi-inverse to the whiskering operation
+`(C ⥤ₗ AddCommGrp.{v}) ⥤ (C ⥤ₗ Type v)`. -/
+noncomputable def forgetEquivalence : (C ⥤ₗ AddCommGrp.{v}) ≌ (C ⥤ₗ Type v) where
+  functor := (LeftExactFunctor.whiskeringRight _ _ _).obj (LeftExactFunctor.of (forget _))
+  inverse := inverse
+  unitIso := unitIso
+  counitIso := Iso.refl _
+
+end
+
+end AddCommGrp

From 101fe191e533f02107663c11fa46890a5961a5ca Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Mon, 17 Feb 2025 06:56:06 +0100
Subject: [PATCH 38/57] feat(CategoryTheory): forgetting the group structure on
 the codomain of left-left exact functors

---
 Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean  |  4 ++--
 Mathlib/CategoryTheory/ChosenFiniteProducts.lean    | 13 +++++++++++++
 .../Monoidal/Internal/Types/CommGrp_.lean           |  9 +++++++++
 3 files changed, 24 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
index a71f7cdbf4f795..b0a00c27989cc2 100644
--- a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
+++ b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
@@ -27,6 +27,7 @@ section
 variable {C : Type u} [Category.{v} C] [Preadditive C] [HasFiniteBiproducts C]
 
 attribute [local instance] hasFiniteProducts_of_hasFiniteBiproducts
+attribute [local instance] AddCommGrp.chosenFiniteProductsAddCommGrp
 
 private noncomputable local instance : ChosenFiniteProducts C :=
   ChosenFiniteProducts.ofFiniteProducts _
@@ -56,8 +57,7 @@ noncomputable def unitIsoAux (F : C ⥤ AddCommGrp.{v}) [PreservesFiniteLimits F
   refine CommGrp_.mkIso Multiplicative.toAdd.toIso (by aesop_cat) ?_
   dsimp [-Functor.comp_map]
   have : F.Additive := Functor.additive_of_preserves_binary_products _
-  rw [Functor.comp_map, F.map_add,
-    Functor.Monoidal.μ_comp F (forget AddCommGrp.{v}) (X := X) (Y := X),
+  rw [Functor.comp_map, F.map_add, Functor.Monoidal.μ_comp X X,
     Category.assoc, ← Functor.map_comp, Preadditive.comp_add, Functor.Monoidal.μ_fst,
     Functor.Monoidal.μ_snd]
   aesop_cat
diff --git a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
index 8d295773dd4850..9ff1a490a640e3 100644
--- a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
+++ b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@@ -651,6 +651,19 @@ lemma μ_fst (X Y : C) : LaxMonoidal.μ F X Y ≫ F.map (fst X Y) = fst (F.obj X
 lemma μ_snd (X Y : C) : LaxMonoidal.μ F X Y ≫ F.map (snd X Y) = snd (F.obj X) (F.obj Y) :=
   (cancel_epi (μIso _ _ _).inv).1 (by simp)
 
+section
+
+variable {F} {E : Type u₂} [Category.{v₂} E] [ChosenFiniteProducts E] {G : D ⥤ E}
+  [PreservesFiniteProducts G]
+
+attribute [-instance] Functor.LaxMonoidal.comp Functor.Monoidal.instComp in
+@[reassoc (attr := simp)]
+lemma μ_comp (X Y : C) :
+    LaxMonoidal.μ (F ⋙ G) X Y = LaxMonoidal.μ G _ _ ≫ G.map (LaxMonoidal.μ F X Y) := by
+  apply (cancel_mono (μIso _ _ _).inv).1
+  apply ChosenFiniteProducts.hom_ext <;> simp [← Functor.comp_obj, ← Functor.map_comp]
+
+end
 
 end
 
diff --git a/Mathlib/CategoryTheory/Monoidal/Internal/Types/CommGrp_.lean b/Mathlib/CategoryTheory/Monoidal/Internal/Types/CommGrp_.lean
index 20248c10a85bec..ff31a53f05a0c0 100644
--- a/Mathlib/CategoryTheory/Monoidal/Internal/Types/CommGrp_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Internal/Types/CommGrp_.lean
@@ -39,6 +39,15 @@ noncomputable def inverse : CommGrp.{u} ⥤ CommGrp_ (Type u) where
         exact CommMonoid.mul_comm y x }
   map f := GrpTypeEquivalenceGrp.inverse.map ((forget₂ CommGrp Grp).map f)
 
+@[simp]
+theorem inverse_obj_X {A : CommGrp.{u}} : (inverse.obj A).X = A := rfl
+@[simp]
+theorem inverse_obj_one {A : CommGrp.{u}} {x} : (inverse.obj A).one x = (1 : A) := rfl
+@[simp]
+theorem inverse_obj_mul {A : CommGrp.{u}} {p} : (inverse.obj A).mul p = (p.1 : A) * p.2 := rfl
+@[simp]
+theorem inverse_obj_inv {A : CommGrp.{u}} {x} : (inverse.obj A).inv x = (x : A)⁻¹ := rfl
+
 end CommGrpTypeEquivalenceCommGrp
 
 /-- The category of commutative group objects in `Type u` is equivalent to the category of

From 9d523826982880fd2e538f89d404727c63432db7 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Mon, 17 Feb 2025 06:57:34 +0100
Subject: [PATCH 39/57] module doc

---
 Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
index b0a00c27989cc2..05ce980662914d 100644
--- a/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
+++ b/Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean
@@ -12,7 +12,9 @@ import Mathlib.CategoryTheory.Preadditive.CommGrp_
 /-!
 # The forgetful functor `(C ⥤ₗ AddCommGroup) ⥤ (C ⥤ₗ Type v)` is an equivalence
 
-We construct a quasi-inverse for the
+This is true as long as `C` is additive.
+
+Here, `C ⥤ₗ D` is the category of finite-limits-preserving functors from `C` to `D`.
 -/
 
 open CategoryTheory MonoidalCategory Limits

From 0882ad57c0f666e2d76958f879b18960810efce2 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Mon, 17 Feb 2025 07:01:07 +0100
Subject: [PATCH 40/57] Fix

---
 Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean b/Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean
index e2548d0b215eb3..a5e28624587d48 100644
--- a/Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean
+++ b/Mathlib/Algebra/Category/Grp/ChosenFiniteProducts.lean
@@ -3,7 +3,6 @@ Copyright (c) 2025 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-import Mathlib.CategoryTheory.ChosenFiniteProducts
 import Mathlib.Algebra.Category.Grp.Biproducts
 import Mathlib.Algebra.Category.Grp.Zero
 import Mathlib.CategoryTheory.Monoidal.Types.Basic

From 769874f8b44008f8dfae1d715f49b63760785ff0 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Mon, 17 Feb 2025 07:27:30 +0100
Subject: [PATCH 41/57] It was not a good simp lemma anyway

---
 Mathlib/CategoryTheory/ChosenFiniteProducts.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
index 9ff1a490a640e3..b47eea1fc79bba 100644
--- a/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
+++ b/Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@@ -657,7 +657,7 @@ variable {F} {E : Type u₂} [Category.{v₂} E] [ChosenFiniteProducts E] {G : D
   [PreservesFiniteProducts G]
 
 attribute [-instance] Functor.LaxMonoidal.comp Functor.Monoidal.instComp in
-@[reassoc (attr := simp)]
+@[reassoc]
 lemma μ_comp (X Y : C) :
     LaxMonoidal.μ (F ⋙ G) X Y = LaxMonoidal.μ G _ _ ≫ G.map (LaxMonoidal.μ F X Y) := by
   apply (cancel_mono (μIso _ _ _).inv).1

From e91ac71407f5efd6c217cacf413f39cc1918a3f4 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 22 Feb 2025 07:32:39 +0100
Subject: [PATCH 42/57] Code

---
 .../ModuleEmbedding/Opposite.lean             | 93 +++++++++++++++++++
 1 file changed, 93 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean
new file mode 100644
index 00000000000000..08eab867196712
--- /dev/null
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean
@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.Abelian.Yoneda
+import Mathlib.CategoryTheory.Generator.Abelian
+import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
+
+universe w v u
+
+/-!
+# Embedding opposites of Grothendieck categories
+
+If `C` is Grothendieck abelian and `F : D ⥤ Cᵒᵖ` is a functor from a small category, we construct
+an object `G : Cᵒᵖ` such that `preadditiveCoyonedaObj G : Cᵒᵖ ⥤ ModuleCat (End G)ᵐᵒᵖ` is faithful
+and exact and its precomsosition with `F` is full if `F` is.
+-/
+
+open CategoryTheory Limits Opposite ZeroObject
+
+namespace CategoryTheory.Abelian.IsGrothendieckAbelian
+
+variable {C : Type u} [Category.{v} C] {D : Type v} [SmallCategory D] (F : D ⥤ Cᵒᵖ)
+
+theorem epi_comp' {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : Epi f) (hg : Epi g) :
+    Epi (f ≫ g) :=
+  inferInstance
+
+namespace OppositeModuleEmbedding
+
+variable [Abelian C] [IsGrothendieckAbelian.{v} C]
+
+variable (C) in
+private noncomputable def projectiveSeparator : Cᵒᵖ :=
+  (has_projective_separator (coseparator Cᵒᵖ) (isCoseparator_coseparator Cᵒᵖ)).choose
+
+private instance : Projective (projectiveSeparator C) :=
+  (has_projective_separator (coseparator Cᵒᵖ) (isCoseparator_coseparator Cᵒᵖ)).choose_spec.1
+
+private theorem isSeparator_projectiveSeparator : IsSeparator (projectiveSeparator C) :=
+  (has_projective_separator (coseparator Cᵒᵖ) (isCoseparator_coseparator Cᵒᵖ)).choose_spec.2
+
+private noncomputable def generator : Cᵒᵖ :=
+  ∐ (fun (X : D) => ∐ fun (_ : projectiveSeparator C ⟶ F.obj X) => projectiveSeparator C)
+
+private theorem exists_epi (X : D) : ∃ f : generator F ⟶ F.obj X, Epi f := by
+  classical
+  refine ⟨Sigma.desc (Pi.single X (𝟙 _)) ≫ Sigma.desc (fun f => f), ?_⟩
+  have h := (isSeparator_iff_epi (projectiveSeparator C)).1
+    isSeparator_projectiveSeparator (F.obj X)
+  suffices Epi (Sigma.desc (Pi.single X (𝟙 _))) from epi_comp' this h
+  exact SplitEpi.epi ⟨Sigma.ι (fun (X : D) => ∐ fun _ => projectiveSeparator C) X, by simp⟩
+
+private instance : Projective (generator F) := by
+  rw [generator]
+  infer_instance
+
+private theorem isSeparator [Nonempty D] : IsSeparator (generator F) := by
+  apply isSeparator_sigma_of_isSeparator _ Classical.ofNonempty
+  apply isSeparator_sigma_of_isSeparator _ 0
+  exact isSeparator_projectiveSeparator
+
+/-- Given a functor `F : D ⥤ Cᵒᵖ`, where `C` is Grothendieck abelian, this is a ring `R` such that
+`Cᵒᵖ` has a nice embedding into `ModuleCat (EmbeddingRing F)`; see
+`OppositeModuleEmbedding.embedding`. -/
+def EmbeddingRing : Type v := (End (generator F))ᵐᵒᵖ
+
+noncomputable instance : Ring (EmbeddingRing F) :=
+  inferInstanceAs <| Ring (End (generator F))ᵐᵒᵖ
+
+/-- This is a functor `embedding F : Cᵒᵖ ⥤ ModuleCat (EmbeddingRing F)`. We have that `embedding F`
+is faithful and preserves finite limits and colimits. Furthermore, `F ⋙ embedding F` is full. -/
+noncomputable def embedding : Cᵒᵖ ⥤ ModuleCat.{v} (EmbeddingRing F) :=
+  preadditiveCoyonedaObj (generator F)
+
+instance [Nonempty D] : (embedding F).Faithful :=
+  (isSeparator_iff_faithful_preadditiveCoyonedaObj _).1 (isSeparator F)
+
+instance [Nonempty D] [F.Full] : (F ⋙ embedding F).Full :=
+  full_comp_preadditiveCoyonedaObj _ (isSeparator F) (exists_epi F)
+
+instance : PreservesFiniteLimits (embedding F) := by
+  rw [embedding]
+  apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize
+  infer_instance
+
+instance : PreservesFiniteColimits (embedding F) := by
+  apply preservesFiniteColimits_preadditiveCoyonedaObj_of_projective
+
+end OppositeModuleEmbedding
+
+end CategoryTheory.Abelian.IsGrothendieckAbelian

From 5c926970bc6dbfa3be37dfa164f0b196b9771afe Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 22 Feb 2025 07:38:25 +0100
Subject: [PATCH 43/57] feat(CategoryTheory): explicit argument versions of
 `epi_comp` and `mono_comp`

---
 Mathlib/CategoryTheory/Category/Basic.lean | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/Mathlib/CategoryTheory/Category/Basic.lean b/Mathlib/CategoryTheory/Category/Basic.lean
index 247f3da889691e..081aadebe328b0 100644
--- a/Mathlib/CategoryTheory/Category/Basic.lean
+++ b/Mathlib/CategoryTheory/Category/Basic.lean
@@ -274,12 +274,29 @@ theorem cancel_mono_id (f : X ⟶ Y) [Mono f] {g : X ⟶ X} : g ≫ f = f ↔ g
   convert cancel_mono f
   simp
 
+/-- The composition of epimorphisms is again an epimorphism. This version takes `Epi f` and `Epi g`
+as typeclass arguments. For a version taking them as explicit arguments, see `epi_comp`. -/
 instance epi_comp {X Y Z : C} (f : X ⟶ Y) [Epi f] (g : Y ⟶ Z) [Epi g] : Epi (f ≫ g) :=
   ⟨fun _ _ w => (cancel_epi g).1 <| (cancel_epi_assoc_iff f).1 w⟩
 
+/-- The composition of epimorphisms is again an epimorphism. This version takes `Epi f` and `Epi g`
+as explicit arguments. For a version taking them as typeclass arguments, see `epi_comp`. -/
+theorem epi_comp' {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : Epi f) (hg : Epi g) : Epi (f ≫ g) :=
+  inferInstance
+
+/-- The composition of monomorphisms is again a monomorphism. This version takes `Mono f` and
+`Mono g` as typeclass arguments. For a version taking them as explicit arguments, see `mono_comp'`.
+-/
 instance mono_comp {X Y Z : C} (f : X ⟶ Y) [Mono f] (g : Y ⟶ Z) [Mono g] : Mono (f ≫ g) :=
   ⟨fun _ _ w => (cancel_mono f).1 <| (cancel_mono_assoc_iff g).1 w⟩
 
+/-- The composition of monomorphisms is again a monomorphism. This version takes `Mono f` and
+`Mono g` as explicit arguments. For a version taking them as typeclass arguments, see `mono_comp'`.
+-/
+theorem mono_comp' {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : Mono f) (hg : Mono g) :
+    Mono (f ≫ g) :=
+  inferInstance
+
 theorem mono_of_mono {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Mono (f ≫ g)] : Mono f :=
   ⟨fun _ _ w => (cancel_mono (f ≫ g)).1 <| by simp only [← Category.assoc, w]⟩
 

From 49c35a71013639868e51ea21225b7c046cb13d7c Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 22 Feb 2025 07:39:30 +0100
Subject: [PATCH 44/57] fix

---
 Mathlib/CategoryTheory/Category/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Category/Basic.lean b/Mathlib/CategoryTheory/Category/Basic.lean
index 081aadebe328b0..4aafb2705090b4 100644
--- a/Mathlib/CategoryTheory/Category/Basic.lean
+++ b/Mathlib/CategoryTheory/Category/Basic.lean
@@ -275,7 +275,7 @@ theorem cancel_mono_id (f : X ⟶ Y) [Mono f] {g : X ⟶ X} : g ≫ f = f ↔ g
   simp
 
 /-- The composition of epimorphisms is again an epimorphism. This version takes `Epi f` and `Epi g`
-as typeclass arguments. For a version taking them as explicit arguments, see `epi_comp`. -/
+as typeclass arguments. For a version taking them as explicit arguments, see `epi_comp'`. -/
 instance epi_comp {X Y Z : C} (f : X ⟶ Y) [Epi f] (g : Y ⟶ Z) [Epi g] : Epi (f ≫ g) :=
   ⟨fun _ _ w => (cancel_epi g).1 <| (cancel_epi_assoc_iff f).1 w⟩
 
@@ -291,7 +291,7 @@ instance mono_comp {X Y Z : C} (f : X ⟶ Y) [Mono f] (g : Y ⟶ Z) [Mono g] : M
   ⟨fun _ _ w => (cancel_mono f).1 <| (cancel_mono_assoc_iff g).1 w⟩
 
 /-- The composition of monomorphisms is again a monomorphism. This version takes `Mono f` and
-`Mono g` as explicit arguments. For a version taking them as typeclass arguments, see `mono_comp'`.
+`Mono g` as explicit arguments. For a version taking them as typeclass arguments, see `mono_comp`.
 -/
 theorem mono_comp' {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : Mono f) (hg : Mono g) :
     Mono (f ≫ g) :=

From 1882fbe14b54f1eb81fefbf800d053d5613181e1 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 22 Feb 2025 07:40:20 +0100
Subject: [PATCH 45/57] adapt

---
 Mathlib.lean                                                  | 1 +
 .../GrothendieckCategory/ModuleEmbedding/Opposite.lean        | 4 ----
 2 files changed, 1 insertion(+), 4 deletions(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 0bd1feda99170a..5e5f26ed1673a5 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1707,6 +1707,7 @@ import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types
 import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
 import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda
 import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
+import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
 import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms
 import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
 import Mathlib.CategoryTheory.Abelian.Images
diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean
index 08eab867196712..1f911e7b2d35f1 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean
@@ -23,10 +23,6 @@ namespace CategoryTheory.Abelian.IsGrothendieckAbelian
 
 variable {C : Type u} [Category.{v} C] {D : Type v} [SmallCategory D] (F : D ⥤ Cᵒᵖ)
 
-theorem epi_comp' {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : Epi f) (hg : Epi g) :
-    Epi (f ≫ g) :=
-  inferInstance
-
 namespace OppositeModuleEmbedding
 
 variable [Abelian C] [IsGrothendieckAbelian.{v} C]

From a284b0f5f98f787106f12062ac5a72c98a2b2ae7 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 22 Feb 2025 08:55:00 +0100
Subject: [PATCH 46/57] ?!?!

---
 .../CategoryTheory/Abelian/FreydMitchell.lean | 110 ++++++++++++++++++
 .../GrothendieckAxioms/Indization.lean        |   2 +-
 .../ModuleEmbedding/Opposite.lean             |  12 +-
 Mathlib/CategoryTheory/Abelian/Transfer.lean  |  49 +++++---
 4 files changed, 153 insertions(+), 20 deletions(-)
 create mode 100644 Mathlib/CategoryTheory/Abelian/FreydMitchell.lean

diff --git a/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean b/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean
new file mode 100644
index 00000000000000..2c4f4a231b671c
--- /dev/null
+++ b/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean
@@ -0,0 +1,110 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
+import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization
+
+/-!
+# The Freyd-Mitchell embedding theorem
+
+In this file, we start with an abelian category `C` and construct a full, faithful and exact
+functor `C ⥤ ModuleCat.{max u v} (EmbeddingRing C)`.
+
+## Implementation notes
+
+In the literature you will generally only find this theorem stated for small categories `C`. In
+Lean, we can work around this limitation by passing from `C` to `AsSmall.{max u v} C`, thereby
+enlarging the category of modules that we land in (which should be inconsequential in most
+applications) so that our embedding theorem applies to all abelian categories. If `C` was already a
+small category, then this does not change anything.
+-/
+
+universe v u
+
+open CategoryTheory Limits
+
+namespace CategoryTheory.Abelian
+
+variable {C : Type u} [Category.{v} C] [Abelian C]
+
+namespace FreydMitchell
+
+open ZeroObject in
+instance : Nonempty (AsSmall.{max u v} C) := ⟨0⟩
+
+variable (C) in
+/-- Given an abelian category `C`, this is a ring such that there is a full, faithful and exact
+embedding `C ⥤ ModuleCat (EmbeddingRing C)`. -/
+def EmbeddingRing : Type (max u v) :=
+  IsGrothendieckAbelian.OppositeModuleEmbedding.EmbeddingRing
+    (Ind.yoneda (C := (AsSmall.{max u v} C)ᵒᵖ)).rightOp
+
+noncomputable instance : Ring (EmbeddingRing C) :=
+  inferInstanceAs <| Ring <|
+    IsGrothendieckAbelian.OppositeModuleEmbedding.EmbeddingRing
+      (Ind.yoneda (C := (AsSmall.{max u v} C)ᵒᵖ)).rightOp
+
+variable (C) in
+private def F : C ⥤ AsSmall.{max u v} C :=
+  AsSmall.equiv.functor
+
+variable (C) in
+private noncomputable def G : AsSmall.{max u v} C ⥤ (Ind (AsSmall.{max u v} C)ᵒᵖ)ᵒᵖ :=
+  Ind.yoneda.rightOp
+
+variable (C) in
+private noncomputable def H :
+    (Ind (AsSmall.{max u v} C)ᵒᵖ)ᵒᵖ ⥤ ModuleCat.{max u v} (EmbeddingRing C) :=
+  IsGrothendieckAbelian.OppositeModuleEmbedding.embedding (G C)
+
+variable (C) in
+/-- This is the full, faithful and exact embedding `C ⥤ ModuleCat (EmbeddingRing C)`. The fact that
+such an functor exists is called the Freyd-Mitchell embedding theorem. -/
+noncomputable def functor : C ⥤ ModuleCat.{max u v} (EmbeddingRing C) :=
+  F C ⋙ G C ⋙ H C
+
+instance : (functor C).Faithful := by
+  rw [functor]
+  have : (F C).Faithful := by rw [F]; infer_instance
+  have : (G C).Faithful := by rw [G]; infer_instance
+  have : (H C).Faithful := IsGrothendieckAbelian.OppositeModuleEmbedding.faithful_embedding _
+  infer_instance
+
+instance : (functor C).Full := by
+  rw [functor]
+  have : (F C).Full := by rw [F]; infer_instance
+  have : (G C).Full := by rw [G]; infer_instance
+  have : (G C ⋙ H C).Full := IsGrothendieckAbelian.OppositeModuleEmbedding.full_embedding _
+  infer_instance
+
+instance : PreservesFiniteLimits (functor C) := by
+  rw [functor]
+  have : PreservesFiniteLimits (F C) := by rw [F]; infer_instance
+  have : PreservesFiniteLimits (G C) := by rw [G]; apply preservesFiniteLimits_rightOp
+  have : PreservesFiniteLimits (H C) :=
+    IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteLimits_embedding _
+  infer_instance
+
+instance : PreservesFiniteColimits (functor C) := by
+  rw [functor]
+  have : PreservesFiniteColimits (F C) := by rw [F]; infer_instance
+  have : PreservesFiniteColimits (G C) := by rw [G]; apply preservesFiniteColimits_rightOp
+  have : PreservesFiniteColimits (H C) :=
+    IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteColimits_embedding _
+  infer_instance
+
+end FreydMitchell
+
+/-- The Freyd-Mitchell embedding theorem. See also `FreydMitchell.functor` for an unpacked
+version of this statement. -/
+@[stacks 05PP]
+theorem freyd_mitchell (C : Type u) [Category.{v} C] [Abelian C] :
+    ∃ (R : Type (max u v)) (_ : Ring R) (F : C ⥤ ModuleCat.{max u v} R),
+      F.Full ∧ F.Faithful ∧ PreservesFiniteLimits F ∧ PreservesFiniteColimits F :=
+  ⟨_, _, FreydMitchell.functor C, inferInstance, inferInstance, inferInstance, inferInstance⟩
+
+#print axioms freyd_mitchell
+
+end CategoryTheory.Abelian
diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean
index 0472fd97b1127e..747e2acac5432a 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean
@@ -8,7 +8,7 @@ import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types
 import Mathlib.CategoryTheory.Abelian.Indization
 import Mathlib.CategoryTheory.Limits.Indization.Category
 import Mathlib.CategoryTheory.Generator.Indization
-import Mathlib.CategoryTheory.Abelian.GrothendieckCategory
+import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
 
 /-!
 # AB axioms in the category of ind-objects
diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean
index 1f911e7b2d35f1..cf7fab353a554d 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean
@@ -7,8 +7,6 @@ import Mathlib.CategoryTheory.Abelian.Yoneda
 import Mathlib.CategoryTheory.Generator.Abelian
 import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
 
-universe w v u
-
 /-!
 # Embedding opposites of Grothendieck categories
 
@@ -17,6 +15,8 @@ an object `G : Cᵒᵖ` such that `preadditiveCoyonedaObj G : Cᵒᵖ ⥤ Module
 and exact and its precomsosition with `F` is full if `F` is.
 -/
 
+universe w v u
+
 open CategoryTheory Limits Opposite ZeroObject
 
 namespace CategoryTheory.Abelian.IsGrothendieckAbelian
@@ -70,18 +70,18 @@ is faithful and preserves finite limits and colimits. Furthermore, `F ⋙ embedd
 noncomputable def embedding : Cᵒᵖ ⥤ ModuleCat.{v} (EmbeddingRing F) :=
   preadditiveCoyonedaObj (generator F)
 
-instance [Nonempty D] : (embedding F).Faithful :=
+instance faithful_embedding [Nonempty D] : (embedding F).Faithful :=
   (isSeparator_iff_faithful_preadditiveCoyonedaObj _).1 (isSeparator F)
 
-instance [Nonempty D] [F.Full] : (F ⋙ embedding F).Full :=
+instance full_embedding [Nonempty D] [F.Full] : (F ⋙ embedding F).Full :=
   full_comp_preadditiveCoyonedaObj _ (isSeparator F) (exists_epi F)
 
-instance : PreservesFiniteLimits (embedding F) := by
+instance preservesFiniteLimits_embedding : PreservesFiniteLimits (embedding F) := by
   rw [embedding]
   apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize
   infer_instance
 
-instance : PreservesFiniteColimits (embedding F) := by
+instance preservesFiniteColimits_embedding : PreservesFiniteColimits (embedding F) := by
   apply preservesFiniteColimits_preadditiveCoyonedaObj_of_projective
 
 end OppositeModuleEmbedding
diff --git a/Mathlib/CategoryTheory/Abelian/Transfer.lean b/Mathlib/CategoryTheory/Abelian/Transfer.lean
index bc71c7a1b37c8b..0045a684295ce2 100644
--- a/Mathlib/CategoryTheory/Abelian/Transfer.lean
+++ b/Mathlib/CategoryTheory/Abelian/Transfer.lean
@@ -119,19 +119,6 @@ section Preadditive
 
 variable [Preadditive C]
 
-noncomputable instance homGroup (P Q : ShrinkHoms C) : AddCommGroup (P ⟶ Q : Type w) :=
-  Equiv.addCommGroup (equivShrink _).symm
-
-lemma functor_map_add {P Q : C} (f g : P ⟶ Q) :
-    (functor C).map (f + g) =
-      (functor C).map f + (functor C).map g := by
-  exact map_add (equivShrink.{w} (P ⟶ Q)).symm.addEquiv.symm f g
-
-lemma inverse_map_add {P Q : ShrinkHoms C} (f g : P ⟶ Q) :
-    (inverse C).map (f + g) =
-      (inverse C).map f + (ShrinkHoms.inverse C).map g :=
-  map_add (equivShrink.{w} (P.fromShrinkHoms ⟶ Q.fromShrinkHoms)).symm.addEquiv f g
-
 variable (C)
 
 instance preadditive : Preadditive.{w} (ShrinkHoms C) :=
@@ -158,4 +145,40 @@ noncomputable instance abelian [Abelian C] :
 
 end ShrinkHoms
 
+namespace AsSmall
+
+universe w v u
+
+variable {C : Type u} [Category.{v} C]
+
+section Preadditive
+
+variable [Preadditive C]
+
+variable (C)
+
+instance preadditive : Preadditive (AsSmall.{w} C) :=
+  .ofFullyFaithful equiv.fullyFaithfulInverse
+
+instance : (down (C := C)).Additive :=
+  equiv.symm.fullyFaithfulFunctor.additive_ofFullyFaithful
+
+instance : (up (C := C)).Additive :=
+  equiv.symm.additive_inverse_of_FullyFaithful
+
+instance hasLimitsOfShape (J : Type*) [Category J]
+    [HasLimitsOfShape J C] : HasLimitsOfShape.{_, _, max u v w} J (AsSmall.{w} C) :=
+  Adjunction.hasLimitsOfShape_of_equivalence equiv.inverse
+
+instance hasFiniteLimits [HasFiniteLimits C] :
+    HasFiniteLimits (AsSmall.{w} C) := ⟨fun _ => inferInstance⟩
+
+end Preadditive
+
+variable (C) in
+noncomputable instance abelian [Abelian C] :
+    Abelian (AsSmall.{w} C) := abelianOfEquivalence equiv.inverse
+
+end AsSmall
+
 end CategoryTheory

From f9b1f49740811a72a7074f6974f14826d7ac0790 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 22 Feb 2025 08:55:14 +0100
Subject: [PATCH 47/57] Mathlib.lean

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index baa414ce5cc3d3..c8a662be4ecbc8 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1698,6 +1698,7 @@ import Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
 import Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
 import Mathlib.CategoryTheory.Abelian.Exact
 import Mathlib.CategoryTheory.Abelian.Ext
+import Mathlib.CategoryTheory.Abelian.FreydMitchell
 import Mathlib.CategoryTheory.Abelian.FunctorCategory
 import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
 import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

From 73882284a76b06003afb9a55650348c517b24f47 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 22 Feb 2025 11:50:35 +0100
Subject: [PATCH 48/57] WIP

---
 .../CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean   | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean
index 0472fd97b1127e..747e2acac5432a 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean
@@ -8,7 +8,7 @@ import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types
 import Mathlib.CategoryTheory.Abelian.Indization
 import Mathlib.CategoryTheory.Limits.Indization.Category
 import Mathlib.CategoryTheory.Generator.Indization
-import Mathlib.CategoryTheory.Abelian.GrothendieckCategory
+import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
 
 /-!
 # AB axioms in the category of ind-objects

From faff76851b7f193fb499a5ac904647bd16e54aaf Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 22 Feb 2025 11:58:27 +0100
Subject: [PATCH 49/57] Cleanup

---
 Mathlib/CategoryTheory/Abelian/Indization.lean  | 17 ++++++++---------
 .../CategoryTheory/Preadditive/Indization.lean  |  8 +++++---
 2 files changed, 13 insertions(+), 12 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/Indization.lean b/Mathlib/CategoryTheory/Abelian/Indization.lean
index 67c9ce26579891..5f24e2c736dc6e 100644
--- a/Mathlib/CategoryTheory/Abelian/Indization.lean
+++ b/Mathlib/CategoryTheory/Abelian/Indization.lean
@@ -9,6 +9,11 @@ import Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
 
 /-!
 # The category of ind-objects is abelian
+
+We show that if `C` is a small abelian category, then `Ind C` is an abelian category.
+
+In the file `CategoryTheory.Abelian.GrothendieckAxioms.Indization`, we show that in this situation
+`Ind C` is in fact Grothendieck abelian.
 -/
 
 universe v
@@ -22,15 +27,9 @@ variable {C : Type v} [SmallCategory C] [Abelian C]
 instance {X Y : Ind C} (f : X ⟶ Y) : IsIso (Abelian.coimageImageComparison f) := by
   obtain ⟨I, _, _, F, G, ϕ, ⟨i⟩⟩ := Ind.exists_nonempty_arrow_mk_iso_ind_lim (f := f)
   let i' := coimageImageComparisonFunctor.mapIso i
-  dsimp at i'
-  rw [Arrow.isIso_iff_isIso_of_isIso i'.hom]
-  have : Limits.HasFiniteBiproducts (Ind C) :=
-    Limits.HasFiniteBiproducts.of_hasFiniteCoproducts
-  have : Limits.HasZeroObject (Ind C) :=
-    Limits.hasZeroObject_of_hasFiniteBiproducts _
-  have : (Ind.lim I (C := C)).PreservesZeroMorphisms :=
-    Functor.preservesZeroMorphisms_of_preserves_terminal_object
-  rw [Arrow.isIso_iff_isIso_of_isIso (PreservesCoimageImageComparison.iso (Ind.lim I) ϕ).inv]
+  dsimp only [coimageImageComparisonFunctor_obj, Arrow.mk_left, Arrow.mk_right, Arrow.mk_hom] at i'
+  rw [Arrow.isIso_iff_isIso_of_isIso i'.hom,
+    Arrow.isIso_iff_isIso_of_isIso (PreservesCoimageImageComparison.iso (Ind.lim I) ϕ).inv]
   infer_instance
 
 noncomputable instance : Abelian (Ind C) :=
diff --git a/Mathlib/CategoryTheory/Preadditive/Indization.lean b/Mathlib/CategoryTheory/Preadditive/Indization.lean
index 53673046d5d92b..155101673bd649 100644
--- a/Mathlib/CategoryTheory/Preadditive/Indization.lean
+++ b/Mathlib/CategoryTheory/Preadditive/Indization.lean
@@ -20,11 +20,13 @@ namespace CategoryTheory
 
 variable {C : Type u} [SmallCategory C] [Preadditive C] [HasFiniteColimits C]
 
-attribute [local instance] HasFiniteBiproducts.of_hasFiniteCoproducts
-
+attribute [local instance] HasFiniteBiproducts.of_hasFiniteCoproducts in
 noncomputable instance : Preadditive (Ind C) :=
   .ofFullyFaithful (((Ind.leftExactFunctorEquivalence C).trans
-    AddCommGrp.forgetEquivalence.symm).fullyFaithfulFunctor.comp
+    (AddCommGrp.leftExactFunctorForgetEquivalence _).symm).fullyFaithfulFunctor.comp
       (fullyFaithfulFullSubcategoryInclusion _))
 
+instance : HasFiniteBiproducts (Ind C) :=
+  HasFiniteBiproducts.of_hasFiniteCoproducts
+
 end CategoryTheory

From 0abcc2dc34a3cacc4ea2860d9c45cd5aa606b1f2 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 22 Feb 2025 11:59:39 +0100
Subject: [PATCH 50/57] Docs

---
 .../Abelian/GrothendieckAxioms/Indization.lean            | 3 ++-
 Mathlib/CategoryTheory/Generator/Indization.lean          | 8 ++------
 2 files changed, 4 insertions(+), 7 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean
index 747e2acac5432a..2b9ce592d9cd13 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean
@@ -13,7 +13,8 @@ import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
 /-!
 # AB axioms in the category of ind-objects
 
-We show that `Ind C` satisfies Grothendieck's axiom AB5 if `C` has finite limits.
+We show that `Ind C` satisfies Grothendieck's axiom AB5 if `C` has finite limits and deduce that
+`Ind C` is Grothendieck abelian if `C` is small and abelian.
 -/
 
 universe v u
diff --git a/Mathlib/CategoryTheory/Generator/Indization.lean b/Mathlib/CategoryTheory/Generator/Indization.lean
index 20ca172a335cc2..651a67f28efcbb 100644
--- a/Mathlib/CategoryTheory/Generator/Indization.lean
+++ b/Mathlib/CategoryTheory/Generator/Indization.lean
@@ -10,12 +10,8 @@ import Mathlib.CategoryTheory.Preadditive.Indization
 /-!
 # Separating set in the category of ind-objects
 
-We construct a separating set in the category of ind-objects.
-
-## Future work
-
-Once we have constructed zero morphisms in the category of ind-objects, we will be able to show
-that under sufficient conditions, the category of ind-objects has a separating object.
+We construct a separating set in the category of ind-objects and conclude that if `C` is small
+and additive, then `C` has a separator.
 
 -/
 

From 6330cd338b999735dffa675a2742972dc796a44a Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 22 Feb 2025 12:09:43 +0100
Subject: [PATCH 51/57] Update 1000.yaml

---
 docs/1000.yaml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/docs/1000.yaml b/docs/1000.yaml
index f07ae44fa96b3e..cb2c4113456625 100644
--- a/docs/1000.yaml
+++ b/docs/1000.yaml
@@ -1324,8 +1324,8 @@ Q1146791:
 
 Q1148215:
   title: Mitchell's embedding theorem
-  # ongoing effort: going slowly; lots of work. see e.g.
-  # https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Freyd-Mitchell.20embedding
+  decl: CategoryTheory.Abelian.freyd_mitchell
+  authors: Markus Himmel, Jakob von Raumer, Paul Reichert, Joël Riou
 
 Q1149022:
   title: Fubini's theorem

From ff3622f33771b628c82241b8722207518261c650 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 22 Feb 2025 12:14:09 +0100
Subject: [PATCH 52/57] Update comment in Pseudoelements.lean

---
 Mathlib/CategoryTheory/Abelian/Pseudoelements.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/Pseudoelements.lean b/Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
index 99b89cc0046618..3b2797315316b3 100644
--- a/Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
+++ b/Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
@@ -29,9 +29,10 @@ their action on pseudoelements. Thus, a usual style of proofs in abelian categor
 First, we construct some morphism using universal properties, and then we use diagram chasing
 of pseudoelements to verify that is has some desirable property such as exactness.
 
-It should be noted that the Freyd-Mitchell embedding theorem gives a vastly stronger notion of
-pseudoelement (in particular one that gives extensionality). However, this theorem is quite
-difficult to prove and probably out of reach for a formal proof for the time being.
+It should be noted that the Freyd-Mitchell embedding theorem
+(see `CategoryTheory.Abelian.FreydMitchell`) gives a vastly stronger notion of
+pseudoelement (in particular one that gives extensionality) and this file should be updated to
+go use that instead!
 
 ## Main results
 

From 5021923db9aecfdf3afd3cf20cb848b71c697dae Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 22 Feb 2025 12:21:05 +0100
Subject: [PATCH 53/57] Comment

---
 Mathlib/CategoryTheory/Abelian/FreydMitchell.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean b/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean
index 2c4f4a231b671c..31c8ed2840edf8 100644
--- a/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean
+++ b/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean
@@ -36,7 +36,9 @@ instance : Nonempty (AsSmall.{max u v} C) := ⟨0⟩
 
 variable (C) in
 /-- Given an abelian category `C`, this is a ring such that there is a full, faithful and exact
-embedding `C ⥤ ModuleCat (EmbeddingRing C)`. -/
+embedding `C ⥤ ModuleCat (EmbeddingRing C)`.
+
+It is probably not a good idea to unfold this. -/
 def EmbeddingRing : Type (max u v) :=
   IsGrothendieckAbelian.OppositeModuleEmbedding.EmbeddingRing
     (Ind.yoneda (C := (AsSmall.{max u v} C)ᵒᵖ)).rightOp
@@ -61,7 +63,9 @@ private noncomputable def H :
 
 variable (C) in
 /-- This is the full, faithful and exact embedding `C ⥤ ModuleCat (EmbeddingRing C)`. The fact that
-such an functor exists is called the Freyd-Mitchell embedding theorem. -/
+such an functor exists is called the Freyd-Mitchell embedding theorem.
+
+It is probably not a good idea to unfold this. -/
 noncomputable def functor : C ⥤ ModuleCat.{max u v} (EmbeddingRing C) :=
   F C ⋙ G C ⋙ H C
 

From 0500131726c9f0e9adbed7c5d25cdd03b3c7e945 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 22 Feb 2025 12:30:57 +0100
Subject: [PATCH 54/57] Fix

---
 Mathlib/CategoryTheory/Abelian/FreydMitchell.lean         | 6 ++----
 .../GrothendieckCategory/ModuleEmbedding/Opposite.lean    | 8 ++++----
 2 files changed, 6 insertions(+), 8 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean b/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean
index 31c8ed2840edf8..7459890fdd100a 100644
--- a/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean
+++ b/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean
@@ -101,14 +101,12 @@ instance : PreservesFiniteColimits (functor C) := by
 
 end FreydMitchell
 
-/-- The Freyd-Mitchell embedding theorem. See also `FreydMitchell.functor` for an unpacked
-version of this statement. -/
+/-- The Freyd-Mitchell embedding theorem. See also `FreydMitchell.functor` for a functor which
+has the relevant instances. -/
 @[stacks 05PP]
 theorem freyd_mitchell (C : Type u) [Category.{v} C] [Abelian C] :
     ∃ (R : Type (max u v)) (_ : Ring R) (F : C ⥤ ModuleCat.{max u v} R),
       F.Full ∧ F.Faithful ∧ PreservesFiniteLimits F ∧ PreservesFiniteColimits F :=
   ⟨_, _, FreydMitchell.functor C, inferInstance, inferInstance, inferInstance, inferInstance⟩
 
-#print axioms freyd_mitchell
-
 end CategoryTheory.Abelian
diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean
index 012170fc60f950..ce1966b6be9187 100644
--- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean
+++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/Opposite.lean
@@ -70,18 +70,18 @@ is faithful and preserves finite limits and colimits. Furthermore, `F ⋙ embedd
 noncomputable def embedding : Cᵒᵖ ⥤ ModuleCat.{v} (EmbeddingRing F) :=
   preadditiveCoyonedaObj (generator F)
 
-instance [Nonempty D] : (embedding F).Faithful :=
+instance faithful_embedding [Nonempty D] : (embedding F).Faithful :=
   (isSeparator_iff_faithful_preadditiveCoyonedaObj _).1 (isSeparator F)
 
-instance [Nonempty D] [F.Full] : (F ⋙ embedding F).Full :=
+instance full_embedding [Nonempty D] [F.Full] : (F ⋙ embedding F).Full :=
   full_comp_preadditiveCoyonedaObj _ (isSeparator F) (exists_epi F)
 
-instance : PreservesFiniteLimits (embedding F) := by
+instance preservesFiniteLimits_embedding : PreservesFiniteLimits (embedding F) := by
   rw [embedding]
   apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize
   infer_instance
 
-instance : PreservesFiniteColimits (embedding F) := by
+instance preservesFiniteColimits_embedding : PreservesFiniteColimits (embedding F) := by
   apply preservesFiniteColimits_preadditiveCoyonedaObj_of_projective
 
 end OppositeModuleEmbedding

From 96146bc291aafb0f0c3190750edcb9d0dab7e1d5 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 22 Feb 2025 12:33:33 +0100
Subject: [PATCH 55/57] Busywork

---
 Mathlib/CategoryTheory/Abelian/FreydMitchell.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean b/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean
index 7459890fdd100a..3bb357839185f1 100644
--- a/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean
+++ b/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean
@@ -9,8 +9,9 @@ import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization
 /-!
 # The Freyd-Mitchell embedding theorem
 
-In this file, we start with an abelian category `C` and construct a full, faithful and exact
-functor `C ⥤ ModuleCat.{max u v} (EmbeddingRing C)`.
+Let `C` be an abelian category. We construct a ring `FreydMitchell.EmbeddingRing C` and a functor
+`FreydMitchell.embedding : C ⥤ ModuleCat.{max u v} (EmbeddingRing C)` which is full, faithful and
+exact.
 
 ## Implementation notes
 

From 6063df16683a5492d93593118f4bd9c0bff4ec30 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 22 Feb 2025 12:34:22 +0100
Subject: [PATCH 56/57] Typo

---
 Mathlib/CategoryTheory/Abelian/FreydMitchell.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean b/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean
index 3bb357839185f1..c4c69733cd358c 100644
--- a/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean
+++ b/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean
@@ -64,7 +64,7 @@ private noncomputable def H :
 
 variable (C) in
 /-- This is the full, faithful and exact embedding `C ⥤ ModuleCat (EmbeddingRing C)`. The fact that
-such an functor exists is called the Freyd-Mitchell embedding theorem.
+such a functor exists is called the Freyd-Mitchell embedding theorem.
 
 It is probably not a good idea to unfold this. -/
 noncomputable def functor : C ⥤ ModuleCat.{max u v} (EmbeddingRing C) :=

From 55e2d9d46dc914e963ef4db3ed28ffcb9cae3ada Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sun, 23 Feb 2025 21:04:09 +0100
Subject: [PATCH 57/57] add overview

---
 .../CategoryTheory/Abelian/FreydMitchell.lean | 49 +++++++++++++++++++
 1 file changed, 49 insertions(+)

diff --git a/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean b/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean
index c4c69733cd358c..cca1e190ed3997 100644
--- a/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean
+++ b/Mathlib/CategoryTheory/Abelian/FreydMitchell.lean
@@ -13,6 +13,50 @@ Let `C` be an abelian category. We construct a ring `FreydMitchell.EmbeddingRing
 `FreydMitchell.embedding : C ⥤ ModuleCat.{max u v} (EmbeddingRing C)` which is full, faithful and
 exact.
 
+## Overview over the proof
+
+The usual stategy to prove the Freyd-Mitchell embedding theorem is as follows:
+
+1. Prove that if `D` is a Grothendieck abelian category and `F : C ⥤ Dᵒᵖ` is a functor from a
+small category, then there is a functor `G : Dᵒᵖ ⥤ ModuleCat R` for a suitable `R` such that `G`
+is faithful and exact and `F ⋙ G` is full.
+2. Find a suitable Grothendieck abelian category `D` and a full, faithful and exact functor
+`F : C ⥤ Dᵒᵖ`.
+
+To prove (1), we proceed as follows:
+
+1. Using the Special Adjoint Functor Theorem and the duality between subobjects and quotients in
+abelian categories, we have that Grothendieck abelian categories have all limits (this is shown in
+`Abelian.GrothendieckCategory.Basic`).
+2. Using the small object argument, it is shown that Grothendieck abelian categories have enough
+injectives (see `Abelian.GrothendieckCategory.EnoughInjectives`).
+3. Putting these two together, it follows that Grothendieck abelian categories have an injective
+cogenerator (see `Generator.Abelian`).
+4. By taking a coproduct of copies of the injective cogenerator, we find a projective separator `G`
+in `Dᵒᵖ` such that every object in the image of `F` is a quotient of `G`. Then the additive Hom
+functor `Hom(G, ·) : Dᵒᵖ ⥤ Module (End G)ᵐᵒᵖ` is faithful (because `G` is a separator), left exact
+(because it is a hom functor), right exact (because `G` is projective) and full (because of a
+combination of the aforementioned properties, see `Abelian.Yoneda`). We put this all together in
+the file `Abelian.GrothendieckCategory.ModuleEmbedding.Opposite`.
+
+To prove (2), there are multiple options.
+
+* Some sources (for example Freyd's "Abelian Categories") choose `D := LeftExactFunctor C Ab`. The
+main difficulty with this approach is that it is not obvious that `D` is abelian. This approach has
+a very algebraic flavor and requires a relatively large armount of ad-hoc reasoning.
+* In the Stacks project, it is suggested to choose `D := Sheaf J Ab` for a suitable Grothendieck
+topology on `Cᵒᵖ` and there are reasons to believe that this `D` is in fact equivalent to
+`LeftExactFunctor C Ab`. This approach translates many of the interesting properties along the
+sheafification adjunction from a category of `Ab`-valued presheaves, which in turn inherits many
+interesting properties from the category of abelian groups.
+* Kashiwara and Schapira choose `D := Ind Cᵒᵖ`, which can be shown to be equivalent to
+`LeftExactFunctor C Ab` (see the file `CategoryTheory.Preadditive.Indization`). This approach
+deduces most interesting properties from the category of types.
+
+When work on this theorem commenced in early 2022, all three apporaches were quite out of reach.
+By the time the theorem was proved in early 2025, both the `Sheaf` approach and the `Ind` approach
+were available in mathlib. The code below uses `D := Ind Cᵒᵖ`.
+
 ## Implementation notes
 
 In the literature you will generally only find this theorem stated for small categories `C`. In
@@ -20,6 +64,11 @@ Lean, we can work around this limitation by passing from `C` to `AsSmall.{max u
 enlarging the category of modules that we land in (which should be inconsequential in most
 applications) so that our embedding theorem applies to all abelian categories. If `C` was already a
 small category, then this does not change anything.
+
+## References
+
+* https://stacks.math.columbia.edu/tag/05PL
+* [M. Kashiwara, P. Schapira, *Categories and Sheaves*][Kashiwara2006], Section 9.6
 -/
 
 universe v u