[Merged by Bors] - feat(Algebra/Category/ModuleCat/Presheaf): the adjunction between colimitFunctor and constFunctor

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

@@ -41,6 +41,19 @@ variable {C : Type u} [Category.{v} C] [LocallySmall.{w} C]
   [IsCofiltered C] [InitiallySmall.{w} C]
   {R : Cᵒᵖ ⥤ RingCat.{w}} {cR : Cocone R} (hcR : IsColimit cR)
 
+variable (cR) in
+/-- Given a cocone `cR` for a functor `R : Cᵒᵖ ⥤ RingCat`, this is the
+functor `ModuleCat cR.pt ⥤ PresheafOfModules R` which sends a module `M`
+over `cR.pt` to a presheaf of modules whose underlying presheaf of
+abelian groups is the constant functor `Cᵒᵖ ⥤ AddCommGrpCat` with value `M`. -/
+noncomputable def constFunctor : ModuleCat cR.pt ⥤ PresheafOfModules.{w} R where
+  obj M :=
+    { obj X := (ModuleCat.restrictScalars (cR.ι.app X).hom).obj M
+      map {X Y} f :=
+        (ModuleCat.restrictScalarsComp' _ _ _
+          (by ext; dsimp; rw [← Cocone.w cR f]; dsimp; rfl)).hom.app _ }
+  map φ := { app X := (ModuleCat.restrictScalars (cR.ι.app X).hom).map φ }
+
 section
 
 variable {M : PresheafOfModules.{w} R} {cM : Cocone M.presheaf} (hcM : IsColimit cM)
@@ -187,6 +200,83 @@ noncomputable instance : Module cR.pt (ModuleColimit hcR hcM) where
     obtain ⟨U, r₁, r₂, m, rfl, rfl, rfl⟩ := jointly_surjective₃ r₁ r₂ m
     simp only [smul_eq, ← map_add, add_smul]
 
