refactor(Topology/Sheaves): harmonize names (#36074)

Make the name of the pullback/pushforward adjunction for presheaves `Presheaf.pullbackPushforwardAdjunction`, so it follows the same convention as the name of the similar adjunction for sheaves.

Co-authored-by: morel <smorel@math.princeton.edu>

Author: smorel394

Mathlib/Topology/Sheaves/Presheaf.lean

@@ -27,7 +27,7 @@ and for `ℱ : X.Presheaf C` provide the natural isomorphisms
 
 We also define the functors `pullback C f : Y.Presheaf C ⥤ X.Presheaf c`,
 and provide their adjunction at
-`TopCat.Presheaf.pushforwardPullbackAdjunction`.
+`TopCat.Presheaf.pullbackPushforwardAdjunction`.
 -/
 
 @[expose] public section
@@ -269,20 +269,23 @@ def pullback {X Y : TopCat.{v}} (f : X ⟶ Y) : Y.Presheaf C ⥤ X.Presheaf C :=
   (Opens.map f).op.lan
 
 /-- The pullback and pushforward along a continuous map are adjoint to each other. -/
-def pushforwardPullbackAdjunction {X Y : TopCat.{v}} (f : X ⟶ Y) :
+def pullbackPushforwardAdjunction {X Y : TopCat.{v}} (f : X ⟶ Y) :
     pullback C f ⊣ pushforward C f :=
   Functor.lanAdjunction _ _
 
+@[deprecated (since := "2026-03-03")]
+alias pushforwardPullbackAdjunction := pullbackPushforwardAdjunction
+
 /-- Pulling back along a homeomorphism is the same as pushing forward along its inverse. -/
 def pullbackHomIsoPushforwardInv {X Y : TopCat.{v}} (H : X ≅ Y) :
     pullback C H.hom ≅ pushforward C H.inv :=
-  Adjunction.leftAdjointUniq (pushforwardPullbackAdjunction C H.hom)
+  Adjunction.leftAdjointUniq (pullbackPushforwardAdjunction C H.hom)
     (presheafEquivOfIso C H.symm).toAdjunction
 
 /-- Pulling back along the inverse of a homeomorphism is the same as pushing forward along it. -/
 def pullbackInvIsoPushforwardHom {X Y : TopCat.{v}} (H : X ≅ Y) :
     pullback C H.inv ≅ pushforward C H.hom :=
-  Adjunction.leftAdjointUniq (pushforwardPullbackAdjunction C H.inv)
+  Adjunction.leftAdjointUniq (pullbackPushforwardAdjunction C H.inv)
     (presheafEquivOfIso C H).toAdjunction
 
 variable {C}

Mathlib/Topology/Sheaves/Stalks.lean

@@ -227,15 +227,15 @@ section stalkPullback
 /-- The morphism `ℱ_{f x} ⟶ (f⁻¹ℱ)ₓ` that factors through `(f_*f⁻¹ℱ)_{f x}`. -/
 def stalkPullbackHom (f : X ⟶ Y) (F : Y.Presheaf C) (x : X) :
     F.stalk (f x) ⟶ ((pullback C f).obj F).stalk x :=
-  (stalkFunctor _ (f x)).map ((pushforwardPullbackAdjunction C f).unit.app F) ≫
+  (stalkFunctor _ (f x)).map ((pullbackPushforwardAdjunction C f).unit.app F) ≫
     stalkPushforward _ _ _ x
 
 set_option backward.isDefEq.respectTransparency false in
 @[reassoc (attr := simp)]
 lemma germ_stalkPullbackHom
     (f : X ⟶ Y) (F : Y.Presheaf C) (x : X) (U : Opens Y) (hU : f x ∈ U) :
     F.germ U (f x) hU ≫ stalkPullbackHom C f F x =
-      ((pushforwardPullbackAdjunction C f).unit.app F).app _ ≫
+      ((pullbackPushforwardAdjunction C f).unit.app F).app _ ≫
         ((pullback C f).obj F).germ ((Opens.map f).obj U) x hU := by
   simp [stalkPullbackHom, germ, stalkFunctor, stalkPushforward]
 
@@ -253,23 +253,23 @@ variable {C} in
 lemma pullback_obj_obj_ext {Z : C} {f : X ⟶ Y} {F : Y.Presheaf C} (U : (Opens X)ᵒᵖ)
     {φ ψ : ((pullback C f).obj F).obj U ⟶ Z}
     (h : ∀ (V : Opens Y) (hV : U.unop ≤ (Opens.map f).obj V),
-      ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫
+      ((pullbackPushforwardAdjunction C f).unit.app F).app (op V) ≫
         ((pullback C f).obj F).map (homOfLE hV).op ≫ φ =
-      ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫
+      ((pullbackPushforwardAdjunction C f).unit.app F).app (op V) ≫
         ((pullback C f).obj F).map (homOfLE hV).op ≫ ψ) : φ = ψ := by
   apply ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit F _).hom_ext
   rintro ⟨⟨V⟩, ⟨⟩, ⟨b⟩⟩
