Documentation

TauCeti.AlgebraicGeometry.Cohomology.ClosedImmersion.Linear

Linear cohomology comparison for closed immersions #

For a closed immersion f : X ⟶ Y, the cohomology comparison Hⁿ(Y, f_* M) ≅ Hⁿ(X, M) respects global functions: a scalar r on Y acts on the right through its pullback f^♯ r. When f is a morphism over a commutative ring R, the comparison is therefore R-linear, naturally in the coefficient sheaf M.

Over a field, this preserves cohomology dimensions and truncated Euler characteristics. In particular, finite-dimensionality may be proved on an ambient projective scheme and transferred to a closed subscheme. These comparisons impose no coherence, Noetherianity, or properness assumptions on the schemes or coefficient sheaves.

If the source is finite over the field, the truncated Euler characteristic of the pushed-forward structure sheaf is the rank of the source over the field (Scheme.Hom.eulerCharBelow_pushforward_structureSheaf).

References #

source
theorem AlgebraicGeometry.Scheme.Hom.cohomologyPushforwardIso_hom_smul {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] (M : X.Modules) (n : ℕ) (r : ↑(Y.presheaf.obj (Opposite.op ⊤))) (x : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology ((Modules.pushforward f).obj M) n) :
(CategoryTheory.ConcreteCategory.hom (TauCeti.AlgebraicGeometry.cohomologyPushforwardIso f M n).hom) (r • x) = (CategoryTheory.ConcreteCategory.hom (appTop f)) r • (CategoryTheory.ConcreteCategory.hom (TauCeti.AlgebraicGeometry.cohomologyPushforwardIso f M n).hom) x

The closed-immersion cohomology comparison carries the action of a global function on the ambient scheme to the action of its pullback on the closed subscheme.

source
noncomputable def AlgebraicGeometry.Scheme.Hom.cohomologyPushforwardBaseLinearEquiv {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] (R : Type u) [CommRing R] [X.Over (Spec ↧R)] [Y.Over (Spec ↧R)] [IsOver f (Spec ↧R)] (M : X.Modules) (n : ℕ) :
TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology ((Modules.pushforward f).obj M) n ≃ₗ[R] TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M n

Direct image along a closed immersion over R preserves cohomology as an R-module. The underlying additive equivalence is the closed-immersion cohomology comparison.

Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Hom.cohomologyPushforwardBaseLinearEquiv_apply {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] (R : Type u) [CommRing R] [X.Over (Spec ↧R)] [Y.Over (Spec ↧R)] [IsOver f (Spec ↧R)] (M : X.Modules) (n : ℕ) (x : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology ((Modules.pushforward f).obj M) n) :
    (cohomologyPushforwardBaseLinearEquiv f R M n) x = (CategoryTheory.ConcreteCategory.hom (TauCeti.AlgebraicGeometry.cohomologyPushforwardIso f M n).hom) x

    The linear comparison has the same forward map as the additive comparison.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Hom.cohomologyPushforwardBaseLinearEquiv_symm_apply {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] (R : Type u) [CommRing R] [X.Over (Spec ↧R)] [Y.Over (Spec ↧R)] [IsOver f (Spec ↧R)] (M : X.Modules) (n : ℕ) (x : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M n) :
    (cohomologyPushforwardBaseLinearEquiv f R M n).symm x = (CategoryTheory.ConcreteCategory.hom (TauCeti.AlgebraicGeometry.cohomologyPushforwardIso f M n).inv) x

    The inverse linear comparison has the same map as the inverse additive comparison.

    source
    theorem AlgebraicGeometry.Scheme.Hom.cohomologyPushforwardBaseLinearEquiv_naturality {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] (R : Type u) [CommRing R] [X.Over (Spec ↧R)] [Y.Over (Spec ↧R)] [IsOver f (Spec ↧R)] {M N : X.Modules} (α : M ⟶ N) (n : ℕ) (x : TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology ((Modules.pushforward f).obj M) n) :
    (cohomologyPushforwardBaseLinearEquiv f R N n) ((Modules.cohomologyMapBaseLinear R Y ((Modules.pushforward f).map α) n) x) = (Modules.cohomologyMapBaseLinear R X α n) ((cohomologyPushforwardBaseLinearEquiv f R M n) x)

    The base-linear closed-immersion comparison commutes with maps of coefficient sheaves.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Hom.moduleFinite_cohomology_pushforward_iff {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] (R : Type u) [CommRing R] [X.Over (Spec ↧R)] [Y.Over (Spec ↧R)] [IsOver f (Spec ↧R)] (M : X.Modules) (n : ℕ) :
    Module.Finite R (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology ((Modules.pushforward f).obj M) n) ↔ Module.Finite R (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M n)

    Cohomology of a direct image along a closed immersion is finite over the base ring exactly when the original cohomology is finite.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Hom.finrank_cohomology_pushforward {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] (R : Type u) [CommRing R] [X.Over (Spec ↧R)] [Y.Over (Spec ↧R)] [IsOver f (Spec ↧R)] (M : X.Modules) (n : ℕ) :
    Module.finrank R (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology ((Modules.pushforward f).obj M) n) = Module.finrank R (TauCeti.AlgebraicGeometry.Scheme.Modules.Cohomology M n)

    Direct image along a closed immersion over a commutative ring preserves cohomology finranks, including the value zero assigned to modules of infinite rank.

    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.Hom.eulerCharBelow_pushforward {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] (k : Type u) [Field k] [X.Over (Spec ↧k)] [Y.Over (Spec ↧k)] [IsOver f (Spec ↧k)] (M : X.Modules) (n : ℕ) :
    Modules.eulerCharBelow k Y ((Modules.pushforward f).obj M) n = Modules.eulerCharBelow k X M n

    Direct image along a closed immersion preserves the truncated Euler characteristic. When cohomology is finite-dimensional and vanishes above the truncation, this is the equality of the usual Euler characteristics.

    source
    theorem AlgebraicGeometry.Scheme.Hom.eulerCharBelow_pushforward_structureSheaf {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] (k : Type u) [Field k] [X.Over (Spec ↧k)] [Y.Over (Spec ↧k)] [IsOver f (Spec ↧k)] [IsFinite (X ↘ Spec ↧k)] (s : ↥(Spec ↧k)) (n : ℕ) :
    Modules.eulerCharBelow k Y ((Modules.pushforward f).obj (SheafOfModules.unit X.ringCatSheaf)) (n + 1) = ↑(finrank (X ↘ Spec ↧k) s)

    The Euler characteristic of the direct image of the structure sheaf of a scheme finite over k is its rank over k. Here the Euler characteristic may be truncated at any positive degree n + 1, since all positive cohomology of the finite scheme vanishes.