Documentation

DerivedAlgGeo.Algebra.Homology.DGCategory.Pretriangulated.H0.LinearObjectTwistAdjunction

Scalar-linear object-twist triangles as adjunction twist triangles #

The scalar-linear object-twist triangle for the selected copowers is definitionally the counit-twist triangle of the copower--Hom dg adjunction. For arbitrary scalar-linear evaluation data, the strict dg comparison descends to a natural isomorphism of the full triangle functors on H⁰.

The first component is the canonical comparison to the selected evaluation functor, the second is the identity, and the third is the H⁰ image of the dg twist comparison. This identifies two presentations of the same twist candidate; it supplies neither an autoequivalence nor sphericality.

source
theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistTriangleFunctor_eq_adjunctionTwistTriangleFunctor {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [IsPretriangulated 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.twistTriangleFunctor = DGAdjunction.CounitConeData.twistTriangleFunctor (linearCopowerAdjunction k E) K

For the selected scalar-linear evaluation, the object-twist triangle and the copower--Hom adjunction's counit-twist triangle are definitionally the same functor.

source
noncomputable def CategoryTheory.LinearEvaluationData.TwistConeData.adjunctionTwistTriangleIso {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [IsPretriangulated 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.twistTriangleFunctor ≅ DGAdjunction.CounitConeData.twistTriangleFunctor (linearCopowerAdjunction k E) L

The canonical identification of an arbitrary scalar-linear object-twist triangle with the counit-twist triangle of the selected copower--Hom dg adjunction.

Equations
Instances For
    source
    theorem CategoryTheory.LinearEvaluationData.TwistConeData.adjunctionTwistTriangleIso_hom_app_hom₁ {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [IsPretriangulated 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) (X : H0 C) :
    ((K.adjunctionTwistTriangleIso L).hom.app X).hom₁ = (DGFunctor.h0Iso (V.compareIso (ofHasLinearCopowers k E))).hom.app X

    On first vertices, the adjunction-triangle identification is the H⁰ image of the canonical comparison to the selected evaluation functor.

    source
    theorem CategoryTheory.LinearEvaluationData.TwistConeData.adjunctionTwistTriangleIso_hom_app_hom₂ {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [IsPretriangulated 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) (X : H0 C) :
    ((K.adjunctionTwistTriangleIso L).hom.app X).hom₂ = CategoryStruct.id X

    On middle vertices, the adjunction-triangle identification is the identity.

    source
    theorem CategoryTheory.LinearEvaluationData.TwistConeData.adjunctionTwistTriangleIso_hom_app_hom₃ {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [IsPretriangulated 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) (X : H0 C) :
    ((K.adjunctionTwistTriangleIso L).hom.app X).hom₃ = (DGFunctor.h0Iso (K.adjunctionTwistIso L)).hom.app X

    On third vertices, the comparison is the H⁰ image of the dg object-twist/adjunction-twist identification.

    source
    theorem CategoryTheory.LinearEvaluationData.TwistConeData.adjunctionTwistTriangleIso_self {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [IsPretriangulated 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.adjunctionTwistTriangleIso K = Iso.refl K.twistTriangleFunctor

    For a selected cone compared with itself, the identification of the two triangle presentations is the identity.

    source
    theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistTriangleIsoOfEvaluation_trans_adjunctionTwistTriangleIso {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [IsPretriangulated 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.twistTriangleIsoOfEvaluation L ≪≫ L.adjunctionTwistTriangleIso M = K.adjunctionTwistTriangleIso M

    Changing scalar-linear evaluation data first and then identifying the adjunction presentation gives the direct triangle identification.