The twist triangle of a dg adjunction

For a dg adjunction L ⊣ R the counit is a closed degree-zero dg natural transformation L R ⟶ id_D, and a choice of objectwise cones for it is CounitConeData, whose cone functor is the twist candidate. Feeding that choice to ConeData.triangleFunctor gives

H⁰ D ⥤ Triangle (H⁰ D), X ↦ (L R X ⟶ X ⟶ T X ⟶ (L R X)⟦1⟧),

every value distinguished. This is Anno--Logvinenko's twist triangle read as a triangle of functors on H⁰ rather than object by object.

The unit side is the same construction in C, and its cone is the unshifted cone of id_C ⟶ R L; the conventional cotwist is a shift of it, which this file does not take.

What is claimed, and what is not

The only claims here are that the triangle is functorial, that every value is distinguished, and that the construction does not depend on the chosen cones (twistTriangleIso). All three are immediate from the generic cone-triangle layer; nothing about adjunctions is used beyond the counit being closed.

Nothing here says the twist is an autoequivalence, calls the adjunction spherical, or relates the triangle to the other three of Anno--Logvinenko's four. Those need the Morita and quasi-functor framework the roadmap lists as open, and the repository's dg adjunctions are the strict kind, not homotopy adjunctions of bimodules.

Where the first two maps come from

twistTriangleFunctor_obj_mor₁ identifies the first map with the counit read on H⁰, which is DGAdjunction.h0Counit, and ..._mor₂ identifies the second with the canonical inclusion id_D ⟶ T. Both are the point of the construction: the triangle's maps are the adjunction's own data, not new choices.

noncomputable def CategoryTheory.DGAdjunction.CounitConeData.twistTriangleFunctor {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) [IsPretriangulated D] (K : A.CounitConeData) : Functor (H0 D) (Pretriangulated.Triangle (H0 D))

The twist triangle of a dg adjunction, as a functor on H⁰.

X ↦ (L R X ⟶ X ⟶ T X ⟶ (L R X)⟦1⟧), with T the twist candidate.

Equations

• CategoryTheory.DGAdjunction.CounitConeData.twistTriangleFunctor A K = CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.triangleFunctor K ⋯

theorem CategoryTheory.DGAdjunction.CounitConeData.twistTriangleFunctor_obj_mem_distinguishedTriangles {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) [IsPretriangulated D] (K : A.CounitConeData) (X : H0 D) : (twistTriangleFunctor A K).obj X ∈ H0.distinguishedTriangles D

Every value of the twist triangle functor is distinguished.

@[simp]

theorem CategoryTheory.DGAdjunction.CounitConeData.twistTriangleFunctor_obj_obj₁ {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) [IsPretriangulated D] (K : A.CounitConeData) (X : H0 D) : ((twistTriangleFunctor A K).obj X).obj₁ = (R.comp L).h0.obj X

@[simp]

theorem CategoryTheory.DGAdjunction.CounitConeData.twistTriangleFunctor_obj_obj₂ {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) [IsPretriangulated D] (K : A.CounitConeData) (X : H0 D) : ((twistTriangleFunctor A K).obj X).obj₂ = X

@[simp]

theorem CategoryTheory.DGAdjunction.CounitConeData.twistTriangleFunctor_obj_obj₃ {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) [IsPretriangulated D] (K : A.CounitConeData) (X : H0 D) : ((twistTriangleFunctor A K).obj X).obj₃ = (twist A K).h0.obj X

theorem CategoryTheory.DGAdjunction.CounitConeData.twistTriangleFunctor_obj_mor₁ {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) [IsPretriangulated D] (K : A.CounitConeData) (X : H0 D) : ((twistTriangleFunctor A K).obj X).mor₁ = A.h0Counit.app X

The first map is the counit, read on H⁰.

theorem CategoryTheory.DGAdjunction.CounitConeData.twistTriangleFunctor_obj_mor₂ {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) [IsPretriangulated D] (K : A.CounitConeData) (X : H0 D) : ((twistTriangleFunctor A K).obj X).mor₂ = (DGFunctor.HomogeneousNatTrans.h0 (inclusion A K) ⋯).app X

