Presenting dg-adjunction cone triangles on ordinary categories

A strict dg adjunction and a choice of cones for its counit give a natural family of distinguished triangles on the target homotopy category. A DGAdjunction.H0Presentation identifies the transported left and right functors with named ordinary functors F and G on categories X and Y.

This file transports the raw dg counit triangle through the target equivalence and feeds its endpoint comparisons to Triangle.FirstMapNormalizationData. The resulting family has literal first map (P.toAdjunction A).counit : G ⋙ F ⟶ 𝟭 Y, literal first two vertices, and the transported dg twist as its unchanged third vertex.

For the counit side, the target equivalence's CommShift and triangulatedness are supplied where needed; for the unit side, the corresponding data are supplied on the source equivalence. A plain category equivalence provides neither. The construction does not identify the transported dg twist with an independently chosen ordinary or Fourier--Mukai twist, make it exact, or assert sphericality.

The unit-side mirror transports the raw dg unit-cone triangle through the source equivalence and normalizes it to have literal first map (P.toAdjunction A).unit : 𝟭 X ⟶ F ⋙ G. Its third vertex is the transported unshifted unit cone. No inverse rotation or identification with the conventional [-1] cotwist is performed here.

@[reducible, inline]

noncomputable abbrev CategoryTheory.DGAdjunction.CounitConeData.transportedTwist {C : Type uC} {D : Type uD} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {A : DGAdjunction L R} (K : A.CounitConeData) (eD : H0 D ≌ Y) : Functor Y Y

The dg counit cone functor transported from H⁰ D to the ordinary target category. No exactness is asserted.

Equations

• K.transportedTwist eD = eD.inverse.comp ((CategoryTheory.DGAdjunction.CounitConeData.twist A K).h0.comp eD.functor)

noncomputable def CategoryTheory.DGAdjunction.CounitConeData.rawTransportedTwistTriangle {C : Type uC} {D : Type uD} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eD : H0 D ≌ Y} {A : DGAdjunction L R} [IsPretriangulated D] (K : A.CounitConeData) [HasShift Y ℤ] [eD.functor.CommShift ℤ] : Functor Y (Pretriangulated.Triangle Y)

The raw dg counit triangle, reindexed along the target equivalence and mapped to the ordinary target category.

Equations

• K.rawTransportedTwistTriangle = (eD.inverse.comp (CategoryTheory.DGAdjunction.CounitConeData.twistTriangleFunctor A K)).comp eD.functor.mapTriangle

@[simp]

theorem CategoryTheory.DGAdjunction.CounitConeData.rawTransportedTwistTriangle_obj_obj₃ {C : Type uC} {D : Type uD} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eD : H0 D ≌ Y} {A : DGAdjunction L R} [IsPretriangulated D] (K : A.CounitConeData) [HasShift Y ℤ] [eD.functor.CommShift ℤ] (Z : Y) : (K.rawTransportedTwistTriangle.obj Z).obj₃ = (K.transportedTwist eD).obj Z

@[simp]

theorem CategoryTheory.DGAdjunction.CounitConeData.rawTransportedTwistTriangle_obj_mor₁ {C : Type uC} {D : Type uD} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eD : H0 D ≌ Y} {A : DGAdjunction L R} [IsPretriangulated D] (K : A.CounitConeData) [HasShift Y ℤ] [eD.functor.CommShift ℤ] (Z : Y) : (K.rawTransportedTwistTriangle.obj Z).mor₁ = eD.functor.map (A.h0Counit.app (eD.inverse.obj Z))

noncomputable def CategoryTheory.DGAdjunction.CounitConeData.rawTransportedTwistTriangleObj₂Iso {C : Type uC} {D : Type uD} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eD : H0 D ≌ Y} {A : DGAdjunction L R} [IsPretriangulated D] (K : A.CounitConeData) [HasShift Y ℤ] [eD.functor.CommShift ℤ] : K.rawTransportedTwistTriangle.comp Pretriangulated.Triangle.π₂ ≅ Functor.id Y

The second projection of the raw transported dg counit triangle, identified with the identity functor of the ordinary target category.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.DGAdjunction.CounitConeData.rawTransportedTwistTriangleObj₂Iso_hom_app {C : Type uC} {D : Type uD} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eD : H0 D ≌ Y} {A : DGAdjunction L R} [IsPretriangulated D] (K : A.CounitConeData) [HasShift Y ℤ] [eD.functor.CommShift ℤ] (Z : Y) : K.rawTransportedTwistTriangleObj₂Iso.hom.app Z = eD.counit.app Z

