chore(CategoryTheory): rename ConcreteCategory to HasForget (leanprover-community#20809)

This is the first step towards a concrete category redesign, as outlined in this Zulip post: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20category.20class.20redesign/near/493903980

This commit was generated by find-and-replacing `ConcreteCategory` and `concreteCategory` with `HasForget` and `hasForget` respectively, making sure not to touch imports. I did not look too closely at the changes, since we should be going over everything during the redesign anyway.

`ConcreteCategory` is now temporarily an alias for `HasForget`, with a deprecation warning.

The `ConcreteCategory` namespace itself was not renamed, since we'll eventually be redoing those results for the new `ConcreteCategory` class.

Author: Vierkantor

Mathlib/Algebra/Category/AlgebraCat/Basic.lean

@@ -127,7 +127,7 @@ lemma hom_inv_apply {A B : AlgebraCat.{v} R} (e : A ≅ B) (x : B) : e.hom (e.in
 instance : Inhabited (AlgebraCat R) :=
   ⟨of R R⟩
 
-instance : ConcreteCategory.{v} (AlgebraCat.{v} R) where
+instance : HasForget.{v} (AlgebraCat.{v} R) where
   forget :=
     { obj := fun R => R
       map := fun f => f.hom }

Mathlib/Algebra/Category/BialgebraCat/Basic.lean

@@ -95,7 +95,7 @@ abbrev ofHom {X Y : Type v} [Ring X] [Ring Y]
     Hom.toBialgHom (𝟙 M) = BialgHom.id _ _ :=
   rfl
 
-instance concreteCategory : ConcreteCategory.{v} (BialgebraCat.{v} R) where
+instance hasForget : HasForget.{v} (BialgebraCat.{v} R) where
   forget :=
     { obj := fun M => M
       map := fun f => f.toBialgHom }

Mathlib/Algebra/Category/BoolRing.lean

@@ -71,7 +71,7 @@ lemma hom_ext {R S : BoolRing} {f g : R ⟶ S} (hf : f.hom = g.hom) : f = g :=
 abbrev ofHom {R S : Type u} [BooleanRing R] [BooleanRing S] (f : R →+* S) : of R ⟶ of S :=
   ⟨f⟩
 
-instance : ConcreteCategory BoolRing where
+instance : HasForget BoolRing where
   forget :=
     { obj := fun R ↦ R
       map := fun f ↦ f.hom }

Mathlib/Algebra/Category/CoalgebraCat/Basic.lean

@@ -96,7 +96,7 @@ abbrev ofHom {X Y : Type v} [AddCommGroup X] [Module R X] [AddCommGroup Y] [Modu
     Hom.toCoalgHom (𝟙 M) = CoalgHom.id _ _ :=
   rfl
 
-instance concreteCategory : ConcreteCategory.{v} (CoalgebraCat.{v} R) where
+instance hasForget : HasForget.{v} (CoalgebraCat.{v} R) where
   forget :=
     { obj := fun M => M
       map := fun f => f.toCoalgHom }

Mathlib/Algebra/Category/FGModuleCat/Basic.lean

@@ -46,7 +46,7 @@ def FGModuleCat :=
   FullSubcategory fun V : ModuleCat.{u} R => Module.Finite R V
 -- Porting note: still no derive handler via `dsimp`.
 -- see https://github.com/leanprover-community/mathlib4/issues/5020
--- deriving LargeCategory, ConcreteCategory,Preadditive
+-- deriving LargeCategory, HasForget,Preadditive
 
 variable {R}
 
@@ -72,7 +72,7 @@ instance : LargeCategory (FGModuleCat R) := by
   dsimp [FGModuleCat]
   infer_instance
 
-instance : ConcreteCategory (FGModuleCat R) := by
+instance : HasForget (FGModuleCat R) := by
   dsimp [FGModuleCat]
   infer_instance
 

Mathlib/Algebra/Category/Grp/Basic.lean

@@ -42,7 +42,7 @@ deriving instance LargeCategory for Grp
 attribute [to_additive] instGrpLargeCategory
 
 @[to_additive]
-instance concreteCategory : ConcreteCategory Grp := by
+instance hasForget : HasForget Grp := by
   dsimp only [Grp]
   infer_instance
 
@@ -171,7 +171,7 @@ deriving instance LargeCategory for CommGrp
 attribute [to_additive] instCommGrpLargeCategory
 
 @[to_additive]
-instance concreteCategory : ConcreteCategory CommGrp := by
+instance hasForget : HasForget CommGrp := by
   dsimp only [CommGrp]
   infer_instance
 

Mathlib/Algebra/Category/Grp/FiniteGrp.lean

@@ -44,7 +44,7 @@ instance : CoeSort FiniteGrp.{u} (Type u) where
 instance : Category FiniteGrp := InducedCategory.category FiniteGrp.toGrp
 
 @[to_additive]
-instance : ConcreteCategory FiniteGrp := InducedCategory.concreteCategory FiniteGrp.toGrp
+instance : HasForget FiniteGrp := InducedCategory.hasForget FiniteGrp.toGrp
 
 @[to_additive]
 instance (G : FiniteGrp) : Group G := inferInstanceAs <| Group G.toGrp

Mathlib/Algebra/Category/GrpWithZero.lean

@@ -56,7 +56,7 @@ lemma coe_id {X : GrpWithZero} : (𝟙 X : X → X) = id := rfl
 
 lemma coe_comp {X Y Z : GrpWithZero} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
-instance groupWithZeroConcreteCategory : ConcreteCategory GrpWithZero where
+instance groupWithZeroHasForget : HasForget GrpWithZero where
   forget :=
   { obj := fun G => G
     map := fun f => f.toFun }

Mathlib/Algebra/Category/HopfAlgebraCat/Basic.lean

@@ -94,7 +94,7 @@ abbrev ofHom {X Y : Type v} [Ring X] [Ring Y]
     Hom.toBialgHom (𝟙 M) = BialgHom.id _ _ :=
   rfl
 
-instance concreteCategory : ConcreteCategory.{v} (HopfAlgebraCat.{v} R) where
+instance hasForget : HasForget.{v} (HopfAlgebraCat.{v} R) where
   forget :=
     { obj := fun M => M
       map := fun f => f.toBialgHom }

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -188,7 +188,7 @@ end
 instance : Inhabited (ModuleCat R) :=
   ⟨of R R⟩
 
-instance moduleConcreteCategory : ConcreteCategory.{v} (ModuleCat.{v} R) where
+instance moduleHasForget : HasForget.{v} (ModuleCat.{v} R) where
   forget :=
     { obj := fun R => R
       map := fun f => f.hom }