The four Anno--Logvinenko triangles, as functors on H⁰

EnhancedAdjunctionCones holds the four dg cone choices attached to a dg functor with a left and a right dg adjoint. Each one is a CounitConeData or a UnitConeData, so each gives a functor into triangles of H⁰ by the generic construction, with every value distinguished:

triangle	in	shape
twist	H⁰ B	S R X ⟶ X ⟶ T X ⟶ (S R X)⟦1⟧
dual twist	H⁰ B	C X⟦-1⟧ ⟶ X ⟶ S L X ⟶ C X
cotwist	H⁰ A	C' X⟦-1⟧ ⟶ X ⟶ R S X ⟶ C' X
dual cotwist	H⁰ A	L S X ⟶ X ⟶ T' X ⟶ (L S X)⟦1⟧

These are Anno--Logvinenko's four triangles read as triangles of functors, which is the form their argument uses.

The shift on two of the four is one inverse rotation

EnhancedAdjunctionCones stores the dual twist and the cotwist as unshifted cones, because the conventional functors are their ⟦-1⟧ shifts. Rather than shift the cone functor and then rebuild a triangle, the triangle of the unshifted cone is inversely rotated: invRotate sends X ⟶ Y ⟶ Z ⟶ X⟦1⟧ to Z⟦-1⟧ ⟶ X ⟶ Y ⟶ Z, so it applies the shift and reorders in one step, and Pretriangulated.inv_rot_of_distTriang carries distinguishedness across for free.

The unshifted triangles are kept under their Cone names, since the TwistCotwistEquivalenceConditions are stated against the unshifted cone functors.

The conventional shifted dg functors are named dualTwistFunctor and cotwistFunctor. Their H⁰ functors are naturally isomorphic to the corresponding unshifted cone functor followed by the ordinary [-1] shift. Thus the first vertices below are values of the named dg functors on the nose, while ordinary categorical properties can be transported through a reusable comparison.

What is not claimed

That the functor is spherical, or that any relation among the four triangles holds. TwistCotwistEquivalenceConditions records the usual equivalence pair as data and no theorem upgrades it; that implication is Anno--Logvinenko's, and it runs through Morita quasi-functors and higher cone coherence that this repository does not have. Exactness below does include the conventional shifted dual twist and cotwist: it is transported from their unshifted cones through the sign-correct shifted-functor interface.

Nothing here is new mathematics. Every declaration is a thin wrapper over the generic cone-triangle, cone-exactness/3-by-3, or shifted-functor exactness layer, which is the point of having built those layers first.

The two triangles in H⁰ B

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.twistTriangleFunctor {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] : Functor (H0 B) (Pretriangulated.Triangle (H0 B))

The twist triangle. S R X ⟶ X ⟶ T X ⟶ (S R X)⟦1⟧, from the counit of the right adjunction.

Equations

• P.twistTriangleFunctor = CategoryTheory.DGAdjunction.CounitConeData.twistTriangleFunctor P.rightAdj P.twist

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.twistTriangleFunctor_obj_mem_distinguishedTriangles {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] (X : H0 B) : P.twistTriangleFunctor.obj X ∈ H0.distinguishedTriangles B

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.twistTriangleFunctor_obj_mor₁ {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] (X : H0 B) : (P.twistTriangleFunctor.obj X).mor₁ = P.rightAdj.h0Counit.app X

The first map of the twist triangle is the right adjunction's counit.

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualTwistConeTriangleFunctor {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] : Functor (H0 B) (Pretriangulated.Triangle (H0 B))

The unshifted dual-twist triangle. X ⟶ S L X ⟶ C X ⟶ X⟦1⟧, from the unit of the left adjunction. The conventional dual twist is C⟦-1⟧.

Equations

