Adjoint-comparison conditions for enhanced functors

For an EnhancedAdjunctionCones package, the generic dg-cone layer constructs the two canonical closed comparison transformations

L T[-1] ⟶ R and R ⟶ C L.

This file records the corresponding Anno--Logvinenko conditions at the ordinary categorical boundary: both induced natural transformations on H⁰ are isomorphisms. The fields use Mathlib's IsIso predicate on the canonical maps themselves, rather than storing unrelated natural isomorphisms.

These conditions do not imply sphericality in this repository. In particular, nothing here derives them from TwistCotwistEquivalenceConditions or supplies the Morita quasi-functor and higher cone coherence needed for the two-of-four theorem.

structure CategoryTheory.Triangulated.SphericalTwist.AdjointComparisonConditions {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] : Prop

The two adjoint-comparison conditions for selected enhanced cones.

They assert invertibility only after passage to H⁰, and only for the canonical maps constructed from the selected cone and adjunction data.

• twist : IsIso (DGAdjunction.CounitConeData.twistAdjointComparisonH0 P.leftAdj P.rightAdj P.twist)

  The canonical comparison L T[-1] ⟶ R is invertible on H⁰.

• cotwist : IsIso (DGAdjunction.UnitConeData.cotwistAdjointComparisonH0 P.leftAdj P.rightAdj P.cotwistCone)

  The canonical comparison R ⟶ C L is invertible on H⁰.

noncomputable def CategoryTheory.Triangulated.SphericalTwist.AdjointComparisonConditions.twistIso {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 : AdjointComparisonConditions P) : ((P.twistFunctor.shiftedFunctor (-1)).comp L).h0 ≅ R.h0

The canonical twist-side comparison, packaged as Mathlib's selected isomorphism.

Equations

• h.twistIso = CategoryTheory.asIso (CategoryTheory.DGAdjunction.CounitConeData.twistAdjointComparisonH0 P.leftAdj P.rightAdj P.twist)

noncomputable def CategoryTheory.Triangulated.SphericalTwist.AdjointComparisonConditions.cotwistIso {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 : AdjointComparisonConditions P) : R.h0 ≅ (L.comp P.cotwistConeFunctor).h0

The canonical cotwist-side comparison, packaged as Mathlib's selected isomorphism.

Equations

• h.cotwistIso = CategoryTheory.asIso (CategoryTheory.DGAdjunction.UnitConeData.cotwistAdjointComparisonH0 P.leftAdj P.rightAdj P.cotwistCone)

noncomputable def CategoryTheory.Triangulated.SphericalTwist.AdjointComparisonConditions.cotwistShiftedIso {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 : AdjointComparisonConditions P) [IsPretriangulated A] : R.h0 ≅ ((L.comp P.cotwistFunctor).shiftedFunctor 1).h0

The cotwist comparison in Anno--Logvinenko's conventional shifted form R ≅ (F L)[1], where F = C[-1].

The final isomorphism is Mathlib's opposite-shift cancellation for the HasShift structure on closed dg functors.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.SphericalTwist.AdjointComparisonConditions.cotwistShiftedIso_hom {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 : AdjointComparisonConditions P) [IsPretriangulated A] : h.cotwistShiftedIso.hom = DGAdjunction.UnitConeData.cotwistAdjointComparisonShiftedH0 P.leftAdj P.rightAdj P.cotwistCone

The hom of cotwistShiftedIso is the canonical shifted-target comparison, not an independently chosen natural isomorphism.