theorem CategoryTheory.DGAdjunction.CounitConeData.rawTransportedTwistTriangle_obj_distinguished {C : Type uC} {D : Type uD} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eD : H0 D ≌ Y} {A : DGAdjunction L R} [IsPretriangulated D] (K : A.CounitConeData) [HasShift Y ℤ] [eD.functor.CommShift ℤ] [Limits.HasZeroObject Y] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [eD.functor.IsTriangulated] (Z : Y) : K.rawTransportedTwistTriangle.obj Z ∈ Pretriangulated.distinguishedTriangles

Every value of the transported raw dg counit triangle is distinguished when the target equivalence is triangulated.

@[reducible, inline]

noncomputable abbrev CategoryTheory.DGAdjunction.UnitConeData.transportedUnitCone {C : Type uC} {D : Type uD} {X : Type uX} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] {L : DGFunctor C D} {R : DGFunctor D C} {A : DGAdjunction L R} (K : A.UnitConeData) (eC : H0 C ≌ X) : Functor X X

The dg unit-cone functor transported from H⁰ C to the ordinary source category. This is the unshifted cone; no cotwist shift or exactness is asserted.

Equations

• K.transportedUnitCone eC = eC.inverse.comp ((CategoryTheory.DGAdjunction.UnitConeData.unitCone A K).h0.comp eC.functor)

noncomputable def CategoryTheory.DGAdjunction.UnitConeData.rawTransportedUnitTriangle {C : Type uC} {D : Type uD} {X : Type uX} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {A : DGAdjunction L R} [IsPretriangulated C] (K : A.UnitConeData) [HasShift X ℤ] [eC.functor.CommShift ℤ] : Functor X (Pretriangulated.Triangle X)

The raw dg unit triangle, reindexed along the source equivalence and mapped to the ordinary source category.

Equations

• K.rawTransportedUnitTriangle = (eC.inverse.comp (CategoryTheory.DGAdjunction.UnitConeData.unitTriangleFunctor A K)).comp eC.functor.mapTriangle

@[simp]

theorem CategoryTheory.DGAdjunction.UnitConeData.rawTransportedUnitTriangle_obj_obj₃ {C : Type uC} {D : Type uD} {X : Type uX} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {A : DGAdjunction L R} [IsPretriangulated C] (K : A.UnitConeData) [HasShift X ℤ] [eC.functor.CommShift ℤ] (Z : X) : (K.rawTransportedUnitTriangle.obj Z).obj₃ = (K.transportedUnitCone eC).obj Z

@[simp]

theorem CategoryTheory.DGAdjunction.UnitConeData.rawTransportedUnitTriangle_obj_mor₁ {C : Type uC} {D : Type uD} {X : Type uX} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {A : DGAdjunction L R} [IsPretriangulated C] (K : A.UnitConeData) [HasShift X ℤ] [eC.functor.CommShift ℤ] (Z : X) : (K.rawTransportedUnitTriangle.obj Z).mor₁ = eC.functor.map (A.h0Unit.app (eC.inverse.obj Z))

noncomputable def CategoryTheory.DGAdjunction.UnitConeData.rawTransportedUnitTriangleObj₁Iso {C : Type uC} {D : Type uD} {X : Type uX} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {A : DGAdjunction L R} [IsPretriangulated C] (K : A.UnitConeData) [HasShift X ℤ] [eC.functor.CommShift ℤ] : K.rawTransportedUnitTriangle.comp Pretriangulated.Triangle.π₁ ≅ Functor.id X

The first projection of the raw transported dg unit triangle, identified with the identity functor of the ordinary source category.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.DGAdjunction.UnitConeData.rawTransportedUnitTriangleObj₁Iso_hom_app {C : Type uC} {D : Type uD} {X : Type uX} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {A : DGAdjunction L R} [IsPretriangulated C] (K : A.UnitConeData) [HasShift X ℤ] [eC.functor.CommShift ℤ] (Z : X) : K.rawTransportedUnitTriangleObj₁Iso.hom.app Z = eC.counit.app Z

theorem CategoryTheory.DGAdjunction.UnitConeData.rawTransportedUnitTriangle_obj_distinguished {C : Type uC} {D : Type uD} {X : Type uX} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {A : DGAdjunction L R} [IsPretriangulated C] (K : A.UnitConeData) [HasShift X ℤ] [eC.functor.CommShift ℤ] [Limits.HasZeroObject X] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [eC.functor.IsTriangulated] (Z : X) : K.rawTransportedUnitTriangle.obj Z ∈ Pretriangulated.distinguishedTriangles

Every value of the transported raw dg unit triangle is distinguished when the source equivalence is triangulated.

