Documentation

DerivedAlgGeo.AlgebraicGeometry.DerivedCategory.Tensor.Relative

The relative derived tensor input: pullback compatibility #

The relative tier of the Tensor/ owner. Tensor/BoundedCoherent.lean and Tensor/Coherent.lean both speak about a single scheme base change; this file is about a morphism of them, and records how a coherent derived tensor on the source relates to one on the target across derived pullback.

HasMonoidalDerivedPullback f is that record. It extends Mathlib's Functor.Monoidal, which includes the tensorator and unit comparison, their naturality, associativity and unitality laws, and proofs that the lax and oplax maps are inverse. Tensor and unit compatibility therefore cannot be selected independently at each theorem site.

Still a supplied capability #

Like the tiers it builds on, this file inhabits nothing. Strong monoidality of derived pullback is a theorem about a morphism of schemes that this repository does not prove, and HasMonoidalDerivedPullback is where a caller discharges it. Arbitrary derived pullback itself remains SF8 #554's obligation; this class consumes the existing HasCoherentPullback contract rather than restating it.

Placement #

MO1.10 (#1321) extracted this file's contents from DerivedCategory/FourierMukai/DerivedTensorCoherence.lean. Separating it from Tensor/Coherent.lean is the ledger's requirement that the unbounded, bounded-coherent and relative inputs be distinguishable: a consumer needing only the absolute coherent tensor imports Tensor/Coherent.lean and never mentions a morphism. 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.HasMonoidalDerivedPullback {S : Scheme} {T U : Families.SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [Families.SchemeBaseChange.HasCoherentPullback f] [HasCoherentDerivedTensor T] [HasCoherentDerivedTensor U] extends (AlgebraicGeometry.DerivedCategory.Families.SchemeBaseChange.boundedCoherentDerivedPullback f).Monoidal :
Type (u + 1)

Derived pullback as a strong monoidal functor.

Mathlib's Functor.Monoidal root includes the tensorator and unit comparison, their naturality, associativity and unitality laws, and proofs that the lax and oplax maps are inverse. Thus tensor and unit compatibility cannot be selected independently at each theorem site.

Instances
    source
    noncomputable def AlgebraicGeometry.DerivedCategory.FourierMukai.monoidalDerivedPullbackTensorIso {S : Scheme} {T U : Families.SchemeBaseChange S} (f : T ⟶ U) [IsLocallyNoetherian (CategoryTheory.Over.left T)] [IsLocallyNoetherian (CategoryTheory.Over.left U)] [Families.SchemeBaseChange.HasCoherentPullback f] [HasCoherentDerivedTensor T] [HasCoherentDerivedTensor U] [HasMonoidalDerivedPullback f] (K : SchemeBoundedCoherentDerivedCategory (CategoryTheory.Over.left U)) :
    ((derivedTensor U).obj K).comp (Families.SchemeBaseChange.boundedCoherentDerivedPullback f) ≅ (Families.SchemeBaseChange.boundedCoherentDerivedPullback f).comp ((derivedTensor T).obj ((Families.SchemeBaseChange.boundedCoherentDerivedPullback f).obj K))

    Strong monoidality in the orientation consumed by the kernel ledgers: f*(K ⊗ -) ≅ f*K ⊗ f*(-).

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

      The pullback of the source unit acts as a left unit, derived from the strong monoidal unit comparison and the target left unitor.

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

        The pullback of the source unit acts as a right unit, derived from the strong monoidal unit comparison and the target right unitor.

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