Dg cone diagrams of Fourier--Mukai kernels #
When the kernel category W of a correspondence carries a dg enhancement
e : Enhancement W, a DGCategory.ConePresentation e.dgCat is a chosen cone
diagram at the enhancement level, and e.coneTriangleFunctor reads it as a
triangle of kernels. For each source object, the correspondence's
kernel-evaluation functor maps that triangle to a triangle in the target
category. More strongly, a globally shift-coherent exact kernel family turns
a fixed kernel cone into a functor from source objects to distinguished
transform triangles.
The kernel category is enhanced, not identified with an H⁰ on the nose:
a geometric kernel category such as Dᵇ(Coh(X × Y)) is only equivalent to
the H⁰ of its enhancement, and the comparison equivalence is exactly the
datum Enhancement carries. The shift and exactness compatibility of that
comparison are instance hypotheses here; supplying them for a concrete
enhancement is part of the geometric realization, as is exactness of kernel
evaluation itself.
noncomputable def
CategoryTheory.Triangulated.FourierMukai.Correspondence.kernelConeTransformTriangleFunctor
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
(corr : Correspondence X Y W)
(E : X)
[(corr.kernelEvaluation E).CommShift ℤ]
:
The pointwise transform of the functorial dg cone family of an enhanced kernel category, evaluated at one source object. Its objects are the triangles obtained by applying kernel evaluation to the source, target, and cone kernels; its morphisms retain the maps induced by dg homotopy-coherent cone morphisms.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.Correspondence.kernelConeTransformTriangleFunctor_obj₁
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
(corr : Correspondence X Y W)
(E : X)
[(corr.kernelEvaluation E).CommShift ℤ]
(A : DGCategory.ConePresentation e.dgCat)
:
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.Correspondence.kernelConeTransformTriangleFunctor_obj₂
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
(corr : Correspondence X Y W)
(E : X)
[(corr.kernelEvaluation E).CommShift ℤ]
(A : DGCategory.ConePresentation e.dgCat)
:
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.Correspondence.kernelConeTransformTriangleFunctor_obj₃
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
(corr : Correspondence X Y W)
(E : X)
[(corr.kernelEvaluation E).CommShift ℤ]
(A : DGCategory.ConePresentation e.dgCat)
:
theorem
CategoryTheory.Triangulated.FourierMukai.Correspondence.kernelConeTransformTriangleFunctor_obj_distinguished
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
[Limits.HasZeroObject Y]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[Limits.HasZeroObject W]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
(corr : Correspondence X Y W)
(E : X)
[e.equiv.functor.IsTriangulated]
[(corr.kernelEvaluation E).CommShift ℤ]
[(corr.kernelEvaluation E).IsTriangulated]
(A : DGCategory.ConePresentation e.dgCat)
:
Exactness in the kernel variable sends every enhanced kernel cone to a pointwise distinguished triangle of transforms.
@[reducible, inline]
abbrev
CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelEvaluationExact
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
[Limits.HasZeroObject Y]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[Limits.HasZeroObject W]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
(corr : Correspondence X Y W)
:
Type (max (max u'' u) v')
Exactness of a correspondence in the kernel variable, with shift comparisons globally natural in the source object.
This is the Fourier--Mukai name for the generic Functor.ExactFamily carried
by kernelTransform. Its shift structure is Mathlib's ordinary CommShift
into the pointwise-shifted functor category, so source naturality and the
zero/addition coherences are part of that canonical interface.
Equations
- corr.KernelEvaluationExact = corr.kernelTransform.ExactFamily
Instances For
noncomputable def
CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelEvaluationExact.coneTriangleFunctor
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
[Limits.HasZeroObject Y]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[Limits.HasZeroObject W]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
{corr : Correspondence X Y W}
(h : corr.KernelEvaluationExact)
(E : X)
:
The pointwise transform-triangle functor obtained from a correspondence whose kernel-variable exactness has been chosen once.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelEvaluationExact.coneTriangleFunctor_obj₁
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
[Limits.HasZeroObject Y]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[Limits.HasZeroObject W]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
{corr : Correspondence X Y W}
(h : corr.KernelEvaluationExact)
(E : X)
(A : DGCategory.ConePresentation e.dgCat)
:
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelEvaluationExact.coneTriangleFunctor_obj₂
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
[Limits.HasZeroObject Y]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[Limits.HasZeroObject W]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
{corr : Correspondence X Y W}
(h : corr.KernelEvaluationExact)
(E : X)
(A : DGCategory.ConePresentation e.dgCat)
:
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelEvaluationExact.coneTriangleFunctor_obj₃
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
[Limits.HasZeroObject Y]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[Limits.HasZeroObject W]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
{corr : Correspondence X Y W}
(h : corr.KernelEvaluationExact)
(E : X)
(A : DGCategory.ConePresentation e.dgCat)
:
theorem
CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelEvaluationExact.coneTriangleFunctor_obj_distinguished
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
[Limits.HasZeroObject Y]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[Limits.HasZeroObject W]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
{corr : Correspondence X Y W}
(h : corr.KernelEvaluationExact)
[e.equiv.functor.IsTriangulated]
(E : X)
(A : DGCategory.ConePresentation e.dgCat)
:
Every pointwise transform triangle supplied by kernel-variable exactness is distinguished.
noncomputable def
CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelEvaluationExact.coneTriangleInSource
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
[Limits.HasZeroObject Y]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[Limits.HasZeroObject W]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
{corr : Correspondence X Y W}
(h : corr.KernelEvaluationExact)
(A : DGCategory.ConePresentation e.dgCat)
:
A fixed enhanced kernel cone gives a triangle of transform functors, natural in the source object.
This is the orientation needed by mutations and twists. The earlier
coneTriangleFunctor E is recovered by evaluating this functor at E; it is
retained because varying the cone presentation is useful independently.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelEvaluationExact.coneTriangleInSource_obj_obj₁
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
[Limits.HasZeroObject Y]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[Limits.HasZeroObject W]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
{corr : Correspondence X Y W}
(h : corr.KernelEvaluationExact)
(A : DGCategory.ConePresentation e.dgCat)
(E : X)
:
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelEvaluationExact.coneTriangleInSource_obj_obj₂
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
[Limits.HasZeroObject Y]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[Limits.HasZeroObject W]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
{corr : Correspondence X Y W}
(h : corr.KernelEvaluationExact)
(A : DGCategory.ConePresentation e.dgCat)
(E : X)
:
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelEvaluationExact.coneTriangleInSource_obj_obj₃
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
[Limits.HasZeroObject Y]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[Limits.HasZeroObject W]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
{corr : Correspondence X Y W}
(h : corr.KernelEvaluationExact)
(A : DGCategory.ConePresentation e.dgCat)
(E : X)
:
theorem
CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelEvaluationExact.coneTriangleInSource_obj
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
[Limits.HasZeroObject Y]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[Limits.HasZeroObject W]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
{corr : Correspondence X Y W}
(h : corr.KernelEvaluationExact)
(A : DGCategory.ConePresentation e.dgCat)
(E : X)
:
Evaluation of the source-natural transform triangle is the previously constructed pointwise image of the kernel cone.
theorem
CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelEvaluationExact.coneTriangleInSource_obj_distinguished
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
[Limits.HasZeroObject Y]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[Limits.HasZeroObject W]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
{corr : Correspondence X Y W}
(h : corr.KernelEvaluationExact)
[e.equiv.functor.IsTriangulated]
(A : DGCategory.ConePresentation e.dgCat)
(E : X)
:
Every member of the source-natural transform triangle is distinguished.
@[reducible, inline]
abbrev
CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelEvaluationExact.pointwiseDistinguishedTriangleProperty
{Y : Type u'}
[Category.{v', u'} Y]
[HasShift Y ℤ]
[Limits.HasZeroObject Y]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
:
The object property used as the codomain of an exact family of pointwise kernel-cone triangles.
Equations
Instances For
noncomputable def
CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelEvaluationExact.distinguishedConeTriangleFunctor
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
[Limits.HasZeroObject Y]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[Limits.HasZeroObject W]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
{corr : Correspondence X Y W}
(h : corr.KernelEvaluationExact)
[e.equiv.functor.IsTriangulated]
(E : X)
:
The pointwise kernel-cone functor with its codomain restricted to distinguished triangles. Consumers that need exact families can use this functor directly instead of carrying a separate objectwise proof.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelEvaluationExact.distinguishedConeTriangleFunctor_obj_val
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
[Limits.HasZeroObject Y]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[Limits.HasZeroObject W]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
{corr : Correspondence X Y W}
(h : corr.KernelEvaluationExact)
[e.equiv.functor.IsTriangulated]
(E : X)
(A : DGCategory.ConePresentation e.dgCat)
:
noncomputable def
CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelEvaluationExact.distinguishedConeTriangleInSource
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
[Limits.HasZeroObject Y]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[Limits.HasZeroObject W]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
{corr : Correspondence X Y W}
(h : corr.KernelEvaluationExact)
[e.equiv.functor.IsTriangulated]
(A : DGCategory.ConePresentation e.dgCat)
:
A fixed enhanced kernel cone as a source-indexed functor valued directly in distinguished triangles.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelEvaluationExact.distinguishedConeTriangleInSource_obj_val
{X : Type u}
{Y : Type u'}
{W : Type u''}
[Category.{v, u} X]
[Category.{v', u'} Y]
[Category.{v'', u''} W]
[HasShift Y ℤ]
[HasShift W ℤ]
(e : Enhancement W)
[e.equiv.functor.CommShift ℤ]
[Limits.HasZeroObject Y]
[Preadditive Y]
[∀ (n : ℤ), (shiftFunctor Y n).Additive]
[Pretriangulated Y]
[Limits.HasZeroObject W]
[Preadditive W]
[∀ (n : ℤ), (shiftFunctor W n).Additive]
[Pretriangulated W]
{corr : Correspondence X Y W}
(h : corr.KernelEvaluationExact)
[e.equiv.functor.IsTriangulated]
(A : DGCategory.ConePresentation e.dgCat)
(E : X)
: