Documentation

TauCeti.AlgebraicGeometry.Cohomology.Module.Base

Base-ring actions on the cohomology of a sheaf of modules on a scheme #

For a scheme over a base commutative ring, restricting the global-functions actions of TauCeti.AlgebraicGeometry.Cohomology.Module.Basic along the induced map on global functions gives the corresponding actions of the base ring: the module structure on cohomology, the linearity of the maps induced by morphisms of coefficient sheaves, and the degree-zero identification with global sections.

The base-ring statements live in their own file, rather than alongside the global-functions ones, to keep each file's kernel-checking time inside the CI per-file budget: every declaration here re-checks the full CategoryTheory.Sheaf.H instance terms, which is expensive.

source
@[instance_reducible, instance 900]
noncomputable instance AlgebraicGeometry.Scheme.Modules.cohomologyBaseModule (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] (M : X.Modules) (i : ℕ) :
Module R (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M i)

Cohomology of a scheme over a commutative ring is a module over the base ring. As for globalSectionsBaseModule, the priority is below the default so that cohomologyModule, the canonical action of Γ(X, ⊤), is still the one found when the base ring is the ring of global functions itself.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem AlgebraicGeometry.Scheme.Modules.base_smul_cohomology (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] (M : X.Modules) (i : ℕ) (r : R) (x : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M i) :
r • x = (baseRingToGlobalSections R X) r • x
source
noncomputable def AlgebraicGeometry.Scheme.Modules.cohomologyMapBaseLinear (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] {M N : X.Modules} (f : M ⟶ N) (i : ℕ) :
TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M i →ₗ[R] TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology N i

The map on cohomology induced by a morphism of coefficient sheaves on a scheme over a commutative ring is linear over the base ring.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Modules.cohomologyMapBaseLinear_apply (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] {M N : X.Modules} (f : M ⟶ N) (i : ℕ) (x : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M i) :
    (cohomologyMapBaseLinear R X f i) x = (CategoryTheory.ConcreteCategory.hom ((TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyFunctor X i).map f)) x
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Modules.cohomologyMapBaseLinear_id (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] (M : X.Modules) (i : ℕ) :
    cohomologyMapBaseLinear R X (CategoryTheory.CategoryStruct.id M) i = LinearMap.id
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Modules.cohomologyMapBaseLinear_comp (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] {M N P : X.Modules} (f : M ⟶ N) (g : N ⟶ P) (i : ℕ) :
    cohomologyMapBaseLinear R X (CategoryTheory.CategoryStruct.comp f g) i = cohomologyMapBaseLinear R X g i ∘ₗ cohomologyMapBaseLinear R X f i
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Modules.cohomologyMapBaseLinear_zero (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] (M N : X.Modules) (i : ℕ) :
    cohomologyMapBaseLinear R X 0 i = 0
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Modules.cohomologyMapBaseLinear_add (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] {M N : X.Modules} (f g : M ⟶ N) (i : ℕ) :
    cohomologyMapBaseLinear R X (f + g) i = cohomologyMapBaseLinear R X f i + cohomologyMapBaseLinear R X g i
    source
    noncomputable def AlgebraicGeometry.Scheme.Modules.cohomologyZeroBaseLinearEquiv (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] (M : X.Modules) :
    TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M 0 ≃ₗ[R] ↑(M.presheaf.obj (Opposite.op ⊤))

    For a scheme over a commutative ring, the canonical identification of zeroth cohomology with global sections is linear over the base ring.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.Modules.cohomologyZeroBaseLinearEquiv_apply (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] (M : X.Modules) (x : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M 0) :
      (cohomologyZeroBaseLinearEquiv R X M) x = (TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyZeroEquiv M) x
      source
      theorem AlgebraicGeometry.Scheme.Modules.cohomologyZeroBaseLinearEquiv_naturality (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] {M N : X.Modules} (f : M ⟶ N) (x : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M 0) :
      (cohomologyZeroBaseLinearEquiv R X N) ((cohomologyMapBaseLinear R X f 0) x) = (CategoryTheory.ConcreteCategory.hom (Hom.app f ⊤)) ((cohomologyZeroBaseLinearEquiv R X M) x)

      The base-linear identification of degree-zero cohomology with global sections is natural in the coefficient sheaf: it carries the degree-zero cohomology map of f to the global-sections map of f.