Documentation

DerivedAlgGeo.AlgebraicGeometry.DerivedCategory.DivisorSequence

Coherent short exact sequences in derived categories #

Mathlib's ShortExact.singleTriangle is the canonical passage from a short exact sequence in an abelian category to a distinguished triangle in its derived category. This file exposes that construction for coherent sheaves on a locally Noetherian scheme, together with its functorial maps in both the ambient and bounded derived categories. The bounded construction consumes the generic full-triangulated-subcategory lifting API.

The effective Cartier-divisor API already constructs the coherent twisted sequence

0 ⟶ O_X(E-D) ⟶ O_X(E) ⟶ O_X(E) ⊗ i_* O_D ⟶ 0.

EffectiveCartierDivisor.cohTwistTriangle is its derived-category triangle. The closing API tensors this sequence by arbitrary LineBundleData, giving canonical coherent and bounded triangles with endpoint comparisons. The connecting morphism is always supplied by the derived-category construction; it is not chosen objectwise. Geometric consumers remain responsible only for claims such as residual orthogonality of the quotient.

source
noncomputable def AlgebraicGeometry.DerivedCategory.cohShortExactTriangle {X : Scheme} [IsLocallyNoetherian X] {S : CategoryTheory.ShortComplex (Coh X)} (hS : S.ShortExact) :
CategoryTheory.Pretriangulated.Triangle (SchemeCoherentDerivedCategory X)

The canonical derived triangle attached to a short exact sequence of coherent sheaves.

