Normalizing transformed kernel cones

A fixed enhanced kernel cone gives a source-natural triangle whose first two vertices are transforms of the enhancement's chosen endpoint lifts. Concrete applications usually present those transforms by more meaningful functors and identify the first map with a named natural transformation.

Correspondence.KernelConeNormalizationData packages exactly that endpoint comparison square. Together with exactness in the kernel variable, it transports the raw cone triangle to a source-natural triangle with literal first map and literal first two vertices. The categorical transport is delegated to Triangle.FirstMapNormalizationData; this file retains the kernel-specific cone, enhancement, and shift comparisons.

The result is only a family of pointwise distinguished triangles. It does not give a distinguished triangle in a functor category, make the third functor exact, or compare different enhanced arrows or cone choices. The selected cone nevertheless has a reusable shifted-kernel presentation: shift it first in the enhancement's homotopy category, compare that kernel with the ordinary shift through the enhancement equivalence, and then use the kernel family's existing CommShift comparison. No parallel shift structure is introduced.

structure CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] (corr : Correspondence X Y W) (e : Enhancement W) (A : DGCategory.ConePresentation e.dgCat) (F G : Functor X Y) (α : F ⟶ G) : Type (max uX vY)

Endpoint data identifying the transformed arrow of an enhanced kernel cone with a named natural transformation between literal functors.

The isomorphisms point from the raw endpoint transforms to the literal functors, so square is exactly the first square needed to compare the raw cone triangle with its normalized form.

• sourceIso : corr.transform (e.equiv.functor.obj A.source) ≅ F

  Comparison from the raw source transform to the literal source functor.

• targetIso : corr.transform (e.equiv.functor.obj A.target) ≅ G

  Comparison from the raw target transform to the literal target functor.

• square : CategoryStruct.comp (corr.transformMap (e.equiv.functor.map (H0.homMk A.arrow))) self.targetIso.hom = CategoryStruct.comp self.sourceIso.hom α

  The transformed enhanced arrow is the named natural transformation after the endpoint comparisons.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.coneKernel {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) : W

The ordinary kernel represented by the selected enhanced cone.

Equations

• N.coneKernel = e.equiv.functor.obj (have this := A.cone; this)

@[reducible, inline]

abbrev CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.coneTransform {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) : Functor X Y

The transform of the selected cone, with no application-specific name.

Equations

• N.coneTransform = corr.transform N.coneKernel

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.shiftedConeKernel {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) (n : ℤ) : W

The kernel obtained by shifting the selected cone in the enhancement's homotopy category before transporting it to the ordinary kernel category.

Equations

• N.shiftedConeKernel n = e.equiv.functor.obj ((CategoryTheory.shiftFunctor (CategoryTheory.H0 e.dgCat) n).obj (have this := A.cone; this))

