From ecef68622cf98f6d42c459e5b5a079aeecdd9842 Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Fri, 15 Jul 2022 12:02:32 +0000
Subject: [PATCH] feat(algebra/category/Group):  The forgetful-units adjunction
 between `Group` and `Mon`. (#15330)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
---
 src/algebra/category/Group/adjunctions.lean | 54 +++++++++++++++++++++
 1 file changed, 54 insertions(+)

diff --git a/src/algebra/category/Group/adjunctions.lean b/src/algebra/category/Group/adjunctions.lean
index 5b99034bb7177..64f2caf41d79c 100644
--- a/src/algebra/category/Group/adjunctions.lean
+++ b/src/algebra/category/Group/adjunctions.lean
@@ -118,3 +118,57 @@ adjunction.mk_of_hom_equiv
   hom_equiv_naturality_left_symm' := λ G H A f g, by { ext1, refl } }
 
 end abelianization
+
+/-- The functor taking a monoid to its subgroup of units. -/
+@[simps]
+def Mon.units : Mon.{u} ⥤ Group.{u} :=
+{ obj := λ R, Group.of Rˣ,
+  map := λ R S f, Group.of_hom $ units.map f,
+  map_id' := λ X, monoid_hom.ext (λ x, units.ext rfl),
+  map_comp' := λ X Y Z f g, monoid_hom.ext (λ x, units.ext rfl) }
+
+/-- The forgetful-units adjunction between `Group` and `Mon`. -/
+def Group.forget₂_Mon_adj : forget₂ Group Mon ⊣ Mon.units.{u} :=
+{ hom_equiv := λ X Y,
+  { to_fun := λ f, monoid_hom.to_hom_units f,
+    inv_fun := λ f, (units.coe_hom Y).comp f,
+    left_inv := λ f, monoid_hom.ext $ λ _, rfl,
+    right_inv := λ f, monoid_hom.ext $ λ _, units.ext rfl },
+  unit :=
+  { app := λ X, { ..(@to_units X _).to_monoid_hom },
+    naturality' := λ X Y f, monoid_hom.ext $ λ x, units.ext rfl },
+  counit :=
+  { app := λ X, units.coe_hom X,
+    naturality' := λ X Y f, monoid_hom.ext $ λ x, rfl },
+  hom_equiv_unit' := λ X Y f, monoid_hom.ext $ λ _, units.ext rfl,
+  hom_equiv_counit' := λ X Y f, monoid_hom.ext $ λ _, rfl }
+
+instance : is_right_adjoint Mon.units.{u} :=
+⟨_, Group.forget₂_Mon_adj⟩
+
+/-- The functor taking a monoid to its subgroup of units. -/
+@[simps]
+def CommMon.units : CommMon.{u} ⥤ CommGroup.{u} :=
+{ obj := λ R, CommGroup.of Rˣ,
+  map := λ R S f, CommGroup.of_hom $ units.map f,
+  map_id' := λ X, monoid_hom.ext (λ x, units.ext rfl),
+  map_comp' := λ X Y Z f g, monoid_hom.ext (λ x, units.ext rfl) }
+
+/-- The forgetful-units adjunction between `CommGroup` and `CommMon`. -/
+def CommGroup.forget₂_CommMon_adj : forget₂ CommGroup CommMon ⊣ CommMon.units.{u} :=
+{ hom_equiv := λ X Y,
+  { to_fun := λ f, monoid_hom.to_hom_units f,
+    inv_fun := λ f, (units.coe_hom Y).comp f,
+    left_inv := λ f, monoid_hom.ext $ λ _, rfl,
+    right_inv := λ f, monoid_hom.ext $ λ _, units.ext rfl },
+  unit :=
+  { app := λ X, { ..(@to_units X _).to_monoid_hom },
+    naturality' := λ X Y f, monoid_hom.ext $ λ x, units.ext rfl },
+  counit :=
+  { app := λ X, units.coe_hom X,
+    naturality' := λ X Y f, monoid_hom.ext $ λ x, rfl },
+  hom_equiv_unit' := λ X Y f, monoid_hom.ext $ λ _, units.ext rfl,
+  hom_equiv_counit' := λ X Y f, monoid_hom.ext $ λ _, rfl }
+
+instance : is_right_adjoint CommMon.units.{u} :=
+⟨_, CommGroup.forget₂_CommMon_adj⟩