Equations
Instances For
    source
    theorem AlgebraicGeometry.DerivedCategory.cohShortExactTriangle_distinguished {X : Scheme} [IsLocallyNoetherian X] {S : CategoryTheory.ShortComplex (Coh X)} (hS : S.ShortExact) :
    cohShortExactTriangle hS ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

    The coherent short-exact triangle is distinguished.

    source
    noncomputable def AlgebraicGeometry.DerivedCategory.cohShortExactTriangleMap {X : Scheme} [IsLocallyNoetherian X] {S₁ S₂ : CategoryTheory.ShortComplex (Coh X)} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (f : S₁ ⟶ S₂) :
    cohShortExactTriangle h₁ ⟶ cohShortExactTriangle h₂

    A map of short exact coherent sequences induces a map of their derived triangles. In particular, the connecting morphisms are natural for the same sequence maps used by the source and target triangles.

    Equations
    Instances For
      source
      @[simp]
      theorem AlgebraicGeometry.DerivedCategory.cohShortExactTriangleMap_id {X : Scheme} [IsLocallyNoetherian X] {S : CategoryTheory.ShortComplex (Coh X)} (hS : S.ShortExact) :
      cohShortExactTriangleMap hS hS (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.id (cohShortExactTriangle hS)

      The coherent short-exact triangle map preserves identities.

      source
      @[simp]
      theorem AlgebraicGeometry.DerivedCategory.cohShortExactTriangleMap_comp {X : Scheme} [IsLocallyNoetherian X] {S₁ S₂ S₃ : CategoryTheory.ShortComplex (Coh X)} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (h₃ : S₃.ShortExact) (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃) :
      cohShortExactTriangleMap h₁ h₃ (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (cohShortExactTriangleMap h₁ h₂ f) (cohShortExactTriangleMap h₂ h₃ g)

      The coherent short-exact triangle map preserves composition.

      source
      theorem AlgebraicGeometry.DerivedCategory.cohShortExactTriangleMap_comp_assoc {X : Scheme} [IsLocallyNoetherian X] {S₁ S₂ S₃ : CategoryTheory.ShortComplex (Coh X)} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (h₃ : S₃.ShortExact) (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃) {Z : CategoryTheory.Pretriangulated.Triangle (SchemeCoherentDerivedCategory X)} (h : cohShortExactTriangle h₃ ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (cohShortExactTriangleMap h₁ h₃ (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (cohShortExactTriangleMap h₁ h₂ f) (CategoryTheory.CategoryStruct.comp (cohShortExactTriangleMap h₂ h₃ g) h)

      The coherent short-exact triangle map preserves composition.

      source
      theorem AlgebraicGeometry.DerivedCategory.cohShortExactTriangle_onBounded {X : Scheme} [IsLocallyNoetherian X] {S : CategoryTheory.ShortComplex (Coh X)} (hS : S.ShortExact) :
      DerivedCategory.TStructure.t.bounded.OnTriangle (cohShortExactTriangle hS)

      All three objects of a coherent short-exact triangle are bounded for the canonical derived t-structure.

      source
      noncomputable def AlgebraicGeometry.DerivedCategory.cohShortExactBoundedTriangle {X : Scheme} [IsLocallyNoetherian X] {S : CategoryTheory.ShortComplex (Coh X)} (hS : S.ShortExact) :
      CategoryTheory.Pretriangulated.Triangle (SchemeBoundedCoherentDerivedCategory X)

      The canonical short-exact triangle viewed in the bounded coherent derived subcategory.

      Equations
      Instances For
        source
        noncomputable def AlgebraicGeometry.DerivedCategory.cohShortExactBoundedTriangleInclusionIso {X : Scheme} [IsLocallyNoetherian X] {S : CategoryTheory.ShortComplex (Coh X)} (hS : S.ShortExact) :
        let P := DerivedCategory.TStructure.t.bounded; P.ι.mapTriangle.obj (cohShortExactBoundedTriangle hS) ≅ cohShortExactTriangle hS

        The canonical comparison between the bounded lift after inclusion and the original coherent short-exact triangle.

        Equations
        Instances For
          source
          theorem AlgebraicGeometry.DerivedCategory.cohShortExactBoundedTriangle_distinguished {X : Scheme} [IsLocallyNoetherian X] {S : CategoryTheory.ShortComplex (Coh X)} (hS : S.ShortExact) :
          cohShortExactBoundedTriangle hS ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

          The bounded coherent short-exact triangle is distinguished.

          source
          noncomputable def AlgebraicGeometry.DerivedCategory.cohShortExactBoundedTriangleMap {X : Scheme} [IsLocallyNoetherian X] {S₁ S₂ : CategoryTheory.ShortComplex (Coh X)} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (f : S₁ ⟶ S₂) :
          cohShortExactBoundedTriangle h₁ ⟶ cohShortExactBoundedTriangle h₂

          A map of short exact coherent sequences induces a map of their bounded derived triangles.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem AlgebraicGeometry.DerivedCategory.cohShortExactBoundedTriangleMap_id {X : Scheme} [IsLocallyNoetherian X] {S : CategoryTheory.ShortComplex (Coh X)} (hS : S.ShortExact) :
            cohShortExactBoundedTriangleMap hS hS (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.id (cohShortExactBoundedTriangle hS)

            The bounded coherent short-exact triangle map preserves identities.

            source
            @[simp]
            theorem AlgebraicGeometry.DerivedCategory.cohShortExactBoundedTriangleMap_comp {X : Scheme} [IsLocallyNoetherian X] {S₁ S₂ S₃ : CategoryTheory.ShortComplex (Coh X)} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (h₃ : S₃.ShortExact) (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃) :
            cohShortExactBoundedTriangleMap h₁ h₃ (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (cohShortExactBoundedTriangleMap h₁ h₂ f) (cohShortExactBoundedTriangleMap h₂ h₃ g)

            The bounded coherent short-exact triangle map preserves composition.

            source
            theorem AlgebraicGeometry.DerivedCategory.cohShortExactBoundedTriangleMap_comp_assoc {X : Scheme} [IsLocallyNoetherian X] {S₁ S₂ S₃ : CategoryTheory.ShortComplex (Coh X)} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (h₃ : S₃.ShortExact) (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃) {Z : CategoryTheory.Pretriangulated.Triangle (SchemeBoundedCoherentDerivedCategory X)} (h : cohShortExactBoundedTriangle h₃ ⟶ Z) :
            CategoryTheory.CategoryStruct.comp (cohShortExactBoundedTriangleMap h₁ h₃ (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (cohShortExactBoundedTriangleMap h₁ h₂ f) (CategoryTheory.CategoryStruct.comp (cohShortExactBoundedTriangleMap h₂ h₃ g) h)

            The bounded coherent short-exact triangle map preserves composition.

            source
            theorem AlgebraicGeometry.DerivedCategory.cohShortExactBoundedTriangleMap_ambient {X : Scheme} [IsLocallyNoetherian X] {S₁ S₂ : CategoryTheory.ShortComplex (Coh X)} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) (f : S₁ ⟶ S₂) :
            let P := DerivedCategory.TStructure.t.bounded; CategoryTheory.CategoryStruct.comp (cohShortExactBoundedTriangleInclusionIso h₁).inv (CategoryTheory.CategoryStruct.comp (P.ι.mapTriangle.map (cohShortExactBoundedTriangleMap h₁ h₂ f)) (cohShortExactBoundedTriangleInclusionIso h₂).hom) = cohShortExactTriangleMap h₁ h₂ f

            Under the canonical inclusion comparisons, the bounded triangle map is the original coherent derived triangle map.

            source
            noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.cohTwistTriangle {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : EffectiveCartierDivisor) (E : ↥X.CartierDivisor) (hSource : X.coherent (CartierDivisor.associatedSheaf (E - D.divisor))) (hMiddle : X.coherent (CartierDivisor.associatedSheaf E)) :
            CategoryTheory.Pretriangulated.Triangle (DerivedCategory.SchemeCoherentDerivedCategory X)

            The distinguished triangle in D(Coh X) supplied by the twisted exact sequence of an effective Cartier divisor.

            Equations
            Instances For
              source
              theorem AlgebraicGeometry.Scheme.EffectiveCartierDivisor.cohTwistTriangle_distinguished {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : EffectiveCartierDivisor) (E : ↥X.CartierDivisor) (hSource : X.coherent (CartierDivisor.associatedSheaf (E - D.divisor))) (hMiddle : X.coherent (CartierDivisor.associatedSheaf E)) :
              D.cohTwistTriangle E hSource hMiddle ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

              The effective Cartier-divisor twist triangle is distinguished.

              source
              noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.cohTwistBoundedTriangle {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : EffectiveCartierDivisor) (E : ↥X.CartierDivisor) (hSource : X.coherent (CartierDivisor.associatedSheaf (E - D.divisor))) (hMiddle : X.coherent (CartierDivisor.associatedSheaf E)) :
              CategoryTheory.Pretriangulated.Triangle (DerivedCategory.SchemeBoundedCoherentDerivedCategory X)

              The bounded coherent derived triangle supplied by the twisted exact sequence of an effective Cartier divisor.

              Equations
              Instances For
                source
                noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.cohTwistBoundedTriangleInclusionIso {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : EffectiveCartierDivisor) (E : ↥X.CartierDivisor) (hSource : X.coherent (CartierDivisor.associatedSheaf (E - D.divisor))) (hMiddle : X.coherent (CartierDivisor.associatedSheaf E)) :
                let P := DerivedCategory.TStructure.t.bounded; P.ι.mapTriangle.obj (D.cohTwistBoundedTriangle E hSource hMiddle) ≅ D.cohTwistTriangle E hSource hMiddle

                The canonical comparison between the bounded effective-divisor triangle after inclusion and its ambient coherent derived triangle.

                Equations
                Instances For
                  source
                  theorem AlgebraicGeometry.Scheme.EffectiveCartierDivisor.cohTwistBoundedTriangle_distinguished {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : EffectiveCartierDivisor) (E : ↥X.CartierDivisor) (hSource : X.coherent (CartierDivisor.associatedSheaf (E - D.divisor))) (hMiddle : X.coherent (CartierDivisor.associatedSheaf E)) :
                  D.cohTwistBoundedTriangle E hSource hMiddle ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

                  The bounded effective Cartier-divisor twist triangle is distinguished.

                  Canonical twists by arbitrary line bundles #

                  source
                  noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.cohLineBundleTwistTriangle {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : EffectiveCartierDivisor) (L : Modules.LineBundleData X) (E : ↥X.CartierDivisor) :
                  CategoryTheory.Pretriangulated.Triangle (DerivedCategory.SchemeCoherentDerivedCategory X)

                  The distinguished triangle obtained by tensoring a Cartier-divisor sequence with an arbitrary line bundle. Unlike cohTwistTriangle, this API needs no separately supplied coherence proofs.

                  Equations
                  Instances For
                    source
                    theorem AlgebraicGeometry.Scheme.EffectiveCartierDivisor.cohLineBundleTwistTriangle_distinguished {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : EffectiveCartierDivisor) (L : Modules.LineBundleData X) (E : ↥X.CartierDivisor) :
                    D.cohLineBundleTwistTriangle L E ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

                    The line-bundle-twisted Cartier triangle is distinguished.

                    source
                    noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.cohLineBundleTwistBoundedTriangle {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : EffectiveCartierDivisor) (L : Modules.LineBundleData X) (E : ↥X.CartierDivisor) :
                    CategoryTheory.Pretriangulated.Triangle (DerivedCategory.SchemeBoundedCoherentDerivedCategory X)

                    The line-bundle-twisted Cartier triangle in Dᵇ(Coh X).

                    Equations
                    Instances For
                      source
                      theorem AlgebraicGeometry.Scheme.EffectiveCartierDivisor.cohLineBundleTwistBoundedTriangle_distinguished {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : EffectiveCartierDivisor) (L : Modules.LineBundleData X) (E : ↥X.CartierDivisor) :
                      D.cohLineBundleTwistBoundedTriangle L E ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

                      The bounded line-bundle-twisted Cartier triangle is distinguished.

                      source
                      noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.cohLineBundleTwistBoundedTriangleObj₁Iso {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : EffectiveCartierDivisor) (L : Modules.LineBundleData X) (E : ↥X.CartierDivisor) :
                      (D.cohLineBundleTwistBoundedTriangle L E).obj₁ ≅ (L.tensor (CartierDivisor.lineBundleData (E - D.divisor))).boundedDerivedObject

                      The first vertex of the bounded line-bundle-twisted triangle is the canonical derived object of L ⊗ O_X(E-D).

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.cohLineBundleTwistBoundedTriangleObj₂Iso {X : Scheme} [IsIntegral X] [IsLocallyNoetherian X] (D : EffectiveCartierDivisor) (L : Modules.LineBundleData X) (E : ↥X.CartierDivisor) :
                        (D.cohLineBundleTwistBoundedTriangle L E).obj₂ ≅ (L.tensor (CartierDivisor.lineBundleData E)).boundedDerivedObject

                        The second vertex of the bounded line-bundle-twisted triangle is the canonical derived object of L ⊗ O_X(E).

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