noncomputable def CategoryTheory.DGAdjunction.H0Presentation.counitTriangleObj₁Iso {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated D] [HasShift Y ℤ] [eD.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.CounitConeData) : K.rawTransportedTwistTriangle.comp Pretriangulated.Triangle.π₁ ≅ G.comp F

The first projection of the raw transported dg counit triangle, identified with the composite of the named presented right and left adjoints.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.DGAdjunction.H0Presentation.counitFirstMapNormalizationData {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated D] [HasShift Y ℤ] [eD.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.CounitConeData) : Pretriangulated.Triangle.FirstMapNormalizationData K.rawTransportedTwistTriangle (G.comp F) (Functor.id Y) (P.toAdjunction A).counit

The generic first-map normalization data for the transported dg counit triangle. Its named first map is exactly the counit of the ordinary adjunction constructed by P.

Equations

• P.counitFirstMapNormalizationData K = { obj₁Iso := P.counitTriangleObj₁Iso K, obj₂Iso := K.rawTransportedTwistTriangleObj₂Iso, square := ⋯ }

noncomputable def CategoryTheory.DGAdjunction.H0Presentation.counitToTransportedTwist {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated D] [HasShift Y ℤ] [eD.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.CounitConeData) : Functor.id Y ⟶ K.transportedTwist eD

The second map of the presented counit triangle, from the identity to the transported dg twist.

Equations

• P.counitToTransportedTwist K = (P.counitFirstMapNormalizationData K).normalizedSecond

noncomputable def CategoryTheory.DGAdjunction.H0Presentation.transportedTwistToShiftedComposite {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated D] [HasShift Y ℤ] [eD.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.CounitConeData) : K.transportedTwist eD ⟶ (G.comp F).comp (shiftFunctor Y 1)

The connecting map of the presented counit triangle, from the transported dg twist to the shift of the presented adjunction composite.

Equations

• P.transportedTwistToShiftedComposite K = (P.counitFirstMapNormalizationData K).normalizedThird

noncomputable def CategoryTheory.DGAdjunction.H0Presentation.presentedCounitTriangle {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated D] [HasShift Y ℤ] [eD.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.CounitConeData) : Functor Y (Pretriangulated.Triangle Y)

The presented ordinary counit triangle G F ⟶ 𝟭 Y ⟶ transportedTwist ⟶ (G F)⟦1⟧.

Equations

• P.presentedCounitTriangle K = (P.counitFirstMapNormalizationData K).normalizedTriangle

@[simp]

theorem CategoryTheory.DGAdjunction.H0Presentation.presentedCounitTriangle_obj₁ {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated D] [HasShift Y ℤ] [eD.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.CounitConeData) (Z : Y) : ((P.presentedCounitTriangle K).obj Z).obj₁ = (G.comp F).obj Z

@[simp]

theorem CategoryTheory.DGAdjunction.H0Presentation.presentedCounitTriangle_obj₂ {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated D] [HasShift Y ℤ] [eD.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.CounitConeData) (Z : Y) : ((P.presentedCounitTriangle K).obj Z).obj₂ = Z

@[simp]

theorem CategoryTheory.DGAdjunction.H0Presentation.presentedCounitTriangle_obj₃ {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated D] [HasShift Y ℤ] [eD.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.CounitConeData) (Z : Y) : ((P.presentedCounitTriangle K).obj Z).obj₃ = (K.transportedTwist eD).obj Z

@[simp]

theorem CategoryTheory.DGAdjunction.H0Presentation.presentedCounitTriangle_mor₁ {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated D] [HasShift Y ℤ] [eD.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.CounitConeData) (Z : Y) : ((P.presentedCounitTriangle K).obj Z).mor₁ = (P.toAdjunction A).counit.app Z

@[simp]

theorem CategoryTheory.DGAdjunction.H0Presentation.presentedCounitTriangle_mor₂ {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated D] [HasShift Y ℤ] [eD.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.CounitConeData) (Z : Y) : ((P.presentedCounitTriangle K).obj Z).mor₂ = (P.counitToTransportedTwist K).app Z

@[simp]

theorem CategoryTheory.DGAdjunction.H0Presentation.presentedCounitTriangle_mor₃ {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated D] [HasShift Y ℤ] [eD.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.CounitConeData) (Z : Y) : ((P.presentedCounitTriangle K).obj Z).mor₃ = (P.transportedTwistToShiftedComposite K).app Z

noncomputable def CategoryTheory.DGAdjunction.H0Presentation.rawTransportedTwistTriangleIsoPresented {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated D] [HasShift Y ℤ] [eD.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.CounitConeData) : K.rawTransportedTwistTriangle ≅ P.presentedCounitTriangle K