• P.dualTwistConeTriangleFunctor = CategoryTheory.DGAdjunction.UnitConeData.unitTriangleFunctor P.leftAdj P.dualTwistCone

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualTwistConeTriangleFunctor_obj_mem_distinguishedTriangles {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] (X : H0 B) : P.dualTwistConeTriangleFunctor.obj X ∈ H0.distinguishedTriangles B

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualTwistConeTriangleFunctor_obj_mor₁ {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] (X : H0 B) : (P.dualTwistConeTriangleFunctor.obj X).mor₁ = P.leftAdj.h0Unit.app X

The first map of the unshifted dual-twist triangle is the left adjunction's unit.

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualTwistTriangleFunctor {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] : Functor (H0 B) (Pretriangulated.Triangle (H0 B))

The dual-twist triangle. The inverse rotation of the unshifted one, so its first vertex is C X⟦-1⟧, the dual twist:

C X⟦-1⟧ ⟶ X ⟶ S L X ⟶ C X.

Inverse rotation applies the shift and reorders in one step, so the triangle construction itself need not be rebuilt from the separately named shifted cone functor.

Equations

• P.dualTwistTriangleFunctor = P.dualTwistConeTriangleFunctor.comp (CategoryTheory.Pretriangulated.invRotate (CategoryTheory.H0 B))

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualTwistTriangleFunctor_obj_mem_distinguishedTriangles {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] (X : H0 B) : P.dualTwistTriangleFunctor.obj X ∈ H0.distinguishedTriangles B

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualTwistTriangleFunctor_obj_obj₁ {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] (X : H0 B) : (P.dualTwistTriangleFunctor.obj X).obj₁ = P.dualTwistFunctor.h0.obj X

The first vertex of the dual-twist triangle is the dual twist: the value of the dg cone functor, shifted by -1.

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualTwistFunctorH0Iso {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] : P.dualTwistFunctor.h0 ≅ P.dualTwistConeFunctor.h0.comp (shiftFunctor (H0 B) (-1))

The H⁰ dual twist is naturally the unshifted cone followed by [-1].

Equations

• P.dualTwistFunctorH0Iso = P.dualTwistConeFunctor.shiftedFunctorH0Iso (-1)

@[simp]

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualTwistTriangleFunctor_obj_obj₂ {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] (X : H0 B) : (P.dualTwistTriangleFunctor.obj X).obj₂ = X

@[simp]

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualTwistTriangleFunctor_obj_obj₃ {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] (X : H0 B) : (P.dualTwistTriangleFunctor.obj X).obj₃ = (L.comp S).h0.obj X

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualTwistTriangleFunctor_obj_mor₂ {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] (X : H0 B) : (P.dualTwistTriangleFunctor.obj X).mor₂ = P.leftAdj.h0Unit.app X

The second map of the dual-twist triangle is the left adjunction's unit: inverse rotation moves the old first map into second place.

The two triangles in H⁰ A

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistConeTriangleFunctor {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] : Functor (H0 A) (Pretriangulated.Triangle (H0 A))

The unshifted cotwist triangle. X ⟶ R S X ⟶ C' X ⟶ X⟦1⟧, from the unit of the right adjunction. The conventional cotwist is C'⟦-1⟧.

Equations

• P.cotwistConeTriangleFunctor = CategoryTheory.DGAdjunction.UnitConeData.unitTriangleFunctor P.rightAdj P.cotwistCone

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistConeTriangleFunctor_obj_mem_distinguishedTriangles {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] (X : H0 A) : P.cotwistConeTriangleFunctor.obj X ∈ H0.distinguishedTriangles A

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistConeTriangleFunctor_obj_mor₁ {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] (X : H0 A) : (P.cotwistConeTriangleFunctor.obj X).mor₁ = P.rightAdj.h0Unit.app X

The first map of the unshifted cotwist triangle is the right adjunction's unit.

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistTriangleFunctor {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] : Functor (H0 A) (Pretriangulated.Triangle (H0 A))

The cotwist triangle. The inverse rotation of the unshifted one, so its first vertex is C' X⟦-1⟧, the cotwist:

C' X⟦-1⟧ ⟶ X ⟶ R S X ⟶ C' X.

