The scalar-linear object-twist triangle

For scalar-linear evaluation data, a choice of objectwise cones gives the functorial triangle

Hom(E,X) ⊗ E ⟶ X ⟶ T_E X ⟶ (Hom(E,X) ⊗ E)⟦1⟧

on H⁰. Every value is distinguished. The construction is the existing generic cone-triangle functor, and the comparison across evaluation and cone choices is the existing strict-square comparison.

This file is the scalar-linear analogue of the additive object-twist triangle; it does not assert that the two evaluation packages agree. Nor does it claim that the twist is invertible or that the object is spherical.

noncomputable def CategoryTheory.LinearEvaluationData.TwistConeData.twistTriangleFunctor {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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) : Functor (H0 C) (Pretriangulated.Triangle (H0 C))

The scalar-linear object-twist triangle as a functor on H⁰.

Equations

• K.twistTriangleFunctor = CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.triangleFunctor K ⋯

theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistTriangleFunctor_obj_mem_distinguishedTriangles {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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) (X : H0 C) : K.twistTriangleFunctor.obj X ∈ H0.distinguishedTriangles C

The generic cone construction makes the displayed family pointwise distinguished; this is the bridge used by triangle and K₀ consumers.

@[simp]

theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistTriangleFunctor_obj_obj₁ {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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) (X : H0 C) : (K.twistTriangleFunctor.obj X).obj₁ = V.functor.h0.obj X

The first vertex retains the chosen scalar-linear evaluation functor, so downstream formulas can rewrite it without unfolding the cone construction.

@[simp]

theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistTriangleFunctor_obj_obj₂ {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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) (X : H0 C) : (K.twistTriangleFunctor.obj X).obj₂ = X

The middle vertex is the original object, definitionally.

@[simp]

theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistTriangleFunctor_obj_obj₃ {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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) (X : H0 C) : (K.twistTriangleFunctor.obj X).obj₃ = K.twist.h0.obj X

This projection keeps exactness and K₀ consumers in the normal form K.twist.h0 without unfolding the generic cone triangle.

theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistTriangleFunctor_obj_mor₁ {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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) (X : H0 C) : (K.twistTriangleFunctor.obj X).mor₁ = (DGFunctor.HomogeneousNatTrans.h0 V.evaluation ⋯).app X

The cone triangle reuses the existing evaluation transformation on H⁰; it does not introduce a second object-twist arrow.

theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistTriangleFunctor_obj_mor₂ {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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) (X : H0 C) : (K.twistTriangleFunctor.obj X).mor₂ = (DGFunctor.HomogeneousNatTrans.h0 (DGFunctor.HomogeneousNatTrans.ConeData.inr K) ⋯).app X

The second map is definitionally the generic cone inclusion, so the dg-level strict inclusion comparisons descend without another compatibility proof.

@[simp]

theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistTriangleFunctor_map_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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) {X Y : H0 C} (f : X ⟶ Y) : (K.twistTriangleFunctor.map f).hom₁ = V.functor.h0.map f

Naturality on the first vertices is inherited from scalar-linear evaluation.

@[simp]

theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistTriangleFunctor_map_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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) {X Y : H0 C} (f : X ⟶ Y) : (K.twistTriangleFunctor.map f).hom₃ = K.twist.h0.map f

Naturality on the third vertices is the H⁰ action of the twist dg functor.

@[reducible]

noncomputable def CategoryTheory.LinearEvaluationData.TwistConeData.twistH0CommShift {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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) : K.twist.h0.CommShift ℤ

The canonical shift comparison for H⁰ of the scalar-linear object twist.

Equations

• K.twistH0CommShift = K.twist.h0CommShift

theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistH0IsTriangulated {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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) : K.twist.h0.IsTriangulated

The scalar-linear object twist is exact on H⁰. This is independent of, and weaker than, invertibility.

noncomputable def CategoryTheory.LinearEvaluationData.TwistConeData.twistTriangleIso {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] {E : C} {V : LinearEvaluationData k E} (K K' : TwistConeData k V) : K.twistTriangleFunctor ≅ K'.twistTriangleFunctor

The scalar-linear object-twist triangle does not depend on its cone choice.

Equations

• K.twistTriangleIso K' = CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.compareIso ⋯ K K'

noncomputable def CategoryTheory.LinearEvaluationData.TwistConeData.twistTriangleIsoOfEvaluation {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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) {W : LinearEvaluationData k E} (L : TwistConeData k W) : K.twistTriangleFunctor ≅ L.twistTriangleFunctor

The scalar-linear object-twist triangle does not depend on either the evaluation data or the cone choices.

Equations

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

@[simp]

theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistTriangleIsoOfEvaluation_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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) {W : LinearEvaluationData k E} (L : TwistConeData k W) (X : H0 C) : ((K.twistTriangleIsoOfEvaluation L).hom.app X).hom₁ = (DGFunctor.h0Iso (V.compareIso W)).hom.app X

The first component of the triangle comparison is the H⁰ image of the canonical scalar-linear evaluation comparison.

@[simp]

theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistTriangleIsoOfEvaluation_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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) {W : LinearEvaluationData k E} (L : TwistConeData k W) (X : H0 C) : ((K.twistTriangleIsoOfEvaluation L).hom.app X).hom₂ = CategoryStruct.id X

The middle component of the triangle comparison is the identity.

@[simp]

theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistTriangleIsoOfEvaluation_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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) {W : LinearEvaluationData k E} (L : TwistConeData k W) (X : H0 C) : ((K.twistTriangleIsoOfEvaluation L).hom.app X).hom₃ = (DGFunctor.h0Iso (K.compareIso L)).hom.app X

The third component is the H⁰ image of the strict cone-functor comparison.

@[simp]

theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistTriangleIsoOfEvaluation_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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) : K.twistTriangleIsoOfEvaluation K = Iso.refl K.twistTriangleFunctor

Comparing a scalar-linear evaluation and cone choice with itself gives the identity natural isomorphism of triangle functors.

theorem CategoryTheory.LinearEvaluationData.TwistConeData.twistTriangleIsoOfEvaluation_trans {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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) {W X : LinearEvaluationData k E} (L : TwistConeData k W) (M : TwistConeData k X) : K.twistTriangleIsoOfEvaluation L ≪≫ L.twistTriangleIsoOfEvaluation M = K.twistTriangleIsoOfEvaluation M

Scalar-linear twist-triangle comparisons compose coherently across both evaluation and cone choices.