feat(AlgebraicGeometry): the pseudofunctor which sends a scheme to its category of sheaves of modules

Mathlib.lean

@@ -2190,6 +2190,7 @@ public import Mathlib.CategoryTheory.Adjunction.Whiskering
 public import Mathlib.CategoryTheory.Balanced
 public import Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
 public import Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
+public import Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
 public import Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
 public import Mathlib.CategoryTheory.Bicategory.Basic
 public import Mathlib.CategoryTheory.Bicategory.CatEnriched

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

@@ -37,7 +37,7 @@ namespace SheafOfModules
 variable (R : Sheaf J RingCat.{u}) [HasSheafify J AddCommGrpCat.{v}]
   [J.WEqualsLocallyBijective AddCommGrpCat.{v}]
 
-noncomputable instance : Abelian (SheafOfModules.{v} R) := by
+instance : Abelian (SheafOfModules.{v} R) := by
   let adj := PresheafOfModules.sheafificationAdjunction (𝟙 R.val)
   exact abelianOfAdjunction _ _ (asIso (adj.counit)) adj
 

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

@@ -137,6 +137,13 @@ category of sheaves of modules. -/
 noncomputable def pullbackId : pullback.{v} (F := 𝟭 C) (𝟙 S) ≅ 𝟭 _ :=
   ((pullbackPushforwardAdjunction.{v} (F := 𝟭 C) (𝟙 S))).leftAdjointIdIso (pushforwardId S)
 
+variable (S) in
+@[simp]
+lemma conjugateEquiv_pullbackId_hom :
+    conjugateEquiv .id (pullbackPushforwardAdjunction.{v} _) (pullbackId S).hom =
+      (pushforwardId S).inv :=
+  Adjunction.conjugateEquiv_leftAdjointIdIso_hom _ _
+
 variable [(pushforward.{v} φ).IsRightAdjoint]
 
 section
@@ -164,6 +171,14 @@ noncomputable def pullbackComp :
       (φ ≫ (F.sheafPushforwardContinuous RingCat.{u} J K).map ψ))
     (pushforwardComp φ ψ)
 
