feat: if F is fully faithful, then so is F.mapGrp (#27580)

Follow up to #23874. Also remove the corresponding `noncomputable` as they are now unnecessary.

From Toric

Author: YaelDillies

Mathlib/CategoryTheory/Monoidal/CommGrp_.lean

@@ -176,7 +176,7 @@ variable (F) in
 /-- A finite-product-preserving functor takes commutative group objects to commutative group
 objects. -/
 @[simps!]
-noncomputable def mapCommGrp : CommGrp_ C ⥤ CommGrp_ D where
+def mapCommGrp : CommGrp_ C ⥤ CommGrp_ D where
   obj A :=
     { F.mapGrp.obj A.toGrp_ with
       comm :=
@@ -186,6 +186,18 @@ noncomputable def mapCommGrp : CommGrp_ C ⥤ CommGrp_ D where
   map f := F.mapMon.map f
   map_id X := show F.mapMon.map (𝟙 X.toGrp_.toMon_) = _ by aesop_cat
 
+protected instance Faithful.mapCommGrp [F.Faithful] : F.mapCommGrp.Faithful where
+  map_injective hfg := F.mapMon.map_injective hfg
+
+protected instance Full.mapCommGrp [F.Full] [F.Faithful] : F.mapCommGrp.Full where
+  map_surjective := F.mapMon.map_surjective
+
+/-- If `F : C ⥤ D` is a fully faithful monoidal functor, then `Grp(F) : Grp C ⥤ Grp D` is fully
+faithful too. -/
+@[simps]
+protected def FullyFaithful.mapCommGrp (hF : F.FullyFaithful) : F.mapGrp.FullyFaithful where
+  preimage f := .mk <| hF.preimage f.hom
+
 @[simp]
 theorem mapCommGrp_id_one (A : CommGrp_ C) :
     η[((𝟭 C).mapCommGrp.obj A).X] = 𝟙 _ ≫ η[A.X] :=
@@ -208,24 +220,23 @@ theorem comp_mapCommGrp_mul (A : CommGrp_ C) :
 
 /-- The identity functor is also the identity on commutative group objects. -/
 @[simps!]
-noncomputable def mapCommGrpIdIso : mapCommGrp (𝟭 C) ≅ 𝟭 (CommGrp_ C) :=
+def mapCommGrpIdIso : mapCommGrp (𝟭 C) ≅ 𝟭 (CommGrp_ C) :=
   NatIso.ofComponents (fun X ↦ CommGrp_.mkIso (.refl _) (by simp)
     (by simp))
 
 /-- The composition functor is also the composition on commutative group objects. -/
 @[simps!]
-noncomputable def mapCommGrpCompIso : (F ⋙ G).mapCommGrp ≅ F.mapCommGrp ⋙ G.mapCommGrp :=
-  NatIso.ofComponents (fun X ↦ CommGrp_.mkIso (.refl _) (by simp [ε_of_cartesianMonoidalCategory])
-    (by simp [μ_of_cartesianMonoidalCategory]))
+def mapCommGrpCompIso : (F ⋙ G).mapCommGrp ≅ F.mapCommGrp ⋙ G.mapCommGrp :=
+  NatIso.ofComponents fun X ↦ CommGrp_.mkIso (.refl _)
 
 /-- Natural transformations between functors lift to commutative group objects. -/
 @[simps!]
-noncomputable def mapCommGrpNatTrans (f : F ⟶ F') : F.mapCommGrp ⟶ F'.mapCommGrp where
+def mapCommGrpNatTrans (f : F ⟶ F') : F.mapCommGrp ⟶ F'.mapCommGrp where
   app X := .mk' (f.app _)
 
 /-- Natural isomorphisms between functors lift to commutative group objects. -/
 @[simps!]
-noncomputable def mapCommGrpNatIso (e : F ≅ F') : F.mapCommGrp ≅ F'.mapCommGrp :=
+def mapCommGrpNatIso (e : F ≅ F') : F.mapCommGrp ≅ F'.mapCommGrp :=
   NatIso.ofComponents fun X ↦ CommGrp_.mkIso (e.app _)
 
 attribute [local instance] Functor.Braided.ofChosenFiniteProducts in

Mathlib/CategoryTheory/Monoidal/CommMon_.lean

@@ -145,9 +145,11 @@ namespace CategoryTheory
 variable
   {D : Type u₂} [Category.{v₂} D] [MonoidalCategory D] [BraidedCategory D]
   {E : Type u₃} [Category.{v₃} E] [MonoidalCategory E] [BraidedCategory E]
-  {F F' : C ⥤ D} [F.LaxBraided] [F'.LaxBraided] {G : D ⥤ E} [G.LaxBraided]
+  {F F' : C ⥤ D} {G : D ⥤ E}
 
 namespace Functor
+section LaxBraided
+variable [F.LaxBraided] [F'.LaxBraided] [G.LaxBraided]
 
 open scoped Obj
 
@@ -192,12 +194,12 @@ theorem comp_mapCommMon_mul (A : CommMon_ C) :
 
 /-- The identity functor is also the identity on commutative monoid objects. -/
 @[simps!]
-noncomputable def mapCommMonIdIso : mapCommMon (𝟭 C) ≅ 𝟭 (CommMon_ C) :=
+def mapCommMonIdIso : mapCommMon (𝟭 C) ≅ 𝟭 (CommMon_ C) :=
   NatIso.ofComponents fun X ↦ CommMon_.mkIso (.refl _)
 
 /-- The composition functor is also the composition on commutative monoid objects. -/
 @[simps!]
-noncomputable def mapCommMonCompIso : (F ⋙ G).mapCommMon ≅ F.mapCommMon ⋙ G.mapCommMon :=
+def mapCommMonCompIso : (F ⋙ G).mapCommMon ≅ F.mapCommMon ⋙ G.mapCommMon :=
   NatIso.ofComponents fun X ↦ CommMon_.mkIso (.refl _)
 
 variable (C D) in
@@ -208,18 +210,35 @@ def mapCommMonFunctor : LaxBraidedFunctor C D ⥤ CommMon_ C ⥤ CommMon_ D wher
   map α := { app A := .mk' (α.hom.app A.X) }
   map_comp _ _ := rfl
 
+protected instance Faithful.mapCommMon [F.Faithful] : F.mapCommMon.Faithful where
+  map_injective hfg := F.mapMon.map_injective hfg
+
 /-- Natural transformations between functors lift to monoid objects. -/
 @[simps!]
-noncomputable def mapCommMonNatTrans (f : F ⟶ F') [NatTrans.IsMonoidal f] :
-    F.mapCommMon ⟶ F'.mapCommMon where
+def mapCommMonNatTrans (f : F ⟶ F') [NatTrans.IsMonoidal f] : F.mapCommMon ⟶ F'.mapCommMon where
   app X := .mk' (f.app _)
 
 /-- Natural isomorphisms between functors lift to monoid objects. -/
 @[simps!]
-noncomputable def mapCommMonNatIso (e : F ≅ F') [NatTrans.IsMonoidal e.hom] :
-    F.mapCommMon ≅ F'.mapCommMon :=
+def mapCommMonNatIso (e : F ≅ F') [NatTrans.IsMonoidal e.hom] : F.mapCommMon ≅ F'.mapCommMon :=
   NatIso.ofComponents fun X ↦ CommMon_.mkIso (e.app _)
 
+end LaxBraided
+
+section Braided
+variable [F.Braided]
+
+protected instance Full.mapCommMon [F.Full] [F.Faithful] : F.mapCommMon.Full where
+  map_surjective := F.mapMon.map_surjective
+
+/-- If `F : C ⥤ D` is a fully faithful monoidal functor, then `Grp(F) : Grp C ⥤ Grp D` is fully
+faithful too. -/
+@[simps]
+protected def FullyFaithful.mapCommMon (hF : F.FullyFaithful) : F.mapCommMon.FullyFaithful where
+  preimage f := .mk <| hF.preimage f.hom
+
+end Braided
+
 end Functor
 
 open Functor
@@ -229,7 +248,7 @@ variable {F : C ⥤ D} {G : D ⥤ C} (a : F ⊣ G) [F.Braided] [G.LaxBraided] [a
 
 /-- An adjunction of braided functors lifts to an adjunction of their lifts to commutative monoid
 objects. -/
-@[simps] noncomputable def mapCommMon : F.mapCommMon ⊣ G.mapCommMon where
+@[simps] def mapCommMon : F.mapCommMon ⊣ G.mapCommMon where
   unit := mapCommMonIdIso.inv ≫ mapCommMonNatTrans a.unit ≫ mapCommMonCompIso.hom
   counit := mapCommMonCompIso.inv ≫ mapCommMonNatTrans a.counit ≫ mapCommMonIdIso.hom
 
@@ -239,7 +258,7 @@ namespace Equivalence
 
 /-- An equivalence of categories lifts to an equivalence of their commutative monoid objects. -/
 @[simps]
-noncomputable def mapCommMon (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] [e.IsMonoidal] :
+def mapCommMon (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] [e.IsMonoidal] :
     CommMon_ C ≌ CommMon_ D where
   functor := e.functor.mapCommMon
   inverse := e.inverse.mapCommMon

Mathlib/CategoryTheory/Monoidal/Grp_.lean

@@ -338,7 +338,7 @@ open Monoidal
 variable (F) in
 /-- A finite-product-preserving functor takes group objects to group objects. -/
 @[simps!]
-noncomputable def mapGrp : Grp_ C ⥤ Grp_ D where
+def mapGrp : Grp_ C ⥤ Grp_ D where
   obj A :=
     { F.mapMon.obj A.toMon_ with
       grp :=
@@ -351,6 +351,18 @@ noncomputable def mapGrp : Grp_ C ⥤ Grp_ D where
             Functor.Monoidal.toUnit_ε_assoc, ← Functor.map_comp] } }
   map f := F.mapMon.map f
 
+protected instance Faithful.mapGrp [F.Faithful] : F.mapGrp.Faithful where
+  map_injective hfg := F.mapMon.map_injective hfg
+
+protected instance Full.mapGrp [F.Full] [F.Faithful] : F.mapGrp.Full where
+  map_surjective := F.mapMon.map_surjective
+
+/-- If `F : C ⥤ D` is a fully faithful monoidal functor, then `Grp(F) : Grp C ⥤ Grp D` is fully
+faithful too. -/
+@[simps]
+protected def FullyFaithful.mapGrp (hF : F.FullyFaithful) : F.mapGrp.FullyFaithful where
+  preimage f := .mk <| hF.preimage f.hom
+
 @[simp]
 theorem mapGrp_id_one (A : Grp_ C) :
     η[((𝟭 C).mapGrp.obj A).X] = 𝟙 _ ≫ η[A.X] :=
@@ -373,24 +385,22 @@ theorem comp_mapGrp_mul (A : Grp_ C) :
 
 /-- The identity functor is also the identity on group objects. -/
 @[simps!]
-noncomputable def mapGrpIdIso : mapGrp (𝟭 C) ≅ 𝟭 (Grp_ C) :=
-  NatIso.ofComponents (fun X ↦ Grp_.mkIso (.refl _) (by simp)
-    (by simp))
+def mapGrpIdIso : mapGrp (𝟭 C) ≅ 𝟭 (Grp_ C) :=
+  NatIso.ofComponents fun X ↦ Grp_.mkIso (.refl _)
 
 /-- The composition functor is also the composition on group objects. -/
 @[simps!]
-noncomputable def mapGrpCompIso : (F ⋙ G).mapGrp ≅ F.mapGrp ⋙ G.mapGrp :=
-  NatIso.ofComponents (fun X ↦ Grp_.mkIso (.refl _) (by simp [ε_of_cartesianMonoidalCategory])
-    (by simp [μ_of_cartesianMonoidalCategory]))
+def mapGrpCompIso : (F ⋙ G).mapGrp ≅ F.mapGrp ⋙ G.mapGrp :=
+  NatIso.ofComponents fun X ↦ Grp_.mkIso (.refl _)
 
 /-- Natural transformations between functors lift to group objects. -/
 @[simps!]
-noncomputable def mapGrpNatTrans (f : F ⟶ F') : F.mapGrp ⟶ F'.mapGrp where
+def mapGrpNatTrans (f : F ⟶ F') : F.mapGrp ⟶ F'.mapGrp where
   app X := .mk' (f.app _)
 
 /-- Natural isomorphisms between functors lift to group objects. -/
 @[simps!]
-noncomputable def mapGrpNatIso (e : F ≅ F') : F.mapGrp ≅ F'.mapGrp :=
+def mapGrpNatIso (e : F ≅ F') : F.mapGrp ≅ F'.mapGrp :=
   NatIso.ofComponents fun X ↦ Grp_.mkIso (e.app _)
 
 attribute [local instance] Monoidal.ofChosenFiniteProducts in
@@ -408,7 +418,7 @@ namespace Adjunction
 variable {F : C ⥤ D} {G : D ⥤ C} (a : F ⊣ G) [F.Monoidal] [G.Monoidal]
 
 /-- An adjunction of monoidal functors lifts to an adjunction of their lifts to group objects. -/
-@[simps] noncomputable def mapGrp : F.mapGrp ⊣ G.mapGrp where
+@[simps] def mapGrp : F.mapGrp ⊣ G.mapGrp where
   unit := mapGrpIdIso.inv ≫ mapGrpNatTrans a.unit ≫ mapGrpCompIso.hom
   counit := mapGrpCompIso.inv ≫ mapGrpNatTrans a.counit ≫ mapGrpIdIso.hom
 
@@ -418,7 +428,7 @@ namespace Equivalence
 variable (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal]
 
 /-- An equivalence of categories lifts to an equivalence of their group objects. -/
-@[simps] noncomputable def mapGrp : Grp_ C ≌ Grp_ D where
+@[simps] def mapGrp : Grp_ C ≌ Grp_ D where
   functor := e.functor.mapGrp
   inverse := e.inverse.mapGrp
   unitIso := mapGrpIdIso.symm ≪≫ mapGrpNatIso e.unitIso ≪≫ mapGrpCompIso

Mathlib/CategoryTheory/Monoidal/Mon_.lean

@@ -304,25 +304,25 @@ theorem comp_mapMon_mul (X : Mon_ C) :
 
 /-- The identity functor is also the identity on monoid objects. -/
 @[simps!]
-noncomputable def mapMonIdIso : mapMon (𝟭 C) ≅ 𝟭 (Mon_ C) :=
+def mapMonIdIso : mapMon (𝟭 C) ≅ 𝟭 (Mon_ C) :=
   NatIso.ofComponents fun X ↦ Mon_.mkIso (.refl _)
 
 /-- The composition functor is also the composition on monoid objects. -/
 @[simps!]
-noncomputable def mapMonCompIso : (F ⋙ G).mapMon ≅ F.mapMon ⋙ G.mapMon :=
+def mapMonCompIso : (F ⋙ G).mapMon ≅ F.mapMon ⋙ G.mapMon :=
   NatIso.ofComponents fun X ↦ Mon_.mkIso (.refl _)
 
 protected instance Faithful.mapMon [F.Faithful] : F.mapMon.Faithful where
   map_injective {_X _Y} _f _g hfg := Mon_.Hom.ext <| map_injective congr(($hfg).hom)
 
 /-- Natural transformations between functors lift to monoid objects. -/
 @[simps!]
-noncomputable def mapMonNatTrans (f : F ⟶ F') [NatTrans.IsMonoidal f] : F.mapMon ⟶ F'.mapMon where
+def mapMonNatTrans (f : F ⟶ F') [NatTrans.IsMonoidal f] : F.mapMon ⟶ F'.mapMon where
   app X := .mk' (f.app _)
 
 /-- Natural isomorphisms between functors lift to monoid objects. -/
 @[simps!]
-noncomputable def mapMonNatIso (e : F ≅ F') [NatTrans.IsMonoidal e.hom] : F.mapMon ≅ F'.mapMon :=
+def mapMonNatIso (e : F ≅ F') [NatTrans.IsMonoidal e.hom] : F.mapMon ≅ F'.mapMon :=
   NatIso.ofComponents fun X ↦ Mon_.mkIso (e.app _)
 
 end LaxMonoidal
@@ -351,6 +351,7 @@ instance FullyFaithful.isMon_Hom_preimage (hF : F.FullyFaithful) {X Y : C}
 
 /-- If `F : C ⥤ D` is a fully faithful monoidal functor, then `Mon(F) : Mon C ⥤ Mon D` is fully
 faithful too. -/
+@[simps]
 protected def FullyFaithful.mapMon (hF : F.FullyFaithful) : F.mapMon.FullyFaithful where
   preimage {X Y} f := .mk' <| hF.preimage f.hom
 
@@ -372,7 +373,7 @@ namespace Adjunction
 variable {F : C ⥤ D} {G : D ⥤ C} (a : F ⊣ G) [F.Monoidal] [G.LaxMonoidal] [a.IsMonoidal]
 
 /-- An adjunction of monoidal functors lifts to an adjunction of their lifts to monoid objects. -/
-@[simps] noncomputable def mapMon : F.mapMon ⊣ G.mapMon where
+@[simps] def mapMon : F.mapMon ⊣ G.mapMon where
   unit := mapMonIdIso.inv ≫ mapMonNatTrans a.unit ≫ mapMonCompIso.hom
   counit := mapMonCompIso.inv ≫ mapMonNatTrans a.counit ≫ mapMonIdIso.hom
 
@@ -382,7 +383,7 @@ namespace Equivalence
 
 /-- An equivalence of categories lifts to an equivalence of their monoid objects. -/
 @[simps]
-noncomputable def mapMon (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] :
+def mapMon (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal] :
     Mon_ C ≌ Mon_ D where
   functor := e.functor.mapMon
   inverse := e.inverse.mapMon