chore(category_theory/*): make all forgetful functors use explicit arguments (#4139)

As suggested as #4131 (comment), for the sake of more uniform API.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/algebra/homology/chain_complex.lean

@@ -19,8 +19,6 @@ and it seems we can use it straightforwardly:
 example (C : chain_complex V) : C.X 5 ⟶ C.X 6 := C.d 5
 ```
 
-We define the forgetful functor to `ℤ`-graded objects, and show that
-`chain_complex V` is concrete when `V` is, and `V` has coproducts.
 -/
 
 universes v u

src/algebraic_geometry/presheafed_space.lean

@@ -152,11 +152,16 @@ by { op_induction U, cases U, simp only [id_c], dsimp, simp, }
   (α ≫ β).c.app U = (β.c).app U ≫ (α.c).app (op ((opens.map (β.base)).obj (unop U))) ≫
     (Top.presheaf.pushforward.comp _ _ _).inv.app U := rfl
 
+section
+variables (C)
+
 /-- The forgetful functor from `PresheafedSpace` to `Top`. -/
 def forget : PresheafedSpace C ⥤ Top :=
 { obj := λ X, (X : Top.{v}),
   map := λ X Y f, f.base }
 
+end
+
 /--
 The restriction of a presheafed space along an open embedding into the space.
 -/

src/algebraic_geometry/sheafed_space.lean

@@ -92,6 +92,8 @@ by { op_induction U, cases U, simp only [id_c], dsimp, simp, }
   (α ≫ β).c.app U = (β.c).app U ≫ (α.c).app (op ((opens.map (β.base)).obj (unop U))) ≫
     (Top.presheaf.pushforward.comp _ _ _).inv.app U := rfl
 
+variables (C)
+
 /-- The forgetful functor from `SheafedSpace` to `Top`. -/
 def forget : SheafedSpace C ⥤ Top :=
 { obj := λ X, (X : Top.{v}),

src/category_theory/grothendieck.lean

@@ -124,12 +124,17 @@ instance : category (grothendieck F) :=
       refl, },
   end, }
 
+section
+variables (F)
+
 /-- The forgetful functor from `grothendieck F` to the source category. -/
 @[simps]
 def forget : grothendieck F ⥤ C :=
 { obj := λ X, X.1,
   map := λ X Y f, f.1, }
 
+end
+
 universe w
 variables (G : C ⥤ Type w)
 

src/category_theory/limits/over.lean

@@ -18,38 +18,38 @@ variable {X : C}
 
 namespace category_theory.functor
 
-@[simps] def to_cocone (F : J ⥤ over X) : cocone (F ⋙ over.forget) :=
+@[simps] def to_cocone (F : J ⥤ over X) : cocone (F ⋙ over.forget X) :=
 { X := X,
   ι := { app := λ j, (F.obj j).hom } }
 
-@[simps] def to_cone (F : J ⥤ under X) : cone (F ⋙ under.forget) :=
+@[simps] def to_cone (F : J ⥤ under X) : cone (F ⋙ under.forget X) :=
 { X := X,
   π := { app := λ j, (F.obj j).hom } }
 
 end category_theory.functor
 
 namespace category_theory.over
 
-@[simps] def colimit (F : J ⥤ over X) [has_colimit (F ⋙ forget)] : cocone F :=
-{ X := mk $ colimit.desc (F ⋙ forget) F.to_cocone,
+@[simps] def colimit (F : J ⥤ over X) [has_colimit (F ⋙ forget X)] : cocone F :=
+{ X := mk $ colimit.desc (F ⋙ forget X) F.to_cocone,
   ι :=
-  { app := λ j, hom_mk $ colimit.ι (F ⋙ forget) j,
+  { app := λ j, hom_mk $ colimit.ι (F ⋙ forget X) j,
     naturality' :=
     begin
       intros j j' f,
-      have := colimit.w (F ⋙ forget) f,
+      have := colimit.w (F ⋙ forget X) f,
       tidy
     end } }
 
-def forget_colimit_is_colimit (F : J ⥤ over X) [has_colimit (F ⋙ forget)] :
-  is_colimit (forget.map_cocone (colimit F)) :=
-is_colimit.of_iso_colimit (colimit.is_colimit (F ⋙ forget)) (cocones.ext (iso.refl _) (by tidy))
+def forget_colimit_is_colimit (F : J ⥤ over X) [has_colimit (F ⋙ forget X)] :
+  is_colimit ((forget X).map_cocone (colimit F)) :=
+is_colimit.of_iso_colimit (colimit.is_colimit (F ⋙ forget X)) (cocones.ext (iso.refl _) (by tidy))
 
-instance : reflects_colimits (forget : over X ⥤ C) :=
+instance : reflects_colimits (forget X) :=
 { reflects_colimits_of_shape := λ J 𝒥,
   { reflects_colimit := λ F,
     by constructor; exactI λ t ht,
-    { desc := λ s, hom_mk (ht.desc (forget.map_cocone s))
+    { desc := λ s, hom_mk (ht.desc ((forget X).map_cocone s))
         begin
           apply ht.hom_ext, intro j,
           rw [←category.assoc, ht.fac],
@@ -58,17 +58,17 @@ instance : reflects_colimits (forget : over X ⥤ C) :=
           exact (w (t.ι.app j)).symm,
         end,
       fac' := begin
-        intros s j, ext, exact ht.fac (forget.map_cocone s) j
+        intros s j, ext, exact ht.fac ((forget X).map_cocone s) j
         -- TODO: Ask Simon about multiple ext lemmas for defeq types (comma_morphism & over.category.hom)
       end,
       uniq' :=
       begin
         intros s m w,
         ext1 j,
-        exact ht.uniq (forget.map_cocone s) m.left (λ j, congr_arg comma_morphism.left (w j))
+        exact ht.uniq ((forget X).map_cocone s) m.left (λ j, congr_arg comma_morphism.left (w j))
       end } } }
 
-instance has_colimit {F : J ⥤ over X} [has_colimit (F ⋙ forget)] : has_colimit F :=
+instance has_colimit {F : J ⥤ over X} [has_colimit (F ⋙ forget X)] : has_colimit F :=
 has_colimit.mk { cocone := colimit F,
   is_colimit := reflects_colimit.reflects (forget_colimit_is_colimit F) }
 
@@ -79,43 +79,43 @@ instance has_colimits_of_shape [has_colimits_of_shape J C] :
 instance has_colimits [has_colimits C] : has_colimits (over X) :=
 { has_colimits_of_shape := λ J 𝒥, by resetI; apply_instance }
 
-instance forget_preserves_colimit {X : C} {F : J ⥤ over X} [has_colimit (F ⋙ forget)] :
-  preserves_colimit F (forget : over X ⥤ C) :=
+instance forget_preserves_colimit {X : C} {F : J ⥤ over X} [has_colimit (F ⋙ forget X)] :
+  preserves_colimit F (forget X) :=
 preserves_colimit_of_preserves_colimit_cocone
   (reflects_colimit.reflects (forget_colimit_is_colimit F)) (forget_colimit_is_colimit F)
 
 instance forget_preserves_colimits_of_shape [has_colimits_of_shape J C] {X : C} :
-  preserves_colimits_of_shape J (forget : over X ⥤ C) :=
+  preserves_colimits_of_shape J (forget X) :=
 { preserves_colimit := λ F, by apply_instance }
 
 instance forget_preserves_colimits [has_colimits C] {X : C} :
-  preserves_colimits (forget : over X ⥤ C) :=
+  preserves_colimits (forget X) :=
 { preserves_colimits_of_shape := λ J 𝒥, by apply_instance }
 
 end category_theory.over
 
 namespace category_theory.under
 
-@[simps] def limit (F : J ⥤ under X) [has_limit (F ⋙ forget)] : cone F :=
-{ X := mk $ limit.lift (F ⋙ forget) F.to_cone,
+@[simps] def limit (F : J ⥤ under X) [has_limit (F ⋙ forget X)] : cone F :=
+{ X := mk $ limit.lift (F ⋙ forget X) F.to_cone,
   π :=
-  { app := λ j, hom_mk $ limit.π (F ⋙ forget) j,
+  { app := λ j, hom_mk $ limit.π (F ⋙ forget X) j,
     naturality' :=
     begin
       intros j j' f,
-      have := (limit.w (F ⋙ forget) f).symm,
+      have := (limit.w (F ⋙ forget X) f).symm,
       tidy
     end } }
 
-def forget_limit_is_limit (F : J ⥤ under X) [has_limit (F ⋙ forget)] :
-  is_limit (forget.map_cone (limit F)) :=
-is_limit.of_iso_limit (limit.is_limit (F ⋙ forget)) (cones.ext (iso.refl _) (by tidy))
+def forget_limit_is_limit (F : J ⥤ under X) [has_limit (F ⋙ forget X)] :
+  is_limit ((forget X).map_cone (limit F)) :=
+is_limit.of_iso_limit (limit.is_limit (F ⋙ forget X)) (cones.ext (iso.refl _) (by tidy))
 
-instance : reflects_limits (forget : under X ⥤ C) :=
+instance : reflects_limits (forget X) :=
 { reflects_limits_of_shape := λ J 𝒥,
   { reflects_limit := λ F,
     by constructor; exactI λ t ht,
-    { lift := λ s, hom_mk (ht.lift (forget.map_cone s))
+    { lift := λ s, hom_mk (ht.lift ((forget X).map_cone s))
         begin
           apply ht.hom_ext, intro j,
           rw [category.assoc, ht.fac],
@@ -124,16 +124,16 @@ instance : reflects_limits (forget : under X ⥤ C) :=
           exact (w (t.π.app j)).symm,
         end,
       fac' := begin
-        intros s j, ext, exact ht.fac (forget.map_cone s) j
+        intros s j, ext, exact ht.fac ((forget X).map_cone s) j
       end,
       uniq' :=
       begin
         intros s m w,
         ext1 j,
-        exact ht.uniq (forget.map_cone s) m.right (λ j, congr_arg comma_morphism.right (w j))
+        exact ht.uniq ((forget X).map_cone s) m.right (λ j, congr_arg comma_morphism.right (w j))
       end } } }
 
-instance has_limit {F : J ⥤ under X} [has_limit (F ⋙ forget)] : has_limit F :=
+instance has_limit {F : J ⥤ under X} [has_limit (F ⋙ forget X)] : has_limit F :=
 has_limit.mk { cone := limit F,
   is_limit := reflects_limit.reflects (forget_limit_is_limit F) }
 
@@ -145,7 +145,7 @@ instance has_limits [has_limits C] : has_limits (under X) :=
 { has_limits_of_shape := λ J 𝒥, by resetI; apply_instance }
 
 instance forget_preserves_limits [has_limits C] {X : C} :
-  preserves_limits (forget : under X ⥤ C) :=
+  preserves_limits (forget X) :=
 { preserves_limits_of_shape := λ J 𝒥,
   { preserves_limit := λ F, by exactI
     preserves_limit_of_preserves_limit_cone

src/category_theory/limits/shapes/constructions/over/connected.lean

@@ -29,7 +29,7 @@ namespace creates_connected
 diagram legs to the specific object.
 -/
 def nat_trans_in_over {B : C} (F : J ⥤ over B) :
-  F ⋙ forget ⟶ (category_theory.functor.const J).obj B :=
+  F ⋙ forget B ⟶ (category_theory.functor.const J).obj B :=
 { app := λ j, (F.obj j).hom }
 
 local attribute [tidy] tactic.case_bash
@@ -39,27 +39,27 @@ local attribute [tidy] tactic.case_bash
 where the connected assumption is used.
 -/
 @[simps]
-def raise_cone [connected J] {B : C} {F : J ⥤ over B} (c : cone (F ⋙ forget)) :
+def raise_cone [connected J] {B : C} {F : J ⥤ over B} (c : cone (F ⋙ forget B)) :
   cone F :=
 { X := over.mk (c.π.app (default J) ≫ (F.obj (default J)).hom),
   π :=
   { app := λ j, over.hom_mk (c.π.app j) (nat_trans_from_connected (c.π ≫ nat_trans_in_over F) j) } }
 
 lemma raised_cone_lowers_to_original [connected J] {B : C} {F : J ⥤ over B}
-  (c : cone (F ⋙ forget)) (t : is_limit c) :
-  forget.map_cone (raise_cone c) = c :=
+  (c : cone (F ⋙ forget B)) (t : is_limit c) :
+  (forget B).map_cone (raise_cone c) = c :=
 by tidy
 
 /-- (Impl) Show that the raised cone is a limit. -/
-def raised_cone_is_limit [connected J] {B : C} {F : J ⥤ over B} {c : cone (F ⋙ forget)} (t : is_limit c) :
+def raised_cone_is_limit [connected J] {B : C} {F : J ⥤ over B} {c : cone (F ⋙ forget B)} (t : is_limit c) :
   is_limit (raise_cone c) :=
-{ lift := λ s, over.hom_mk (t.lift (forget.map_cone s)) (by { dsimp, simp }),
+{ lift := λ s, over.hom_mk (t.lift ((forget B).map_cone s)) (by { dsimp, simp }),
   uniq' := λ s m K, by { ext1, apply t.hom_ext, intro j, simp [← K j] } }
 
 end creates_connected
 
 /-- The forgetful functor from the over category creates any connected limit. -/
-instance forget_creates_connected_limits [connected J] {B : C} : creates_limits_of_shape J (forget : over B ⥤ C) :=
+instance forget_creates_connected_limits [connected J] {B : C} : creates_limits_of_shape J (forget B) :=
 { creates_limit := λ K,
     creates_limit_of_reflects_iso (λ c t,
       { lifted_cone := creates_connected.raise_cone c,
@@ -68,6 +68,6 @@ instance forget_creates_connected_limits [connected J] {B : C} : creates_limits_
 
 /-- The over category has any connected limit which the original category has. -/
 instance has_connected_limits {B : C} [connected J] [has_limits_of_shape J C] : has_limits_of_shape J (over B) :=
-{ has_limit := λ F, has_limit_of_created F (forget : over B ⥤ C) }
+{ has_limit := λ F, has_limit_of_created F (forget B) }
 
 end category_theory.over

src/category_theory/monad/bundled.lean

@@ -57,11 +57,16 @@ instance : category (Monad C) :=
   id := λ _, monad_hom.id _,
   comp := λ _ _ _, monad_hom.comp }
 
+section
+variables (C)
+
 /-- The forgetful functor from `Monad C` to `C ⥤ C`. -/
 def forget : Monad C ⥤ (C ⥤ C) :=
 { obj := func,
   map := λ _ _ f, f.to_nat_trans }
 
+end
+
 @[simp]
 lemma comp_to_nat_trans {M N L : Monad C} (f : M ⟶ N) (g : N ⟶ L) :
   (f ≫ g).to_nat_trans = nat_trans.vcomp f.to_nat_trans g.to_nat_trans := rfl
@@ -95,11 +100,16 @@ instance : category (Comonad C) :=
   id := λ _, comonad_hom.id _,
   comp := λ _ _ _, comonad_hom.comp }
 
+section
+variables (C)
+
 /-- The forgetful functor from `CoMonad C` to `C ⥤ C`. -/
 def forget : Comonad C ⥤ (C ⥤ C) :=
 { obj := func,
   map := λ _ _ f, f.to_nat_trans }
 
+end
+
 @[simp]
 lemma comp_to_nat_trans {M N L : Comonad C} (f : M ⟶ N) (g : N ⟶ L) :
   (f ≫ g).to_nat_trans = nat_trans.vcomp f.to_nat_trans g.to_nat_trans := rfl

src/category_theory/monoidal/internal.lean

@@ -99,13 +99,16 @@ instance : category (Mon_ C) :=
 @[simp] lemma comp_hom' {M N K : Mon_ C} (f : M ⟶ N) (g : N ⟶ K) :
   (f ≫ g : hom M K).hom = f.hom ≫ g.hom := rfl
 
+section
 variables (C)
 
 /-- The forgetful functor from monoid objects to the ambient category. -/
 def forget : Mon_ C ⥤ C :=
 { obj := λ A, A.X,
   map := λ A B f, f.hom, }
 
+end
+
 instance {A B : Mon_ C} (f : A ⟶ B) [e : is_iso ((forget C).map f)] : is_iso f.hom := e
 
 /-- The forgetful functor from monoid objects to the ambient category reflects isomorphisms. -/
@@ -258,6 +261,11 @@ def regular : Mod A :=
 
 instance : inhabited (Mod A) := ⟨regular A⟩
 
+/-- The forgetful functor from module objects to the ambient category. -/
+def forget : Mod A ⥤ C :=
+{ obj := λ A, A.X,
+  map := λ A B f, f.hom, }
+
 open category_theory.monoidal_category
 
 /--

src/category_theory/over.lean

@@ -89,15 +89,19 @@ direction gives a commutative triangle.
 def iso_mk {f g : over X} (hl : f.left ≅ g.left) (hw : hl.hom ≫ g.hom = f.hom . obviously) : f ≅ g :=
 comma.iso_mk hl (eq_to_iso (subsingleton.elim _ _)) (by simp [hw])
 
+section
+variable (X)
 /--
 The forgetful functor mapping an arrow to its domain.
 
 See https://stacks.math.columbia.edu/tag/001G.
 -/
 def forget : over X ⥤ T := comma.fst _ _
 
-@[simp] lemma forget_obj {U : over X} : forget.obj U = U.left := rfl
-@[simp] lemma forget_map {U V : over X} {f : U ⟶ V} : forget.map f = f.left := rfl
+end
+
+@[simp] lemma forget_obj {U : over X} : (forget X).obj U = U.left := rfl
+@[simp] lemma forget_map {U V : over X} {f : U ⟶ V} : (forget X).map f = f.left := rfl
 
 /--
 A morphism `f : X ⟶ Y` induces a functor `over X ⥤ over Y` in the obvious way.
@@ -122,9 +126,9 @@ nat_iso.of_components (λ X, iso_mk (iso.refl _) (by tidy)) (by tidy)
 
 end
 
-instance forget_reflects_iso : reflects_isomorphisms (forget : over X ⥤ T) :=
-{ reflects := λ X Y f t, by exactI
-  { inv := over.hom_mk t.inv ((as_iso (forget.map f)).inv_comp_eq.2 (over.w f).symm) } }
+instance forget_reflects_iso : reflects_isomorphisms (forget X) :=
+{ reflects := λ Y Z f t, by exactI
+  { inv := over.hom_mk t.inv ((as_iso ((forget X).map f)).inv_comp_eq.2 (over.w f).symm) } }
 
 section iterated_slice
 variables (f : over X)
@@ -156,11 +160,11 @@ def iterated_slice_equiv : over f ≌ over f.left :=
     (λ X Y g, by { ext, dsimp, simp }) }
 
 lemma iterated_slice_forward_forget :
-  iterated_slice_forward f ⋙ forget = forget ⋙ forget :=
+  iterated_slice_forward f ⋙ forget f.left = forget f ⋙ forget X :=
 rfl
 
 lemma iterated_slice_backward_forget_forget :
-  iterated_slice_backward f ⋙ forget ⋙ forget = forget :=
+  iterated_slice_backward f ⋙ forget f ⋙ forget X = forget f.left :=
 rfl
 
 end iterated_slice
@@ -235,11 +239,15 @@ lemma iso_mk_hom_right {f g : under X} (hr : f.right ≅ g.right) (hw : f.hom 
 lemma iso_mk_inv_right {f g : under X} (hr : f.right ≅ g.right) (hw : f.hom ≫ hr.hom = g.hom) :
   (iso_mk hr hw).inv.right = hr.inv := rfl
 
+section
+variables (X)
 /-- The forgetful functor mapping an arrow to its domain. -/
 def forget : under X ⥤ T := comma.snd _ _
 
-@[simp] lemma forget_obj {U : under X} : forget.obj U = U.right := rfl
-@[simp] lemma forget_map {U V : under X} {f : U ⟶ V} : forget.map f = f.right := rfl
+end
+
+@[simp] lemma forget_obj {U : under X} : (forget X).obj U = U.right := rfl
+@[simp] lemma forget_map {U V : under X} {f : U ⟶ V} : (forget X).map f = f.right := rfl
 
 /-- A morphism `X ⟶ Y` induces a functor `under Y ⥤ under X` in the obvious way. -/
 def map {Y : T} (f : X ⟶ Y) : under Y ⥤ under X := comma.map_left _ $ discrete.nat_trans (λ _, f)