From 76a0306659b4756541b50aafe890e3aa55da09fe Mon Sep 17 00:00:00 2001
From: Pim Otte <potte@quintor.nl>
Date: Mon, 22 May 2023 19:14:58 +0000
Subject: [PATCH] feat: port Algebra.Category.GroupWithZero (#3962)

---
 Mathlib.lean                                  |   1 +
 .../Algebra/Category/GroupWithZeroCat.lean    | 111 ++++++++++++++++++
 2 files changed, 112 insertions(+)
 create mode 100644 Mathlib/Algebra/Category/GroupWithZeroCat.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index ae1b68f61ecb5..08036277bed16 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -37,6 +37,7 @@ import Mathlib.Algebra.Category.GroupCat.Limits
 import Mathlib.Algebra.Category.GroupCat.Preadditive
 import Mathlib.Algebra.Category.GroupCat.ZModuleEquivalence
 import Mathlib.Algebra.Category.GroupCat.Zero
+import Mathlib.Algebra.Category.GroupWithZeroCat
 import Mathlib.Algebra.Category.ModuleCat.Basic
 import Mathlib.Algebra.Category.ModuleCat.EpiMono
 import Mathlib.Algebra.Category.ModuleCat.Kernels
diff --git a/Mathlib/Algebra/Category/GroupWithZeroCat.lean b/Mathlib/Algebra/Category/GroupWithZeroCat.lean
new file mode 100644
index 0000000000000..b23fd8ed10f47
--- /dev/null
+++ b/Mathlib/Algebra/Category/GroupWithZeroCat.lean
@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+
+! This file was ported from Lean 3 source module algebra.category.GroupWithZero
+! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.Category.Bipointed
+import Mathlib.Algebra.Category.MonCat.Basic
+
+/-!
+# The category of groups with zero
+
+This file defines `GroupWithZeroCat`, the category of groups with zero.
+-/
+
+
+universe u
+
+open CategoryTheory Order
+
+/-- The category of groups with zero. -/
+def GroupWithZeroCat :=
+  Bundled GroupWithZero
+set_option linter.uppercaseLean3 false in
+#align GroupWithZero GroupWithZeroCat
+
+namespace GroupWithZeroCat
+
+instance : CoeSort GroupWithZeroCat (Type _) :=
+  Bundled.coeSort
+
+instance (X : GroupWithZeroCat) : GroupWithZero X :=
+  X.str
+
+/-- Construct a bundled `GroupWithZeroCat` from a `GroupWithZero`. -/
+def of (α : Type _) [GroupWithZero α] : GroupWithZeroCat :=
+  Bundled.of α
+set_option linter.uppercaseLean3 false in
+#align GroupWithZero.of GroupWithZeroCat.of
+
+instance : Inhabited GroupWithZeroCat :=
+  ⟨of (WithZero PUnit)⟩
+
+instance : LargeCategory.{u} GroupWithZeroCat where
+  Hom X Y := MonoidWithZeroHom X Y
+  id X := MonoidWithZeroHom.id X
+  comp f g := g.comp f
+  id_comp := MonoidWithZeroHom.comp_id
+  comp_id := MonoidWithZeroHom.id_comp
+  assoc _ _ _ := MonoidWithZeroHom.comp_assoc _ _ _
+
+-- porting note: was not necessary in mathlib
+instance {M N : GroupWithZeroCat} : FunLike (M ⟶ N) M (fun _ => N) :=
+  ⟨fun f => f.toFun, fun f g h => by
+    cases f
+    cases g
+    congr
+    apply FunLike.coe_injective'
+    exact h⟩
+
+-- porting note: added
+lemma coe_id {X : GroupWithZeroCat} : (𝟙 X : X → X) = id := rfl
+
+-- porting note: added
+lemma coe_comp {X Y Z : GroupWithZeroCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
+
+instance groupWithZeroConcreteCategory : ConcreteCategory GroupWithZeroCat where
+  forget :=
+  { obj := fun G => G
+    map := fun f => f.toFun }
+  forget_faithful := ⟨fun h => FunLike.coe_injective h⟩
+
+-- porting note: added
+@[simp] lemma forget_map (f : X ⟶ Y) : (forget GroupWithZeroCat).map f = f := rfl
+instance hasForgetToBipointed : HasForget₂ GroupWithZeroCat Bipointed
+    where forget₂ :=
+      { obj := fun X => ⟨X, 0, 1⟩
+        map := fun f => ⟨f, f.map_zero', f.map_one'⟩ }
+set_option linter.uppercaseLean3 false in
+#align GroupWithZero.has_forget_to_Bipointed GroupWithZeroCat.hasForgetToBipointed
+
+instance hasForgetToMon : HasForget₂ GroupWithZeroCat MonCat
+    where forget₂ :=
+      { obj := fun X => ⟨ X , _ ⟩
+        map := fun f => f.toMonoidHom }
+set_option linter.uppercaseLean3 false in
+#align GroupWithZero.has_forget_to_Mon GroupWithZeroCat.hasForgetToMon
+
+-- porting note: this instance was not necessary in mathlib
+instance {X Y : GroupWithZeroCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
+  coe (f : X →*₀ Y) := f
+
+/-- Constructs an isomorphism of groups with zero from a group isomorphism between them. -/
+@[simps]
+def Iso.mk {α β : GroupWithZeroCat.{u}} (e : α ≃* β) : α ≅ β where
+  hom := (e : α →*₀ β)
+  inv := (e.symm : β →*₀ α)
+  hom_inv_id := by
+    ext
+    exact e.symm_apply_apply _
+  inv_hom_id := by
+    ext
+    exact e.apply_symm_apply _
+set_option linter.uppercaseLean3 false in
+#align GroupWithZero.iso.mk GroupWithZeroCat.Iso.mk
+
+end GroupWithZeroCat