Documentation

TauCeti.AlgebraicGeometry.Modules.GlobalSections

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. It also records the restriction of this action to the base ring for a scheme over a commutative ring.

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

source
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.
Instances For
    source
    @[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)
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Modules.globalSectionsSmul_zero {X : Scheme} (M : X.Modules) :
    M.globalSectionsSmul 0 = 0
    source
    @[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
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Modules.globalSectionsSmul_one {X : Scheme} (M : X.Modules) :
    M.globalSectionsSmul 1 = CategoryTheory.CategoryStruct.id M
    source
    @[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)
    source
    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
    Instances For
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.Modules.globalSectionsAction_apply {X : Scheme} (M : X.Modules) (r : ↑(X.presheaf.obj (Opposite.op ⊤))) :
      M.globalSectionsAction r = M.globalSectionsSmul r
      source
      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.

      source
      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.

      source
      noncomputable def AlgebraicGeometry.Scheme.Modules.baseRingToGlobalSections (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec (CommRingCat.of 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.
      Instances For
        source
        @[simp]
        theorem AlgebraicGeometry.Scheme.Modules.baseRingToGlobalSections_apply (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec (CommRingCat.of R))] (r : R) :
        (baseRingToGlobalSections R X) r = (CategoryTheory.ConcreteCategory.hom (Hom.appTop (X ↘ Spec (CommRingCat.of R)))) ((CategoryTheory.ConcreteCategory.hom (ΓSpecIso (CommRingCat.of 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.

        source
        @[instance_reducible, instance 900]
        noncomputable instance AlgebraicGeometry.Scheme.Modules.globalSectionsBaseModule (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec (CommRingCat.of 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
        source
        @[simp]
        theorem AlgebraicGeometry.Scheme.Modules.base_smul_globalSections (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec (CommRingCat.of R))] (M : X.Modules) (r : R) (x : ↑(M.presheaf.obj (Opposite.op ⊤))) :
        r • x = (baseRingToGlobalSections R X) r • x