Documentation

TauCeti.AlgebraicGeometry.Cohomology.Trivial

Cohomology of the trivial line bundle and the structure sheaf #

The trivial line bundle is constructed as the free sheaf on one generator. This file records the canonical base-linear comparison between its cohomology and the cohomology of the structure sheaf, and shows that on a nonempty scheme H⁰(X, 𝒪_X) has rank one over the global functions (AlgebraicGeometry.Scheme.Modules.finrank_globalSections_cohomology_zero_trivial_eq_one).

source
noncomputable def AlgebraicGeometry.Scheme.Modules.trivialCohomologyBaseLinearEquiv (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] (i : ℕ) :
have M := SheafOfModules.unit X.ringCatSheaf; TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology (TauCeti.AlgebraicGeometry.InvertibleSheaf.trivial X).obj i ≃ₗ[R] TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M i

The cohomology of the trivial line bundle is base-linearly equivalent to that of the structure sheaf.

Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Modules.trivialCohomologyBaseLinearEquiv_apply (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] (i : ℕ) (x : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology (TauCeti.AlgebraicGeometry.InvertibleSheaf.trivial X).obj i) :
    (trivialCohomologyBaseLinearEquiv R X i) x = (cohomologyMapBaseLinear R X (TauCeti.AlgebraicGeometry.InvertibleSheaf.trivialObjIsoUnit X).hom i) x
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Modules.trivialCohomologyBaseLinearEquiv_symm_apply (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] (i : ℕ) (x : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology (SheafOfModules.unit X.ringCatSheaf) i) :
    (LinearEquiv.symm (trivialCohomologyBaseLinearEquiv R X i)) x = (cohomologyMapBaseLinear R X (TauCeti.AlgebraicGeometry.InvertibleSheaf.trivialObjIsoUnit X).inv i) x
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Modules.finrank_globalSections_cohomology_zero_trivial_eq_one {X : Scheme} [Nonempty ↥X] :
    Module.finrank (↑(X.presheaf.obj (Opposite.op ⊤))) (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology (TauCeti.AlgebraicGeometry.InvertibleSheaf.trivial X).obj 0) = 1

    On a nonempty scheme, H⁰(X, 𝒪_X) is free of rank one over the ring Γ(X, 𝒪_X) of global functions: it is identified with Γ(X, 𝒪_X) itself.