Documentation

DerivedAlgGeo.AlgebraicGeometry.Cohomology.Finiteness.RestrictedTwistExt

Ext-finiteness from restricted projective twists #

The restriction of an ambient projective-space twist was already known to be intrinsically invertible. LineBundleData.ofIsInvertible upgrades that theorem to the explicit inverse data consumed by the line-bundle Ext/cohomology comparison. Consequently Ext in X.Modules from a restricted twist to a coherent target is finite-dimensional in every degree and has finite finrank support.

This file does not compare Ext in X.Modules with Ext in Coh X. It only discharges the restricted-twist finiteness premise in the coherent-source dévissage.

source
noncomputable def AlgebraicGeometry.ProjectivePresentation.restrictedTwistLineBundleData {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] (P : ProjectivePresentation k X) (d : ℤ) :
Scheme.Modules.LineBundleData X

The restriction of the degree-d ambient projective twist, packaged with its canonical sheafified-dual tensor inverse.

Equations
Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.ProjectivePresentation.restrictedTwistLineBundleData_line {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] (P : ProjectivePresentation k X) (d : ℤ) :
    (P.restrictedTwistLineBundleData d).line = (Coh.ι X).obj (P.restrictedTwist d)
    source
    theorem AlgebraicGeometry.ProjectivePresentation.module_finite_restrictedTwistExt {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] (P : ProjectivePresentation k X) [Nontrivial P.index] (d : ℤ) (G : Coh X) (n : ℕ) :
    Module.Finite k (CategoryTheory.Abelian.Ext ((Coh.ι X).obj (P.restrictedTwist d)) ((Coh.ι X).obj G) n)

    Ambient Ext from a restricted projective twist to a coherent sheaf is finite-dimensional in every nonnegative degree.

    source
    theorem AlgebraicGeometry.ProjectivePresentation.restrictedTwistExt_subsingleton_of_bound_lt {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : ProjectivePresentation k X) [Nontrivial P.index] (d : ℤ) (G : Coh X) (n : ℕ) (hn : P.finiteCohomology.bound { obj := (P.restrictedTwistLineBundleData d).inverse.tensorObj ((Coh.ι X).obj G), property := ⋯ } < n) :
    Subsingleton (CategoryTheory.Abelian.Ext ((Coh.ι X).obj (P.restrictedTwist d)) ((Coh.ι X).obj G) n)

    Ambient Ext from a restricted twist vanishes above the cohomological bound of the coherent inverse twist.

    source
    theorem AlgebraicGeometry.ProjectivePresentation.restrictedTwistExt_finrankSupport_finite {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : ProjectivePresentation k X) [Nontrivial P.index] (d : ℤ) (G : Coh X) :
    (Function.support fun (n : ℕ) => ↑(Module.finrank k (CategoryTheory.Abelian.Ext ((Coh.ι X).obj (P.restrictedTwist d)) ((Coh.ι X).obj G) n))).Finite

    Only finitely many ambient Ext degrees from a restricted projective twist to a coherent target have nonzero finrank.