The raw transported dg counit triangle and its presented form are naturally isomorphic.

Equations

• P.rawTransportedTwistTriangleIsoPresented K = (P.counitFirstMapNormalizationData K).rawIsoNormalized

@[simp]

theorem CategoryTheory.DGAdjunction.H0Presentation.rawTransportedTwistTriangleIsoPresented_hom_app_hom₁ {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated D] [HasShift Y ℤ] [eD.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.CounitConeData) (Z : Y) : ((P.rawTransportedTwistTriangleIsoPresented K).hom.app Z).hom₁ = (P.counitTriangleObj₁Iso K).hom.app Z

@[simp]

theorem CategoryTheory.DGAdjunction.H0Presentation.rawTransportedTwistTriangleIsoPresented_hom_app_hom₂ {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated D] [HasShift Y ℤ] [eD.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.CounitConeData) (Z : Y) : ((P.rawTransportedTwistTriangleIsoPresented K).hom.app Z).hom₂ = K.rawTransportedTwistTriangleObj₂Iso.hom.app Z

@[simp]

theorem CategoryTheory.DGAdjunction.H0Presentation.rawTransportedTwistTriangleIsoPresented_hom_app_hom₃ {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated D] [HasShift Y ℤ] [eD.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.CounitConeData) (Z : Y) : ((P.rawTransportedTwistTriangleIsoPresented K).hom.app Z).hom₃ = CategoryStruct.id (K.rawTransportedTwistTriangle.obj Z).obj₃

theorem CategoryTheory.DGAdjunction.H0Presentation.presentedCounitTriangle_obj_distinguished {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated D] [HasShift Y ℤ] [eD.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.CounitConeData) [Limits.HasZeroObject Y] [Preadditive Y] [∀ (n : ℤ), (shiftFunctor Y n).Additive] [Pretriangulated Y] [eD.functor.IsTriangulated] (Z : Y) : (P.presentedCounitTriangle K).obj Z ∈ Pretriangulated.distinguishedTriangles

Every value of the presented ordinary counit triangle is distinguished.

noncomputable def CategoryTheory.DGAdjunction.H0Presentation.unitTriangleObj₂Iso {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated C] [HasShift X ℤ] [eC.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.UnitConeData) : K.rawTransportedUnitTriangle.comp Pretriangulated.Triangle.π₂ ≅ F.comp G

The second projection of the raw transported dg unit triangle, identified with the composite of the named presented left and right adjoints.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.DGAdjunction.H0Presentation.unitFirstMapNormalizationData {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated C] [HasShift X ℤ] [eC.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.UnitConeData) : Pretriangulated.Triangle.FirstMapNormalizationData K.rawTransportedUnitTriangle (Functor.id X) (F.comp G) (P.toAdjunction A).unit

The generic first-map normalization data for the transported dg unit triangle. Its named first map is exactly the unit of the ordinary adjunction constructed by P.

Equations

• P.unitFirstMapNormalizationData K = { obj₁Iso := K.rawTransportedUnitTriangleObj₁Iso, obj₂Iso := P.unitTriangleObj₂Iso K, square := ⋯ }

noncomputable def CategoryTheory.DGAdjunction.H0Presentation.compositeToTransportedUnitCone {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated C] [HasShift X ℤ] [eC.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.UnitConeData) : F.comp G ⟶ K.transportedUnitCone eC

The second map of the presented unit triangle, from the adjunction composite to the transported unshifted unit cone.

Equations

• P.compositeToTransportedUnitCone K = (P.unitFirstMapNormalizationData K).normalizedSecond

noncomputable def CategoryTheory.DGAdjunction.H0Presentation.transportedUnitConeToShiftedIdentity {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated C] [HasShift X ℤ] [eC.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.UnitConeData) : K.transportedUnitCone eC ⟶ (Functor.id X).comp (shiftFunctor X 1)

The connecting map of the presented unit triangle, from the transported unshifted unit cone to the shift of the identity.

Equations

• P.transportedUnitConeToShiftedIdentity K = (P.unitFirstMapNormalizationData K).normalizedThird

noncomputable def CategoryTheory.DGAdjunction.H0Presentation.presentedUnitTriangle {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated C] [HasShift X ℤ] [eC.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.UnitConeData) : Functor X (Pretriangulated.Triangle X)

The presented ordinary unit triangle 𝟭 X ⟶ F G ⟶ transportedUnitCone ⟶ (𝟭 X)⟦1⟧.

Equations

• P.presentedUnitTriangle K = (P.unitFirstMapNormalizationData K).normalizedTriangle

@[simp]

