Global-functions actions on sheaves of modules

This file constructs the canonical action of the ring of global functions on a sheaf of modules on a scheme, shows that multiplication by a global unit is an isomorphism, and records how the action is carried along a morphism of schemes f : X ⟶ Y: pushing forward multiplication by f^♯ r is multiplication by r, and pulling back multiplication by r is multiplication by f^♯ r (Scheme.Modules.pushforward_map_globalSectionsSmul and Scheme.Modules.pullback_map_globalSectionsSmul). It also records the restriction of this action to the base ring for a scheme over a commutative ring, and the morphism Scheme.baseRingToStructurePresheaf from the constant presheaf of the base ring to the structure presheaf. Pullback of local functions by a morphism over the base preserves these images (AlgebraicGeometry.Scheme.Modules.app_baseRingToStructurePresheaf).

These constructions are independent of sheaf cohomology. They supply the scalar actions used by TauCeti.AlgebraicGeometry.Cohomology.Module.Basic.

def AlgebraicGeometry.Scheme.Modules.globalSectionsSmul {X : Scheme} (M : X.Modules) (r : ↑(X.presheaf.obj (Opposite.op ⊤))) : M ⟶ M

Multiplication by a global function, as a morphism of sheaves of modules.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.globalSectionsSmul_app {X : Scheme} (M : X.Modules) (r : ↑(X.presheaf.obj (Opposite.op ⊤))) (U : X.Opens) : Hom.app (M.globalSectionsSmul r) U = smul ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map (TopologicalSpace.Opens.leTop U).op)) r)

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.globalSectionsSmul_zero {X : Scheme} (M : X.Modules) : M.globalSectionsSmul 0 = 0

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.globalSectionsSmul_add {X : Scheme} (M : X.Modules) (r s : ↑(X.presheaf.obj (Opposite.op ⊤))) : M.globalSectionsSmul (r + s) = M.globalSectionsSmul r + M.globalSectionsSmul s

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.globalSectionsSmul_one {X : Scheme} (M : X.Modules) : M.globalSectionsSmul 1 = CategoryTheory.CategoryStruct.id M

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.globalSectionsSmul_mul {X : Scheme} (M : X.Modules) (r s : ↑(X.presheaf.obj (Opposite.op ⊤))) : M.globalSectionsSmul (r * s) = CategoryTheory.CategoryStruct.comp (M.globalSectionsSmul s) (M.globalSectionsSmul r)

instance AlgebraicGeometry.Scheme.Modules.isIso_globalSectionsSmul_units {X : Scheme} (M : X.Modules) (u : (↑(X.presheaf.obj (Opposite.op ⊤)))ˣ) : CategoryTheory.IsIso (M.globalSectionsSmul ↑u)

Multiplication by a global unit is an isomorphism, with inverse multiplication by the inverse unit.

def AlgebraicGeometry.Scheme.Modules.globalSectionsAction {X : Scheme} (M : X.Modules) : ↑(X.presheaf.obj (Opposite.op ⊤)) →+* CategoryTheory.End M

The action of global functions on a sheaf of modules, bundled as a ring homomorphism into the endomorphism ring of the sheaf.

Equations

• M.globalSectionsAction = { toFun := M.globalSectionsSmul, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.globalSectionsAction_apply {X : Scheme} (M : X.Modules) (r : ↑(X.presheaf.obj (Opposite.op ⊤))) : M.globalSectionsAction r = M.globalSectionsSmul r

theorem AlgebraicGeometry.Scheme.Modules.globalSectionsSmul_naturality {X : Scheme} {M N : X.Modules} (f : M ⟶ N) (r : ↑(X.presheaf.obj (Opposite.op ⊤))) : CategoryTheory.CategoryStruct.comp (M.globalSectionsSmul r) f = CategoryTheory.CategoryStruct.comp f (N.globalSectionsSmul r)

Multiplication by a global function is natural in the sheaf of modules.

theorem AlgebraicGeometry.Scheme.Modules.globalSectionsSmul_naturality_assoc {X : Scheme} {M N : X.Modules} (f : M ⟶ N) (r : ↑(X.presheaf.obj (Opposite.op ⊤))) {Z : X.Modules} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp (M.globalSectionsSmul r) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (N.globalSectionsSmul r) h)

Multiplication by a global function is natural in the sheaf of modules.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pushforward_map_globalSectionsSmul {X Y : Scheme} (f : X ⟶ Y) (N : X.Modules) (r : ↑(Y.presheaf.obj (Opposite.op ⊤))) : (pushforward f).map (N.globalSectionsSmul ((CategoryTheory.ConcreteCategory.hom (Hom.appTop f)) r)) = ((pushforward f).obj N).globalSectionsSmul r

