feat(Algebra/ModuleCat/Presheaf): composition of pushforwards and pullbacks and compatibilites

Mathlib.lean

@@ -114,7 +114,11 @@ import Mathlib.Algebra.Category.ModuleCat.Presheaf
 import Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian
 import Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
 import Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
+import Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
+import Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
+import Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
 import Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
+import Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
 import Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
 import Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
 import Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
@@ -1423,6 +1427,7 @@ import Mathlib.CategoryTheory.Adjunction.Limits
 import Mathlib.CategoryTheory.Adjunction.Mates
 import Mathlib.CategoryTheory.Adjunction.Opposites
 import Mathlib.CategoryTheory.Adjunction.Over
+import Mathlib.CategoryTheory.Adjunction.PartialAdjoint
 import Mathlib.CategoryTheory.Adjunction.Reflective
 import Mathlib.CategoryTheory.Adjunction.Restrict
 import Mathlib.CategoryTheory.Adjunction.Triple

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -33,22 +33,63 @@ variable [Ring R]
 /-- The free functor `Type u ⥤ ModuleCat R` sending a type `X` to the
 free `R`-module with generators `x : X`, implemented as the type `X →₀ R`.
 -/
-@[simps]
 def free : Type u ⥤ ModuleCat R where
   obj X := ModuleCat.of R (X →₀ R)
   map {X Y} f := Finsupp.lmapDomain _ _ f
   map_id := by intros; exact Finsupp.lmapDomain_id _ _
   map_comp := by intros; exact Finsupp.lmapDomain_comp _ _ _ _
 
