Documentation

DerivedAlgGeo.Algebra.Homology.DGCategory.Pretriangulated.LinearObjectTwistAdjunction

Scalar-linear object twists as adjunction counit twists #

When all scalar-linear copowers exist, the selected evaluation transformation is definitionally the counit of the copower--Hom dg adjunction. Consequently its cone data is already DGAdjunction.CounitConeData; no transport or second cone construction is needed.

An arbitrary LinearEvaluationData choice need not be definitionally the selected one. Its canonical evaluation comparison forms a strict square with the adjunction counit, so the existing cone comparison identifies the two twist functors in Z⁰. The comparison commutes strictly with the canonical inclusion and coheres with changes of scalar-linear evaluation data.

This is an identification of twist candidates. It does not construct Perf(k), restrict the source of the adjunction, produce an adjoint on the other side, or assert sphericality or invertibility.

source
theorem CategoryTheory.linearCopowerAdjunction_counitConeData_eq (k : Type w) [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [HasLinearCopowers k C] (E : C) :
(linearCopowerAdjunction k E).CounitConeData = LinearEvaluationData.TwistConeData k (LinearEvaluationData.ofHasLinearCopowers k E)

The selected scalar-linear evaluation cone data and the counit cone data of the copower--Hom dg adjunction are definitionally the same type.

source
noncomputable def CategoryTheory.LinearEvaluationData.TwistConeData.adjunctionTwistIso {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [HasLinearCopowers k C] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) (L : (linearCopowerAdjunction k E).CounitConeData) :
(have this := K.twist; this) ≅ have this := DGAdjunction.CounitConeData.twist (linearCopowerAdjunction k E) L; this

The canonical Z⁰ identification of a scalar-linear object twist with a counit-cone twist of the selected copower--Hom dg adjunction.

Equations
Instances For
    source
    theorem CategoryTheory.LinearEvaluationData.TwistConeData.adjunctionTwistIso_eq_compareIso {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [HasLinearCopowers k C] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) (L : (linearCopowerAdjunction k E).CounitConeData) :
    K.adjunctionTwistIso L = K.compareIso L

    The adjunction-twist comparison is exactly the existing canonical cone comparison to the selected scalar-linear evaluation data.

    source
    theorem CategoryTheory.LinearEvaluationData.TwistConeData.adjunctionTwistIso_hom_val {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [HasLinearCopowers k C] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) (L : (linearCopowerAdjunction k E).CounitConeData) :
    ↑(K.adjunctionTwistIso L).hom = (DGFunctor.HomogeneousNatTrans.ConeData.isConeOf K).lift (DGFunctor.HomogeneousNatTrans.ConeData.isConeOf L) (V.compare (ofHasLinearCopowers k E)) (DGFunctor.HomogeneousNatTrans.id (DGFunctor.id C)) 0

    The forward adjunction-twist comparison is the strict cone lift of the canonical evaluation comparison and the identity target map.

    source
    theorem CategoryTheory.LinearEvaluationData.TwistConeData.inclusion_comp_adjunctionTwistIso_hom_val {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [HasLinearCopowers k C] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) (L : (linearCopowerAdjunction k E).CounitConeData) :
    ((DGFunctor.HomogeneousNatTrans.composition (DGFunctor.id C) K.twist (DGAdjunction.CounitConeData.twist (linearCopowerAdjunction k E) L) 0 0 0 ⋯) (DGFunctor.HomogeneousNatTrans.ConeData.inr K)) ↑(K.adjunctionTwistIso L).hom = DGAdjunction.CounitConeData.inclusion (linearCopowerAdjunction k E) L

    The adjunction-twist identification strictly preserves the canonical map from the identity functor into the cone.

    source
    theorem CategoryTheory.LinearEvaluationData.TwistConeData.adjunctionTwistIso_self {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [HasLinearCopowers k C] {E : C} (K : TwistConeData k (ofHasLinearCopowers k E)) :
    K.adjunctionTwistIso K = Iso.refl (have this := K.twist; this)

    For the selected evaluation data and the same cone choice, the object-twist/adjunction-twist identification is the identity.

    source
    theorem CategoryTheory.LinearEvaluationData.TwistConeData.twist_eq_adjunctionTwist {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [HasLinearCopowers k C] {E : C} (K : TwistConeData k (ofHasLinearCopowers k E)) :
    K.twist = DGAdjunction.CounitConeData.twist (linearCopowerAdjunction k E) K

    For the selected evaluation data, the object-twist functor and the adjunction counit-twist functor are definitionally identical.

    source
    theorem CategoryTheory.LinearEvaluationData.TwistConeData.compareIso_trans_adjunctionTwistIso {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [HasLinearCopowers k C] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) {W : LinearEvaluationData k E} (L : TwistConeData k W) (M : (linearCopowerAdjunction k E).CounitConeData) :
    K.compareIso L ≪≫ L.adjunctionTwistIso M = K.adjunctionTwistIso M

    Changing arbitrary scalar-linear evaluation data before comparing with the adjunction twist gives the direct adjunction-twist comparison.