Comparing presented dg and Fourier--Mukai twists #
Suppose a strict dg adjunction is presented on ordinary categories by a pair of Fourier--Mukai transforms. A chosen dg cone on its counit and an independently chosen enhanced Fourier--Mukai cone then give two pointwise distinguished counit triangles with the same first two vertices and the same first map.
Mathlib's isoTriangleOfIso₁₂ supplies a noncanonical isomorphism between
the two triangles at each target object. Its third component compares the
ordinary transport of the actual dg twist with the Fourier--Mukai twist.
The unconditional completion is chosen separately at each object and
therefore supplies no naturality. A separate PresentedCounitComparisonData
interface records a genuinely supplied natural twist isomorphism and its two
remaining triangle squares; from that input the file constructs the natural
counit-triangle isomorphism. It does not construct this input or prove
independence of either cone choice. Under an explicit equivalence hypothesis
on the dg twist at H⁰, the comparison packages the selected kernel as a
KernelAutoequivalence; it does not prove that hypothesis or sphericality. A
further ShiftCompatibility
refinement can select a Fourier--Mukai CommShift structure compatible with
the comparison; exactness then transfers through Mathlib's existing
Functor.isTriangulated_of_iso theorem.
noncomputable def
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.presentedCounitTriangleObjIso
{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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eB.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : Y)
:
At each target object, the presented dg counit triangle is noncanonically isomorphic to the independently chosen Fourier--Mukai counit triangle.
The isomorphism is the identity on the adjunction-composite and identity
vertices. Its third component is the choice made by triangulated-category
completion and is not asserted to be natural in Z.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.presentedCounitTriangleObjIso_hom_hom₁
{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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eB.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : Y)
:
(presentedCounitTriangleObjIso adj H K S hE Z).hom.hom₁ = CategoryStruct.id (((C'.transform Q).comp (C.transform P)).obj Z)
The first component of the counit-triangle comparison is the identity.
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.presentedCounitTriangleObjIso_hom_hom₂
{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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eB.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : Y)
:
The second component of the counit-triangle comparison is the identity.
noncomputable def
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.transportedTwistObjIso
{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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eB.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : Y)
:
The resulting noncanonical objectwise comparison between the transported actual dg twist and the Fourier--Mukai twist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Supplied natural comparison data #
@[reducible, inline]
abbrev
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.PresentedCounitComparisonData
{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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
:
Type (max uY vY)
The genuinely additional data required to supply a separate natural counit-cone comparison of the same triangle families considered objectwise above.
This is a semantic abbreviation of the generic comparison between two first-map normalizations. It stores a natural isomorphism of the twist functors and compatibility with the two remaining triangle maps.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.PresentedCounitComparisonData.ofTwistIso
{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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(iso : K.transportedTwist eB ≅ S.twist)
(second : CategoryStruct.comp (H.counitToTransportedTwist K) iso.hom = S.counitToTwist hE)
(third : H.transportedTwistToShiftedComposite K = CategoryStruct.comp iso.hom (S.twistToShiftedComposite hE))
:
PresentedCounitComparisonData adj H K S hE
Supply a natural comparison of the transported dg and Fourier--Mukai twists, together with exactly the two triangle-map squares not fixed by the common adjunction counit.
Equations
- CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.PresentedCounitComparisonData.ofTwistIso adj H K S hE iso second third = { thirdIso := iso, second := second, third := third }
Instances For
noncomputable def
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.PresentedCounitComparisonData.presentedCounitTriangleIso
{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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedCounitComparisonData adj H K S hE)
:
The supplied comparison data determine a natural isomorphism between the presented dg and Fourier--Mukai counit-triangle families.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.PresentedCounitComparisonData.presentedCounitTriangleIso_hom_app_hom₁
{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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedCounitComparisonData adj H K S hE)
(Z : Y)
:
((presentedCounitTriangleIso adj H K S hE N).hom.app Z).hom₁ = CategoryStruct.id (((C'.transform Q).comp (C.transform P)).obj Z)
The natural counit-triangle comparison is the identity on the adjunction composite vertex.
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.PresentedCounitComparisonData.presentedCounitTriangleIso_hom_app_hom₂
{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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedCounitComparisonData adj H K S hE)
(Z : Y)
:
The natural counit-triangle comparison is the identity on the identity vertex.
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.PresentedCounitComparisonData.presentedCounitTriangleIso_hom_app_hom₃
{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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedCounitComparisonData adj H K S hE)
(Z : Y)
:
The third component of the natural counit-triangle comparison is the supplied twist isomorphism.
noncomputable def
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.PresentedCounitComparisonData.transportedTwistIso
{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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedCounitComparisonData adj H K S hE)
:
The induced natural isomorphism from the transported actual dg twist to the Fourier--Mukai twist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.PresentedCounitComparisonData.transportedTwistIso_hom
{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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedCounitComparisonData adj H K S hE)
:
The projected twist isomorphism is the third-vertex isomorphism supplied by the endpoint-strict comparison data.
theorem
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.PresentedCounitComparisonData.transportedTwist_isKernelFunctor
{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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedCounitComparisonData adj H K S hE)
:
E.IsKernelFunctor (K.transportedTwist eB)
The transported actual dg twist is a kernel functor once a natural comparison with the selected Fourier--Mukai twist has been supplied.
theorem
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.PresentedCounitComparisonData.twist_isEquivalence
{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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedCounitComparisonData adj H K S hE)
(hK : (DGAdjunction.CounitConeData.twist adj K).h0.IsEquivalence)
:
An explicit equivalence hypothesis on H⁰ of the dg twist transfers to the
selected Fourier--Mukai twist through the supplied natural comparison.
@[reducible]
noncomputable def
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.PresentedCounitComparisonData.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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedCounitComparisonData adj H K S hE)
(hK : (DGAdjunction.CounitConeData.twist adj K).h0.IsEquivalence)
:
The selected twist kernel, packaged as a kernel autoequivalence under the
explicit equivalence hypothesis on H⁰ of the dg twist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Compatibility with selected shift structures #
@[reducible, inline]
abbrev
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.PresentedCounitComparisonData.ShiftCompatibility
{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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedCounitComparisonData adj H K S hE)
:
Type (max uY vY)
The twist-specific specialization of the shared comparison-shift package.
The source is fixed to the canonical shift structure on the transported H⁰
dg twist; the target structure remains independently selected by the
realization.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[implicit_reducible]
noncomputable def
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.PresentedCounitComparisonData.ShiftCompatibility.instCommShiftTransportedTwistInt
{A : Type uA}
{B : Type uB}
{Y : Type uY}
[DGCategory A]
[DGCategory B]
[Category.{vY, uY} Y]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eB : H0 B ≌ Y}
[IsPretriangulated B]
[HasShift Y ℤ]
[eB.functor.CommShift ℤ]
(adj : DGAdjunction L R)
(K : adj.CounitConeData)
:
(K.transportedTwist eB).CommShift ℤ
The selected transported H⁰ shift structure on the dg twist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.PresentedCounitComparisonData.ShiftCompatibility.twistCommShift
{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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedCounitComparisonData adj H K S hE)
(h : ShiftCompatibility adj H K S hE N)
:
The selected shift structure on the Fourier--Mukai twist.
Equations
Instances For
@[reducible, inline]
abbrev
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.PresentedCounitComparisonData.ShiftCompatibility.transportedTwistIso_commShift
{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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedCounitComparisonData adj H K S hE)
(h : ShiftCompatibility adj H K S hE N)
:
NatTrans.CommShift (transportedTwistIso adj H K S hE N).hom ℤ
The twist comparison respects its selected source and target shift structures.
Equations
- ⋯ = ⋯
Instances For
theorem
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.PresentedCounitComparisonData.ShiftCompatibility.twistIsTriangulated
{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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedCounitComparisonData adj H K S hE)
(h : ShiftCompatibility adj H K S hE N)
[eB.functor.IsTriangulated]
:
The Fourier--Mukai twist is triangulated relative to the selected target shift structure when the supplied comparison respects shifts.
theorem
CategoryTheory.Triangulated.FourierMukai.CounitKernelConeData.PresentedCounitComparisonData.ShiftCompatibility.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]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
{eB : H0 B ≌ Y}
{C : Correspondence X Y W₁}
{C' : Correspondence Y X W₂}
{E : Correspondence Y Y W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C' C E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.CounitConeData)
(S : CounitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedCounitComparisonData adj H K S hE)
(h : ShiftCompatibility adj H K S hE N)
[eB.functor.IsTriangulated]
(hK : (DGAdjunction.CounitConeData.twist adj K).h0.IsEquivalence)
:
(twistKernelAutoequivalence adj H K S hE N hK).equiv.IsTriangulated
The kernel autoequivalence of the selected Fourier--Mukai twist is an exact equivalence relative to the selected target shift package.