Documentation

TauCeti.AlgebraicGeometry.Cohomology.Module.Basic

Scalar actions on the cohomology of a sheaf of modules on a scheme #

This file equips the cohomology of a sheaf of modules on a scheme with its canonical module structure over the ring of global functions. The construction first realizes a global function as a scalar endomorphism of the coefficient sheaf, then applies the cohomology functor. No coherence or quasi-coherence hypothesis is imposed on the coefficient sheaf.

The resulting action agrees in degree zero with the usual action on global sections, and every map on cohomology induced by a morphism of coefficient sheaves is linear. For a scheme over a base commutative ring, TauCeti.AlgebraicGeometry.Cohomology.Module.Base restricts these actions along the induced map on global functions to actions of the base ring.

source
noncomputable def AlgebraicGeometry.Scheme.Modules.cohomologyAction {X : Scheme} (M : X.Modules) (i : ℕ) :
↑(X.presheaf.obj (Opposite.op ⊤)) →+* AddMonoid.End (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M i)

The action of global functions on cohomology, bundled as a ring homomorphism into additive endomorphisms.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Modules.cohomologyAction_apply {X : Scheme} (M : X.Modules) (i : ℕ) (r : ↑(X.presheaf.obj (Opposite.op ⊤))) (x : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M i) :
    ((M.cohomologyAction i) r) x = (CategoryTheory.ConcreteCategory.hom ((TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyFunctor X i).map (M.globalSectionsSmul r))) x
    source
    @[instance_reducible]
    noncomputable instance AlgebraicGeometry.Scheme.Modules.cohomologyModule {X : Scheme} (M : X.Modules) (i : ℕ) :
    Module (↑(X.presheaf.obj (Opposite.op ⊤))) (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M i)

    Cohomology is canonically a module over the ring of global functions.

    Equations
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Modules.cohomology_smul {X : Scheme} (M : X.Modules) (i : ℕ) (r : ↑(X.presheaf.obj (Opposite.op ⊤))) (x : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M i) :
    r • x = (CategoryTheory.ConcreteCategory.hom ((TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyFunctor X i).map (M.globalSectionsSmul r))) x

    Scalar multiplication on cohomology is induced by the cohomology map of the corresponding scalar endomorphism of the coefficient sheaf.

    source
    noncomputable def AlgebraicGeometry.Scheme.Modules.cohomologyMapLinear {X : Scheme} {M N : X.Modules} (f : M ⟶ N) (i : ℕ) :
    TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M i →ₗ[↑(X.presheaf.obj (Opposite.op ⊤))] TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology N i

    The map on cohomology induced by a morphism of coefficient sheaves is linear over global functions.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.Modules.cohomologyMapLinear_apply {X : Scheme} {M N : X.Modules} (f : M ⟶ N) (i : ℕ) (x : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M i) :
      (cohomologyMapLinear f i) x = (CategoryTheory.ConcreteCategory.hom ((TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyFunctor X i).map f)) x
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.Modules.cohomologyMapLinear_id {X : Scheme} (M : X.Modules) (i : ℕ) :
      cohomologyMapLinear (CategoryTheory.CategoryStruct.id M) i = LinearMap.id
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.Modules.cohomologyMapLinear_comp {X : Scheme} {M N P : X.Modules} (f : M ⟶ N) (g : N ⟶ P) (i : ℕ) :
      cohomologyMapLinear (CategoryTheory.CategoryStruct.comp f g) i = cohomologyMapLinear g i ∘ₗ cohomologyMapLinear f i
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.Modules.cohomologyMapLinear_zero {X : Scheme} (M N : X.Modules) (i : ℕ) :
      cohomologyMapLinear 0 i = 0
      source
      @[simp]
      theorem AlgebraicGeometry.Scheme.Modules.cohomologyMapLinear_add {X : Scheme} {M N : X.Modules} (f g : M ⟶ N) (i : ℕ) :
      cohomologyMapLinear (f + g) i = cohomologyMapLinear f i + cohomologyMapLinear g i
      source
      noncomputable def AlgebraicGeometry.Scheme.Modules.cohomologyZeroLinearEquiv {X : Scheme} (M : X.Modules) :
      TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M 0 ≃ₗ[↑(X.presheaf.obj (Opposite.op ⊤))] ↑(M.presheaf.obj (Opposite.op ⊤))

      The canonical identification of zeroth cohomology with global sections is linear over global functions.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem AlgebraicGeometry.Scheme.Modules.cohomologyZeroLinearEquiv_apply {X : Scheme} (M : X.Modules) (x : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M 0) :
        M.cohomologyZeroLinearEquiv x = (TauCeti.AlgebraicGeometry.Scheme.Modules.cohomologyZeroEquiv M) x