Documentation

DerivedAlgGeo.AlgebraicGeometry.DerivedCategory.CartierDivisor

Cartier divisors as coherent derived objects #

This file transports the canonical CartierDivisor.lineBundleData bridge into Coh X, D(Coh X), and Dᵇ(Coh X). The canonical objects are aliases of the generic LineBundleData adapters, so there is no second choice of representative. Comparison isomorphisms identify them with an associated sheaf packaged using any independently supplied coherence proof; this is the form needed by existing short-exact-sequence APIs.

source
noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.coh {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) :
Coh X

The associated sheaf of a Cartier divisor, canonically packaged as a coherent sheaf.

Equations
Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.CartierDivisor.coh_obj {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) :
    (coh D).obj = associatedSheaf D
    source
    noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.cohIso {X : Scheme} [IsIntegral X] (D : ↥X.CartierDivisor) (h : X.coherent (associatedSheaf D)) :
    coh D ≅ { obj := associatedSheaf D, property := h }

    Compare the canonical coherent object with the same associated sheaf packaged using an independently supplied proof of coherence.

    Equations
    Instances For
      source
      noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.derivedObject {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : ↥X.CartierDivisor) :
      DerivedCategory.SchemeCoherentDerivedCategory X

      The associated line bundle placed canonically in degree zero of D(Coh X).

      Equations
      Instances For
        source
        @[simp]
        theorem AlgebraicGeometry.Scheme.CartierDivisor.derivedObject_eq_single {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : ↥X.CartierDivisor) :
        derivedObject D = (DerivedCategory.singleFunctor (Coh X) 0).obj (coh D)
        source
        theorem AlgebraicGeometry.Scheme.CartierDivisor.derivedObject_perfect {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : ↥X.CartierDivisor) :
        DerivedCategory.schemePerfect X (derivedObject D)

        A Cartier divisor's degree-zero derived object is perfect because its associated sheaf is a line bundle.

        source
        theorem AlgebraicGeometry.Scheme.CartierDivisor.derivedObject_bounded {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : ↥X.CartierDivisor) :
        DerivedCategory.TStructure.t.bounded (derivedObject D)

        A Cartier divisor's degree-zero derived object is bounded for the canonical t-structure.

        source
        noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.derivedObjectIso {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : ↥X.CartierDivisor) (h : X.coherent (associatedSheaf D)) :
        derivedObject D ≅ (DerivedCategory.singleFunctor (Coh X) 0).obj { obj := associatedSheaf D, property := h }

        Compare the canonical derived object with the degree-zero object formed from an independently supplied coherence proof.

        Equations
        Instances For
          source
          noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.boundedDerivedObject {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : ↥X.CartierDivisor) :
          DerivedCategory.SchemeBoundedCoherentDerivedCategory X

          The canonical Cartier-divisor object of Dᵇ(Coh X). Its underlying derived object is exactly derivedObject D.

          Equations
          Instances For
            source
            @[simp]
            theorem AlgebraicGeometry.Scheme.CartierDivisor.boundedDerivedObject_obj {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : ↥X.CartierDivisor) :
            (boundedDerivedObject D).obj = derivedObject D
            source
            noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.boundedDerivedObjectOfCoherence {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : ↥X.CartierDivisor) (h : X.coherent (associatedSheaf D)) :
            DerivedCategory.SchemeBoundedCoherentDerivedCategory X

            The bounded degree-zero object formed from an independently supplied coherence proof. This is the comparison target used by short exact sequences whose endpoints predate the canonical Cartier-divisor adapter.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem AlgebraicGeometry.Scheme.CartierDivisor.boundedDerivedObjectOfCoherence_obj {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : ↥X.CartierDivisor) (h : X.coherent (associatedSheaf D)) :
              (boundedDerivedObjectOfCoherence D h).obj = (DerivedCategory.singleFunctor (Coh X) 0).obj { obj := associatedSheaf D, property := h }
              source
              noncomputable def AlgebraicGeometry.Scheme.CartierDivisor.boundedDerivedObjectIso {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : ↥X.CartierDivisor) (h : X.coherent (associatedSheaf D)) :
              boundedDerivedObject D ≅ boundedDerivedObjectOfCoherence D h

              The canonical bounded object agrees, up to the fully faithful full-subcategory lift, with every proof-packaged degree-zero representative.

              Equations
              Instances For