Restricted-twist presentations on a projective variety

Let ι : X ↪ Pⁿ be a projective presentation. Serre's theorem gives a finite sum of negative twists surjecting onto ι_* F. Coherent pullback is right exact, so pulling that map back remains an epimorphism. Composing with the adjunction counit ι^* ι_* F ⟶ F produces the desired restricted-twist quotient as soon as that counit is known to be epi.

Pushforward along the closed immersion is faithful because its underlying continuous map is inducing. The general adjunction theorem therefore makes the counit epic, which discharges that premise without assuming the stronger standard isomorphism ι^* ι_* F ≅ F. The kernel of the resulting quotient is formed afresh in Coh X, so no exactness of closed-immersion pullback is asserted or used.

Main results

• ProjectivePresentation.restrictedTwist is the pullback of the ambient projective twist;
• ProjectivePresentation.restrictedTwist_isInvertible proves its underlying module sheaf is intrinsically invertible;
• ProjectivePresentation.exists_shortExact_coproduct_restrictedTwist_of_counit_epi records the exact categorical reduction through the counit;
• ProjectivePresentation.exists_shortExact_coproduct_restrictedTwist gives the unconditional coherent restricted-twist presentation.

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

The restriction to X of the degree-d twisting sheaf from the chosen ambient projective space. This definition requires no exactness or monoidal structure on pullback.

Equations

• P.restrictedTwist d = (AlgebraicGeometry.Coh.pullback P.embedding).obj (AlgebraicGeometry.Proj.projectiveSpaceTwist P.index k d)

theorem AlgebraicGeometry.ProjectivePresentation.restrictedTwist_isInvertible {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] (P : ProjectivePresentation k X) (d : ℤ) : (have this := (Coh.ι X).obj (P.restrictedTwist d); this).IsInvertible

The underlying module sheaf of every restricted twist is invertible. Pullback preserves rank-one local trivializations, so this needs no monoidal structure on the pullback functor.

theorem AlgebraicGeometry.ProjectivePresentation.exists_shortExact_coproduct_restrictedTwist_of_counit_epi {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : ProjectivePresentation k X) [Nontrivial P.index] (F : Coh X) (hcounit : CategoryTheory.Epi ((Scheme.Modules.pullbackPushforwardAdjunction P.embedding).counit.app ((Coh.ι X).obj F))) : ∃ (S : CategoryTheory.ShortComplex (Coh X)) (_ : S.ShortExact) (x : S.X₃ ≅ F) (N : ℕ) (_ : 1 ≤ N) (I : Type u) (x : Finite I), S.X₂ = ∐ fun (x : I) => P.restrictedTwist (-↑N)

A coherent sheaf is a quotient of finitely many restricted negative twists, provided the closed-immersion pullback/pushforward counit is epi at that sheaf.

This is the exact reduction supplied by the current APIs. The premise is expected to follow from the standard theorem ι^* ι_* F ≅ F for a closed immersion; no such theorem is available at the current Mathlib pin.

theorem AlgebraicGeometry.ProjectivePresentation.exists_shortExact_coproduct_restrictedTwist {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] (P : ProjectivePresentation k X) [Nontrivial P.index] (F : Coh X) : ∃ (S : CategoryTheory.ShortComplex (Coh X)) (_ : S.ShortExact) (x : S.X₃ ≅ F) (N : ℕ) (_ : 1 ≤ N) (I : Type u) (x : Finite I), S.X₂ = ∐ fun (x : I) => P.restrictedTwist (-↑N)

Every coherent sheaf on a projective variety is a quotient of finitely many restricted negative twists.

The closed-immersion pullback/pushforward counit is epic because module-sheaf pushforward along an inducing map is faithful. This conclusion does not require pullback to be exact, nor does it claim the stronger counit isomorphism.