Equations

• P.cotwistTriangleFunctor = P.cotwistConeTriangleFunctor.comp (CategoryTheory.Pretriangulated.invRotate (CategoryTheory.H0 A))

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistTriangleFunctor_obj_mem_distinguishedTriangles {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] (X : H0 A) : P.cotwistTriangleFunctor.obj X ∈ H0.distinguishedTriangles A

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistTriangleFunctor_obj_obj₁ {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] (X : H0 A) : (P.cotwistTriangleFunctor.obj X).obj₁ = P.cotwistFunctor.h0.obj X

The first vertex of the cotwist triangle is the cotwist: the value of the dg cone functor, shifted by -1.

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistFunctorH0Iso {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] : P.cotwistFunctor.h0 ≅ P.cotwistConeFunctor.h0.comp (shiftFunctor (H0 A) (-1))

The H⁰ cotwist is naturally the unshifted cone followed by [-1].

Equations

• P.cotwistFunctorH0Iso = P.cotwistConeFunctor.shiftedFunctorH0Iso (-1)

@[simp]

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistTriangleFunctor_obj_obj₂ {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] (X : H0 A) : (P.cotwistTriangleFunctor.obj X).obj₂ = X

@[simp]

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistTriangleFunctor_obj_obj₃ {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] (X : H0 A) : (P.cotwistTriangleFunctor.obj X).obj₃ = (S.comp R).h0.obj X

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistTriangleFunctor_obj_mor₂ {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] (X : H0 A) : (P.cotwistTriangleFunctor.obj X).mor₂ = P.rightAdj.h0Unit.app X

The second map of the cotwist triangle is the right adjunction's unit.

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualCotwistTriangleFunctor {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] : Functor (H0 A) (Pretriangulated.Triangle (H0 A))

The dual-cotwist triangle. L S X ⟶ X ⟶ T' X ⟶ (L S X)⟦1⟧, from the counit of the left adjunction.

Equations

• P.dualCotwistTriangleFunctor = CategoryTheory.DGAdjunction.CounitConeData.twistTriangleFunctor P.leftAdj P.dualCotwist

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualCotwistTriangleFunctor_obj_mem_distinguishedTriangles {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] (X : H0 A) : P.dualCotwistTriangleFunctor.obj X ∈ H0.distinguishedTriangles A

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualCotwistTriangleFunctor_obj_mor₁ {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] (X : H0 A) : (P.dualCotwistTriangleFunctor.obj X).mor₁ = P.leftAdj.h0Counit.app X

The first map of the dual-cotwist triangle is the left adjunction's counit.

The equivalence conditions, spent

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.twistH0Equivalence {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) (h : TwistCotwistEquivalenceConditions P) : H0 B ≌ H0 B

The twist is an autoequivalence of H⁰ B.

TwistCotwistEquivalenceConditions records that the twist is a quasi-equivalence, and DGFunctor.h0Equivalence turns a quasi-equivalence into an equivalence on H⁰. This is the first categorical invertibility statement about a twist in this repository: everything before it was either numerical, on K₀, or a construction with no invertibility attached.

No pretriangulated hypothesis is needed: this is an equivalence of ordinary categories, and the cone triangles above play no part in it. This definition alone says nothing about exactness; twistH0EquivalenceIsTriangulated combines it with the exactness package below. Nothing here calls the functor spherical: the Anno--Logvinenko implication from this pair of conditions to all four spherical conditions is still out of reach.

Equations

• P.twistH0Equivalence h = P.twistFunctor.h0Equivalence ⋯

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistConeH0Equivalence {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) (h : TwistCotwistEquivalenceConditions P) : H0 A ≌ H0 A

The unshifted cotwist cone is an autoequivalence of H⁰ A.

The conventional cotwist is its ⟦-1⟧ shift; requiring the unshifted cone functor to be a quasi-equivalence is the shift-free form of the same condition.

Equations