theorem CategoryTheory.DGAdjunction.H0Presentation.presentedUnitTriangle_obj₁ {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated C] [HasShift X ℤ] [eC.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.UnitConeData) (Z : X) : ((P.presentedUnitTriangle K).obj Z).obj₁ = Z

@[simp]

theorem CategoryTheory.DGAdjunction.H0Presentation.presentedUnitTriangle_obj₂ {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated C] [HasShift X ℤ] [eC.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.UnitConeData) (Z : X) : ((P.presentedUnitTriangle K).obj Z).obj₂ = (F.comp G).obj Z

@[simp]

theorem CategoryTheory.DGAdjunction.H0Presentation.presentedUnitTriangle_obj₃ {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated C] [HasShift X ℤ] [eC.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.UnitConeData) (Z : X) : ((P.presentedUnitTriangle K).obj Z).obj₃ = (K.transportedUnitCone eC).obj Z

@[simp]

theorem CategoryTheory.DGAdjunction.H0Presentation.presentedUnitTriangle_mor₁ {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated C] [HasShift X ℤ] [eC.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.UnitConeData) (Z : X) : ((P.presentedUnitTriangle K).obj Z).mor₁ = (P.toAdjunction A).unit.app Z

@[simp]

theorem CategoryTheory.DGAdjunction.H0Presentation.presentedUnitTriangle_mor₂ {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated C] [HasShift X ℤ] [eC.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.UnitConeData) (Z : X) : ((P.presentedUnitTriangle K).obj Z).mor₂ = (P.compositeToTransportedUnitCone K).app Z

@[simp]

theorem CategoryTheory.DGAdjunction.H0Presentation.presentedUnitTriangle_mor₃ {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated C] [HasShift X ℤ] [eC.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.UnitConeData) (Z : X) : ((P.presentedUnitTriangle K).obj Z).mor₃ = (P.transportedUnitConeToShiftedIdentity K).app Z

noncomputable def CategoryTheory.DGAdjunction.H0Presentation.rawTransportedUnitTriangleIsoPresented {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated C] [HasShift X ℤ] [eC.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.UnitConeData) : K.rawTransportedUnitTriangle ≅ P.presentedUnitTriangle K

The raw transported dg unit triangle and its presented form are naturally isomorphic.

Equations

• P.rawTransportedUnitTriangleIsoPresented K = (P.unitFirstMapNormalizationData K).rawIsoNormalized

@[simp]

theorem CategoryTheory.DGAdjunction.H0Presentation.rawTransportedUnitTriangleIsoPresented_hom_app_hom₁ {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated C] [HasShift X ℤ] [eC.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.UnitConeData) (Z : X) : ((P.rawTransportedUnitTriangleIsoPresented K).hom.app Z).hom₁ = K.rawTransportedUnitTriangleObj₁Iso.hom.app Z

@[simp]

theorem CategoryTheory.DGAdjunction.H0Presentation.rawTransportedUnitTriangleIsoPresented_hom_app_hom₂ {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated C] [HasShift X ℤ] [eC.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.UnitConeData) (Z : X) : ((P.rawTransportedUnitTriangleIsoPresented K).hom.app Z).hom₂ = (P.unitTriangleObj₂Iso K).hom.app Z

@[simp]

theorem CategoryTheory.DGAdjunction.H0Presentation.rawTransportedUnitTriangleIsoPresented_hom_app_hom₃ {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated C] [HasShift X ℤ] [eC.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.UnitConeData) (Z : X) : ((P.rawTransportedUnitTriangleIsoPresented K).hom.app Z).hom₃ = CategoryStruct.id (K.rawTransportedUnitTriangle.obj Z).obj₃

theorem CategoryTheory.DGAdjunction.H0Presentation.presentedUnitTriangle_obj_distinguished {C : Type uC} {D : Type uD} {X : Type uX} {Y : Type uY} [DGCategory C] [DGCategory D] [Category.{vX, uX} X] [Category.{vY, uY} Y] {L : DGFunctor C D} {R : DGFunctor D C} {eC : H0 C ≌ X} {eD : H0 D ≌ Y} {F : Functor X Y} {G : Functor Y X} {A : DGAdjunction L R} [IsPretriangulated C] [HasShift X ℤ] [eC.functor.CommShift ℤ] (P : H0Presentation eC eD F G) (K : A.UnitConeData) [Limits.HasZeroObject X] [Preadditive X] [∀ (n : ℤ), (shiftFunctor X n).Additive] [Pretriangulated X] [eC.functor.IsTriangulated] (Z : X) : (P.presentedUnitTriangle K).obj Z ∈ Pretriangulated.distinguishedTriangles

Every value of the presented ordinary unit triangle is distinguished.