Documentation

DerivedAlgGeo.AlgebraicGeometry.DerivedCategory.Tensor.BoundedCoherent

The bounded coherent derived tensor product, as a supplied capability #

HasDerivedTensor Z is the geometry-level contract for a derived tensor product on Dᵇ(Coh Z), exact in both variables. It is a supplied capability, not a construction: this file inhabits nothing, and no scheme in this repository is shown to admit one.

What this file does not assert #

Dᵇ(Coh Z) is not automatically closed under arbitrary derived tensor. On a singular scheme the derived tensor of two bounded coherent complexes need not be bounded, and nothing here asserts otherwise. A caller instantiating HasDerivedTensor is asserting exactly that closure in whatever generality it supplies the class; relocating the class to this owner established it nowhere.

Neither is this class obtained by restricting the unbounded K-flat tensor product of Tensor/Unbounded.lean. That restriction is a missing theorem, not a definition.

No monoidal structure is asked for: not associativity, not symmetry, not a unit. A consumer that rebrackets or unitalizes derived tensor products wants Tensor/Coherent.lean instead, whose HasCoherentDerivedTensor packages the coherence as one MonoidalCategory and maps into this class one way only.

Placement #

MO1.10 (#1321) extracted this capability from DerivedCategory/FourierMukai/KernelCorrespondence.lean. Fourier--Mukai is a consumer: a transform needs a tensor, but a tensor is not about transforms, and a caller wanting a general derived tensor should not have to import kernels, convolution or correspondences to get one. Per the cutover ledger's standing decision that paths move and namespaces do not, the declarations keep the AlgebraicGeometry.DerivedCategory.FourierMukai namespace they were introduced with; the path, not the namespace, records what they are about.

References #

source
class AlgebraicGeometry.DerivedCategory.FourierMukai.HasDerivedTensor {S : Scheme} (Z : Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left Z)] :
Type (u + 1)

Derived tensor product on Dᵇ(Coh Z), supplied.

The ⊗^L slot of a Fourier--Mukai correspondence, and of anything else that twists a bounded coherent complex by another one. Stated as a bifunctor, matching Correspondence.tensor, so that tensor.obj K is "twist by the kernel K". Its exactness is packaged once as an ExactBifunctor: both partial tensor functors are exact, the shift comparisons are natural in the fixed variable, and the two shift directions satisfy Mathlib's Koszul compatibility law.

This two-slot contract is what kernel variation actually needs. A fixed Fourier--Mukai transform consumes exactness in the second tensor variable, whereas varying the kernel and taking its cone consumes exactness in the first. Independent one-slot witnesses would not supply the required global naturality.

No monoidal structure is asked for: not associativity, not symmetry, not a unit. Correspondence uses none of them, and FourierMukai/Basic.lean's own docstring is explicit that it assumes none.

Nothing inhabits this class. In particular it is not a theorem here that Dᵇ(Coh Z) is closed under derived tensor; on a singular Z it is not.

