Enhanced cone data for spherical-functor constructions

Anno--Logvinenko attach four functorial triangles to a functor with left and right dg adjoints: twist, dual twist, cotwist, and dual cotwist. This file packages the four underlying dg cone choices without calling the functor spherical.

That distinction is essential. Sphericality additionally requires autoequivalence and adjoint-comparison conditions (or a theorem deriving all four conditions from a sufficient pair in the Morita-enhanced setting). TwistCotwistEquivalenceConditions records the commonly used equivalence pair as explicit data, but no theorem here upgrades it to sphericality. Doing so requires the specific adjoint-comparison transformations and higher cone coherence developed in the literature. The former are constructed at the generic dg-cone root and packaged for this data in EnhancedAdjunctionComparison; the latter is not yet a repository primitive.

structure CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] (S : DGFunctor A B) (L R : DGFunctor B A) : Type (max (max u u') v)

The four dg adjunction maps and their chosen objectwise cones for a dg functor S : A ⟶ B with left adjoint L and right adjoint R.

The fields named dualTwistCone and cotwistCone are unshifted cones. The conventional dual twist and cotwist are their shifts by -1.

• leftAdj : DGAdjunction L S

  The left adjunction L ⊣ S.

• rightAdj : DGAdjunction S R

  The right adjunction S ⊣ R.

• twist : self.rightAdj.CounitConeData

  Cone of S R ⟶ id_B: the twist.

• dualTwistCone : self.leftAdj.UnitConeData

  Cone of id_B ⟶ S L; its [-1] shift is the dual twist.

• cotwistCone : self.rightAdj.UnitConeData

  Cone of id_A ⟶ R S; its [-1] shift is the cotwist.

• dualCotwist : self.leftAdj.CounitConeData

  Cone of L S ⟶ id_A: the dual cotwist.

noncomputable def CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.chosen {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} [IsPretriangulated A] [IsPretriangulated B] (leftAdj : DGAdjunction L S) (rightAdj : DGAdjunction S R) : EnhancedAdjunctionCones S L R

A pretriangulated source and target provide all four objectwise cone choices associated to supplied left and right dg adjunctions.

Equations

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

@[reducible, inline]

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

The dg twist endofunctor Cone(S R ⟶ id_B).

Equations

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

@[reducible, inline]

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

The unshifted cone underlying the dual twist.

Equations

• P.dualTwistConeFunctor = CategoryTheory.DGAdjunction.UnitConeData.unitCone P.leftAdj P.dualTwistCone

@[reducible, inline]

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

The unshifted cone underlying the cotwist.

Equations

• P.cotwistConeFunctor = CategoryTheory.DGAdjunction.UnitConeData.unitCone P.rightAdj P.cotwistCone

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.dualTwistFunctor {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] : DGFunctor B B

The conventional dg dual twist: the [-1] shift of its stored unit cone.

Equations

• P.dualTwistFunctor = P.dualTwistConeFunctor.shiftedFunctor (-1)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.SphericalTwist.EnhancedAdjunctionCones.cotwistFunctor {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] : DGFunctor A A

The conventional dg cotwist: the [-1] shift of its stored unit cone.

Equations

• P.cotwistFunctor = P.cotwistConeFunctor.shiftedFunctor (-1)

@[reducible, inline]

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

The dg dual-cotwist endofunctor Cone(L S ⟶ id_A).

Equations

• P.dualCotwistFunctor = CategoryTheory.DGAdjunction.CounitConeData.twist P.leftAdj P.dualCotwist

structure CategoryTheory.Triangulated.SphericalTwist.TwistCotwistEquivalenceConditions {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (P : EnhancedAdjunctionCones S L R) : Prop

The twist/cotwist equivalence pair used by the main spherical-functor criterion, expressed at the repository's current dg level.

The cotwist is conventionally cotwistConeFunctor[-1]; requiring the unshifted cone functor to be a quasi-equivalence is the shift-free form of the same condition. This structure is deliberately not named IsSpherical: the Anno--Logvinenko implication from this pair to all spherical conditions uses Morita quasi-functors and higher cone coherence not yet formalized here.

• twist : P.twistFunctor.IsQuasiEquivalence

  The counit-cone twist is a quasi-equivalence.

• cotwist : P.cotwistConeFunctor.IsQuasiEquivalence

  The unshifted cone underlying the cotwist is a quasi-equivalence.