+variable {R}
+
+/-- Constructor for elements in the module `(free R).obj X`. -/
+noncomputable def freeMk {X : Type u} (x : X) : (free R).obj X := Finsupp.single x 1
+
+@[ext 1200]
+lemma free_hom_ext {X : Type u} {M : ModuleCat.{u} R} {f g : (free R).obj X ⟶ M}
+    (h : ∀ (x : X), f (freeMk x) = g (freeMk x)) :
+    f = g :=
+  (Finsupp.lhom_ext' (fun x ↦ LinearMap.ext_ring (h x)))
+
+/-- The morphism of modules `(free R).obj X ⟶ M` corresponding
+to a map `f : X ⟶ M`. -/
+noncomputable def freeDesc {X : Type u} {M : ModuleCat.{u} R} (f : X ⟶ M) :
+    (free R).obj X ⟶ M :=
+  Finsupp.lift M R X f
+
+@[simp]
+lemma freeDesc_apply {X : Type u} {M : ModuleCat.{u} R} (f : X ⟶ M) (x : X) :
+    freeDesc f (freeMk x) = f x := by
+  dsimp [freeDesc]
+  erw [Finsupp.lift_apply, Finsupp.sum_single_index]
+  all_goals simp
+
+@[simp]
+lemma free_map_apply {X Y : Type u} (f : X → Y) (x : X) :
+    (free R).map f (freeMk x) = freeMk (f x) := by
+  apply Finsupp.mapDomain_single
+
+/-- The bijection `((free R).obj X ⟶ M) ≃ (X → M)` when `X` is a type and `M` a module. -/
+@[simps]
+def freeHomEquiv {X : Type u} {M : ModuleCat.{u} R} :
+    ((free R).obj X ⟶ M) ≃ (X ⟶ M) where
+  toFun φ x := φ (freeMk x)
+  invFun ψ := freeDesc ψ
+  left_inv _ := by ext; simp
+  right_inv _ := by ext; simp
+
+variable (R)
+
 /-- The free-forgetful adjunction for R-modules.
 -/
 def adj : free R ⊣ forget (ModuleCat.{u} R) :=
   Adjunction.mkOfHomEquiv
-    { homEquiv := fun X M => (Finsupp.lift M R X).toEquiv.symm
-      homEquiv_naturality_left_symm := fun {_ _} M f g =>
-        Finsupp.lhom_ext' fun x =>
-          LinearMap.ext_ring
-            (Finsupp.sum_mapDomain_index_addMonoidHom fun y => (smulAddHom R M).flip (g y)).symm }
+    { homEquiv := fun _ _ => freeHomEquiv
+      homEquiv_naturality_left_symm := fun {X Y M} f g ↦ by ext; simp [freeHomEquiv] }
+
+@[simp]
+lemma adj_homEquiv (X : Type u) (M : ModuleCat.{u} R) :
+    (adj R).homEquiv X M = freeHomEquiv := by
+  simp only [adj, Adjunction.mkOfHomEquiv_homEquiv]
 
 instance : (forget (ModuleCat.{u} R)).IsRightAdjoint  :=
   (adj R).isRightAdjoint

Mathlib/Algebra/Category/ModuleCat/Presheaf/EpiMono.lean

@@ -0,0 +1,34 @@
+/-
+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
+-/
+
+import Mathlib.Algebra.Category.ModuleCat.Presheaf
+
+/-!
+# Epimorphisms and monomorphisms in the category of presheaves of modules
+
+In this file, we shall give characterizations of epimorphisms and monomorphisms (TODO)
+in the category of presheaves of modules.
+
+So far, we have only obtained the lemma `epi_of_surjective`.
+
+-/
+
+universe v v₁ u₁ u
+
+open CategoryTheory
+
+namespace PresheafOfModules
+
+variable {C : Type u₁} [Category.{v₁} C] {R : Cᵒᵖ ⥤ RingCat.{u}}
+  {M₁ M₂ : PresheafOfModules.{v} R} {f : M₁ ⟶ M₂}
+
+lemma epi_of_surjective (hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Surjective (f.app X)) : Epi f where
+  left_cancellation {M₃} g₁ g₂ hg := by
+    ext X m₂
+    obtain ⟨m₁, rfl⟩ := hf m₂
+    exact congr_fun ((evaluation R X ⋙ forget _).congr_map hg) m₁
+
+end PresheafOfModules

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

@@ -0,0 +1,116 @@
+/-
+Copyright (c) 2024 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin, Joel Riou
+-/
+import Mathlib.Algebra.Category.ModuleCat.Presheaf
+import Mathlib.Algebra.Category.ModuleCat.Adjunctions
+
+/-! The free presheaf of modules on a presheaf of sets
+
+In this file, given a presheaf of rings `R` on a category `C`,
+we construct the functor
+`PresheafOfModules.free (Cᵒᵖ ⥤ Type u) ⥤ PresheafOfModules.{u} R`
+which sends a presheaf of types to the corresponding presheaf of free modules.
+`PresheafOfModules.freeAdjunction` shows that this functor is the left
+adjoint to the forget functor.
+
+## Notes
+
+This contribution was created as part of the AIM workshop
+"Formalizing algebraic geometry" in June 2024.
+
+-/
+
+universe u v₁ u₁
+
+open CategoryTheory
+
+namespace PresheafOfModules
+
+variable {C : Type u₁} [Category.{v₁} C] (R : Cᵒᵖ ⥤ RingCat.{u})
+
+variable {R} in
+/-- Given a presheaf of types `F : Cᵒᵖ ⥤ Type u`, this is the presheaf
+of modules over `R` which sends `X : Cᵒᵖ` to the free `R.obj X`-module on `F.obj X`. -/
+@[simps]
+noncomputable def freeObj (F : Cᵒᵖ ⥤ Type u) : PresheafOfModules.{u} R where
+  obj := fun X ↦ (ModuleCat.free (R.obj X)).obj (F.obj X)
+  map := fun {X Y} f ↦ ModuleCat.freeDesc
+      (fun x ↦ ModuleCat.freeMk (F.map f x))
+  map_id := by aesop
+
+/-- The free presheaf of modules functors `(Cᵒᵖ ⥤ Type u) ⥤ PresheafOfModules.{u} R`. -/
+@[simps]
+noncomputable def free : (Cᵒᵖ ⥤ Type u) ⥤ PresheafOfModules.{u} R where
+  obj := freeObj
+  map {F G} φ :=
+    { app := fun X ↦ (ModuleCat.free (R.obj X)).map (φ.app X)
+      naturality := fun {X Y} f ↦ by
+        dsimp
+        ext x
+        simp only [ModuleCat.coe_comp, Function.comp_apply, ModuleCat.freeDesc_apply,
+          ModuleCat.restrictScalars.map_apply, ModuleCat.free_map_apply]
+        congr 1
+        exact NatTrans.naturality_apply φ f x }
+
+section
+
+variable {R}
+
+variable {F : Cᵒᵖ ⥤ Type u} {G G' : PresheafOfModules.{u} R}
+
+/-- The morphism of presheaves of modules `freeObj F ⟶ G` corresponding to
+a morphism `F ⟶ G.presheaf ⋙ forget _` of presheaves of types. -/
+@[simps]
+noncomputable def freeObjDesc (φ : F ⟶ G.presheaf ⋙ forget _) : freeObj F ⟶ G where
+  app X := ModuleCat.freeDesc (φ.app X)
+  naturality {X Y} f := by
+    dsimp
+    ext x
+    simpa using NatTrans.naturality_apply φ f x
+
+variable (F R) in
+/-- The unit of `PresheafOfModules.freeAdjunction`. -/
+@[simps]
+noncomputable def freeAdjunctionUnit : F ⟶ (freeObj (R := R) F).presheaf ⋙ forget _ where
+  app X x := ModuleCat.freeMk x
+  naturality X Y f := by ext; simp [presheaf]
+
+/-- The bijection `(freeObj F ⟶ G) ≃ (F ⟶ G.presheaf ⋙ forget _)` when
+`F` is a presheaf of types and `G` a presheaf of modules. -/
+noncomputable def freeHomEquiv : (freeObj F ⟶ G) ≃ (F ⟶ G.presheaf ⋙ forget _) where
+  toFun ψ := freeAdjunctionUnit R F ≫ whiskerRight ((toPresheaf _).map ψ) _
+  invFun φ := freeObjDesc φ
+  left_inv ψ := by ext1 X; dsimp; ext x; simp [toPresheaf]
+  right_inv φ := by ext; simp [toPresheaf]
+
+lemma free_hom_ext {ψ ψ' : freeObj F ⟶ G}
+    (h : freeAdjunctionUnit R F ≫ whiskerRight ((toPresheaf _).map ψ) _ =
+      freeAdjunctionUnit R F ≫ whiskerRight ((toPresheaf _).map ψ') _ ) : ψ = ψ' :=
+  freeHomEquiv.injective h
+
+variable (R) in
+/-- The free presheaf of modules functor is left adjoint to the forget functor
+`PresheafOfModules.{u} R ⥤ Cᵒᵖ ⥤ Type u`. -/
+noncomputable def freeAdjunction :
+    free.{u} R ⊣ (toPresheaf R ⋙ (whiskeringRight _ _ _).obj (forget Ab)) :=
+  Adjunction.mkOfHomEquiv
+    { homEquiv := fun _ _ ↦ freeHomEquiv
+      homEquiv_naturality_left_symm := fun {F₁ F₂ G} f g ↦
+        free_hom_ext (by ext; simp [freeHomEquiv, toPresheaf])
+      homEquiv_naturality_right := fun {F G₁ G₂} f g ↦ rfl }
+
+variable (F G) in
+@[simp]
+lemma freeAdjunction_homEquiv : (freeAdjunction R).homEquiv F G = freeHomEquiv := by
+  simp [freeAdjunction, Adjunction.mkOfHomEquiv_homEquiv]
+
+variable (R F) in
+@[simp]
+lemma freeAdjunction_unit_app :
+    (freeAdjunction R).unit.app F = freeAdjunctionUnit R F := rfl
+
+end
+
+end PresheafOfModules