Documentation

DerivedAlgGeo.AlgebraicGeometry.ProjectiveSpectrum.Modules.TwistInvertible

The twisting sheaf is invertible #

O(d) on Proj π’œ is a locally free rank-one sheaf as soon as degree-one elements generate A over π’œ 0. This is the hypothesis quasi-coherence and coherence already take, unchanged.

Why this file exists, and the route it fixes #

#584 asks for the twist F(d) = F βŠ— O(d) of an arbitrary module sheaf on Proj. The sheafified tensor product in Modules/Tensor/Basic.lean is stated for a locally free rank-one factor β€” its comparison maps are inverted by sheafification only there, and its associator needs the outer factors invertible. So F(d) cannot be built at all until O(d) is known to be invertible, and the issue left the route open between:

This file takes the first route, and the reason is that the second does not reach the statement #570 needs. The graded-shift description covers associated sheaves only, while #570 surjects onto an arbitrary coherent F; identifying every coherent sheaf on Proj with an associated sheaf is Serre's theorem, which is downstream rather than available. The graded shift is kept as the computational special case β€” the Čech lane computes with it and needs no tensor β€” and the comparison between the two descriptions is what deliverable 4 of #584 asks for.

Why it is short #

Nothing here is new mathematics; the local triviality was built already, for a different conclusion. TwistCoherence.lean needed exactly the same charts to prove O(d) coherent, so intShiftOverSelfIso β€” the twist is isomorphic to the structure sheaf over a degree-one chart, at either sign of d β€” is on hand. Invertibility is that isomorphism composed with associatedSheafSelfIso and handed to IsInvertible.of_trivializations, over the cover degreeOneCharts_coversTop already supplies.

The degree-one hypothesis is not an artifact #

TwistCoherence.lean records why, and the same applies here: on a chart Dβ‚Š(f) with deg f = m, O(d) is trivial only when m ∣ d. There is no trivialization on charts of arbitrary positive degree to be had, so the generating family must be taken in degree one.

source
noncomputable def AlgebraicGeometry.Proj.twistingSheafOverUnitIso {A ΟƒA : Type u} [CommRing A] [SetLike ΟƒA A] [AddSubgroupClass ΟƒA A] (π’œ : β„• β†’ ΟƒA) [GradedRing π’œ] (f : β†₯(π’œ 1)) (d : β„€) :
SheafOfModules.unit (CategoryTheory.Sheaf.over (Proj π’œ).ringCatSheaf (Scheme.Hom.opensRange (standardAway π’œ (degreeOneStandardChart π’œ f)))) β‰… (have this := twistingSheaf π’œ d; this).over (Scheme.Hom.opensRange (standardAway π’œ (degreeOneStandardChart π’œ f)))

On a degree-one chart, the twisting sheaf is isomorphic to the unit module.

The Iso.refl is SheafOfModules.overUnitIso, inlined rather than imported: the unit of a slice and the slice of the unit are the same object, and naming it here would cost the whole CoherentSheaf.Abelian.Extensions import for a rfl.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem AlgebraicGeometry.Proj.twistingSheaf_isInvertible {A ΟƒA : Type u} [CommRing A] [SetLike ΟƒA A] [AddSubgroupClass ΟƒA A] (π’œ : β„• β†’ ΟƒA) [GradedRing π’œ] {I : Type u} (g : I β†’ β†₯(π’œ 1)) (d : β„€) (hg : Algebra.adjoin (β†₯(π’œ 0)) (Set.range fun (j : I) => ↑(g j)) = ⊀) :
    (have this := twistingSheaf π’œ d; this).IsInvertible

    The twisting sheaf O(d) is invertible, at either sign of d, as soon as degree-one elements generate A over π’œ 0.

    This is what makes Modules/Tensor/Basic.lean applicable to O(d), and hence what lets F(d) be defined for an arbitrary module sheaf F. The hypothesis is the one coherence already takes.

    source
    noncomputable def AlgebraicGeometry.Proj.tensorTwistOverChartIso {A ΟƒA : Type u} [CommRing A] [SetLike ΟƒA A] [AddSubgroupClass ΟƒA A] (π’œ : β„• β†’ ΟƒA) [GradedRing π’œ] (F : (Proj π’œ).Modules) (f : β†₯(π’œ 1)) (d : β„€) :
    SheafOfModules.over (F.tensorObj (twistingSheaf π’œ d)) (Scheme.Hom.opensRange (standardAway π’œ (degreeOneStandardChart π’œ f))) β‰… SheafOfModules.over F (Scheme.Hom.opensRange (standardAway π’œ (degreeOneStandardChart π’œ f)))

    On a degree-one chart, the twist is the sheaf itself.

    F(d) = F βŠ— O(d) restricted to Dβ‚Š(f) for f of degree one is just F restricted there, because O(d) is trivial on that chart (twistingSheafOverUnitIso) and tensoring with a trivialized factor does nothing to the restriction (tensorOverIsoOfTrivializationRight).

    F is arbitrary β€” not an associated sheaf, not coherent, not even quasi-coherent. This is the passage #585 needs: the per-chart sections that ChartExtension.lean produces live on different sheaves, one per chart, and this is what carries each of them into the single sheaf F(d).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For