Documentation

TauCeti.AlgebraicGeometry.Cohomology.Biproduct

Cohomology of finite direct sums of sheaves of modules #

Sheaf cohomology is an additive functor of the coefficient sheaf, so it commutes with finite direct sums. For a scheme X over a commutative ring R this file records that commutation as an R-linear equivalence

Hⁱ(X, ⨁ⱼ Mⱼ) ≃ₗ[R] ∀ j, Hⁱ(X, Mⱼ),

whose components are the maps induced by the projections of the biproduct. Mathlib's CategoryTheory.Functor.mapBiproduct gives the additive version of this commutation; the point here is linearity over the base ring, which the dimension counts below need. For a direct sum of |I| copies of one sheaf M over a field it gives dim Hⁱ(X, ⨁_{I} M) = |I| · dim Hⁱ(X, M), and hence χ(X, ⨁_{I} M) = |I| · χ(X, M) for the truncated Euler characteristic Scheme.Modules.eulerCharBelow. For M = 𝒪_X this computes, through TauCeti.SheafOfModules.biproductIsoFree, the Euler characteristic of the free sheaf 𝒪_X^I, a trivial vector bundle. These counts hold with no finiteness hypothesis on Hⁱ(X, M), since Module.finrank takes the value 0 on both sides when Hⁱ(X, M) is infinite-dimensional and I is nonempty.

Main declarations #

source
noncomputable def AlgebraicGeometry.Scheme.Modules.cohomologyBiproductLinearEquiv (R : Type u) [CommRing R] {X : Scheme} [X.Over (Spec ↧R)] {J : Type u_1} [Fintype J] (F : J → X.Modules) [CategoryTheory.Limits.HasBiproduct F] (i : ℕ) :
TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology (⨁ F) i ≃ₗ[R] (j : J) → TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology (F j) i

Cohomology commutes with finite direct sums. For a finite family of sheaves of modules Mⱼ on a scheme over a commutative ring R, the maps induced by the projections of the biproduct give an R-linear equivalence Hⁱ(X, ⨁ⱼ Mⱼ) ≃ₗ[R] ∀ j, Hⁱ(X, Mⱼ).

Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Modules.cohomologyBiproductLinearEquiv_apply (R : Type u) [CommRing R] {X : Scheme} [X.Over (Spec ↧R)] {J : Type u_1} [Fintype J] (F : J → X.Modules) [CategoryTheory.Limits.HasBiproduct F] (i : ℕ) (x : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology (⨁ F) i) (j : J) :
    (cohomologyBiproductLinearEquiv R F i) x j = (cohomologyMapBaseLinear R X (CategoryTheory.Limits.biproduct.π F j) i) x

    The j-th component of cohomologyBiproductLinearEquiv is the map on cohomology induced by the j-th projection of the biproduct.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Modules.cohomologyBiproductLinearEquiv_symm_apply (R : Type u) [CommRing R] {X : Scheme} [X.Over (Spec ↧R)] {J : Type u_1} [Fintype J] (F : J → X.Modules) [CategoryTheory.Limits.HasBiproduct F] (i : ℕ) (v : (j : J) → TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology (F j) i) :
    (cohomologyBiproductLinearEquiv R F i).symm v = ∑ j : J, (cohomologyMapBaseLinear R X (CategoryTheory.Limits.biproduct.ι F j) i) (v j)

    The inverse of cohomologyBiproductLinearEquiv sums the maps on cohomology induced by the inclusions of the summands.

    source
    theorem AlgebraicGeometry.Scheme.Modules.finrank_cohomology_biproduct_const {X : Scheme} (k : Type u) [Field k] [X.Over (Spec ↧k)] (M : X.Modules) (I : Type u_2) [Fintype I] [CategoryTheory.Limits.HasBiproduct fun (x : I) => M] (i : ℕ) :
    Module.finrank k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology (⨁ fun (x : I) => M) i) = Fintype.card I * Module.finrank k (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M i)

    Dimension of the cohomology of a finite direct sum of copies of a sheaf. Over a field k, dim Hⁱ(X, ⨁_{I} M) = |I| · dim Hⁱ(X, M) for every finite type I. No finiteness of Hⁱ(X, M) is needed: when it is infinite-dimensional and I is nonempty both sides are 0. Applied to M = 𝒪_X, this computes the cohomology of the free sheaf 𝒪_X^I.

    source
    theorem AlgebraicGeometry.Scheme.Modules.eulerCharBelow_biproduct_const {X : Scheme} (k : Type u) [Field k] [X.Over (Spec ↧k)] (M : X.Modules) (I : Type u_2) [Fintype I] [CategoryTheory.Limits.HasBiproduct fun (x : I) => M] (n : ℕ) :
    eulerCharBelow k X (⨁ fun (x : I) => M) n = ↑(Fintype.card I) * eulerCharBelow k X M n

    The truncated Euler characteristic of a finite direct sum of copies of a sheaf: χ(X, ⨁_{I} M) = |I| · χ(X, M), with no finiteness hypothesis.

    source
    theorem AlgebraicGeometry.Scheme.Modules.eulerCharBelow_free (X : Scheme) (k : Type u) [Field k] [X.Over (Spec ↧k)] (I : Type u) [Fintype I] (n : ℕ) :
    eulerCharBelow k X (SheafOfModules.free I) n = ↑(Fintype.card I) * eulerCharBelow k X (SheafOfModules.unit X.ringCatSheaf) n

    The truncated Euler characteristic of the free sheaf on a finite type: χ(X, 𝒪_X^I) = |I| · χ(X, 𝒪_X), with no finiteness hypothesis.