refactor(*): get rid of (forget _).obj and (forget _).map (#21727)

This PR tries getting rid of `HasForget.forget` by searching for `\(forget .*\).(obj|map)` and removing all the occurrences where they could become `ConcreteCategory.hom`. In particular, they should no longer be written in any theorem statement. There are still a few places, generally in the middle of proving properties of the forgetful functor itself, where it was nicer to keep `HasForget`.

The final step is to modify the `elementwise` attribute to produce `ConcreteCategory` lemmas, and the refactor itself is done. After that point, we should still go through and try to clean up the workarounds left behind. But that can be done at a lower priority.



Co-authored-by: Johan Commelin <johan@commelin.net>

Author: Vierkantor

Mathlib/Algebra/Category/AlgebraCat/Limits.lean

@@ -100,9 +100,6 @@ def limitCone : Cone F where
 def limitConeIsLimit : IsLimit (limitCone.{v, w} F) := by
   refine
     IsLimit.ofFaithful (forget (AlgebraCat R)) (Types.Small.limitConeIsLimit.{v, w} _)
-      -- Porting note: in mathlib3 the function term
-      -- `fun v => ⟨fun j => ((forget (AlgebraCat R)).mapCone s).π.app j v`
-      -- was provided by unification, and the last argument `(fun s => _)` was `(fun s => rfl)`.
       (fun s => ofHom
         { toFun := _, map_one' := ?_, map_mul' := ?_, map_zero' := ?_, map_add' := ?_,
           commutes' := ?_ })

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -206,20 +206,11 @@ instance : Inhabited (ModuleCat R) :=
 definitional equality issues. -/
 lemma forget_obj {M : ModuleCat.{v} R} : (forget (ModuleCat.{v} R)).obj M = M := rfl
 
-/- Not a `@[simp]` lemma since the LHS is a categorical arrow and the RHS is a plain function. -/
+@[simp]
 lemma forget_map {M N : ModuleCat.{v} R} (f : M ⟶ N) :
     (forget (ModuleCat.{v} R)).map f = f :=
   rfl
 
--- Porting note:
--- One might hope these two instances would not be needed,
--- as we already have `AddCommGroup M` and `Module R M`,
--- but sometimes we seem to need these when rewriting by lemmas about generic concrete categories.
-instance {M : ModuleCat.{v} R} : AddCommGroup ((forget (ModuleCat R)).obj M) :=
-  (inferInstance : AddCommGroup M)
-instance {M : ModuleCat.{v} R} : Module R ((forget (ModuleCat R)).obj M) :=
-  (inferInstance : Module R M)
-
 instance hasForgetToAddCommGroup : HasForget₂ (ModuleCat R) AddCommGrp where
   forget₂ :=
     { obj := fun M => AddCommGrp.of M

Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

@@ -97,7 +97,7 @@ lemma comp_app {M₁ M₂ M₃ : PresheafOfModules R} (f : M₁ ⟶ M₂) (g : M
 
 lemma naturality_apply (f : M₁ ⟶ M₂) {X Y : Cᵒᵖ} (g : X ⟶ Y) (x : M₁.obj X) :
     Hom.app f Y (M₁.map g x) = M₂.map g (Hom.app f X x) :=
-  congr_fun ((forget _).congr_map (Hom.naturality f g)) x
+  CategoryTheory.congr_fun (Hom.naturality f g) x
 
 /-- Constructor for isomorphisms in the category of presheaves of modules. -/
 @[simps!]
@@ -190,7 +190,7 @@ def homMk (φ : M₁.presheaf ⟶ M₂.presheaf)
       map_smul' := hφ X }
   naturality := fun f ↦ by
     ext x
-    exact congr_fun ((forget _).congr_map (φ.naturality f)) x
+    exact CategoryTheory.congr_fun (φ.naturality f) x
 
 instance : Zero (M₁ ⟶ M₂) where
   zero := { app := fun _ ↦ 0 }

Mathlib/Algebra/Category/ModuleCat/Sheaf.lean

@@ -211,13 +211,13 @@ noncomputable def homEquivOfIsLocallyBijective : (M₂ ⟶ N) ≃ (M₁ ⟶ N) w
           ((PresheafOfModules.toPresheaf R).map ψ)
         simp only [← hφ, Equiv.symm_apply_apply]
         replace hφ : ∀ (Z : Cᵒᵖ) (x : M₁.obj Z), φ.app Z (f.app Z x) = ψ.app Z x :=
-          fun Z x ↦ congr_fun ((forget _).congr_map (congr_app hφ Z)) x
+          fun Z x ↦ CategoryTheory.congr_fun (congr_app hφ Z) x
         intro X r y
         apply hN.isSeparated _ _
           (Presheaf.imageSieve_mem J ((toPresheaf R).map f) y)
         rintro Y p ⟨x : M₁.obj _, hx : f.app _ x = M₂.map p.op y⟩
         have hφ' : ∀ (z : M₂.obj X), φ.app _ (M₂.map p.op z) =
-            N.map p.op (φ.app _ z) := congr_fun ((forget _).congr_map (φ.naturality p.op))
+            N.map p.op (φ.app _ z) := CategoryTheory.congr_fun (φ.naturality p.op)
         change N.map p.op (φ.app X (r • y)) = N.map p.op (r • φ.app X y)
         rw [← hφ', M₂.map_smul, ← hx, ← (f.app _).hom.map_smul, hφ, (ψ.app _).hom.map_smul,
           ← hφ, hx, N.map_smul, hφ'])

Mathlib/Algebra/Category/ModuleCat/Sheaf/ChangeOfRings.lean

@@ -55,7 +55,7 @@ noncomputable def restrictHomEquivOfIsLocallySurjective
     apply hM₂.isSeparated _ _ (Presheaf.imageSieve_mem J α r')
     rintro Y p ⟨r : R.obj _, hr⟩
     have hg : ∀ (z : M₁.obj X), g.app _ (M₁.map p.op z) = M₂.map p.op (g.app X z) :=
-      fun z ↦ congr_fun ((forget _).congr_map (g.naturality p.op)) z
+      fun z ↦ CategoryTheory.congr_fun (g.naturality p.op) z
     change M₂.map p.op (g.app X (r' • m)) = M₂.map p.op (r' • show M₂.obj X from g.app X m)
     dsimp at hg ⊢
     rw [← hg, M₂.map_smul, ← hg, ← hr]

Mathlib/Algebra/Category/ModuleCat/Tannaka.lean

@@ -35,8 +35,8 @@ def ringEquivEndForget₂ (R : Type u) [Ring R] :
     intro φ
     apply NatTrans.ext
     ext M (x : M)
-    have w := congr_fun ((forget _).congr_map
-      (φ.naturality (ModuleCat.ofHom (LinearMap.toSpanSingleton R M x)))) (1 : R)
+    have w := CategoryTheory.congr_fun
+      (φ.naturality (ModuleCat.ofHom (LinearMap.toSpanSingleton R M x))) (1 : R)
     exact w.symm.trans (congr_arg (φ.app M) (one_smul R x))
   map_add' := by
     intros

Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

@@ -294,7 +294,7 @@ def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) where
     (F ⋙ forget MonCat)).fac ((forget MonCat).mapCocone t) j) x
   uniq t m h := MonCat.ext fun y => congr_fun
       ((Types.TypeMax.colimitCoconeIsColimit (F ⋙ forget MonCat)).uniq ((forget MonCat).mapCocone t)
-        ((forget MonCat).map m)
+        ⇑(ConcreteCategory.hom m)
         fun j => funext fun x => ConcreteCategory.congr_hom (h j) x) y
 
 @[to_additive]
@@ -370,7 +370,7 @@ def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) where
     ConcreteCategory.coe_ext <|
       (Types.TypeMax.colimitCoconeIsColimit.{v, u} (F ⋙ forget CommMonCat.{max v u})).uniq
         ((forget CommMonCat.{max v u}).mapCocone t)
-        ((forget CommMonCat.{max v u}).map m) fun j => funext fun x =>
+        ⇑(ConcreteCategory.hom m) fun j => funext fun x =>
           CategoryTheory.congr_fun (h j) x
 
 @[to_additive forget₂AddMonPreservesFilteredColimits]

Mathlib/Algebra/Homology/ImageToKernel.lean

@@ -57,11 +57,12 @@ theorem imageToKernel_arrow (w : f ≫ g = 0) :
   simp [imageToKernel]
 
 @[simp]
-lemma imageToKernel_arrow_apply [HasForget V] (w : f ≫ g = 0)
-    (x : (forget V).obj (Subobject.underlying.obj (imageSubobject f))) :
+lemma imageToKernel_arrow_apply {FV : V → V → Type*} {CV : V → Type*}
+    [∀ X Y, FunLike (FV X Y) (CV X) (CV Y)] [ConcreteCategory V FV] (w : f ≫ g = 0)
+    (x : ToType (Subobject.underlying.obj (imageSubobject f))) :
     (kernelSubobject g).arrow (imageToKernel f g w x) =
       (imageSubobject f).arrow x := by
-  rw [← CategoryTheory.comp_apply, imageToKernel_arrow]
+  rw [← ConcreteCategory.comp_apply, imageToKernel_arrow]
 
 -- This is less useful as a `simp` lemma than it initially appears,
 -- as it "loses" the information the morphism factors through the image.

Mathlib/AlgebraicGeometry/Spec.lean

@@ -54,7 +54,7 @@ open Spec (structureSheaf)
 def Spec.topObj (R : CommRingCat.{u}) : TopCat :=
   TopCat.of (PrimeSpectrum R)
 
-@[simp] theorem Spec.topObj_forget {R} : (forget TopCat).obj (Spec.topObj R) = PrimeSpectrum R :=
+@[simp] theorem Spec.topObj_forget {R} : ToType (Spec.topObj R) = PrimeSpectrum R :=
   rfl
 
 /-- The induced map of a ring homomorphism on the ring spectra, as a morphism of topological spaces.
@@ -408,16 +408,11 @@ instance isLocalizedModule_toPushforwardStalkAlgHom :
     rw [toPushforwardStalkAlgHom_apply,
       ← (toPushforwardStalk (CommRingCat.ofHom (algebraMap ↑R ↑S)) p).hom.map_zero,
       toPushforwardStalk] at hx
-    -- Porting note: this `change` is manually rewriting `comp_apply`
-    change _ = (TopCat.Presheaf.germ (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)) _*
-      (structureSheaf ↑S).val) ⊤ p trivial (toOpen S ⊤ 0)) at hx
-    rw [map_zero] at hx
-    change (forget CommRingCat).map _ _ = (forget _).map _ _ at hx
-    obtain ⟨U, hpU, i₁, i₂, e⟩ := TopCat.Presheaf.germ_eq _ _ _ _ _ _ hx
+    rw [CommRingCat.comp_apply, map_zero] at hx
+    obtain ⟨U, hpU, i₁, i₂, e⟩ := TopCat.Presheaf.germ_eq (C := CommRingCat) _ _ _ _ _ _ hx
     obtain ⟨_, ⟨r, rfl⟩, hpr, hrU⟩ :=
       PrimeSpectrum.isTopologicalBasis_basic_opens.exists_subset_of_mem_open (show p ∈ U.1 from hpU)
         U.2
-    change PrimeSpectrum.basicOpen r ≤ U at hrU
     apply_fun (Spec.topMap (CommRingCat.ofHom (algebraMap R S)) _* (structureSheaf S).1).map
         (homOfLE hrU).op at e
     simp only [Functor.op_map, map_zero, ← CategoryTheory.comp_apply, toOpen_res] at e
@@ -429,10 +424,7 @@ instance isLocalizedModule_toPushforwardStalkAlgHom :
         this
     obtain ⟨⟨_, n, rfl⟩, e⟩ := (IsLocalization.mk'_eq_zero_iff _ _).mp this
     refine ⟨⟨r, hpr⟩ ^ n, ?_⟩
-    rw [Submonoid.smul_def, Algebra.smul_def]
-    -- Porting note: manually rewrite `Submonoid.coe_pow`
-    change (algebraMap R S) (r ^ n) * x = 0
-    rw [map_pow]
+    rw [Submonoid.smul_def, Algebra.smul_def, SubmonoidClass.coe_pow, map_pow]
     exact e
 
 end StructureSheaf

Mathlib/CategoryTheory/Action/Concrete.lean

@@ -168,17 +168,18 @@ end FintypeCat
 
 section ToMulAction
 
-variable {V : Type (u + 1)} [LargeCategory V] [HasForget V]
+variable {V : Type (u + 1)} [LargeCategory V] {FV : V → V → Type*} {CV : V → Type*}
+variable [∀ X Y, FunLike (FV X Y) (CV X) (CV Y)] [ConcreteCategory V FV]
 
 instance instMulAction {G : MonCat.{u}} (X : Action V G) :
-    MulAction G ((CategoryTheory.forget _).obj X) where
-  smul g x := ((CategoryTheory.forget _).map (X.ρ g)) x
+    MulAction G (ToType X) where
+  smul g x := ConcreteCategory.hom (X.ρ g) x
   one_smul x := by
-    show ((CategoryTheory.forget _).map (X.ρ 1)) x = x
+    show ConcreteCategory.hom (X.ρ 1) x = x
     simp
   mul_smul g h x := by
-    show (CategoryTheory.forget V).map (X.ρ (g * h)) x =
-      ((CategoryTheory.forget V).map (X.ρ h) ≫ (CategoryTheory.forget V).map (X.ρ g)) x
+    show ConcreteCategory.hom (X.ρ (g * h)) x =
+      ConcreteCategory.hom (X.ρ g) ((ConcreteCategory.hom (X.ρ h)) x)
     simp
 
 /- Specialize `instMulAction` to assist typeclass inference. -/