Pushing forward multiplication by the pullback f^♯ r of a global function r on Y gives multiplication by r on the pushforward.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.pullback_map_globalSectionsSmul {X Y : Scheme} (f : X ⟶ Y) (M : Y.Modules) (r : ↑(Y.presheaf.obj (Opposite.op ⊤))) : (pullback f).map (M.globalSectionsSmul r) = ((pullback f).obj M).globalSectionsSmul ((CategoryTheory.ConcreteCategory.hom (Hom.appTop f)) r)

Pulling back multiplication by a global function r on Y gives multiplication by the pullback f^♯ r of r on the pullback.

noncomputable def AlgebraicGeometry.Scheme.Modules.baseRingToGlobalSections (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] : R →+* ↑(X.presheaf.obj (Opposite.op ⊤))

The homomorphism from the base ring to global functions on a scheme over that ring.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.baseRingToGlobalSections_apply (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] (r : R) : (baseRingToGlobalSections R X) r = (CategoryTheory.ConcreteCategory.hom (Hom.appTop (X ↘ Spec ↧R))) ((CategoryTheory.ConcreteCategory.hom (ΓSpecIso ↧R).inv) r)

The base ring acts through the pullback along the structure morphism: r is sent to the global function obtained by pulling back the function on Spec R corresponding to r.

noncomputable def AlgebraicGeometry.Scheme.baseRingToStructurePresheaf (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] : (CategoryTheory.Functor.const X.Opensᵒᵖ).obj ↧R ⟶ X.presheaf

The morphism from the constant presheaf of rings R to the structure presheaf of a scheme over R: on an open U it is the base ring map to global functions followed by restriction to U.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.baseRingToStructurePresheaf_app (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] (U : X.Opensᵒᵖ) : (baseRingToStructurePresheaf R X).app U = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (Modules.baseRingToGlobalSections R X)) (X.presheaf.map (TopologicalSpace.Opens.leTop (Opposite.unop U)).op)

On an open U, the base ring maps to sections over U through global functions followed by restriction to U.

theorem AlgebraicGeometry.Scheme.baseRingToStructurePresheaf_app_eq_appLE (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] (U : X.Opens) : (baseRingToStructurePresheaf R X).app (Opposite.op U) = CategoryTheory.CategoryStruct.comp (ΓSpecIso ↧R).inv (Hom.appLE (X ↘ Spec ↧R) ⊤ U ⋯)

On an open U, the base-ring map R → Γ(X, U) is the composite of R ≅ Γ(Spec R, ⊤) with the map on functions induced by the structure morphism.

theorem AlgebraicGeometry.Scheme.Modules.app_baseRingToStructurePresheaf (R : Type u) [CommRing R] {X : Scheme} [X.Over (Spec ↧R)] {Y : Scheme} [Y.Over (Spec ↧R)] (f : X ⟶ Y) [Hom.IsOver f (Spec ↧R)] (U : Y.Opens) (r : R) : (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.app f U)) ((CategoryTheory.ConcreteCategory.hom ((baseRingToStructurePresheaf R Y).app (Opposite.op U))) r) = (CategoryTheory.ConcreteCategory.hom ((baseRingToStructurePresheaf R X).app (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)))) r

Pullback of local functions along a morphism over Spec R preserves the image of the base ring.

@[instance_reducible, instance 900]

noncomputable instance AlgebraicGeometry.Scheme.Modules.globalSectionsBaseModule (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] (M : X.Modules) : Module R ↑(M.presheaf.obj (Opposite.op ⊤))

Global sections of a sheaf of modules on a scheme over a commutative ring form a module over the base ring. The priority is below the default so that the canonical action of Γ(X, ⊤) is still the one found when the base ring is the ring of global functions itself.

Equations

• AlgebraicGeometry.Scheme.Modules.globalSectionsBaseModule R X M = Module.compHom (↑(M.presheaf.obj (Opposite.op ⊤))) (AlgebraicGeometry.Scheme.Modules.baseRingToGlobalSections R X)

@[simp]

theorem AlgebraicGeometry.Scheme.Modules.base_smul_globalSections (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] (M : X.Modules) (r : R) (x : ↑(M.presheaf.obj (Opposite.op ⊤))) : r • x = (baseRingToGlobalSections R X) r • x