The twist of an object

The Seidel--Thomas twist of an object E is the cone of the evaluation map

RHom(E,X) ⊗ E ⟶ X.

EvaluationData E is a choice of the tensoring for every X, its functor is RHom(E,-) ⊗ E, and its evaluation is the degree-zero transformation to the identity. evaluation_isClosed is what this construction needs: a closed degree-zero transformation has objectwise cones, and those cones assemble to a dg endofunctor exactly as the counit's do for an adjunction.

Why this is a second twist, not a duplicate of the first

DGAdjunction.CounitConeData.twist is the cone of an adjunction counit L R ⟶ id. This one is the cone of a transformation attached to a single object, with no adjunction in sight. The two agree when RHom(E,-) and - ⊗ E are the adjoint pair of a spherical functor out of Perf(k), but the repository has no Perf(k) as a dg category, so that comparison cannot be stated here and is not attempted. What the object form buys is that it is available now from evaluation data plus chosen cones, with the cone choices supplied automatically in a pretriangulated category.

What is claimed, and what is not

The cone exists, is a dg endofunctor, and receives the canonical inclusion from the identity. Its dg-functor isomorphism class is independent of both the evaluation data and the objectwise cone choices; the canonical comparisons commute strictly with the inclusions and satisfy identity and composition coherence. Nothing here says the twist is an autoequivalence, calls E spherical, or connects it to SerreFunctor.IsSphericalObject; those are the seams the roadmap records.

Exactness

Every dg functor preserves both shifts and the strong split cone witnesses used here. For shifts this follows by mapping the invertible homogeneous element; for cones the mapped fst and snd projections explicitly invert the mapped splitting. Thus the twist is exact on H⁰ without an evaluation-specific hypothesis. The structured preservesChosenCones constructor below retains its endpoint argument for compatibility and to expose the cone functor's 3-by-3 proof, but callers may always use DGFunctor.preservesChosenCones K.twist directly.

noncomputable def CategoryTheory.EvaluationData.preservesChosenConesOfCompare {C : Type u} [DGCategory C] {E : C} (V W : EvaluationData E) (hV : V.functor.PreservesChosenCones) : W.functor.PreservesChosenCones

Cone preservation for the evaluation functor transports across a change of evaluation data. This structured compatibility theorem remains useful even though every dg functor now supplies cone preservation directly.

Equations

• V.preservesChosenConesOfCompare W hV = hV.ofIso (V.compareIso W)

theorem CategoryTheory.EvaluationData.compare_evaluation_square {C : Type u} [DGCategory C] {E : C} (V W : EvaluationData E) : ((DGFunctor.HomogeneousNatTrans.composition V.functor (DGFunctor.id C) (DGFunctor.id C) 0 0 0 ⋯) V.evaluation) (DGFunctor.HomogeneousNatTrans.id (DGFunctor.id C)) = ((DGFunctor.HomogeneousNatTrans.composition V.functor W.functor (DGFunctor.id C) 0 0 0 ⋯) (V.compare W)) W.evaluation

The canonical comparison between evaluation functors and the identity on the target form a strictly commuting square of dg natural transformations.

@[reducible, inline]

abbrev CategoryTheory.EvaluationData.TwistConeData {C : Type u} [DGCategory C] {E : C} (V : EvaluationData E) : Type (max u v)

Chosen objectwise cones of the evaluation map RHom(E,X) ⊗ E ⟶ X.

Equations

• V.TwistConeData = CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData V.evaluation

noncomputable def CategoryTheory.EvaluationData.chosenTwistConeData {C : Type u} [DGCategory C] {E : C} (V : EvaluationData E) [IsPretriangulated C] : V.TwistConeData

A pretriangulated category supplies cones of all evaluation components.

Equations

• V.chosenTwistConeData = CategoryTheory.DGFunctor.HomogeneousNatTrans.chosenConeData V.evaluation ⋯

@[reducible, inline]

noncomputable abbrev CategoryTheory.EvaluationData.TwistConeData.twist {C : Type u} [DGCategory C] {E : C} {V : EvaluationData E} (K : V.TwistConeData) : DGFunctor C C

The twist of the object E: the dg endofunctor Cone(RHom(E,-) ⊗ E ⟶ id).

Equations

• K.twist = CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.functor K

@[reducible, inline]

noncomputable abbrev CategoryTheory.EvaluationData.TwistConeData.inclusion {C : Type u} [DGCategory C] {E : C} {V : EvaluationData E} (K : V.TwistConeData) : ↥((DGFunctor.id C).HomogeneousNatTrans K.twist 0)

The canonical closed transformation id ⟶ T_E.

Equations

• K.inclusion = CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.inr K

theorem CategoryTheory.EvaluationData.TwistConeData.inclusion_isClosed {C : Type u} [DGCategory C] {E : C} {V : EvaluationData E} (K : V.TwistConeData) : DGFunctor.HomogeneousNatTrans.IsClosed K.inclusion