-  simpa [pushforwardPullbackAdjunction, Functor.lanAdjunction_unit]
+  simpa [pullbackPushforwardAdjunction, Functor.lanAdjunction_unit]
     using h V (leOfHom b)
 
 @[reassoc (attr := simp)]
-lemma pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk
+lemma pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk
     (f : X ⟶ Y) (F : Y.Presheaf C) (U : Opens X) (x : X) (hx : x ∈ U) (V : Opens Y)
     (hV : U ≤ (Opens.map f).obj V) :
-    ((pushforwardPullbackAdjunction C f).unit.app F).app (op V) ≫
+    ((pullbackPushforwardAdjunction C f).unit.app F).app (op V) ≫
       ((pullback C f).obj F).map (homOfLE hV).op ≫ germToPullbackStalk C f F U x hx =
         F.germ _ (f x) (hV hx) := by
-  simpa [pushforwardPullbackAdjunction] using
+  simpa [pullbackPushforwardAdjunction] using
     ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit F (op U)).fac _
       (CostructuredArrow.mk (homOfLE hV).op)
 
@@ -281,15 +281,15 @@ lemma germToPullbackStalk_stalkPullbackHom
       ((pullback C f).obj F).germ _ x hx := by
   ext V hV
   dsimp
-  simp only [pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk_assoc,
+  simp only [pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk_assoc,
     germ_stalkPullbackHom, germ_res]
 
 @[reassoc (attr := simp)]
-lemma pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk
+lemma pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk
     (f : X ⟶ Y) (F : Y.Presheaf C) (V : (Opens Y)ᵒᵖ) (x : X) (hx : f x ∈ V.unop) :
-    ((pushforwardPullbackAdjunction C f).unit.app F).app V ≫ germToPullbackStalk C f F _ x hx =
+    ((pullbackPushforwardAdjunction C f).unit.app F).app V ≫ germToPullbackStalk C f F _ x hx =
       F.germ _ (f x) hx := by
-  simpa using pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk
+  simpa using pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk
     C f F ((Opens.map f).obj V.unop) x hx V.unop (by rfl)
 
 set_option backward.isDefEq.respectTransparency false in
@@ -305,8 +305,8 @@ def stalkPullbackInv (f : X ⟶ Y) (F : Y.Presheaf C) (x : X) :
             ext W hW
             dsimp [OpenNhds.inclusion]
             rw [Category.comp_id, ← Functor.map_comp_assoc,
-              pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk]
-            erw [pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk] } }
+              pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk]
+            erw [pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk] } }
 
 @[reassoc (attr := simp)]
 lemma germ_stalkPullbackInv (f : X ⟶ Y) (F : Y.Presheaf C) (x : X) (V : Opens X) (hV : x ∈ V) :
@@ -324,7 +324,7 @@ def stalkPullbackIso (f : X ⟶ Y) (F : Y.Presheaf C) (x : X) :
     ext U hU
     dsimp
     rw [germ_stalkPullbackHom_assoc, germ_stalkPullbackInv, Category.comp_id,
-      pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk]
+      pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk]
   inv_hom_id := by
     ext V hV
     dsimp