+/-- Auxiliary definition for `homEquiv`. This is the universal property
+of `PresheafOfModules.ModuleColimit`, as an abelian group. -/
+noncomputable def homEquiv' {N : Type w} [AddCommGroup N] :
+    (ModuleColimit hcR hcM →+ N) ≃+ (M.presheaf ⟶ (Functor.const _).obj (.of N)) where
+  toEquiv := (ConcreteCategory.homEquiv (X := AddCommGrpCat.of (ModuleColimit hcR hcM))
+    (Y := AddCommGrpCat.of N)).symm.trans hcM.homEquiv
+  map_add' _ _ := rfl
+
+omit [LocallySmall.{w, v, u} C] [IsCofiltered C] [InitiallySmall C] in
+lemma homEquiv'_app_apply {N : ModuleCat.{w} cR.pt}
+    (α : ModuleColimit hcR hcM →+ N) {X : Cᵒᵖ} (x : M.obj X) :
+    dsimp% (homEquiv' hcR hcM α).app X x = α (cM.ι.app X x) :=
+  rfl
+
+omit [LocallySmall.{w, v, u} C] [IsCofiltered C] [InitiallySmall C] in
+lemma homEquiv'_symm_apply {N : ModuleCat.{w} cR.pt}
+    (β : M.presheaf ⟶ (Functor.const _).obj (.of N)) {X : Cᵒᵖ} (x : M.obj X) :
+    (homEquiv' hcR hcM).symm β (cM.ι.app X x) = β.app X x :=
+  ConcreteCategory.congr_hom (hcM.ι_app_homEquiv_symm β X) x
+
+lemma map_smul_homEquiv'_iff {N : ModuleCat.{w} cR.pt}
+    (α : ModuleColimit hcR hcM →+ N) :
+    dsimp% (∀ (U : Cᵒᵖ) (r : R.obj U) (m : M.obj U), (homEquiv' hcR hcM α).app U (r • m) =
+        letI m' : N := (homEquiv' hcR hcM α).app U m; letI r' : cR.pt := cR.ι.app U r
+        r' • m') ↔
+    ∀ (r : cR.pt) (m : ModuleColimit hcR hcM), α (r • m) = r • α m := by
+  refine ⟨fun h r m ↦ ?_, fun h U r m ↦ ?_⟩
+  · obtain ⟨U, r, m, rfl, rfl⟩ := jointly_surjective₂ r m
+    refine Eq.trans ?_ ((homEquiv'_app_apply ..).symm.trans (h U r m))
+    congr 1
+    apply smul_eq
+  · rw [homEquiv'_app_apply, homEquiv'_app_apply, ← h]
+    congr 1
+    exact (smul_eq ..).symm
+
+/-- This is the universal property of `PresheafOfModules.ModuleColimit` as a module.
+See also `PresheafOfModules.colimitAdjunction`. -/
+noncomputable def homEquiv {N : ModuleCat.{w} cR.pt} :
+    (ModuleCat.of cR.pt (ModuleColimit hcR hcM) ⟶ N) ≃+ (M ⟶ (constFunctor cR).obj N) where
+  toFun φ := PresheafOfModules.homMk
+    (homEquiv' hcR hcM ((forget₂ _ AddCommGrpCat).map φ).hom)
+      ((map_smul_homEquiv'_iff hcR hcM ((forget₂ _ AddCommGrpCat).map φ).hom).2 (by simp))
+  invFun ψ := ModuleCat.ofHom
+    { toFun := (homEquiv' hcR hcM).symm ((toPresheaf _).map ψ)
+      map_add' := by simp
+      map_smul' := by
+        obtain ⟨φ, hφ⟩ := (homEquiv' hcR hcM).surjective ((toPresheaf _).map ψ)
+        simp only [← hφ, AddEquiv.symm_apply_apply, RingHom.id_apply]
+        refine (map_smul_homEquiv'_iff hcR hcM φ).1 (fun U r m ↦ ?_)
+        rw [hφ]
+        erw [toPresheaf_map_app_apply]
+        rw [map_smul]
+        rfl}
+  left_inv φ := (forget₂ _ AddCommGrpCat).map_injective (by
+    ext : 1
+    exact (homEquiv' hcR hcM).left_inv ((forget₂ _ AddCommGrpCat).map φ).hom)
+  right_inv ψ := (toPresheaf _).map_injective ((homEquiv' hcR hcM).right_inv _)
+  map_add' φ₁ φ₂ := (toPresheaf _).map_injective
+    ((homEquiv' hcR hcM).map_add ((forget₂ _ AddCommGrpCat).map φ₁).hom
+      ((forget₂ _ AddCommGrpCat).map φ₂).hom)
+
+@[simp]
+lemma homEquiv_app_apply {N : ModuleCat.{w} cR.pt}
+    (α : ModuleCat.of cR.pt (ModuleColimit hcR hcM) ⟶ N) {X : Cᵒᵖ} (x : M.obj X) :
+    dsimp% (homEquiv hcR hcM α).app X x = α (cM.ι.app X x) :=
+  rfl
+
+lemma homEquiv_naturality_right {N N' : ModuleCat.{w} cR.pt}
+    (φ : ModuleCat.of cR.pt (ModuleColimit hcR hcM) ⟶ N) (g : N ⟶ N') :
+    homEquiv hcR hcM (φ ≫ g) = homEquiv hcR hcM φ ≫ (constFunctor cR).map g := rfl
+
+@[simp]
+lemma homEquiv_symm_apply {N : ModuleCat.{w} cR.pt} (β : M ⟶ (constFunctor cR).obj N)
+    {X : Cᵒᵖ} (x : M.obj X) :
+    dsimp% (homEquiv hcR hcM).symm β (cM.ι.app X x) = β.app X x := by
+  exact homEquiv'_symm_apply ..
+
 section
 
 variable {M' : PresheafOfModules.{w} R} {cM' : Cocone M'.presheaf}
@@ -229,6 +319,27 @@ lemma comp_map
 
 end
 
+lemma homEquiv_naturality_left {M' : PresheafOfModules.{w} R} {cM' : Cocone M'.presheaf}
+    (hcM' : IsColimit cM') {N : ModuleCat.{w} cR.pt}
+    (φ' : ModuleCat.of cR.pt (ModuleColimit hcR hcM') ⟶ N)
+    (f : M ⟶ M') :
+    homEquiv hcR hcM (ModuleCat.ofHom (map hcR hcM hcM' f) ≫ φ') =
+      f ≫ homEquiv hcR hcM' φ' := by
+  ext U m
+  simp only [homEquiv_app_apply, ModuleCat.hom_comp, ModuleCat.hom_ofHom, LinearMap.coe_comp,
+    Function.comp_apply, comp_app]
+  apply congr_arg
+  exact map_apply hcR hcM hcM' f m
+
+lemma homEquiv_naturality_left_symm {M' : PresheafOfModules.{w} R} {cM' : Cocone M'.presheaf}
+    (hcM' : IsColimit cM') {N : ModuleCat.{w} cR.pt}
+    (f : M ⟶ M') (g : M' ⟶ (constFunctor cR).obj N) :
+    (homEquiv hcR hcM).symm (f ≫ g) =
+      ModuleCat.ofHom (map hcR hcM hcM' f) ≫ (homEquiv hcR hcM').symm g :=
+  (homEquiv hcR hcM).injective (by
+    obtain ⟨g, rfl⟩ := (homEquiv hcR hcM').surjective g
+    simp [homEquiv_naturality_left])
+
 end ModuleColimit
 
 end
@@ -241,4 +352,31 @@ noncomputable def colimitFunctor : PresheafOfModules.{w} R ⥤ ModuleCat.{w} cR.
   map f := ModuleCat.ofHom (ModuleColimit.map _ _ _ f)
   map_comp f g := by ext : 1; exact (ModuleColimit.comp_map ..).symm
 
+/-- Given a presheaf of rings `R` on a cofiltered category, this is the
+adjunction between `colimitFunctor : PresheafOfModules R ⥤ ModuleCat cR.pt`
+and the constant functor. -/
+noncomputable def colimitAdjunction :
+    colimitFunctor.{w} hcR ⊣ constFunctor.{w} cR :=
+  Adjunction.mkOfHomEquiv
+    { homEquiv _ _ := (ModuleColimit.homEquiv _ _).toEquiv
+      homEquiv_naturality_left_symm _ _ := ModuleColimit.homEquiv_naturality_left_symm _ _ _ _ _
+      homEquiv_naturality_right _ _ := ModuleColimit.homEquiv_naturality_right _ _ _ _ }
+
+lemma colimitAdjunction_homEquiv
+    (F : PresheafOfModules R) (G : ModuleCat cR.pt) :
+    dsimp% (colimitAdjunction.{w} hcR).homEquiv F G =
+      (ModuleColimit.homEquiv hcR
+        (colimit.isColimit F.presheaf)).toEquiv := by
+  simp [colimitAdjunction]
+
+open ModuleColimit in
+lemma colimitAdjunction_homEquiv_symm_apply
+    {F : PresheafOfModules R} {G : ModuleCat cR.pt}
+    (β : F ⟶ (constFunctor cR).obj G) {X : Cᵒᵖ} (m : F.obj X) :
+    ((colimitAdjunction.{w} hcR).homEquiv F G).symm β
+      (ModuleColimit.ιM (hcR := hcR) (hcM := colimit.isColimit F.presheaf) m) =
+        β.app X m := by
+  rw [colimitAdjunction_homEquiv]
+  apply homEquiv_symm_apply
+
 end PresheafOfModules