The second map is the canonical inclusion id_D ⟶ T.

@[simp]

theorem CategoryTheory.DGAdjunction.CounitConeData.twistTriangleFunctor_map_hom₁ {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) [IsPretriangulated D] (K : A.CounitConeData) {X Y : H0 D} (f : X ⟶ Y) : ((twistTriangleFunctor A K).map f).hom₁ = (R.comp L).h0.map f

@[simp]

theorem CategoryTheory.DGAdjunction.CounitConeData.twistTriangleFunctor_map_hom₃ {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) [IsPretriangulated D] (K : A.CounitConeData) {X Y : H0 D} (f : X ⟶ Y) : ((twistTriangleFunctor A K).map f).hom₃ = (twist A K).h0.map f

noncomputable def CategoryTheory.DGAdjunction.CounitConeData.twistTriangleIso {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) [IsPretriangulated D] (K K' : A.CounitConeData) : twistTriangleFunctor A K ≅ twistTriangleFunctor A K'

The twist triangle does not depend on the chosen cones.

Equations

• CategoryTheory.DGAdjunction.CounitConeData.twistTriangleIso A K K' = CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.compareIso ⋯ K K'

noncomputable def CategoryTheory.DGAdjunction.UnitConeData.unitTriangleFunctor {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) [IsPretriangulated C] (K : A.UnitConeData) : Functor (H0 C) (Pretriangulated.Triangle (H0 C))

The unit triangle of a dg adjunction, as a functor on H⁰.

X ↦ (X ⟶ R L X ⟶ C X ⟶ X⟦1⟧), with C the unshifted cone of the unit. The conventional cotwist is a shift of C, which this file does not take.

Equations

• CategoryTheory.DGAdjunction.UnitConeData.unitTriangleFunctor A K = CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.triangleFunctor K ⋯

theorem CategoryTheory.DGAdjunction.UnitConeData.unitTriangleFunctor_obj_mem_distinguishedTriangles {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) [IsPretriangulated C] (K : A.UnitConeData) (X : H0 C) : (unitTriangleFunctor A K).obj X ∈ H0.distinguishedTriangles C

Every value of the unit triangle functor is distinguished.

@[simp]

theorem CategoryTheory.DGAdjunction.UnitConeData.unitTriangleFunctor_obj_obj₁ {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) [IsPretriangulated C] (K : A.UnitConeData) (X : H0 C) : ((unitTriangleFunctor A K).obj X).obj₁ = X

@[simp]

theorem CategoryTheory.DGAdjunction.UnitConeData.unitTriangleFunctor_obj_obj₂ {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) [IsPretriangulated C] (K : A.UnitConeData) (X : H0 C) : ((unitTriangleFunctor A K).obj X).obj₂ = (L.comp R).h0.obj X

@[simp]

theorem CategoryTheory.DGAdjunction.UnitConeData.unitTriangleFunctor_obj_obj₃ {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) [IsPretriangulated C] (K : A.UnitConeData) (X : H0 C) : ((unitTriangleFunctor A K).obj X).obj₃ = (unitCone A K).h0.obj X

theorem CategoryTheory.DGAdjunction.UnitConeData.unitTriangleFunctor_obj_mor₁ {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) [IsPretriangulated C] (K : A.UnitConeData) (X : H0 C) : ((unitTriangleFunctor A K).obj X).mor₁ = A.h0Unit.app X

The first map is the unit, read on H⁰.

noncomputable def CategoryTheory.DGAdjunction.UnitConeData.unitTriangleIso {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) [IsPretriangulated C] (K K' : A.UnitConeData) : unitTriangleFunctor A K ≅ unitTriangleFunctor A K'

The unit triangle does not depend on the chosen cones.

Equations

• CategoryTheory.DGAdjunction.UnitConeData.unitTriangleIso A K K' = CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.compareIso ⋯ K K'