• P.cotwistConeH0Equivalence h = P.cotwistConeFunctor.h0Equivalence ⋯

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistH0Equivalence {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] (h : TwistCotwistEquivalenceConditions P) : H0 A ≌ H0 A

The conventional cotwist is an autoequivalence of H⁰ A.

The recorded condition is stated for the unshifted cone. The reusable shifted-functor comparison transports its induced H⁰ equivalence across the conventional [-1] shift. This remains an equivalence of ordinary categories; cotwistH0EquivalenceIsTriangulated separately packages its exactness, and no sphericality is inferred here.

Equations

• P.cotwistH0Equivalence h = P.cotwistConeFunctor.shiftedFunctorH0Equivalence (-1) ⋯

Exactness

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.twistPreservesShifts {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) : P.twistFunctor.PreservesShifts

The twist preserves shifts.

Unconditional: every dg functor preserves shifts (DGFunctor.preservesShifts), because a shift element is a closed two-sided invertible element. Cone preservation is unconditional as well; the structured accessor below retains endpoint arguments only to expose the 3-by-3 construction.

Equations

• P.twistPreservesShifts = CategoryTheory.DGAdjunction.CounitConeData.preservesShifts P.rightAdj P.twist

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistConePreservesShifts {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) : P.cotwistConeFunctor.PreservesShifts

The unshifted cotwist cone preserves shifts too.

Equations

• P.cotwistConePreservesShifts = CategoryTheory.DGAdjunction.UnitConeData.preservesShifts P.rightAdj P.cotwistCone

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualTwistConePreservesShifts {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) : P.dualTwistConeFunctor.PreservesShifts

The unshifted dual-twist cone preserves shifts.

Equations

• P.dualTwistConePreservesShifts = CategoryTheory.DGAdjunction.UnitConeData.preservesShifts P.leftAdj P.dualTwistCone

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualCotwistPreservesShifts {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) : P.dualCotwistFunctor.PreservesShifts

The dual cotwist preserves shifts.

Equations

• P.dualCotwistPreservesShifts = CategoryTheory.DGAdjunction.CounitConeData.preservesShifts P.leftAdj P.dualCotwist

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.twistPreservesChosenCones {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) (hSc : S.PreservesChosenCones) (hRc : R.PreservesChosenCones) : P.twistFunctor.PreservesChosenCones

The structured 3-by-3 cone witness for the twist. The endpoint arguments are redundant for existence but expose the counit-cone proof.

Equations

• P.twistPreservesChosenCones hSc hRc = CategoryTheory.DGAdjunction.CounitConeData.preservesChosenCones P.rightAdj P.twist hSc hRc

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistConePreservesChosenCones {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) (hSc : S.PreservesChosenCones) (hRc : R.PreservesChosenCones) : P.cotwistConeFunctor.PreservesChosenCones

Structured cone preservation for the unshifted cotwist cone; the endpoint arguments are redundant.

Equations

• P.cotwistConePreservesChosenCones hSc hRc = CategoryTheory.DGAdjunction.UnitConeData.preservesChosenCones P.rightAdj P.cotwistCone hSc hRc

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualTwistConePreservesChosenCones {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) (hLc : L.PreservesChosenCones) (hSc : S.PreservesChosenCones) : P.dualTwistConeFunctor.PreservesChosenCones

Structured cone preservation for the unshifted dual-twist cone; the endpoint arguments are redundant.

Equations

• P.dualTwistConePreservesChosenCones hLc hSc = CategoryTheory.DGAdjunction.UnitConeData.preservesChosenCones P.leftAdj P.dualTwistCone hLc hSc

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualCotwistPreservesChosenCones {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) (hLc : L.PreservesChosenCones) (hSc : S.PreservesChosenCones) : P.dualCotwistFunctor.PreservesChosenCones

Structured cone preservation for the dual cotwist; the endpoint arguments are redundant.

Equations

