PresheafOfModules map_smul' difficulties

Stream: mathlib4

[Raphael Douglas Giles]

Hi there,

I've been working a bit recently with presheaves of modules in mathlib and I've found that almost every time I define a presheaf of modules it is a real pain to show that scalar multiplication is respected. For example, here is a snippet from something I've been working on recently about adapting some of the work on LocalPredicates to the case of sheaves of modules:

import Mathlib

open CategoryTheory

open AlgebraicGeometry Scheme Opposite TopCat TopologicalSpace

variable {X : Scheme} (F : X.Modules)

macro:max "Γₘ("F:term","U:term")" : term =>
  `((SheafOfModules.val $F).obj (op $U))

structure LinearLocalPredicate (F : X.Modules) where
    P : {U : X.Opens} → Γₘ(F, U) → Prop
    zero {U : X.Opens} : P (0 : Γₘ(F, U))
    add {U : X.Opens} {f g : Γₘ(F, U)} (hf : P f) (hg : P g) : P (f + g)
    smul {U : X.Opens} (a : Γ(X, U)) {f : Γₘ(F, U)} (hf : P f) : P (a • f)
    res {U V : X.Opens} (k : V ≤ U) (f : Γₘ(F, U)) (hf : P f) :
      P (F.val.presheaf.map (homOfLE k).op f)
    local_prop {U : X.Opens} (f : Γₘ(F, U)) :
      (∀ x ∈ U, ∃ (V : X.Opens) (k : V ≤ U) (_ : x ∈ V), P <| F.val.presheaf.map (homOfLE k).op f)
      → P f

def submodule (F : X.Modules) (Fp : LinearLocalPredicate F) (U : X.Opens) :
    Submodule Γ(X, U) Γₘ(F, U) where
  carrier := Fp.P
  add_mem' hf hg := Fp.add hf hg
  zero_mem' := Fp.zero
  smul_mem' := Fp.smul

set_option synthInstance.maxHeartbeats 0
set_option maxHeartbeats 0
noncomputable
def presheaf (F : X.Modules) (Fp : LinearLocalPredicate F) : PresheafOfModules X.ringCatSheaf.val where
  obj U := ModuleCat.of (↑(X.ringCatSheaf.val.obj U)) (submodule F Fp (unop U))
  map := by
    intro U V l
    apply ModuleCat.ofHom (Y := (ModuleCat.restrictScalars
                (RingCat.Hom.hom (X.ringCatSheaf.val.map l))).obj
                (ModuleCat.of ↑(X.ringCatSheaf.val.obj V) ↥(submodule F Fp (unop V))))
    exact {
      toFun x := ⟨F.val.presheaf.map l x.1, Fp.res (le_of_op_hom l) x x.2⟩
      map_add' := by aesop
      map_smul' := by
        intro a x
        simp_all only [sheafCompose_obj_val, Functor.comp_obj, CommRingCat.forgetToRingCat_obj, Functor.comp_map,
          CommRingCat.forgetToRingCat_map_hom, op_unop, PresheafOfModules.presheaf_obj_coe, SetLike.val_smul,
          RingHom.id_apply]
        apply Subtype.ext
        simp [Scheme.sheaf, SheafedSpace.sheaf] at a
        let k : Algebra Γ(X, unop U) ↑Γ(X, unop V) := (X.presheaf.map l).hom.toAlgebra
        let o : Module Γ(X, unop V) (F.val.obj V) := ModuleCat.isModule (F.val.obj V)
        let p : Module Γ(X, unop U) (F.val.obj V) := RestrictScalars.module Γ(X, unop U) Γ(X, unop V) (F.val.obj V)
        let : IsScalarTower ↑(X.presheaf.obj U) ↑Γ(X, unop V) ↑(F.val.obj V) := ModuleCat.Algebra.instIsScalarTowerCarrier
        rw [Submodule.coe_smul_of_tower a (p := (submodule F Fp (unop V)))]
        simp
        have := PresheafOfModules.map_smul (F.val) l a x
        rw [← PresheafOfModules.presheaf_map_apply_coe, ← PresheafOfModules.presheaf_map_apply_coe] at this
        convert this
    }

The map_smul' definition should be as trivial as the map_add' definition, but as you can see I've had help the typeclass inference system along quite a bit. The resulting code is also extremely slow; I've had to set the max heartbeats to 0 for this definition to run. Does anyone know of a better way to show that scalar multiplication is preserved?

[Andrew Yang]

I think docs#PresheafOfModules.ofPresheaf is designed for this. In particular,

set_option synthInstance.maxHeartbeats 0 in
noncomputable
def presheafAb (F : X.Modules) (Fp : LinearLocalPredicate F) : X.Opensᵒᵖ ⥤ Ab where
  obj U := .of (submodule F Fp (unop U))
  map {U V} l := AddCommGrp.ofHom
    { toFun x := ⟨F.val.presheaf.map l x.1, Fp.res (le_of_op_hom l) x x.2⟩
      map_zero' := by aesop
      map_add' := by aesop }
  map_comp {U V W} f g := by sorry

instance (F : X.Modules) (Fp : LinearLocalPredicate F) {U} :
    Module (X.ringCatSheaf.val.obj U) ((presheafAb F Fp).obj U) :=
  inferInstanceAs (Module Γ(X, U.unop) (submodule F Fp _))

noncomputable
def presheaf (F : X.Modules) (Fp : LinearLocalPredicate F) : PresheafOfModules X.ringCatSheaf.val :=
  .ofPresheaf (presheafAb F Fp) fun {_ _} f r x ↦ Subtype.ext (F.val.map_smul f r x.1)

[Andrew Yang]

And you can remove the max heartbeat by attribute [instance 1100] AddCommMonoid.toAddMonoid but this is probably more of a hack than a solution.

[Raphael Douglas Giles]

Ahh interesting, thanks for that that seems much better. The docs (docs#PresheafOfModules.ofPresheaf) seem to discourage use of ofPresheaf in favour of PresheafOfModules.mk, do you know why that is?

[Joël Riou]

The basic preferred API involves bundled objects in ModuleCat (R.obj X) for all X and "restriction" maps involve restriction of scalars functors. Then, if we can use mk directly, it is better, but if the obj fields are given as ModuleCat.of ..., it is certainly more convenient to use mk'.

[Andrew Yang]

I would like to hijack this thread to discuss about the design decisions about PresheafOfModules. In particular I think the fact that M.map i x does not have type M.obj U for some U (only semireducibly defeq to one) is quite annoying, causes erws, and also clogs the infoview. It is also hard to apply results about sheaves to a "dependent type sheaf" like M.
The current definition has its benefits, as can clearly be seen from the abundance of results already established about them, and I am not proposing we change the definition. But I think at some boundary we should have better API to hide this away from end users.
Currently my plan is to put the API boundary on Scheme.Modules, and only upstream to PresheafOfModules when there is practical evidence that this is useful. There are three options that I can come up with:

1. Define Γ(M, U) as notation for M.presheaf.obj (op U), a type of Ab (AddCommGrpCat). The restriction maps are Γ(M, U) ⟶ Γ(M, V) (in Ab), with a lemma saying M.map i (r • x) = X.presheaf.map i r • M.map i x. This removes the defeq abuse with Module.restrictScalars and makes the infoview much cleaner, but the down side is that it is a weird mix between bundled and unbundled. This is the easiest to achieve and is what I tried in #31854.

2. Define Γ(M, U) as notation for (↥M.obj (op U) : Type u). The restriction maps are Γ(M, U) →ₛₗ[X.presheaf.map i] Γ(M, V). I haven't given this much thought because this doesn't seem like a good idea but I'm including it here in case someone thinks otherwise.

3. Define Γ(M, U) to be in the (yet to be implemented) category of RingMod. RingMod is the concrete category whose objects are (R, M) with R a ring and M an R module, and the homs are pairs of a ring hom and a semilinear map. There was this idea to idea to define a PresheafOfModules to be a presheaf valued in RingMod whose projection to RingCat is isomorphic to the given sheaf but this iso is clearly annoying to work with. But here if we build the Sheaf RingMod ad-hoc, we can make the first projection defeq to the sheaf of rings and this annoying iso goes away. In particular restriction maps are still Γ(M, U) ⟶ Γ(M, V) but it bundles the semilinearity and things might work better etc. But this still requires using defeq in some way and I am not sure if this is better.

cc @Christian Merten @Joël Riou , and also @Kim Morrison who I think expressed a desire to get rid of the defeq abuse as well?

[Joël Riou]

I am very much ok for introducing API separation to improve the usability of the API for modules on schemes by trying 1.
However, but this should not be upstreamed to the general SheafOfModules API: 1. was the design for (pre)sheaves of modules before my refactor PR #16667 which improved significantly automation (in particular, less erw...).