The object twist from scalar-linear evaluation data

The cone of the scalar-linear evaluation map

DGLinear.homComplex k E X ⊗ₖ E ⟶ X

is the direct scalar-linear version of the Seidel--Thomas object twist. This file only packages the existing generic cone interface under LinearEvaluationData.TwistConeData. Cone construction and structured cone-functor comparisons remain owned by HomogeneousNatTrans.ConeData; automatic shift and chosen-cone preservation are owned by the generic pretriangulated dg-functor layer.

No comparison with additive EvaluationData is asserted: the two evaluation packages represent different universal properties. Cone preservation is automatic for every dg functor by the generic split-cone theorem; this file still makes no autoequivalence claim for the resulting twist.

noncomputable def CategoryTheory.LinearEvaluationData.preservesChosenConesOfCompare (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] {E : C} (V W : LinearEvaluationData k E) (hV : V.functor.PreservesChosenCones) : W.functor.PreservesChosenCones

Cone preservation for scalar-linear evaluation transports across a change of selected evaluation data. This remains useful compatibility data even though the capability is automatic for every dg functor.

Equations

• CategoryTheory.LinearEvaluationData.preservesChosenConesOfCompare k V W hV = hV.ofIso (V.compareIso W)

theorem CategoryTheory.LinearEvaluationData.compare_evaluation_square (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] {E : C} (V W : LinearEvaluationData k 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 scalar-linear evaluation comparison and the identity on the target form a strictly commuting square.

@[reducible, inline]

abbrev CategoryTheory.LinearEvaluationData.TwistConeData (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] {E : C} (V : LinearEvaluationData k E) : Type (max u v)

Chosen objectwise cones of scalar-linear evaluation.

Equations

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

noncomputable def CategoryTheory.LinearEvaluationData.chosenTwistConeData (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] {E : C} (V : LinearEvaluationData k E) [IsPretriangulated C] : TwistConeData k V

A pretriangulated category supplies cones of all scalar-linear evaluation components.

Equations

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.LinearEvaluationData.TwistConeData.twist {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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) : DGFunctor C C

The scalar-linear object twist: the cone of evaluation.

Equations

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

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

The scalar-linear object twist is independent, up to a canonical closed degree-zero isomorphism, of both the evaluation data and the cone choices.

Equations

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

@[simp]

theorem CategoryTheory.LinearEvaluationData.TwistConeData.compareIso_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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) {W : LinearEvaluationData k E} (L : TwistConeData k W) : ↑(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

The forward cone comparison is the generic lift of the evaluation comparison and the identity target map.

@[simp]

theorem CategoryTheory.LinearEvaluationData.TwistConeData.compareIso_inv_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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) {W : LinearEvaluationData k E} (L : TwistConeData k W) : ↑(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

Exposing the inverse as the reverse strict-square lift lets downstream coherence proofs avoid unfolding isoOfStrictSquare.

theorem CategoryTheory.LinearEvaluationData.TwistConeData.inclusion_comp_compareIso_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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) {W : LinearEvaluationData k E} (L : TwistConeData k W) : ((DGFunctor.HomogeneousNatTrans.composition (DGFunctor.id C) K.twist L.twist 0 0 0 ⋯) (DGFunctor.HomogeneousNatTrans.ConeData.inr K)) ↑(K.compareIso L).hom = DGFunctor.HomogeneousNatTrans.ConeData.inr L

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

theorem CategoryTheory.LinearEvaluationData.TwistConeData.compareIso_self_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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) : ↑(K.compareIso K).hom = DGFunctor.HomogeneousNatTrans.id K.twist

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

@[simp]

theorem CategoryTheory.LinearEvaluationData.TwistConeData.compareIso_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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) : K.compareIso K = Iso.refl (have this := K.twist; this)

The scalar-linear twist comparison from a choice to itself is the identity isomorphism.

theorem CategoryTheory.LinearEvaluationData.TwistConeData.compareIso_hom_val_comp {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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) {W X : LinearEvaluationData k E} (L : TwistConeData k W) (M : TwistConeData k X) : ((DGFunctor.HomogeneousNatTrans.composition K.twist L.twist M.twist 0 0 0 ⋯) ↑(K.compareIso L).hom) ↑(L.compareIso M).hom = ↑(K.compareIso M).hom

Strict composition descends from the corresponding law for linear evaluation comparisons, so changing choices in stages gives the direct cone comparison already before passing to H⁰.

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

The strict composition law packages as transitivity of the canonical isomorphisms in the closed degree-zero dg-functor category.

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

The scalar-linear object twist preserves shifts.

Equations

• K.preservesShifts = K.twist.preservesShifts

noncomputable def CategoryTheory.LinearEvaluationData.TwistConeData.preservesChosenCones {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] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) (hV : V.functor.PreservesChosenCones) : K.twist.PreservesChosenCones

The structured 3-by-3 cone-preservation witness for the scalar-linear object twist. Its endpoint argument is redundant but records the generic cone functor construction explicitly.

Equations

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