Comparing presented dg and Fourier--Mukai cotwists #
Suppose a strict dg adjunction is presented on ordinary categories by a pair of Fourier--Mukai transforms. A chosen dg cone on its unit and an independently chosen enhanced Fourier--Mukai cone then give two pointwise distinguished unit triangles with the same first two vertices and the same first map.
Mathlib's isoTriangleOfIso₁₂ therefore supplies a noncanonical
isomorphism between the two triangles at each source object. Applying
invRotate gives the corresponding comparison between the conventional
cotwist triangles, with Mathlib retaining ownership of the sign and shift
cancellation. The first component compares the transported dg cotwist object
with the Fourier--Mukai cotwist object.
The unconditional completion chosen by isoTriangleOfIso₁₂ is made
separately at each object and therefore supplies no naturality. A separate
PresentedUnitComparisonData interface records a genuinely supplied natural
cone isomorphism and its two remaining triangle squares; from that input the
file constructs natural unit- and cotwist-triangle isomorphisms. It does not
construct this input or prove independence of either cone choice. Under an
explicit H⁰ equivalence hypothesis on the unshifted dg unit cone, the
comparison packages the selected shifted 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 conventional cotwist comparison; exactness
then transfers through Mathlib's existing Functor.isTriangulated_of_iso
theorem. Compatibility of the composite comparison from the actual shifted
dg cone is derived from that refinement rather than stored separately.
noncomputable def
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.presentedUnitTriangleObjIso
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eA.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : X)
:
At each object, the presented dg unit triangle is noncanonically isomorphic to the independently chosen Fourier--Mukai unit triangle.
The isomorphism is the identity on the identity and adjunction-composite
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.AdjunctionUnitKernelConeData.presentedUnitTriangleObjIso_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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eA.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : X)
:
The first component of the unit-triangle comparison is the identity.
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.presentedUnitTriangleObjIso_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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eA.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : X)
:
(presentedUnitTriangleObjIso adj H K S hE Z).hom.hom₂ = CategoryStruct.id (((C.transform P).comp (C'.transform Q)).obj Z)
The second component of the unit-triangle comparison is the identity.
noncomputable def
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.transportedUnitConeObjIso
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eA.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : X)
:
The resulting noncanonical objectwise comparison between the transported dg unit cone and the Fourier--Mukai unit cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.presentedCotwistTriangleObjIso
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eA.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : X)
:
Inverse rotation of the unit-triangle comparison gives a noncanonical objectwise comparison of the conventional cotwist triangles.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.presentedCotwistTriangleObjIso_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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eA.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : X)
:
The second component of the cotwist-triangle comparison is the identity.
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.presentedCotwistTriangleObjIso_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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eA.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : X)
:
(presentedCotwistTriangleObjIso adj H K S hE Z).hom.hom₃ = CategoryStruct.id (((C.transform P).comp (C'.transform Q)).obj Z)
The third component of the cotwist-triangle comparison is the identity.
noncomputable def
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.transportedCotwistObjIso
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eA.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : X)
:
The resulting noncanonical objectwise comparison between the transported dg cotwist and the Fourier--Mukai cotwist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.transportedDGCotwistObjIso
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
[eA.functor.IsTriangulated]
[e.equiv.functor.IsTriangulated]
(Z : X)
:
The actual shifted dg cone, after H⁰ and ordinary transport, is
noncanonically objectwise isomorphic to the Fourier--Mukai cotwist.
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.AdjunctionUnitKernelConeData.PresentedUnitComparisonData
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
:
Type (max uX vX)
The genuinely additional data required to supply a separate natural unit-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 unit-cone 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.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.ofConeIso
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(iso : K.transportedUnitCone eA ≅ S.cotwistCone)
(second : CategoryStruct.comp (H.compositeToTransportedUnitCone K) iso.hom = S.compositeToCotwistCone hE)
(third : H.transportedUnitConeToShiftedIdentity K = CategoryStruct.comp iso.hom (S.cotwistConeToShiftedIdentity hE))
:
PresentedUnitComparisonData adj H K S hE
Supply a natural comparison of the transported dg and Fourier--Mukai unit cones, together with exactly the two triangle-map squares not fixed by the common adjunction unit.
Equations
- CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.ofConeIso adj H K S hE iso second third = { thirdIso := iso, second := second, third := third }
Instances For
noncomputable def
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.presentedUnitTriangleIso
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
:
The supplied comparison data determine a natural isomorphism between the presented dg and Fourier--Mukai unit-triangle families.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.presentedUnitTriangleIso_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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
(Z : X)
:
The natural unit-triangle comparison is the identity on the identity vertex.
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.presentedUnitTriangleIso_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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
(Z : X)
:
((presentedUnitTriangleIso adj H K S hE N).hom.app Z).hom₂ = CategoryStruct.id (((C.transform P).comp (C'.transform Q)).obj Z)
The natural unit-triangle comparison is the identity on the adjunction composite vertex.
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.presentedUnitTriangleIso_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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
(Z : X)
:
The third component of the natural unit-triangle comparison is the supplied unit-cone isomorphism.
noncomputable def
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.transportedUnitConeIso
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
:
The supplied natural isomorphism between the two unshifted unit-cone functors.
Equations
Instances For
noncomputable def
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.presentedCotwistTriangleIso
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
:
Inverse rotation upgrades the natural unit-triangle comparison to a natural comparison of the conventional cotwist triangles.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.presentedCotwistTriangleIso_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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
(Z : X)
:
The natural cotwist-triangle comparison is the identity on its identity vertex.
@[simp]
theorem
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.presentedCotwistTriangleIso_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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
(Z : X)
:
((presentedCotwistTriangleIso adj H K S hE N).hom.app Z).hom₃ = CategoryStruct.id (((C.transform P).comp (C'.transform Q)).obj Z)
The natural cotwist-triangle comparison is the identity on its adjunction composite vertex.
noncomputable def
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.transportedCotwistIso
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
:
The induced natural isomorphism from the conventional transported dg cotwist to the Fourier--Mukai cotwist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.transportedDGCotwistIso
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
:
The transport of the actual shifted dg unit cone is naturally isomorphic to the Fourier--Mukai cotwist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.transportedCotwist_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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
:
E.IsKernelFunctor (K.transportedCotwist eA)
The conventional transported dg cotwist is a kernel functor once a natural comparison with the selected Fourier--Mukai cotwist has been supplied.
theorem
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.transportedDGCotwist_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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
:
E.IsKernelFunctor (K.transportedDGCotwist eA)
The transport of the actual shifted dg unit cone is a kernel functor through the composite natural comparison.
theorem
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.cotwist_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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
(hK : (DGAdjunction.UnitConeData.unitCone adj K).h0.IsEquivalence)
:
An explicit equivalence hypothesis on H⁰ of the unshifted dg unit cone
transfers to the selected conventional Fourier--Mukai cotwist.
@[reducible]
noncomputable def
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.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]
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
(hK : (DGAdjunction.UnitConeData.unitCone adj K).h0.IsEquivalence)
:
The selected shifted cotwist kernel, packaged as a kernel autoequivalence
under the explicit equivalence hypothesis on H⁰ of the unshifted dg unit
cone.
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.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
:
Type (max uX vX)
The cotwist-specific specialization of the shared comparison-shift
package. The source is fixed to the canonical sign-correct shift structure on
the conventional pointwise [-1] cotwist. Compatibility of the intermediate
comparison from the actual shifted dg cone is derived canonically and is not
stored here.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[implicit_reducible]
noncomputable def
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.ShiftCompatibility.instCommShiftTransportedCotwistInt
{A : Type uA}
{B : Type uB}
{X : Type uX}
[DGCategory A]
[DGCategory B]
[Category.{vX, uX} X]
{L : DGFunctor A B}
{R : DGFunctor B A}
{eA : H0 A ≌ X}
[IsPretriangulated A]
[HasShift X ℤ]
[Preadditive X]
[∀ (n : ℤ), (shiftFunctor X n).Additive]
[eA.functor.CommShift ℤ]
(adj : DGAdjunction L R)
(K : adj.UnitConeData)
:
(K.transportedCotwist eA).CommShift ℤ
The sign-correct shift structure on the conventional pointwise [-1] cotwist.
Equations
Instances For
@[reducible, inline]
abbrev
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.ShiftCompatibility.cotwistCommShift
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
(h : ShiftCompatibility adj H K S hE N)
:
The selected shift structure on the Fourier--Mukai cotwist.
Equations
Instances For
@[reducible, inline]
abbrev
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.ShiftCompatibility.transportedCotwistIso_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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
(h : ShiftCompatibility adj H K S hE N)
:
NatTrans.CommShift (transportedCotwistIso adj H K S hE N).hom ℤ
The conventional cotwist comparison respects its selected source and target shift structures.
Equations
- ⋯ = ⋯
Instances For
theorem
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.ShiftCompatibility.transportedDGCotwistIso_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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
(h : ShiftCompatibility adj H K S hE N)
[eA.functor.Additive]
:
NatTrans.CommShift (transportedDGCotwistIso adj H K S hE N).hom ℤ
The composite comparison from the actual shifted dg cotwist to the Fourier--Mukai cotwist respects the canonical source shift package and the selected Fourier--Mukai shift package.
theorem
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.ShiftCompatibility.cotwistIsTriangulated
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
(h : ShiftCompatibility adj H K S hE N)
[eA.functor.IsTriangulated]
:
The Fourier--Mukai cotwist is triangulated relative to the selected target shift structure when the conventional cotwist comparison respects shifts.
theorem
CategoryTheory.Triangulated.FourierMukai.AdjunctionUnitKernelConeData.PresentedUnitComparisonData.ShiftCompatibility.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]
{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 X X W}
{P : W₁}
{Q : W₂}
{e : Enhancement W}
{D : ConvolutionData C C' E}
{U : 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 ℤ]
(adj : DGAdjunction L R)
(H : DGAdjunction.H0Presentation eA eB (C.transform P) (C'.transform Q))
(K : adj.UnitConeData)
(S : AdjunctionUnitKernelConeData C C' E e P (RightAdjointKernelData.ofH0Presentation H adj) D U)
(hE : E.KernelEvaluationExact)
(N : PresentedUnitComparisonData adj H K S hE)
(h : ShiftCompatibility adj H K S hE N)
[eA.functor.IsTriangulated]
(hK : (DGAdjunction.UnitConeData.unitCone adj K).h0.IsEquivalence)
:
(cotwistKernelAutoequivalence adj H K S hE N hK).equiv.IsTriangulated
The kernel autoequivalence of the selected Fourier--Mukai cotwist is an exact equivalence relative to the selected target shift package.