feat: presheaf of modules over a presheaf of rings (#4670)

This is extracted from the draft PR #4116 which tries to compare this definition with the definition in terms of a presheaf in `RingMod`.



Co-authored-by: Oliver Nash <github@olivernash.org>
Co-authored-by: Christopher Hoskin <christopher.hoskin@gmail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
Co-authored-by: Matthew Robert Ballard <k.buzzard@imperial.ac.uk>
Co-authored-by: Peter Nelson <71660771+apnelson1@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
Co-authored-by: Thomas Browning <tb65536@uw.edu>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Matthew Robert Ballard <matt@mrb.email>
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Arend Mellendijk <arend.mellendijk@gmail.com>
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com>
Co-authored-by: Bulhwi Cha <chabulhwi@semmalgil.com>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: negiizhao <egresf@gmail.com>
Co-authored-by: Alex J Best <alex.j.best@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
Co-authored-by: Jz Pan <acme_pjz@hotmail.com>

Mathlib.lean

@@ -72,6 +72,7 @@ import Mathlib.Algebra.Category.ModuleCat.Limits
 import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
 import Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
 import Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
+import Mathlib.Algebra.Category.ModuleCat.Presheaf
 import Mathlib.Algebra.Category.ModuleCat.Products
 import Mathlib.Algebra.Category.ModuleCat.Projective
 import Mathlib.Algebra.Category.ModuleCat.Simple

Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

@@ -0,0 +1,131 @@
+/-
+Copyright (c) 2023 Scott Morrison All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import Mathlib.Algebra.Category.ModuleCat.Basic
+import Mathlib.Algebra.Category.Ring.Basic
+
+/-!
+# Presheaves of modules over a presheaf of rings.
+
+We give a hands-on description of a presheaf of modules over a fixed presheaf of rings,
+as a presheaf of abelian groups with additional data.
+
+## Future work
+
+* Compare this to the definition as a presheaf of pairs `(R, M)` with specified first part.
+* Compare this to the definition as a module object of the presheaf of rings
+  thought of as a monoid object.
+* (Pre)sheaves of modules over a given sheaf of rings are an abelian category.
+* Presheaves of modules over a presheaf of commutative rings form a monoidal category.
+* Pushforward and pullback.
+-/
+
+universe v₁ u₁ u
+
+open CategoryTheory LinearMap Opposite
+
+variable {C : Type u₁} [Category.{v₁} C]
+
+/-- A presheaf of modules over a given presheaf of rings,
+described as a presheaf of abelian groups, and the extra data of the action at each object,
+and a condition relating functoriality and scalar multiplication. -/
+structure PresheafOfModules (R : Cᵒᵖ ⥤ RingCat.{u}) where
+  presheaf : Cᵒᵖ ⥤ AddCommGroupCat.{v}
+  module : ∀ X : Cᵒᵖ, Module (R.obj X) (presheaf.obj X)
+  map_smul : ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (r : R.obj X) (x : presheaf.obj X),
+    presheaf.map f (r • x) = R.map f r • presheaf.map f x
+
+namespace PresheafOfModules
+
+variable {R : Cᵒᵖ ⥤ RingCat.{u}}
+
+attribute [instance] PresheafOfModules.module
+
+/-- The bundled module over an object `X`. -/
+def obj (P : PresheafOfModules R) (X : Cᵒᵖ) : ModuleCat (R.obj X) :=
+  ModuleCat.of _ (P.presheaf.obj X)
+
+/--
+If `P` is a presheaf of modules over a presheaf of rings `R`, both over some category `C`,
+and `f : X ⟶ Y` is a morphism in `Cᵒᵖ`, we construct the `R.map f`-semilinear map
+from the `R.obj X`-module `P.presheaf.obj X` to the `R.obj Y`-module `P.presheaf.obj Y`.
+ -/
+def map (P : PresheafOfModules R) {X Y : Cᵒᵖ} (f : X ⟶ Y) :
+    P.obj X →ₛₗ[R.map f] P.obj Y :=
+  { toAddHom := (P.presheaf.map f).toAddHom,
+    map_smul' := P.map_smul f, }
+
+@[simp]
+theorem map_apply (P : PresheafOfModules R) {X Y : Cᵒᵖ} (f : X ⟶ Y) (x) :
+    P.map f x = (P.presheaf.map f) x :=
+  rfl
+
+instance (X : Cᵒᵖ) : RingHomId (R.map (𝟙 X)) where
+  eq_id := R.map_id X
+
+instance {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) :
+    RingHomCompTriple (R.map f) (R.map g) (R.map (f ≫ g)) where
+  comp_eq := (R.map_comp f g).symm
+
+@[simp]
+theorem map_id (P : PresheafOfModules R) (X : Cᵒᵖ) :
+    P.map (𝟙 X) = LinearMap.id' := by
+  ext
+  simp
+
+@[simp]
+theorem map_comp (P : PresheafOfModules R) {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) :
+    P.map (f ≫ g) = (P.map g).comp (P.map f) := by
+  ext
+  simp
+
+/-- A morphism of presheaves of modules. -/
+structure Hom (P Q : PresheafOfModules R) where
+  hom : P.presheaf ⟶ Q.presheaf
+  map_smul : ∀ (X : Cᵒᵖ) (r : R.obj X) (x : P.presheaf.obj X), hom.app X (r • x) = r • hom.app X x
+
+namespace Hom
+
+/-- The identity morphism on a presheaf of modules. -/
+def id (P : PresheafOfModules R) : Hom P P where
+  hom := 𝟙 _
+  map_smul _ _ _ := rfl
+
+/-- Composition of morphisms of presheaves of modules. -/
+def comp {P Q R : PresheafOfModules R} (f : Hom P Q) (g : Hom Q R) : Hom P R where
+  hom := f.hom ≫ g.hom
+  map_smul _ _ _ := by simp [Hom.map_smul]
+
+end Hom
+
+instance : Category (PresheafOfModules R) where
+  Hom := Hom
+  id := Hom.id
+  comp f g := Hom.comp f g
+
+variable {P Q : PresheafOfModules R}
+
+/--
+The `(X : Cᵒᵖ)`-component of morphism between presheaves of modules
+over a presheaf of rings `R`, as an `R.obj X`-linear map. -/
+def Hom.app (f : Hom P Q) (X : Cᵒᵖ) : P.obj X →ₗ[R.obj X] Q.obj X :=
+  { toAddHom := (f.hom.app X).toAddHom
+    map_smul' := f.map_smul X }
+
+@[ext]
+theorem Hom.ext {f g : P ⟶ Q} (w : ∀ X, f.app X = g.app X) : f = g := by
+  cases f; cases g;
+  congr
+  ext X x
+  exact LinearMap.congr_fun (w X) x
+
+/-- The functor from presheaves of modules over a specified presheaf of rings,
+to presheaves of abelian groups.
+-/
+def toPresheaf : PresheafOfModules R ⥤ (Cᵒᵖ ⥤ AddCommGroupCat) where
+  obj P := P.presheaf
+  map f := f.hom
+
+end PresheafOfModules

Mathlib/Algebra/Module/LinearMap.lean

@@ -275,6 +275,21 @@ theorem id_coe : ((LinearMap.id : M →ₗ[R] M) : M → M) = _root_.id :=
   rfl
 #align linear_map.id_coe LinearMap.id_coe
 
+/-- A generalisation of `LinearMap.id` that constructs the identity function
+as a `σ`-semilinear map for any ring homomorphism `σ` which we know is the identity. -/
+@[simps]
+def id' {σ : R →+* R} [RingHomId σ] : M →ₛₗ[σ] M where
+  toFun x := x
+  map_add' x y := rfl
+  map_smul' r x := by
+    have := (RingHomId.eq_id : σ = _)
+    subst this
+    rfl
+
+@[simp, norm_cast]
+theorem id'_coe {σ : R →+* R} [RingHomId σ] : ((id' : M →ₛₗ[σ] M) : M → M) = _root_.id :=
+  rfl
+
 end
 
 section

Mathlib/Algebra/Ring/CompTypeclasses.lean

@@ -11,6 +11,7 @@ import Mathlib.Algebra.Ring.Equiv
 # Propositional typeclasses on several ring homs
 
 This file contains three typeclasses used in the definition of (semi)linear maps:
+* `RingHomId σ`, which expresses the fact that `σ₂₃ = id`
 * `RingHomCompTriple σ₁₂ σ₂₃ σ₁₃`, which expresses the fact that `σ₂₃.comp σ₁₂ = σ₁₃`
 * `RingHomInvPair σ₁₂ σ₂₁`, which states that `σ₁₂` and `σ₂₁` are inverses of each other
 * `RingHomSurjective σ`, which states that `σ` is surjective
@@ -45,6 +46,17 @@ variable {R₁ : Type*} {R₂ : Type*} {R₃ : Type*}
 
 variable [Semiring R₁] [Semiring R₂] [Semiring R₃]
 
+/-- Class that expresses that a ring homomorphism is in fact the identity. -/
+-- This at first seems not very useful. However we need this when considering
+-- modules over some diagram in the category of rings,
+-- e.g. when defining presheaves over a presheaf of rings.
+-- See `Mathlib.Algebra.Category.ModuleCat.Presheaf`.
+class RingHomId {R : Type _} [Semiring R] (σ : R →+* R) : Prop where
+  eq_id : σ = RingHom.id R
+
+instance {R : Type _} [Semiring R] : RingHomId (RingHom.id R) where
+  eq_id := rfl
+
 /-- Class that expresses the fact that three ring homomorphisms form a composition triple. This is
 used to handle composition of semilinear maps. -/
 class RingHomCompTriple (σ₁₂ : R₁ →+* R₂) (σ₂₃ : R₂ →+* R₃) (σ₁₃ : outParam (R₁ →+* R₃)) :

Mathlib/LinearAlgebra/Charpoly/ToMatrix.lean

@@ -36,6 +36,7 @@ namespace LinearMap
 
 section Basic
 
+set_option maxHeartbeats 250000 in
 /-- `charpoly f` is the characteristic polynomial of the matrix of `f` in any basis. -/
 @[simp]
 theorem charpoly_toMatrix {ι : Type w} [DecidableEq ι] [Fintype ι] (b : Basis ι R M) :