Documentation

DerivedAlgGeo.AlgebraicGeometry.DerivedCategory.Tensor.Coherent

Coherent derived tensor products #

HasDerivedTensor is the bare capability of Tensor/BoundedCoherent.lean: a bifunctor exact in both variables. Consumers that rebracket or unitalize need more. In particular, independently choosing an associator and two unitors does not say that different routes through a fourfold tensor product agree.

HasCoherentDerivedTensor is the stable root for those consumers. It packages the tensor as a Mathlib MonoidalCategory, so naturality, the pentagon, and the triangle are fields of one structure rather than unrelated theorem-specific capabilities. Its ExactBifunctor field retains the complete two-slot exactness and Koszul shift coherence used by Fourier--Mukai transforms and kernel variation.

The instance below is the one-way migration adapter

HasCoherentDerivedTensor -> HasDerivedTensor.

There is intentionally no adapter in the other direction: a raw bifunctor is not promoted to coherent data. Raw instances remain useful for intermediate realizations that only construct a single transform, but public convolution, associativity, and unit APIs require this coherent root.

Still a supplied capability #

Coherence is more to supply, not less. Nothing here inhabits either class, and extending MonoidalCategory does not make Dᵇ(Coh Z) closed under derived tensor; on a singular Z it is not. A caller instantiating HasCoherentDerivedTensor asserts the closure and the coherence together.

Placement #

MO1.10 (#1321) extracted this file's contents from DerivedCategory/FourierMukai/DerivedTensorCoherence.lean, splitting the relative tier -- strong monoidality of derived pullback along a morphism -- into Tensor/Relative.lean. 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.

References #

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

A derived tensor product together with its complete monoidal coherence.

Extending MonoidalCategory makes functoriality, associator and unitor naturality, the pentagon, and the triangle part of the same root structure. The remaining field records exactness and compatible shifts of the complete tensor bifunctor.

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

    The exact-bifunctor witness carried by coherent derived tensor.

    Equations
    Instances For
      source
      theorem AlgebraicGeometry.DerivedCategory.FourierMukai.HasCoherentDerivedTensor.additive {S : Scheme} {Z : Families.SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasCoherentDerivedTensor Z] (K : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) :
      ((CategoryTheory.MonoidalCategory.curriedTensor (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z))).obj K).Additive

      Legacy projection: additivity of each left tensor twist.

      source
      @[reducible]
      noncomputable def AlgebraicGeometry.DerivedCategory.FourierMukai.HasCoherentDerivedTensor.commShift {S : Scheme} {Z : Families.SchemeBaseChange S} [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasCoherentDerivedTensor Z] (K : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) :
      ((CategoryTheory.MonoidalCategory.curriedTensor (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z))).obj K).CommShift ℤ

      Legacy projection: shift coherence of each left tensor twist.

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

        Legacy projection: triangulatedness of each left tensor twist.

        source
        @[implicit_reducible]
        noncomputable instance AlgebraicGeometry.DerivedCategory.FourierMukai.hasDerivedTensorOfCoherent {S : Scheme} (Z : Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasCoherentDerivedTensor Z] :
        HasDerivedTensor Z

        Forget coherence when a consumer only needs the raw tensor bifunctor.

        This is deliberately one-way: no raw HasDerivedTensor is upgraded to a coherent tensor product.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        noncomputable def AlgebraicGeometry.DerivedCategory.FourierMukai.coherentDerivedTensorAssoc {S : Scheme} (Z : Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasCoherentDerivedTensor Z] (A B : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) :
        ((derivedTensor Z).obj B).comp ((derivedTensor Z).obj A) ≅ (derivedTensor Z).obj (((derivedTensor Z).obj A).obj B)

        The coherent associator in the orientation used by the kernel ledgers: A ⊗ (B ⊗ -) ≅ (A ⊗ B) ⊗ -.

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev AlgebraicGeometry.DerivedCategory.FourierMukai.coherentDerivedTensorUnit {S : Scheme} (Z : Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasCoherentDerivedTensor Z] :
          SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)

          The tensor unit selected by the coherent root.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def AlgebraicGeometry.DerivedCategory.FourierMukai.coherentDerivedTensorLeftUnitor {S : Scheme} (Z : Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasCoherentDerivedTensor Z] :
            (derivedTensor Z).obj (coherentDerivedTensorUnit Z) ≅ CategoryTheory.Functor.id (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z))

            The coherent left unitor as an isomorphism of twist functors.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def AlgebraicGeometry.DerivedCategory.FourierMukai.coherentDerivedTensorRightUnitor {S : Scheme} (Z : Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasCoherentDerivedTensor Z] :
              (derivedTensor Z).flip.obj (coherentDerivedTensorUnit Z) ≅ CategoryTheory.Functor.id (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z))

              The coherent right unitor as an isomorphism of twist functors.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem AlgebraicGeometry.DerivedCategory.FourierMukai.coherentDerivedTensor_pentagon {S : Scheme} (Z : Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasCoherentDerivedTensor Z] (W X Y V : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) :
                CategoryTheory.MonoidalCategory.Pentagon W X Y V

                The pentagon law exposed at the derived-tensor root.

                source
                theorem AlgebraicGeometry.DerivedCategory.FourierMukai.coherentDerivedTensor_triangle {S : Scheme} (Z : Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasCoherentDerivedTensor Z] (X Y : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z)) :
                CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X (CategoryTheory.MonoidalCategoryStruct.tensorUnit (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z))) Y).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom) = CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom Y

                The triangle law exposed at the derived-tensor root.

                source
                @[implicit_reducible]
                instance AlgebraicGeometry.DerivedCategory.FourierMukai.hasCoherentDerivedTensorIsCompatibleWithTriangulation {S : Scheme} (Z : Families.SchemeBaseChange S) [IsLocallyNoetherian (CategoryTheory.Over.left Z)] [HasCoherentDerivedTensor Z] :
                CategoryTheory.MonoidalCategory.IsCompatibleWithTriangulation (SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left Z))

                A coherent geometric derived tensor realizes the generic compatibility interface between monoidal and triangulated structure from CategoryTheory/Monoidal/Triangulated.lean. The instance lives with the geometric object it is about, as Abelian (ModuleCat R) lives with ModuleCat, rather than in an instance leaf below the categorical source.

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