feat(Algebra/Category/ModuleCat/Sheaf): O_S ⟶ f_* O_X and f^* O_S ≅ O_X (#30398)

Author: joelriou

Mathlib.lean

@@ -185,6 +185,7 @@ import Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
 import Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
 import Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits
 import Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
+import Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
 import Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
 import Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
 import Mathlib.Algebra.Category.ModuleCat.Simple

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

@@ -18,7 +18,7 @@ a type `I` to the coproduct of copies indexed by `I` of `unit R`.
 * In case the category `C` has a terminal object `X`, promote `freeHomEquiv`
   into an adjunction between `freeFunctor` and the evaluation functor at `X`.
   (Alternatively, assuming specific universe parameters, we could show that
-  `freeHomEquiv` is a left adjoint to `SheafOfModules.sectionsFunctor`.)
+  `freeFunctor` is a left adjoint to `SheafOfModules.sectionsFunctor`.)
 
 -/
 
@@ -34,14 +34,33 @@ namespace SheafOfModules
 /-- The free sheaf of modules on a certain type `I`. -/
 noncomputable def free (I : Type u) : SheafOfModules.{u} R := ∐ (fun (_ : I) ↦ unit R)
 
+/-- The inclusions `unit R ⟶ free I`. -/
+noncomputable def ιFree {I : Type u} (i : I) : unit R ⟶ free I :=
+  Sigma.ι (fun (_ : I) ↦ unit R) i
+
+
+/-- The tautological cofan with point `free I : SheafOfModules R`. -/
+noncomputable def freeCofan (I : Type u) : Cofan (fun (_ : I) ↦ unit R) :=
+  Cofan.mk (P := free I) ιFree
+
+@[simp]
+lemma freeCofan_inj {I : Type u} (i : I) :
+    (freeCofan (R := R) I).inj i = ιFree i := rfl
+
+/-- `free I` is the colimit of copies of `unit R` indexed by `I`. -/
+noncomputable def isColimitFreeCofan (I : Type u) :
+    IsColimit (freeCofan (R := R) I) :=
+  coproductIsCoproduct _
+
 /-- The data of a morphism `free I ⟶ M` from a free sheaf of modules is
 equivalent to the data of a family `I → M.sections` of sections of `M`. -/
 noncomputable def freeHomEquiv (M : SheafOfModules.{u} R) {I : Type u} :
     (free I ⟶ M) ≃ (I → M.sections) where
-  toFun f i := M.unitHomEquiv (Sigma.ι (fun (_ : I) ↦ unit R) i ≫ f)
-  invFun s := Sigma.desc (fun i ↦ M.unitHomEquiv.symm (s i))
-  left_inv s := Sigma.hom_ext _ _ (by simp)
-  right_inv f := by ext1 i; simp
+  toFun f i := M.unitHomEquiv (ιFree i ≫ f)
+  invFun s := Cofan.IsColimit.desc (isColimitFreeCofan I) (fun i ↦ M.unitHomEquiv.symm (s i))
+  left_inv s := Cofan.IsColimit.hom_ext (isColimitFreeCofan I) _ _
+    (fun i ↦ by simp [← freeCofan_inj])
+  right_inv f := by ext1 i; simp [← freeCofan_inj]
 
 lemma freeHomEquiv_comp_apply {M N : SheafOfModules.{u} R} {I : Type u}
     (f : free I ⟶ M) (p : M ⟶ N) (i : I) :
