Documentation

DerivedAlgGeo.CategoryTheory.Triangulated.FourierMukai.DGAdjunctionTwistCotwistAutoequivalence

Kernel autoequivalences from enhanced twist/cotwist conditions #

SphericalTwist.TwistCotwistEquivalenceConditions records that the dg twist and the unshifted dg cotwist cone of an EnhancedAdjunctionCones package are quasi-equivalences. The Fourier--Mukai comparison layer asks for the weaker consequences that their H⁰ functors are equivalences before packaging the selected kernels as KernelAutoequivalences.

This file is the adapter between those canonical interfaces. It specializes the existing twist and cotwist kernel constructors to the corresponding cone fields and obtains their equivalence hypotheses from the recorded quasi-equivalences. The twist and cotwist remain independent declarations: their endocorrespondences, kernel categories, enhancements, and convolution data need not agree, so no paired kernel record is introduced.

The conditions alone provide ordinary equivalences, not compatible target shift structures. The exactness wrappers therefore continue to require the existing Fourier--Mukai ShiftCompatibility inputs and triangulated endpoint presentations. No dual-twist or dual-cotwist equivalence, inverse-kernel formula, dg quasi-equivalence of a Fourier--Mukai transform, or sphericality is inferred.

Twist kernel #

source
@[reducible]
noncomputable def CategoryTheory.Triangulated.SphericalTwist.TwistCotwistEquivalenceConditions.twistKernelAutoequivalence {A : Type uA} {B : Type uB} {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [DGCategory A] [DGCategory B] [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {S : DGFunctor A B} {L R : DGFunctor B A} {eA : H0 A ≌ X} {eB : H0 B ≌ Y} {C : FourierMukai.Correspondence X Y W₁} {C' : FourierMukai.Correspondence Y X W₂} {E : FourierMukai.Correspondence Y Y W} {P : W₁} {Q : W₂} {e : Enhancement W} {D : FourierMukai.ConvolutionData C' C E} {U : FourierMukai.UnitKernelData E} [IsPretriangulated B] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [eB.functor.CommShift ℤ] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] {cones : EnhancedAdjunctionCones S L R} (h : TwistCotwistEquivalenceConditions cones) (H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q)) (T : FourierMukai.CounitKernelConeData C C' E e P (FourierMukai.RightAdjointKernelData.ofH0Presentation H cones.rightAdj) D U) (hE : E.KernelEvaluationExact) (N : FourierMukai.CounitKernelConeData.PresentedCounitComparisonData cones.rightAdj H cones.twist T hE) :
FourierMukai.KernelAutoequivalence Y W

The selected Fourier--Mukai twist kernel is an autoequivalence under the canonical enhanced twist/cotwist equivalence conditions.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CategoryTheory.Triangulated.SphericalTwist.TwistCotwistEquivalenceConditions.twistKernelAutoequivalenceIsTriangulated {A : Type uA} {B : Type uB} {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [DGCategory A] [DGCategory B] [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {S : DGFunctor A B} {L R : DGFunctor B A} {eA : H0 A ≌ X} {eB : H0 B ≌ Y} {C : FourierMukai.Correspondence X Y W₁} {C' : FourierMukai.Correspondence Y X W₂} {E : FourierMukai.Correspondence Y Y W} {P : W₁} {Q : W₂} {e : Enhancement W} {D : FourierMukai.ConvolutionData C' C E} {U : FourierMukai.UnitKernelData E} [IsPretriangulated B] [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [eB.functor.CommShift ℤ] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] {cones : EnhancedAdjunctionCones S L R} [eB.functor.IsTriangulated] (h : TwistCotwistEquivalenceConditions cones) (H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q)) (T : FourierMukai.CounitKernelConeData C C' E e P (FourierMukai.RightAdjointKernelData.ofH0Presentation H cones.rightAdj) D U) (hE : E.KernelEvaluationExact) (N : FourierMukai.CounitKernelConeData.PresentedCounitComparisonData cones.rightAdj H cones.twist T hE) (hN : FourierMukai.CounitKernelConeData.PresentedCounitComparisonData.ShiftCompatibility cones.rightAdj H cones.twist T hE N) :
    (h.twistKernelAutoequivalence H T hE N).equiv.IsTriangulated

    The selected twist kernel autoequivalence is exact when the existing Fourier--Mukai comparison respects the selected target shift structure.

    Cotwist kernel #

    source
    @[reducible]
    noncomputable def CategoryTheory.Triangulated.SphericalTwist.TwistCotwistEquivalenceConditions.cotwistKernelAutoequivalence {A : Type uA} {B : Type uB} {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [DGCategory A] [DGCategory B] [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {S : DGFunctor A B} {L R : DGFunctor B A} {eA : H0 A ≌ X} {eB : H0 B ≌ Y} {C : FourierMukai.Correspondence X Y W₁} {C' : FourierMukai.Correspondence Y X W₂} {E : FourierMukai.Correspondence X X W} {P : W₁} {Q : W₂} {e : Enhancement W} {D : FourierMukai.ConvolutionData C C' E} {U : FourierMukai.UnitKernelData E} [IsPretriangulated A] [Limits.HasZeroObject X] [HasShift X ℤ] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [eA.functor.CommShift ℤ] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] {cones : EnhancedAdjunctionCones S L R} (h : TwistCotwistEquivalenceConditions cones) (H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q)) (T : FourierMukai.AdjunctionUnitKernelConeData C C' E e P (FourierMukai.RightAdjointKernelData.ofH0Presentation H cones.rightAdj) D U) (hE : E.KernelEvaluationExact) (N : FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData cones.rightAdj H cones.cotwistCone T hE) :
    FourierMukai.KernelAutoequivalence X W

    The selected shifted Fourier--Mukai cotwist kernel is an autoequivalence under the canonical enhanced twist/cotwist equivalence conditions.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem CategoryTheory.Triangulated.SphericalTwist.TwistCotwistEquivalenceConditions.cotwistKernelAutoequivalenceIsTriangulated {A : Type uA} {B : Type uB} {X : Type uX} {Y : Type uY} {W₁ : Type u₁} {W₂ : Type u₂} {W : Type uW} [DGCategory A] [DGCategory B] [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{v₁, u₁} W₁] [Category.{v₂, u₂} W₂] [Category.{vW, uW} W] {S : DGFunctor A B} {L R : DGFunctor B A} {eA : H0 A ≌ X} {eB : H0 B ≌ Y} {C : FourierMukai.Correspondence X Y W₁} {C' : FourierMukai.Correspondence Y X W₂} {E : FourierMukai.Correspondence X X W} {P : W₁} {Q : W₂} {e : Enhancement W} {D : FourierMukai.ConvolutionData C C' E} {U : FourierMukai.UnitKernelData E} [IsPretriangulated A] [Limits.HasZeroObject X] [HasShift X ℤ] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [eA.functor.CommShift ℤ] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] {cones : EnhancedAdjunctionCones S L R} [eA.functor.IsTriangulated] (h : TwistCotwistEquivalenceConditions cones) (H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q)) (T : FourierMukai.AdjunctionUnitKernelConeData C C' E e P (FourierMukai.RightAdjointKernelData.ofH0Presentation H cones.rightAdj) D U) (hE : E.KernelEvaluationExact) (N : FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData cones.rightAdj H cones.cotwistCone T hE) (hN : FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.ShiftCompatibility cones.rightAdj H cones.cotwistCone T hE N) :
      (h.cotwistKernelAutoequivalence H T hE N).equiv.IsTriangulated

      The selected cotwist kernel autoequivalence is exact when the existing Fourier--Mukai comparison respects the selected target shift structure.