chore(CategoryTheory): move instances from FullSubcategory to ObjectProperty.FullSubcategory (leanprover-community#38221)

Move some instances for `CategoryTheory.ObjectProperty.FullSubcategory` to the correct namespace.

Author: peabrainiac

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

@@ -195,8 +195,7 @@ instance InducedCategory.concreteCategory {C : Type u} {D : Type u'} [Category.{
   comp_apply _ _ _ := ConcreteCategory.comp_apply _ _ _
   id_apply _ := ConcreteCategory.id_apply _
 
-open ObjectProperty in
-instance FullSubcategory.concreteCategory {C : Type u} [Category.{v} C]
+instance ObjectProperty.FullSubcategory.concreteCategory {C : Type u} [Category.{v} C]
     {FC : C → C → Type*} {CC : C → Type w} [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)]
     [ConcreteCategory.{w} C FC]
     (P : ObjectProperty C) : ConcreteCategory P.FullSubcategory (fun X Y => FC X.1 Y.1) where
@@ -207,6 +206,9 @@ instance FullSubcategory.concreteCategory {C : Type u} [Category.{v} C]
   comp_apply _ _ _ := ConcreteCategory.comp_apply _ _ _
   id_apply _ := ConcreteCategory.id_apply _
 
+@[deprecated (since := "2026-04-18")] alias FullSubcategory.concreteCategory :=
+  ObjectProperty.FullSubcategory.concreteCategory
+
 end ConcreteCategory
 
 variable {C : Type u} [Category.{v} C]

Mathlib/CategoryTheory/ConcreteCategory/Forget.lean

@@ -111,10 +111,14 @@ instance InducedCategory.hasForget₂ (f : C → D) : HasForget₂ (InducedCateg
   forget₂ := inducedFunctor f
   forget_comp := rfl
 
-instance FullSubcategory.hasForget₂ (P : ObjectProperty C) : HasForget₂ P.FullSubcategory C where
+instance ObjectProperty.FullSubcategory.hasForget₂ (P : ObjectProperty C) :
+    HasForget₂ P.FullSubcategory C where
   forget₂ := P.ι
   forget_comp := rfl
 
+@[deprecated (since := "2026-04-18")] alias FullSubcategory.hasForget₂ :=
+  ObjectProperty.FullSubcategory.hasForget₂
+
 /-- In order to construct a “partially forgetting” functor, we do not need to verify functor laws;
 it suffices to ensure that compositions agree with `forget₂ C D ⋙ forget D = forget C`.
 -/