feat(algebra/category/GroupWithZero): The category of groups with zero (

#12278)

Define `GroupWithZero`, the category of groups with zero with monoid with zero homs.

src/algebra/category/GroupWithZero.lean

@@ -0,0 +1,57 @@
+/-
+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
+-/
+import algebra.category.Group.basic
+import category_theory.category.Bipointed
+
+/-!
+# The category of groups with zero
+
+This file defines `GroupWithZero`, the category of groups with zero.
+-/
+
+universes u
+
+open category_theory order
+
+/-- The category of groups with zero. -/
+def GroupWithZero := bundled group_with_zero
+
+namespace GroupWithZero
+
+instance : has_coe_to_sort GroupWithZero Type* := bundled.has_coe_to_sort
+instance (X : GroupWithZero) : group_with_zero X := X.str
+
+/-- Construct a bundled `GroupWithZero` from a `group_with_zero`. -/
+def of (α : Type*) [group_with_zero α] : GroupWithZero := bundled.of α
+
+instance : inhabited GroupWithZero := ⟨of (with_zero punit)⟩
+
+instance : large_category.{u} GroupWithZero :=
+{ hom := λ X Y, monoid_with_zero_hom X Y,
+  id := λ X, monoid_with_zero_hom.id X,
+  comp := λ X Y Z f g, g.comp f,
+  id_comp' := λ X Y, monoid_with_zero_hom.comp_id,
+  comp_id' := λ X Y, monoid_with_zero_hom.id_comp,
+  assoc' := λ W X Y Z _ _ _, monoid_with_zero_hom.comp_assoc _ _ _ }
+
+instance : concrete_category GroupWithZero :=
+{ forget := ⟨coe_sort, λ X Y, coe_fn, λ X, rfl, λ X Y Z f g, rfl⟩,
+  forget_faithful := ⟨λ X Y f g h, fun_like.coe_injective h⟩ }
+
+instance has_forget_to_Bipointed : has_forget₂ GroupWithZero Bipointed :=
+{ forget₂ := { obj := λ X, ⟨X, 0, 1⟩, map := λ X Y f, ⟨f, f.map_zero', f.map_one'⟩ } }
+
+instance has_forget_to_Mon : has_forget₂ GroupWithZero Mon :=
+{ forget₂ := { obj := λ X, ⟨X⟩, map := λ X Y, monoid_with_zero_hom.to_monoid_hom } }
+
+/-- Constructs an isomorphism of groups with zero from a group isomorphism between them. -/
+@[simps] def iso.mk {α β : GroupWithZero.{u}} (e : α ≃* β) : α ≅ β :=
+{ 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 _ } }
+
+end GroupWithZero

src/data/equiv/mul_add.lean

@@ -31,8 +31,7 @@ these are deprecated.
 equiv, mul_equiv, add_equiv
 -/
 
-variables {A : Type*} {B : Type*} {M : Type*} {N : Type*}
-  {P : Type*} {Q : Type*} {G : Type*} {H : Type*}
+variables {α β A B M N P Q G H : Type*}
 
 /-- Makes a multiplicative inverse from a bijection which preserves multiplication. -/
 @[to_additive "Makes an additive inverse from a bijection which preserves addition."]
@@ -114,6 +113,13 @@ instance [mul_one_class M] [mul_one_class N] [mul_equiv_class F M N] :
        ... = 1 : right_inv e 1,
   .. mul_equiv_class.mul_hom_class F }
 
+@[priority 100] -- See note [lower instance priority]
+instance to_monoid_with_zero_hom_class {α β : Type*} [mul_zero_one_class α]
+  [mul_zero_one_class β] [mul_equiv_class F α β] : monoid_with_zero_hom_class F α β :=
+{ map_zero := λ e, calc e 0 = e 0 * e (equiv_like.inv e 0) : by rw [←map_mul, zero_mul]
+                        ... = 0 : by { convert mul_zero _, exact equiv_like.right_inv e _ }
+  ..mul_equiv_class.monoid_hom_class _ }
+
 variables {F}
 
 @[simp, to_additive]