chore(CategoryTheory): move Full, Faithful, EssSurj, IsEquivalence and ReflectsIsomorphisms to the Functor namespace (#11985)

These notions on functors are now `Functor.Full`, `Functor.Faithful`, `Functor.EssSurj`, `Functor.IsEquivalence`, `Functor.ReflectsIsomorphisms`. Deprecated aliases are introduced for the previous names.

Author: joelriou

Mathlib/Algebra/Category/AlgebraCat/Basic.lean

@@ -247,7 +247,7 @@ def algEquivIsoAlgebraIso {X Y : Type u} [Ring X] [Ring Y] [Algebra R X] [Algebr
 instance (X : Type u) [Ring X] [Algebra R X] : CoeOut (Subalgebra R X) (AlgebraCat R) :=
   ⟨fun N => AlgebraCat.of R N⟩
 
-instance AlgebraCat.forget_reflects_isos : ReflectsIsomorphisms (forget (AlgebraCat.{u} R)) where
+instance AlgebraCat.forget_reflects_isos : (forget (AlgebraCat.{u} R)).ReflectsIsomorphisms where
   reflects {X Y} f _ := by
     let i := asIso ((forget (AlgebraCat.{u} R)).map f)
     let e : X ≃ₐ[R] Y := { f, i.toEquiv with }

Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean

@@ -99,7 +99,7 @@ def toModuleCatMonoidalFunctor : MonoidalFunctor (AlgebraCat.{u} R) (ModuleCat.{
   unfold instMonoidalCategory
   exact Monoidal.fromInduced (forget₂ (AlgebraCat R) (ModuleCat R)) _
 
-instance : Faithful (toModuleCatMonoidalFunctor R).toFunctor :=
+instance : (toModuleCatMonoidalFunctor R).Faithful :=
   forget₂_faithful _ _
 
 end

Mathlib/Algebra/Category/AlgebraCat/Symmetric.lean

@@ -35,7 +35,7 @@ variable (R) in
 def toModuleCatBraidedFunctor : BraidedFunctor (AlgebraCat.{u} R) (ModuleCat.{u} R) where
   toMonoidalFunctor := toModuleCatMonoidalFunctor R
 
-instance : Faithful (toModuleCatBraidedFunctor R).toFunctor :=
+instance : (toModuleCatBraidedFunctor R).Faithful :=
   forget₂_faithful _ _
 
 instance instSymmetricCategory : SymmetricCategory (AlgebraCat.{u} R) :=

Mathlib/Algebra/Category/FGModuleCat/Basic.lean

@@ -118,7 +118,7 @@ instance : HasForget₂ (FGModuleCat.{u} R) (ModuleCat.{u} R) := by
   dsimp [FGModuleCat]
   infer_instance
 
-instance : Full (forget₂ (FGModuleCat R) (ModuleCat.{u} R)) where
+instance : (forget₂ (FGModuleCat R) (ModuleCat.{u} R)).Full where
   preimage f := f
 
 variable {R}
@@ -183,19 +183,19 @@ def forget₂Monoidal : MonoidalFunctor (FGModuleCat R) (ModuleCat.{u} R) :=
   MonoidalCategory.fullMonoidalSubcategoryInclusion _
 #align fgModule.forget₂_monoidal FGModuleCat.forget₂Monoidal
 
-instance forget₂Monoidal_faithful : Faithful (forget₂Monoidal R).toFunctor := by
+instance forget₂Monoidal_faithful : (forget₂Monoidal R).Faithful := by
   dsimp [forget₂Monoidal]
   -- Porting note (#11187): was `infer_instance`
   exact FullSubcategory.faithful _
 #align fgModule.forget₂_monoidal_faithful FGModuleCat.forget₂Monoidal_faithful
 
-instance forget₂Monoidal_additive : (forget₂Monoidal R).toFunctor.Additive := by
+instance forget₂Monoidal_additive : (forget₂Monoidal R).Additive := by
   dsimp [forget₂Monoidal]
   -- Porting note (#11187): was `infer_instance`
   exact Functor.fullSubcategoryInclusion_additive _
 #align fgModule.forget₂_monoidal_additive FGModuleCat.forget₂Monoidal_additive
 
-instance forget₂Monoidal_linear : (forget₂Monoidal R).toFunctor.Linear R := by
+instance forget₂Monoidal_linear : (forget₂Monoidal R).Linear R := by
   dsimp [forget₂Monoidal]
   -- Porting note (#11187): was `infer_instance`
   exact Functor.fullSubcategoryInclusionLinear _ _

Mathlib/Algebra/Category/GroupCat/Basic.lean

@@ -485,7 +485,7 @@ set_option linter.uppercaseLean3 false in
 end CategoryTheory.Aut
 
 @[to_additive]
-instance GroupCat.forget_reflects_isos : ReflectsIsomorphisms (forget GroupCat.{u}) where
+instance GroupCat.forget_reflects_isos : (forget GroupCat.{u}).ReflectsIsomorphisms where
   reflects {X Y} f _ := by
     let i := asIso ((forget GroupCat).map f)
     let e : X ≃* Y := { i.toEquiv with map_mul' := map_mul _ }
@@ -496,7 +496,7 @@ set_option linter.uppercaseLean3 false in
 #align AddGroup.forget_reflects_isos AddGroupCat.forget_reflects_isos
 
 @[to_additive]
-instance CommGroupCat.forget_reflects_isos : ReflectsIsomorphisms (forget CommGroupCat.{u}) where
+instance CommGroupCat.forget_reflects_isos : (forget CommGroupCat.{u}).ReflectsIsomorphisms where
   reflects {X Y} f _ := by
     let i := asIso ((forget CommGroupCat).map f)
     let e : X ≃* Y := { i.toEquiv with map_mul' := map_mul _}

Mathlib/Algebra/Category/GroupCat/Limits.lean

@@ -86,7 +86,7 @@ reuse the existing limit."]
 noncomputable instance Forget₂.createsLimit :
     CreatesLimit F (forget₂ GroupCat.{u} MonCat.{u}) :=
   -- Porting note: need to add `forget₂ GrpCat MonCat` reflects isomorphism
-  letI : ReflectsIsomorphisms (forget₂ GroupCat.{u} MonCat.{u}) :=
+  letI : (forget₂ GroupCat.{u} MonCat.{u}).ReflectsIsomorphisms :=
     CategoryTheory.reflectsIsomorphisms_forget₂ _ _
   createsLimitOfReflectsIso (K := F) (F := (forget₂ GroupCat.{u} MonCat.{u}))
     fun c' t =>
@@ -258,7 +258,7 @@ and then reuse the existing limit.
   and then reuse the existing limit."]
 noncomputable instance Forget₂.createsLimit :
     CreatesLimit F (forget₂ CommGroupCat GroupCat.{u}) :=
-  letI : ReflectsIsomorphisms (forget₂ CommGroupCat.{u} GroupCat.{u}) :=
+  letI : (forget₂ CommGroupCat.{u} GroupCat.{u}).ReflectsIsomorphisms :=
     CategoryTheory.reflectsIsomorphisms_forget₂ _ _
   letI : Small.{u}
       (Functor.sections ((F ⋙ forget₂ CommGroupCat GroupCat) ⋙ forget GroupCat)) :=

Mathlib/Algebra/Category/GroupCat/ZModuleEquivalence.lean

@@ -26,7 +26,7 @@ universe u
 namespace ModuleCat
 
 /-- The forgetful functor from `ℤ` modules to `AddCommGroup` is full. -/
-instance forget₂AddCommGroupFull : Full (forget₂ (ModuleCat ℤ) AddCommGroupCat.{u}) where
+instance forget₂AddCommGroupFull : (forget₂ (ModuleCat ℤ) AddCommGroupCat.{u}).Full where
   preimage {A B}
     -- `AddMonoidHom.toIntLinearMap` doesn't work here because `A` and `B` are not
     -- definitionally equal to the canonical `AddCommGroup.intModule` module
@@ -41,7 +41,7 @@ set_option linter.uppercaseLean3 false in
 #align Module.forget₂_AddCommGroup_full ModuleCat.forget₂AddCommGroupFull
 
 /-- The forgetful functor from `ℤ` modules to `AddCommGroup` is essentially surjective. -/
-instance forget₂_addCommGroupCat_essSurj : EssSurj (forget₂ (ModuleCat ℤ) AddCommGroupCat.{u}) where
+instance forget₂_addCommGroupCat_essSurj : (forget₂ (ModuleCat ℤ) AddCommGroupCat.{u}).EssSurj where
   mem_essImage A :=
     ⟨ModuleCat.of ℤ A,
       ⟨{  hom := 𝟙 A
@@ -50,8 +50,8 @@ set_option linter.uppercaseLean3 false in
 #align Module.forget₂_AddCommGroup_ess_surj ModuleCat.forget₂_addCommGroupCat_essSurj
 
 noncomputable instance forget₂AddCommGroupIsEquivalence :
-    IsEquivalence (forget₂ (ModuleCat ℤ) AddCommGroupCat.{u}) :=
-  Equivalence.ofFullyFaithfullyEssSurj (forget₂ (ModuleCat ℤ) AddCommGroupCat)
+    (forget₂ (ModuleCat ℤ) AddCommGroupCat.{u}).IsEquivalence :=
+  Functor.IsEquivalence.ofFullyFaithfullyEssSurj (forget₂ (ModuleCat ℤ) AddCommGroupCat)
 set_option linter.uppercaseLean3 false in
 #align Module.forget₂_AddCommGroup_is_equivalence ModuleCat.forget₂AddCommGroupIsEquivalence
 

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -84,7 +84,7 @@ def restrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →
 #align category_theory.Module.restrict_scalars ModuleCat.restrictScalars
 
 instance {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
-    CategoryTheory.Faithful (restrictScalars.{v} f) where
+    (restrictScalars.{v} f).Faithful where
   map_injective h :=
     LinearMap.ext fun x => by simpa only using DFunLike.congr_fun h x
 
@@ -216,7 +216,7 @@ abbrev restrictScalarsComp := restrictScalarsComp'.{v} f g _ rfl
 end
 
 instance restrictScalarsIsEquivalenceOfRingEquiv {R S} [Ring R] [Ring S] (e : R ≃+* S) :
-    IsEquivalence (ModuleCat.restrictScalars e.toRingHom) where
+    (ModuleCat.restrictScalars e.toRingHom).IsEquivalence where
   inverse := ModuleCat.restrictScalars e.symm
   unitIso := NatIso.ofComponents (fun M ↦ LinearEquiv.toModuleIso'
     { __ := AddEquiv.refl M

Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

@@ -208,7 +208,7 @@ lemma toPresheaf_map_app {P Q : PresheafOfModules R}
 
 instance : (toPresheaf R).Additive where
 
-instance : Faithful (toPresheaf R) where
+instance : (toPresheaf R).Faithful where
   map_injective {P Q} f g h := by
     ext X x
     have eq := congr_app h X

Mathlib/Algebra/Category/MonCat/Basic.lean

@@ -402,7 +402,7 @@ the same as (isomorphic to) isomorphisms in `AddCommMonCat` -/
 add_decl_doc addEquivIsoAddCommMonCatIso
 
 @[to_additive]
-instance MonCat.forget_reflects_isos : ReflectsIsomorphisms (forget MonCat.{u}) where
+instance MonCat.forget_reflects_isos : (forget MonCat.{u}).ReflectsIsomorphisms where
   reflects {X Y} f _ := by
     let i := asIso ((forget MonCat).map f)
     -- Again a problem that exists already creeps into other things leanprover/lean4#2644
@@ -415,7 +415,7 @@ set_option linter.uppercaseLean3 false in
 #align AddMon.forget_reflects_isos AddMonCat.forget_reflects_isos
 
 @[to_additive]
-instance CommMonCat.forget_reflects_isos : ReflectsIsomorphisms (forget CommMonCat.{u}) where
+instance CommMonCat.forget_reflects_isos : (forget CommMonCat.{u}).ReflectsIsomorphisms where
   reflects {X Y} f _ := by
     let i := asIso ((forget CommMonCat).map f)
     let e : X ≃* Y := MulEquiv.mk i.toEquiv
@@ -431,6 +431,6 @@ set_option linter.uppercaseLean3 false in
 -- automatically reflects isomorphisms
 -- we could have used `CategoryTheory.ConcreteCategory.ReflectsIso` alternatively
 @[to_additive]
-instance CommMonCat.forget₂Full : Full (forget₂ CommMonCat MonCat) where preimage f := f
+instance CommMonCat.forget₂Full : (forget₂ CommMonCat MonCat).Full where preimage f := f
 
-example : ReflectsIsomorphisms (forget₂ CommMonCat MonCat) := inferInstance
+example : (forget₂ CommMonCat MonCat).ReflectsIsomorphisms := inferInstance