Instances
    source
    def AlgebraicGeometry.DerivedCategory.FourierMukai.HasDerivedTensor.exactBifunctor {S : Scheme} {Z : Families.SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasDerivedTensor Z] :
    derivedTensor.ExactBifunctor

    The exact-bifunctor witness selected by the derived tensor contract.

    Equations
    Instances For
      source
      noncomputable def AlgebraicGeometry.DerivedCategory.FourierMukai.HasDerivedTensor.firstFamily {S : Scheme} {Z : Families.SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasDerivedTensor Z] :
      derivedTensor.ExactFamily

      Exactness of the family obtained by varying the first (kernel) input.

      Equations
      Instances For
        source
        noncomputable def AlgebraicGeometry.DerivedCategory.FourierMukai.HasDerivedTensor.secondFamily {S : Scheme} {Z : Families.SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasDerivedTensor Z] :
        derivedTensor.flip.ExactFamily

        Exactness of the family obtained by varying the second input.

        Equations
        Instances For
          source
          @[reducible]
          noncomputable def AlgebraicGeometry.DerivedCategory.FourierMukai.HasDerivedTensor.commShift {S : Scheme} {Z : Families.SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasDerivedTensor Z] (K : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) :
          (derivedTensor.obj K).CommShift ℤ

          A fixed first input gives a shift-coherent partial tensor functor.

          Equations
          Instances For
            source
            theorem AlgebraicGeometry.DerivedCategory.FourierMukai.HasDerivedTensor.isTriangulated {S : Scheme} {Z : Families.SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasDerivedTensor Z] (K : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) :
            (derivedTensor.obj K).IsTriangulated

            A fixed first input gives a triangulated partial tensor functor.

            source
            theorem AlgebraicGeometry.DerivedCategory.FourierMukai.HasDerivedTensor.additive {S : Scheme} {Z : Families.SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasDerivedTensor Z] (K : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) :
            (derivedTensor.obj K).Additive

            A fixed first input gives an additive partial tensor functor.

            source
            @[reducible]
            noncomputable def AlgebraicGeometry.DerivedCategory.FourierMukai.HasDerivedTensor.flipCommShift {S : Scheme} {Z : Families.SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasDerivedTensor Z] (E : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) :
            (derivedTensor.flip.obj E).CommShift ℤ

            A fixed second input gives a shift-coherent partial tensor functor.

            Equations
            Instances For
              source
              theorem AlgebraicGeometry.DerivedCategory.FourierMukai.HasDerivedTensor.flipIsTriangulated {S : Scheme} {Z : Families.SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasDerivedTensor Z] (E : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) :
              (derivedTensor.flip.obj E).IsTriangulated

              A fixed second input gives a triangulated partial tensor functor.

              source
              theorem AlgebraicGeometry.DerivedCategory.FourierMukai.HasDerivedTensor.flipAdditive {S : Scheme} {Z : Families.SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasDerivedTensor Z] (E : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) :
              (derivedTensor.flip.obj E).Additive

              A fixed second input gives an additive partial tensor functor.

              source
              def AlgebraicGeometry.DerivedCategory.FourierMukai.derivedTensor {S : Scheme} (Z : Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasDerivedTensor Z] :
              CategoryTheory.Functor (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) (CategoryTheory.Functor (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)))

              The derived tensor bifunctor, named.

              Equations
              Instances For
                source
                instance AlgebraicGeometry.DerivedCategory.FourierMukai.derivedTensor_additive {S : Scheme} (Z : Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasDerivedTensor Z] (K : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) :
                ((derivedTensor Z).obj K).Additive
                source
                @[implicit_reducible]
                noncomputable instance AlgebraicGeometry.DerivedCategory.FourierMukai.derivedTensorCommShift {S : Scheme} (Z : Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasDerivedTensor Z] (K : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) :
                ((derivedTensor Z).obj K).CommShift ℤ
                Equations
                source
                instance AlgebraicGeometry.DerivedCategory.FourierMukai.derivedTensor_isTriangulated {S : Scheme} (Z : Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasDerivedTensor Z] (K : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) :
                ((derivedTensor Z).obj K).IsTriangulated
                source
                @[implicit_reducible]
                noncomputable instance AlgebraicGeometry.DerivedCategory.FourierMukai.derivedTensorFlipCommShift {S : Scheme} (Z : Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasDerivedTensor Z] (E : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) :
                ((derivedTensor Z).flip.obj E).CommShift ℤ
                Equations
                source
                instance AlgebraicGeometry.DerivedCategory.FourierMukai.derivedTensorFlip_isTriangulated {S : Scheme} (Z : Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasDerivedTensor Z] (E : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) :
                ((derivedTensor Z).flip.obj E).IsTriangulated
                source
                noncomputable def AlgebraicGeometry.DerivedCategory.FourierMukai.derivedTensorExactBifunctor {S : Scheme} (Z : Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasDerivedTensor Z] :
                (derivedTensor Z).ExactBifunctor

                The derived tensor bifunctor with its exactness in both variables exposed.

                Equations
                Instances For