noncomputable def CategoryTheory.EvaluationData.TwistConeData.compareIso {C : Type u} [DGCategory C] {E : C} {V : EvaluationData E} (K : V.TwistConeData) {W : EvaluationData E} (L : W.TwistConeData) : (have this := K.twist; this) ≅ have this := L.twist; this

The object-twist dg functor is independent, up to a canonical closed degree-zero isomorphism, of both the evaluation data and the chosen cones.

Equations

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

@[simp]

theorem CategoryTheory.EvaluationData.TwistConeData.compareIso_hom_val {C : Type u} [DGCategory C] {E : C} {V : EvaluationData E} (K : V.TwistConeData) {W : EvaluationData E} (L : W.TwistConeData) : ↑(K.compareIso L).hom = (DGFunctor.HomogeneousNatTrans.ConeData.isConeOf K).lift (DGFunctor.HomogeneousNatTrans.ConeData.isConeOf L) (V.compare W) (DGFunctor.HomogeneousNatTrans.id (DGFunctor.id C)) 0

@[simp]

theorem CategoryTheory.EvaluationData.TwistConeData.compareIso_inv_val {C : Type u} [DGCategory C] {E : C} {V : EvaluationData E} (K : V.TwistConeData) {W : EvaluationData E} (L : W.TwistConeData) : ↑(K.compareIso L).inv = (DGFunctor.HomogeneousNatTrans.ConeData.isConeOf L).lift (DGFunctor.HomogeneousNatTrans.ConeData.isConeOf K) (W.compare V) (DGFunctor.HomogeneousNatTrans.id (DGFunctor.id C)) 0

theorem CategoryTheory.EvaluationData.TwistConeData.inclusion_comp_compareIso_hom_val {C : Type u} [DGCategory C] {E : C} {V : EvaluationData E} (K : V.TwistConeData) {W : EvaluationData E} (L : W.TwistConeData) : ((DGFunctor.HomogeneousNatTrans.composition (DGFunctor.id C) K.twist L.twist 0 0 0 ⋯) K.inclusion) ↑(K.compareIso L).hom = L.inclusion

The canonical twist comparison strictly commutes with the inclusions from the identity functor.

theorem CategoryTheory.EvaluationData.TwistConeData.compareIso_self_hom_val {C : Type u} [DGCategory C] {E : C} {V : EvaluationData E} (K : V.TwistConeData) : ↑(K.compareIso K).hom = DGFunctor.HomogeneousNatTrans.id K.twist

The canonical twist comparison from a cone choice to itself is strictly the identity homogeneous natural transformation.

@[simp]

theorem CategoryTheory.EvaluationData.TwistConeData.compareIso_self {C : Type u} [DGCategory C] {E : C} {V : EvaluationData E} (K : V.TwistConeData) : K.compareIso K = Iso.refl (have this := K.twist; this)

The canonical twist comparison from a choice to itself is the identity isomorphism.

theorem CategoryTheory.EvaluationData.TwistConeData.compareIso_hom_val_comp {C : Type u} [DGCategory C] {E : C} {V : EvaluationData E} (K : V.TwistConeData) {W X : EvaluationData E} (L : W.TwistConeData) (M : X.TwistConeData) : ((DGFunctor.HomogeneousNatTrans.composition K.twist L.twist M.twist 0 0 0 ⋯) ↑(K.compareIso L).hom) ↑(L.compareIso M).hom = ↑(K.compareIso M).hom

Canonical twist comparisons compose strictly at the level of their underlying homogeneous natural transformations.

theorem CategoryTheory.EvaluationData.TwistConeData.compareIso_trans {C : Type u} [DGCategory C] {E : C} {V : EvaluationData E} (K : V.TwistConeData) {W X : EvaluationData E} (L : W.TwistConeData) (M : X.TwistConeData) : K.compareIso L ≪≫ L.compareIso M = K.compareIso M

Canonical twist comparison isomorphisms are transitive.

noncomputable def CategoryTheory.EvaluationData.TwistConeData.preservesShifts {C : Type u} [DGCategory C] {E : C} {V : EvaluationData E} (K : V.TwistConeData) : K.twist.PreservesShifts

The object twist preserves shifts.

Kept as the object-twist accessor for the unconditional generic capability.

Equations

• K.preservesShifts = K.twist.preservesShifts

noncomputable def CategoryTheory.EvaluationData.TwistConeData.preservesChosenCones {C : Type u} [DGCategory C] {E : C} {V : EvaluationData E} (K : V.TwistConeData) (hV : V.functor.PreservesChosenCones) : K.twist.PreservesChosenCones

The structured 3-by-3 cone-preservation witness for the object twist.

The endpoint argument is now redundant as a hypothesis, but retaining this constructor records how the cone-functor witness is assembled.

Equations

• K.preservesChosenCones hV = CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.preservesChosenCones K hV (CategoryTheory.DGFunctor.PreservesChosenCones.id C)