Restricting a section of a module sheaf

Four facts about M.presheaf.map on a scheme, each one or two lines and each stated at the generality it actually has: any scheme, any X.Modules. Nothing here mentions Proj, a grading, or quasi-coherence.

Why they are named at all

They are the kind of step a proof takes without comment until it takes it forty times. The #585 glue composes restrictions constantly, and rw cannot be used on goals carrying show-ascription residue, so each composition has to be available as a term. presheaf_map_square_eq has the same origin on the coherence side: in a clean context its rewrites fire, while at the use site the goal carries a transparency defect and only exact works.

Why they are here rather than where they were first needed

#824. resSection_trans, resSection_smul and homApp_res were stated inside Proj/Modules/Glue.lean; presheaf_map_square_eq was in the former Modules/Coherent/Pushforward/BaseChange.lean. Each was placed with its first consumer. The open-square comparison now lives in Modules/Pushforward/BaseChange.lean. Three of the four were then stated over Proj 𝒜 despite the proofs never using the grading — resSection_smul is Scheme.Modules.map_smul verbatim — so another lane would have re-proved them rather than found them.

theorem AlgebraicGeometry.Scheme.Modules.resSection_trans {X : Scheme} (F : X.Modules) {U V W : X.Opens} (h₁ : V ≤ U) (h₂ : W ≤ V) (x : ↑(F.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (F.presheaf.map (CategoryTheory.homOfLE h₂).op)) ((CategoryTheory.ConcreteCategory.hom (F.presheaf.map (CategoryTheory.homOfLE h₁).op)) x) = (CategoryTheory.ConcreteCategory.hom (F.presheaf.map (CategoryTheory.homOfLE ⋯).op)) x

Restriction composes.

theorem AlgebraicGeometry.Scheme.Modules.resSection_smul {X : Scheme} (F : X.Modules) {U V : X.Opens} (h : V ≤ U) (r : ↑(X.presheaf.obj (Opposite.op U))) (x : ↑(F.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (F.presheaf.map (CategoryTheory.homOfLE h).op)) (r • x) = (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE h).op)) r • (CategoryTheory.ConcreteCategory.hom (F.presheaf.map (CategoryTheory.homOfLE h).op)) x

Restriction is semilinear over restriction of scalars.

theorem AlgebraicGeometry.Scheme.Modules.homApp_res {X : Scheme} {M N : X.Modules} (φ : M ⟶ N) {U V : X.Opens} (h : V ≤ U) (x : ↑(M.presheaf.obj (Opposite.op U))) : (CategoryTheory.ConcreteCategory.hom (N.presheaf.map (CategoryTheory.homOfLE h).op)) ((CategoryTheory.ConcreteCategory.hom (Hom.app φ U)) x) = (CategoryTheory.ConcreteCategory.hom (Hom.app φ V)) ((CategoryTheory.ConcreteCategory.hom (M.presheaf.map (CategoryTheory.homOfLE h).op)) x)

A morphism of module sheaves commutes with restriction.

theorem AlgebraicGeometry.Scheme.Modules.presheaf_map_square_eq {X : Scheme} (M : X.Modules) {A B C D : X.Opens} (α : Opposite.op A ⟶ Opposite.op B) (β : Opposite.op B ⟶ Opposite.op C) (γ : Opposite.op A ⟶ Opposite.op D) (δ : Opposite.op D ⟶ Opposite.op C) (x : ↑(M.presheaf.obj (Opposite.op A))) : (AddCommGrpCat.Hom.hom (M.presheaf.map β)) ((AddCommGrpCat.Hom.hom (M.presheaf.map α)) x) = (AddCommGrpCat.Hom.hom (M.presheaf.map δ)) ((AddCommGrpCat.Hom.hom (M.presheaf.map γ)) x)

Any two ways round a square of restrictions agree.

Opens is a poset, so the two composites are M.presheaf.map of parallel morphisms and Subsingleton.elim settles it.