• P.dualCotwistPreservesChosenCones hLc hSc = CategoryTheory.DGAdjunction.CounitConeData.preservesChosenCones P.leftAdj P.dualCotwist hLc hSc

@[reducible]

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistConeH0CommShift {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] : P.cotwistConeFunctor.h0.CommShift ℤ

The shift comparison on H⁰ of the unshifted cotwist cone.

Equations

• P.cotwistConeH0CommShift = P.cotwistConeFunctor.h0CommShift

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistConeH0IsTriangulated {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] : P.cotwistConeFunctor.h0.IsTriangulated

The unshifted cotwist cone is exact on H⁰.

@[reducible]

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistH0CommShift {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] : P.cotwistFunctor.h0.CommShift ℤ

The sign-correct shift comparison on the conventional cotwist.

Equations

• P.cotwistH0CommShift = P.cotwistConeFunctor.shiftedFunctorH0CommShift (-1) P.cotwistConePreservesShifts

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistH0IsTriangulated {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] : P.cotwistFunctor.h0.IsTriangulated

The conventional cotwist is exact on H⁰.

@[reducible]

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualTwistConeH0CommShift {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] : P.dualTwistConeFunctor.h0.CommShift ℤ

The shift comparison on H⁰ of the unshifted dual-twist cone.

Equations

• P.dualTwistConeH0CommShift = P.dualTwistConeFunctor.h0CommShift

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualTwistConeH0IsTriangulated {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] : P.dualTwistConeFunctor.h0.IsTriangulated

The unshifted dual-twist cone is exact on H⁰.

@[reducible]

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualTwistH0CommShift {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] : P.dualTwistFunctor.h0.CommShift ℤ

The sign-correct shift comparison on the conventional dual twist.

Equations

• P.dualTwistH0CommShift = P.dualTwistConeFunctor.shiftedFunctorH0CommShift (-1) P.dualTwistConePreservesShifts

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualTwistH0IsTriangulated {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] : P.dualTwistFunctor.h0.IsTriangulated

The conventional dual twist is exact on H⁰.

@[reducible]

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualCotwistH0CommShift {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] : P.dualCotwistFunctor.h0.CommShift ℤ

The shift comparison on H⁰ of the dual cotwist.

Equations

• P.dualCotwistH0CommShift = P.dualCotwistFunctor.h0CommShift

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualCotwistH0IsTriangulated {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] : P.dualCotwistFunctor.h0.IsTriangulated

The dual cotwist is exact on H⁰.

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.twistH0IsTriangulated {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] : P.twistFunctor.h0.IsTriangulated

The twist is exact on H⁰.

Both dg-level capabilities are available for the twist, so H⁰ of it is a triangulated functor: it commutes with the shift and carries distinguished triangles to distinguished triangles. With the equivalence supplied by the twist/cotwist conditions this is an exact autoequivalence, which is what the word "twist" is supposed to mean.

No endpoint hypotheses are required.

@[reducible]

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.twistH0CommShift {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] : P.twistFunctor.h0.CommShift ℤ

The twist commutes with the shift on H⁰.

This is the twist-specific name for the canonical dg-functor package.

Equations

• P.twistH0CommShift = P.twistFunctor.h0CommShift

Exact equivalences

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.twistH0EquivalenceIsTriangulated {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated B] (h : TwistCotwistEquivalenceConditions P) : (P.twistH0Equivalence h).IsTriangulated

Under the recorded equivalence condition, the twist is a triangulated equivalence of H⁰ B.

The inverse shift comparison and its triangulatedness are the canonical ones transported by Mathlib from the exact forward functor.

theorem CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistH0EquivalenceIsTriangulated {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) [IsPretriangulated A] (h : TwistCotwistEquivalenceConditions P) : (P.cotwistH0Equivalence h).IsTriangulated

Under the recorded equivalence condition, the conventional cotwist is a triangulated equivalence of H⁰ A.

Its forward exactness uses the sign-correct [-1] package; Mathlib then transports the compatible shift structure and exactness to the inverse.