noncomputable def CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.shiftedConeKernelIso {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [HasShift W ℤ] [e.equiv.functor.CommShift ℤ] (n : ℤ) : N.shiftedConeKernel n ≅ (shiftFunctor W n).obj N.coneKernel

The enhancement comparison identifies the transported shifted cone with the shift of its transported ordinary kernel.

Equations

• N.shiftedConeKernelIso n = (CategoryTheory.Functor.commShiftIso e.equiv.functor n).app (have this := A.cone; this)

noncomputable def CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.shiftedConeTransformIso {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [HasShift Y ℤ] [HasShift W ℤ] [e.equiv.functor.CommShift ℤ] (hShift : corr.kernelTransform.CommShift ℤ) (n : ℤ) : corr.transform (N.shiftedConeKernel n) ≅ (shiftFunctor (Functor X Y) n).obj N.coneTransform

A shift-coherent kernel family presents the shifted cone transform by the shifted enhanced cone kernel.

The CommShift structure is passed explicitly because an ExactFamily stores it as data; this avoids installing a competing global instance.

Equations

• N.shiftedConeTransformIso hShift n = corr.transformMapIso (N.shiftedConeKernelIso n) ≪≫ (CategoryTheory.Functor.commShiftIso corr.kernelTransform n).app N.coneKernel

noncomputable def CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.rawTriangle {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) : Functor X (Pretriangulated.Triangle Y)

The unnormalized source-natural triangle obtained by transforming the enhanced kernel cone.

Equations

• N.rawTriangle h = CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelEvaluationExact.coneTriangleInSource e h A

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.rawTriangle_obj₁ {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) (E : X) : ((N.rawTriangle h).obj E).obj₁ = (corr.transform (e.equiv.functor.obj A.source)).obj E

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.rawTriangle_obj₂ {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) (E : X) : ((N.rawTriangle h).obj E).obj₂ = (corr.transform (e.equiv.functor.obj A.target)).obj E

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.rawTriangle_obj₃ {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) (E : X) : ((N.rawTriangle h).obj E).obj₃ = N.coneTransform.obj E

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.rawTriangle_mor₁ {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) : (N.rawTriangle h).whiskerLeft Pretriangulated.Triangle.π₁Toπ₂ = corr.transformMap (e.equiv.functor.map (H0.homMk A.arrow))

The first map of the raw transform triangle.

noncomputable def CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.rawTriangleObj₁Iso {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) : (N.rawTriangle h).comp Pretriangulated.Triangle.π₁ ≅ F

The source comparison typed against the first projection of the raw triangle functor.

Equations

• N.rawTriangleObj₁Iso h = id N.sourceIso

noncomputable def CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.rawTriangleObj₂Iso {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) : (N.rawTriangle h).comp Pretriangulated.Triangle.π₂ ≅ G

The target comparison typed against the second projection of the raw triangle functor.

Equations

• N.rawTriangleObj₂Iso h = id N.targetIso

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.rawTriangle_square {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) : CategoryStruct.comp ((N.rawTriangle h).whiskerLeft Pretriangulated.Triangle.π₁Toπ₂) (N.rawTriangleObj₂Iso h).hom = CategoryStruct.comp (N.rawTriangleObj₁Iso h).hom α

The first comparison square, stated against the raw triangle functor.

noncomputable def CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.firstMapNormalizationData {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) : Pretriangulated.Triangle.FirstMapNormalizationData (N.rawTriangle h) F G α

Forget the kernel origin and retain exactly the categorical data needed to normalize the first map of the raw triangle family.

Equations

• N.firstMapNormalizationData h = { obj₁Iso := N.rawTriangleObj₁Iso h, obj₂Iso := N.rawTriangleObj₂Iso h, square := ⋯ }

noncomputable def CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.normalizedSecond {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) : G ⟶ N.coneTransform

The transported second map from the literal target functor to the cone transform.

Equations

• N.normalizedSecond h = (N.firstMapNormalizationData h).normalizedSecond

noncomputable def CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.normalizedThird {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) : N.coneTransform ⟶ F.comp (shiftFunctor Y 1)

The transported connecting map from the cone transform to the shifted literal source functor.

Equations

• N.normalizedThird h = (N.firstMapNormalizationData h).normalizedThird

noncomputable def CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.normalizedTriangle {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) : Functor X (Pretriangulated.Triangle Y)

The normalized source-natural triangle with literal first map and literal first two vertices.

Equations

• N.normalizedTriangle h = (N.firstMapNormalizationData h).normalizedTriangle

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.normalizedTriangle_obj₁ {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) (E : X) : ((N.normalizedTriangle h).obj E).obj₁ = F.obj E

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.normalizedTriangle_obj₂ {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) (E : X) : ((N.normalizedTriangle h).obj E).obj₂ = G.obj E

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.normalizedTriangle_obj₃ {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) (E : X) : ((N.normalizedTriangle h).obj E).obj₃ = N.coneTransform.obj E

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.normalizedTriangle_mor₁ {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) (E : X) : ((N.normalizedTriangle h).obj E).mor₁ = α.app E

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.normalizedTriangle_mor₂ {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) (E : X) : ((N.normalizedTriangle h).obj E).mor₂ = (N.normalizedSecond h).app E

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.normalizedTriangle_mor₃ {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) (E : X) : ((N.normalizedTriangle h).obj E).mor₃ = (N.normalizedThird h).app E

noncomputable def CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.rawTriangleIsoNormalized {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) : N.rawTriangle h ≅ N.normalizedTriangle h

The raw transform triangle and its endpoint-normalized form are naturally isomorphic.

Equations

• N.rawTriangleIsoNormalized h = (N.firstMapNormalizationData h).rawIsoNormalized

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.rawTriangleIsoNormalized_hom_app_hom₁ {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) (E : X) : ((N.rawTriangleIsoNormalized h).hom.app E).hom₁ = (N.rawTriangleObj₁Iso h).hom.app E

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.rawTriangleIsoNormalized_hom_app_hom₂ {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) (E : X) : ((N.rawTriangleIsoNormalized h).hom.app E).hom₂ = (N.rawTriangleObj₂Iso h).hom.app E

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.rawTriangleIsoNormalized_hom_app_hom₃ {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) (E : X) : ((N.rawTriangleIsoNormalized h).hom.app E).hom₃ = CategoryStruct.id ((N.rawTriangle h).obj E).obj₃

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.normalizedTriangle_obj_distinguished {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) [e.equiv.functor.IsTriangulated] (E : X) : (N.normalizedTriangle h).obj E ∈ Pretriangulated.distinguishedTriangles

Every value of the normalized triangle is distinguished.

noncomputable def CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.distinguishedNormalizedTriangle {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) [e.equiv.functor.IsTriangulated] : Functor X KernelEvaluationExact.pointwiseDistinguishedTriangleProperty.FullSubcategory

The normalized family with codomain restricted to distinguished triangles.

Equations

• N.distinguishedNormalizedTriangle h = CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelEvaluationExact.pointwiseDistinguishedTriangleProperty.lift (N.normalizedTriangle h) ⋯

@[simp]

theorem CategoryTheory.Triangulated.FourierMukai.Correspondence.KernelConeNormalizationData.distinguishedNormalizedTriangle_obj_val {X : Type uX} {Y : Type uY} {W : Type uW} [Category.{vX, uX} X] [Category.{vY, uY} Y] [Category.{vW, uW} W] {corr : Correspondence X Y W} {e : Enhancement W} {A : DGCategory.ConePresentation e.dgCat} {F G : Functor X Y} {α : F ⟶ G} (N : corr.KernelConeNormalizationData e A F G α) [Limits.HasZeroObject Y] [HasShift Y ℤ] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [Limits.HasZeroObject W] [HasShift W ℤ] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.CommShift ℤ] (h : corr.KernelEvaluationExact) [e.equiv.functor.IsTriangulated] (E : X) : ((N.distinguishedNormalizedTriangle h).obj E).obj = (N.normalizedTriangle h).obj E