+@[simp]
+lemma conjugateEquiv_pullbackComp_inv :
+    conjugateEquiv ((pullbackPushforwardAdjunction.{v} φ).comp
+      (pullbackPushforwardAdjunction.{v} ψ))
+    (pullbackPushforwardAdjunction.{v} _) (pullbackComp.{v} φ ψ).inv =
+    (pushforwardComp.{v} φ ψ).hom :=
+  Adjunction.conjugateEquiv_leftAdjointCompIso_inv _ _ _ _
+
 variable {G' : D' ⥤ D''} {R'' : Sheaf K'' RingCat.{u}}
   [Functor.IsContinuous.{u} G' K' K''] [Functor.IsContinuous.{v} G' K' K'']
   [Functor.IsContinuous.{u} (G ⋙ G') K K'']

Mathlib/AlgebraicGeometry/Modules/Sheaf.lean

@@ -1,39 +1,180 @@
 /-
 Copyright (c) 2024 Joël Riou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joël Riou
+Authors: Joël Riou, Andrew Yang
 -/
 module
 
 public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian
+public import Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
 public import Mathlib.AlgebraicGeometry.Modules.Presheaf
+public import Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
+public import Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
+public import Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
 
 /-!
 # The category of sheaves of modules over a scheme
 
 In this file, we define the abelian category of sheaves of modules
-`X.Modules` over a scheme `X`.
+`X.Modules` over a scheme `X`, and study its basic functoriality.
 
 -/
 
 @[expose] public section
 
-universe u
+universe t u
 
-open CategoryTheory
+open CategoryTheory Bicategory
 
 namespace AlgebraicGeometry.Scheme
 
-variable (X : Scheme.{u})
+variable {X Y Z T : Scheme.{u}}
 
+/-- The morphism of sheaves of rings corresponding to a morphism of schemes. -/
+def Hom.toRingCatSheafHom (f : X ⟶ Y) :
+    Y.ringCatSheaf ⟶ ((TopologicalSpace.Opens.map f.base).sheafPushforwardContinuous
+      _ _ _).obj X.ringCatSheaf where
+  val := Functor.whiskerRight f.c _
+
+variable (X) in
 /-- The category of sheaves of modules over a scheme. -/
-abbrev Modules := SheafOfModules.{u} X.ringCatSheaf
+def Modules := SheafOfModules.{u} X.ringCatSheaf
+
+namespace Modules
+
+/-- Morphisms between `𝒪ₓ`-modules. -/
+def Hom (M N : X.Modules) : Type u := SheafOfModules.Hom M N
+
+instance : Category X.Modules where
+  Hom := Modules.Hom
+  __ := inferInstanceAs (Category (SheafOfModules.{u} X.ringCatSheaf))
+
+instance : Preadditive X.Modules :=
+  inferInstanceAs (Preadditive (SheafOfModules.{u} X.ringCatSheaf))
+
+instance : Abelian X.Modules :=
+  inferInstanceAs (Abelian (SheafOfModules.{u} X.ringCatSheaf))
+
+variable (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ T)
+
+/-- The pushforward functor for categories of sheaves of modules over schemes. -/
+noncomputable def pushforward : X.Modules ⥤ Y.Modules :=
+  SheafOfModules.pushforward f.toRingCatSheafHom
+
+/-- The pullback functor for categories of sheaves of modules over schemes. -/
+noncomputable def pullback : Y.Modules ⥤ X.Modules :=
+  SheafOfModules.pullback f.toRingCatSheafHom
+
+/-- The pullback functor for categories of sheaves of modules over schemes
+is left adjoint to the pushforward functor. -/
+noncomputable def pullbackPushforwardAdjunction : pullback f ⊣ pushforward f :=
+  SheafOfModules.pullbackPushforwardAdjunction _
+
+variable (X) in
+/-- The pushforward of sheaves of modules by the identity morphism identifies
+to the identity functor. -/
+noncomputable def pushforwardId : pushforward (𝟙 X) ≅ 𝟭 _ :=
+  SheafOfModules.pushforwardId _
+
+variable (X) in
+/-- The pullback of sheaves of modules by the identity morphism identifies
+to the identity functor. -/
+noncomputable def pullbackId : pullback (𝟙 X) ≅ 𝟭 _ :=
+  SheafOfModules.pullbackId _
+
+variable (X) in
+lemma conjugateEquiv_pullbackId_hom :
+    conjugateEquiv .id (pullbackPushforwardAdjunction (𝟙 X)) (pullbackId X).hom =
+      (pushforwardId X).inv :=
+  SheafOfModules.conjugateEquiv_pullbackId_hom _
+
+/-- The composition of two pushforward functors for sheaves of modules on schemes
+identify to the pushforward for the composition. -/
+noncomputable def pushforwardComp :
+    pushforward f ⋙ pushforward g ≅ pushforward (f ≫ g) :=
+  SheafOfModules.pushforwardComp _ _
+
+/-- The composition of two pullback functors for sheaves of modules on schemes
+identify to the pullback for the composition. -/
+noncomputable def pullbackComp :
+    pullback g ⋙ pullback f ≅ pullback (f ≫ g) :=
+  SheafOfModules.pullbackComp _ _
+
+lemma conjugateEquiv_pullbackComp_inv :
+    conjugateEquiv ((pullbackPushforwardAdjunction g).comp (pullbackPushforwardAdjunction f))
+      (pullbackPushforwardAdjunction (f ≫ g)) (pullbackComp f g).inv =
+    (pushforwardComp f g).hom :=
+  SheafOfModules.conjugateEquiv_pullbackComp_inv _ _
+
+@[reassoc]
+lemma pseudofunctor_associativity :
+    (pullbackComp f (g ≫ h)).inv ≫
+      Functor.whiskerRight (pullbackComp g h).inv _ ≫ (Functor.associator _ _ _).hom ≫
+        Functor.whiskerLeft _ (pullbackComp f g).hom ≫ (pullbackComp (f ≫ g) h).hom =
+    eqToHom (by simp) := by
+  let e₁ := pullbackComp f (g ≫ h)
+  let e₂ := Functor.isoWhiskerRight (pullbackComp g h) (pullback f)
+  let e₃ := Functor.isoWhiskerLeft (pullback h) (pullbackComp f g)
+  let e₄ := pullbackComp (f ≫ g) h
+  change e₁.inv ≫ e₂.inv ≫ (Functor.associator _ _ _).hom ≫ e₃.hom ≫ e₄.hom = _
+  have : e₃.hom ≫ e₄.hom = (Functor.associator _ _ _).inv ≫ e₂.hom ≫ e₁.hom :=
+    congr_arg Iso.hom (SheafOfModules.pullback_assoc.{u}
+      h.toRingCatSheafHom g.toRingCatSheafHom f.toRingCatSheafHom)
+  simp [this]
+
+@[reassoc]
+lemma pseudofunctor_left_unitality :
+    (pullbackComp f (𝟙 Y)).inv ≫
+      Functor.whiskerRight (pullbackId Y).hom (pullback f) ≫ (Functor.leftUnitor _).hom =
+        eqToHom (by simp) := by
+  let e₁ := pullbackComp f (𝟙 _)
+  let e₂ := Functor.isoWhiskerRight (pullbackId Y) (pullback f)
+  let e₃ := (pullback f).leftUnitor
+  change e₁.inv ≫ e₂.hom ≫ e₃.hom = _
+  have : e₁.hom = e₂.hom ≫ e₃.hom :=
+    congr_arg Iso.hom (SheafOfModules.pullback_id_comp.{u} f.toRingCatSheafHom)
+  simp [← this]
+
+@[reassoc]
+lemma pseudofunctor_right_unitality :
+    (pullbackComp (𝟙 X) f).inv ≫
+      Functor.whiskerLeft (pullback f) (pullbackId X).hom ≫ (Functor.rightUnitor _).hom =
+        eqToHom (by simp) := by
+  let e₁ := pullbackComp (𝟙 _) f
+  let e₂ := Functor.isoWhiskerLeft (pullback f) (pullbackId _)
+  let e₃ := (pullback f).rightUnitor
+  change e₁.inv ≫ e₂.hom ≫ e₃.hom = _
+  have : e₁.hom = e₂.hom ≫ e₃.hom :=
+    congr_arg Iso.hom (SheafOfModules.pullback_comp_id.{u} f.toRingCatSheafHom)
+  simp [← this]
+
+/-- The pseudofunctor from `Schemeᵒᵖ` to the bicategory of adjunctions which sends
+a scheme `X` to the category `X.Modules` of sheaves of modules over `X`.
+(This contains both the covariant and the contravariant functorialities of
+these categories.) -/
+noncomputable def pseudofunctor :
+    Pseudofunctor (LocallyDiscrete Scheme.{u}ᵒᵖ) (Adj Cat) :=
+  LocallyDiscrete.mkPseudofunctor
+    (fun X ↦ Adj.mk (Cat.of X.unop.Modules))
+    (fun f ↦ .mk (pullbackPushforwardAdjunction f.unop).toCat)
+    (fun _ ↦ Adj.iso₂Mk (pullbackId _) (pushforwardId _).symm (by
+      dsimp
+      rw [Bicategory.conjugateEquiv_eq_categoryTheoryConjugateEquiv]
+      apply conjugateEquiv_pullbackId_hom))
+    (fun _ _ ↦ Adj.iso₂Mk (pullbackComp _ _).symm (pushforwardComp _ _) (by
+      dsimp
+      rw [Bicategory.conjugateEquiv_eq_categoryTheoryConjugateEquiv,
+        Adjunction.toCat_comp_toCat]
+      apply conjugateEquiv_pullbackComp_inv))
+    (fun _ _ _ ↦ by ext : 1; apply pseudofunctor_associativity _ _ _)
+    (fun _ ↦ by ext : 1; apply pseudofunctor_left_unitality)
+    (fun _ ↦ by ext : 1; apply pseudofunctor_right_unitality)
 
-attribute [local instance] Types.instFunLike Types.instConcreteCategory in
-noncomputable instance : HasSheafify (Opens.grothendieckTopology X) AddCommGrpCat.{u} :=
-  inferInstance
+attribute [simps! obj_obj map_l map_r map_adj] pseudofunctor
+attribute [simps! mapId_hom_τl mapId_hom_τr mapId_inv_τl mapId_inv_τr] pseudofunctor
+attribute [simps! mapComp_hom_τl mapComp_hom_τr] pseudofunctor
+attribute [simps! mapComp_inv_τl mapComp_inv_τr] pseudofunctor
 
-attribute [local instance] Types.instFunLike Types.instConcreteCategory in
-noncomputable instance : Abelian X.Modules := inferInstance
+end Modules
 
 end AlgebraicGeometry.Scheme

Mathlib/CategoryTheory/Adjunction/CompositionIso.lean

@@ -12,9 +12,9 @@ public import Mathlib.CategoryTheory.Adjunction.Mates
 
 In this file, given isomorphisms between compositions of right adjoint functors,
 we obtain isomorphisms between the corresponding compositions of the left adjoint functors,
-and show that the left adjoint functors satisfy properties similar to the left/right
+and show that the left adjoint functors satisfies properties similar to the left/right
 unitality and the associativity of pseudofunctors if the right adjoint functors
-satisfy the corresponding properties.
+satisfies the corresponding properties.
 
 This is used in `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback` to study
 the behaviour with respect to composition of the pullback functors on presheaves
@@ -34,12 +34,23 @@ open Functor
 
 namespace Adjunction
 
+section
+
+variable {F : C₀ ⥤ C₀} {G : C₀ ⥤ C₀} (adj : F ⊣ G) (e : G ≅ 𝟭 C₀)
+
 /-- If a right adjoint functor is isomorphic to the identity functor,
 so is the left adjoint. -/
 @[simps! -isSimp]
 def leftAdjointIdIso {F : C₀ ⥤ C₀} {G : C₀ ⥤ C₀} (adj : F ⊣ G) (e : G ≅ 𝟭 C₀) :
     F ≅ 𝟭 C₀ := (conjugateIsoEquiv .id adj).symm e.symm
 
+@[simp]
+lemma conjugateEquiv_leftAdjointIdIso_hom :
+    conjugateEquiv .id adj (leftAdjointIdIso adj e).hom = e.inv := by
+  simp [leftAdjointIdIso]
+
+end
+
 section
 
 variable {F₀₁ : C₀ ⥤ C₁} {F₁₂ : C₁ ⥤ C₂} {F₀₂ : C₀ ⥤ C₂}
@@ -67,6 +78,13 @@ lemma leftAdjointCompIso_hom (e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀) :
       leftAdjointCompNatTrans adj₀₁ adj₁₂ adj₀₂ e₀₁₂.inv :=
   rfl
 
+@[simp]
+lemma conjugateEquiv_leftAdjointCompIso_inv (e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀) :
+    conjugateEquiv (adj₀₁.comp adj₁₂) adj₀₂
+      (leftAdjointCompIso adj₀₁ adj₁₂ adj₀₂ e₀₁₂).inv = e₀₁₂.hom := by
+  dsimp only [leftAdjointCompIso]
+  simp
+
 end
 
 lemma leftAdjointCompIso_comp_id

Mathlib/CategoryTheory/Bicategory/Adjunction/Basic.lean

@@ -81,6 +81,7 @@ theorem rightZigzag_idempotent_of_left_triangle
       rw [h]; bicategory
 
 /-- Adjunction between two 1-morphisms. -/
+@[ext]
 structure Adjunction (f : a ⟶ b) (g : b ⟶ a) where
   /-- The unit of an adjunction. -/
   unit : 𝟙 a ⟶ f ≫ g

Mathlib/CategoryTheory/Bicategory/Adjunction/Cat.lean

@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.CategoryTheory.Adjunction.Mates
+public import Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
+public import Mathlib.CategoryTheory.Category.Cat
+
+/-!
+# Adjunctions in `Cat`
+
+-/
+
+@[expose] public section
+
+universe v u
+
+namespace CategoryTheory
+
+open Bicategory
+
+section
+
+variable {C D E : Type u} [Category.{v} C] [Category.{v} D] [Category.{v} E]
+  {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G)
+  {F' : D ⥤ E} {G' : E ⥤ D} (adj' : F' ⊣ G')
+
+attribute [local simp] bicategoricalComp Cat.associator_hom_app Cat.associator_inv_app
+  Cat.leftUnitor_hom_app Cat.leftUnitor_inv_app Cat.rightUnitor_hom_app Cat.rightUnitor_inv_app
+  Functor.toCatHom
+
+namespace Adjunction
+
+/-- The adjunction in the bicategorical sense attached to an adjunction between functors. -/
+abbrev toCat : Bicategory.Adjunction F.toCatHom G.toCatHom where
+  unit := adj.unit
+  counit := adj.counit
+
+/-- The adjunction of functors corresponding to an adjunction in the bicategory `Cat`. -/
+abbrev ofCat {C D : Cat} {F : C ⟶ D} {G : D ⟶ C}
+    (adj : Bicategory.Adjunction F G) :
+    Functor.ofCatHom F ⊣ Functor.ofCatHom G where
+  unit := adj.unit
+  counit := adj.counit
+  left_triangle_components X := by simpa using congr_app adj.left_triangle X
+  right_triangle_components X := by simpa using congr_app adj.right_triangle X
+
+@[simp]
+lemma toCat_ofCat
+    {C D : Cat} {F : C ⟶ D} {G : D ⟶ C} (adj : Bicategory.Adjunction F G) :
+    (Adjunction.ofCat adj).toCat = adj := rfl
+
+@[simp]
+lemma ofCat_toCat :
+    Adjunction.ofCat adj.toCat = adj := rfl
+
+lemma toCat_comp_toCat : adj.toCat.comp adj'.toCat = (adj.comp adj').toCat := by
+  cat_disch
+
+end Adjunction
+
+end
+
+namespace Bicategory
+
+@[simp]
+lemma Adjunction.toCat_id (C : Cat.{v, u}) :
+    Adjunction.ofCat (Adjunction.id C) = CategoryTheory.Adjunction.id :=
+  rfl
+
+lemma mateEquiv_eq_categoryTheoryMateEquiv {C D E F : Cat}
+    {G : C ⟶ E} {H : D ⟶ F} {L₁ : C ⟶ D} {R₁ : D ⟶ C} {L₂ : E ⟶ F} {R₂ : F ⟶ E}
+    (adj₁ : Bicategory.Adjunction L₁ R₁) (adj₂ : Bicategory.Adjunction L₂ R₂)
+    (f : G ≫ L₂ ⟶ L₁ ≫ H) :
+    Bicategory.mateEquiv adj₁ adj₂ f =
+      CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) f := by
+  ext X
+  simp [mateEquiv, Adjunction.homEquiv₁, Adjunction.homEquiv₂, Functor.ofCatHom,
+    Cat.rightUnitor_inv_app, Cat.associator_hom_app, Cat.associator_inv_app,
+    Cat.leftUnitor_hom_app]
+
+lemma conjugateEquiv_eq_categoryTheoryConjugateEquiv {C D : Cat}
+    {L₁ L₂ : C ⟶ D} {R₁ R₂ : D ⟶ C}
+    (adj₁ : Bicategory.Adjunction L₁ R₁) (adj₂ : Bicategory.Adjunction L₂ R₂) (f : L₂ ⟶ L₁) :
+    Bicategory.conjugateEquiv adj₁ adj₂ f =
+      CategoryTheory.conjugateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) f := by
+  dsimp [Bicategory.conjugateEquiv]
+  rw [mateEquiv_eq_categoryTheoryMateEquiv]
+  ext X
+  simp [CategoryTheory.conjugateEquiv, Functor.ofCatHom,
+    Cat.rightUnitor_inv_app, Cat.leftUnitor_hom_app]
+
+end Bicategory
+
+end CategoryTheory