@@ -56,6 +75,11 @@ lemma freeHomEquiv_symm_comp {M N : SheafOfModules.{u} R} {I : Type u} (s : I 
 noncomputable abbrev freeSection {I : Type u} (i : I) : (free (R := R) I).sections :=
   (free (R := R) I).freeHomEquiv (𝟙 (free I)) i
 
+lemma unitHomEquiv_symm_freeHomEquiv_apply
+    {I : Type u} {M : SheafOfModules.{u} R} (f : free I ⟶ M) (i : I) :
+    M.unitHomEquiv.symm (M.freeHomEquiv f i) = ιFree i ≫ f := by
+  simp [freeHomEquiv]
+
 section
 
 variable {I J : Type u} (f : I → J)
@@ -75,11 +99,19 @@ lemma sectionMap_freeMap_freeSection (i : I) :
     sectionsMap (freeMap (R := R) f) (freeSection i) = freeSection (f i) := by
   simp [← freeHomEquiv_comp_apply]
 
+@[reassoc (attr := simp)]
+lemma ιFree_freeMap (i : I) :
+    ιFree (R := R) i ≫ freeMap f = ιFree (f i) := by
+  rw [← unitHomEquiv_symm_freeHomEquiv_apply, freeHomEquiv_freeMap]
+  dsimp [freeSection]
+  rw [unitHomEquiv_symm_freeHomEquiv_apply, Category.comp_id]
+
 end
 
 /-- The functor `Type u ⥤ SheafOfModules.{u} R` which sends a type `I` to
 `free I` which is a coproduct indexed by `I` of copies of `R` (thought of as a
 presheaf of modules over itself). -/
+@[simps]
 noncomputable def freeFunctor : Type u ⥤ SheafOfModules.{u} R where
   obj := free
   map f := freeMap f

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

@@ -52,6 +52,9 @@ of sheaves of modules. -/
 noncomputable def pullbackPushforwardAdjunction : pullback.{v} φ ⊣ pushforward.{v} φ :=
   Adjunction.ofIsRightAdjoint (pushforward φ)
 
+instance : (pullback.{v} φ).IsLeftAdjoint :=
+  (pullbackPushforwardAdjunction φ).isLeftAdjoint
+
 end
 
 section

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

@@ -0,0 +1,142 @@
+/-
+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
+-/
+import Mathlib.Algebra.Category.ModuleCat.Sheaf.Free
+import Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
+import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
+import Mathlib.CategoryTheory.Limits.Final.Type
+
+/-!
+# Pullbacks of free sheaves of modules
+
+Let `S` (resp.`R`) be a sheaf of rings on a category `C` (resp. `D`)
+equipped with a Grothendieck topology `J` (resp. `K`).
+Let `F : C ⥤ D` be a continuous functor.
+Let `φ` be a morphism from `S` to the direct image of `R`.
+
+We introduce `unitToPushforwardObjUnit φ` which is the morphism
+in the category `SheafOfModules S` which corresponds to `φ`, and
+show that the adjoint morphism
+`pullbackObjUnitToUnit φ : (pullback.{u} φ).obj (unit S) ⟶ unit R`
+is an isomorphism when `F` is a final functor.
+More generally, the functor `pullback φ` sends the free sheaf
+of modules `free I` to `free I`, see `pullbackObjFreeIso` and
+`freeFunctorCompPullbackIso`.
+-/
+
+universe v v₁ v₂ u₁ u₂ u
+
+open CategoryTheory Limits
+
+namespace SheafOfModules
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
+  {J : GrothendieckTopology C} {K : GrothendieckTopology D} {F : C ⥤ D}
+  {S : Sheaf J RingCat.{u}} {R : Sheaf K RingCat.{u}}
+  [Functor.IsContinuous.{u} F J K]
+  (φ : S ⟶ (F.sheafPushforwardContinuous RingCat.{u} J K).obj R)
+
+/-- The canonical map from the (global) sections of a sheaf of modules
+to the (global) sections of its pushforward. -/
+@[simps]
+def pushforwardSections [Functor.IsContinuous.{v} F J K]
+    {M : SheafOfModules.{v} R} (s : M.sections) :
+    ((pushforward φ).obj M).sections where
+  val _ := s.val _
+  property _ := s.property _
+
+variable (M) in
+lemma bijective_pushforwardSections [Functor.IsContinuous.{v} F J K] [F.Final] :
+    Function.Bijective (pushforwardSections φ (M := M)) :=
+  Functor.bijective_sectionsPrecomp _ _
+
+variable [J.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
+  [K.HasSheafCompose (forget₂ RingCat.{u} AddCommGrpCat.{u})]
+
+/-- The canonical morphism `unit S ⟶ (pushforward.{u} φ).obj (unit R)`
+of sheaves of modules corresponding to a continuous map between ringed sites. -/
+def unitToPushforwardObjUnit : unit S ⟶ (pushforward.{u} φ).obj (unit R) where
+  val.app X := ModuleCat.homMk ((forget₂ RingCat AddCommGrpCat).map (φ.val.app X)) (fun r ↦ by
+    ext m
+    exact ((φ.val.app X).hom.map_mul _ _).symm)
+  val.naturality f := by
+    ext
+    exact ConcreteCategory.congr_hom (φ.val.naturality f) _
+
+lemma unitToPushforwardObjUnit_val_app_apply {X : Cᵒᵖ} (a : S.val.obj X) :
+    (unitToPushforwardObjUnit φ).val.app X a = φ.val.app X a := rfl
+
+lemma pushforwardSections_unitHomEquiv
+    {M : SheafOfModules.{u} R} (f : unit R ⟶ M) :
+    pushforwardSections φ (M.unitHomEquiv f) =
+      ((pushforward φ).obj M).unitHomEquiv
+        (unitToPushforwardObjUnit φ ≫ (pushforward φ).map f) := by
+  ext X
+  have := unitToPushforwardObjUnit_val_app_apply φ (X := X) 1
+  dsimp at this ⊢
+  simp [this, map_one]
+  rfl
+
+variable [(pushforward.{u} φ).IsRightAdjoint]
+
+/-- The canonical morphism `(pullback.{u} φ).obj (unit S) ⟶ unit R`
+of sheaves of modules corresponding to a continuous map between ringed sites. -/
+noncomputable def pullbackObjUnitToUnit :
+    (pullback.{u} φ).obj (unit S) ⟶ unit R :=
+  ((pullbackPushforwardAdjunction.{u} φ).homEquiv _ _).symm (unitToPushforwardObjUnit φ)
+
+@[simp]
+lemma pullbackPushforwardAdjunction_homEquiv_symm_unitToPushforwardObjUnit :
+    ((pullbackPushforwardAdjunction.{u} φ).homEquiv _ _).symm (unitToPushforwardObjUnit φ) =
+      pullbackObjUnitToUnit φ := rfl
+
+@[simp]
+lemma pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit :
+    (pullbackPushforwardAdjunction.{u} φ).homEquiv _ _ (pullbackObjUnitToUnit φ) =
+      unitToPushforwardObjUnit φ :=
+  Equiv.apply_symm_apply _ _
+
+instance [F.Final] : IsIso (pullbackObjUnitToUnit φ) := by
+  rw [isIso_iff_coyoneda_map_bijective]
+  intro M
+  rw [← ((pullbackPushforwardAdjunction.{u} φ).homEquiv _ _).bijective.of_comp_iff',
+    ← (unitHomEquiv _).bijective.of_comp_iff']
+  convert (bijective_pushforwardSections φ M).comp (unitHomEquiv _).bijective
+  ext f : 1
+  dsimp
+  rw [pushforwardSections_unitHomEquiv, EmbeddingLike.apply_eq_iff_eq,
+    Adjunction.homEquiv_naturality_right,
+    pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit]
+
+variable [HasWeakSheafify J AddCommGrpCat.{u}] [HasWeakSheafify K AddCommGrpCat.{u}]
+  [J.WEqualsLocallyBijective AddCommGrpCat.{u}]
+  [K.WEqualsLocallyBijective AddCommGrpCat.{u}] [F.Final]
+
+/-- The pullback of a free sheaf of modules is a free sheaf of modules. -/
+noncomputable def pullbackObjFreeIso (I : Type u) :
+    (pullback φ).obj (free I) ≅ free I :=
+  (asIso (sigmaComparison _ _)).symm ≪≫
+    Sigma.mapIso (fun _ ↦ asIso (pullbackObjUnitToUnit φ))
+
+@[reassoc (attr := simp)]
+lemma pullback_map_ιFree_comp_pullbackObjFreeIso_hom {I : Type u} (i : I) :
+    (pullback φ).map (ιFree i) ≫ (pullbackObjFreeIso φ I).hom =
+      pullbackObjUnitToUnit φ ≫ ιFree i := by
+  simp [pullbackObjFreeIso, ιFree]
+
+@[reassoc (attr := simp)]
+lemma pullbackObjFreeIso_hom_naturality {I J : Type u} (f : I → J) :
+    (pullback φ).map (freeMap f) ≫ (pullbackObjFreeIso φ J).hom =
+      (pullbackObjFreeIso φ I).hom ≫ freeMap f :=
+  Cofan.IsColimit.hom_ext (isColimitCofanMkObjOfIsColimit (pullback φ) _ _
+    (isColimitFreeCofan (R := S) I)) _ _ (fun i ↦ by simp [← Functor.map_comp_assoc])
+
+/-- The canonical isomorphism `freeFunctor ⋙ pullback φ ≅ freeFunctor` for a
+continuous map between ringed sites, when the underlying functor between the sites
+is final. -/
+noncomputable def freeFunctorCompPullbackIso : freeFunctor ⋙ pullback φ ≅ freeFunctor :=
+  NatIso.ofComponents (pullbackObjFreeIso φ)
+
+end SheafOfModules

Mathlib/CategoryTheory/Limits/Preserves/Shapes/Products.lean

@@ -76,6 +76,12 @@ lemma PreservesProduct.of_iso_comparison [i : IsIso (piComparison G f)] :
   exact @IsLimit.ofPointIso _ _ _ _ _ _ _
     (limit.isLimit (Discrete.functor fun j : J => G.obj (f j))) i
 
+@[reassoc (attr := simp)]
+lemma inv_piComparison_comp_map_π [IsIso (piComparison G f)] (j : J) :
+     inv (piComparison G f) ≫ G.map (Pi.π _ j) =
+      Pi.π (fun x ↦ (G.obj (f x))) j := by
+  simp only [IsIso.inv_comp_eq, piComparison_comp_π]
+
 variable [PreservesLimit (Discrete.functor f) G]
 
 /--
@@ -139,6 +145,12 @@ lemma PreservesCoproduct.of_iso_comparison [i : IsIso (sigmaComparison G f)] :
   exact @IsColimit.ofPointIso _ _ _ _ _ _ _
     (colimit.isColimit (Discrete.functor fun j : J => G.obj (f j))) i
 
+@[reassoc (attr := simp)]
+lemma map_ι_comp_inv_sigmaComparison [IsIso (sigmaComparison G f)] (j : J) :
+    G.map (Sigma.ι _ j) ≫ inv (sigmaComparison G f) =
+      Sigma.ι (fun x ↦ (G.obj (f x))) j := by
+  simp
+
 variable [PreservesColimit (Discrete.functor f) G]
 
 /-- If `G` preserves colimits,