Route (b): the dg object twists are `SphericalTwistData` #

SphericalTwistData (in Definition.lean) is an interface that constructs nothing. This file shows that route (b) of its encoding note, the dg enhancement, discharges every field, so that the three instance fields of T are not an unsatisfiable demand.

Main definitions #

LinearEvaluationData.TwistConeData.toSphericalTwistData and EvaluationData.TwistConeData.toSphericalTwistData — the scalar-linear and the additive realization, each given the Euler copower formula.

Implementation notes #

For a pretriangulated dg category C and an object E, the object twist T_E = Cone(Hom(E,-) ⊗ E ⟶ id) is a dg functor, and

T.Additive, T.CommShift ℤ and T.IsTriangulated on H⁰ C are proved: DGFunctor.h0CommShift and DGFunctor.h0IsTriangulated hold for every dg functor;
the evaluation triangle is the existing functor twistTriangleFunctor : H⁰ C ⥤ Triangle (H⁰ C), every value of which is distinguished; the three structure maps and their naturality are its three projections.

The one input beyond the dg construction is the copower's class, the field copower_class: the rank-one formula [Hom(E,X) ⊗ E] = χ(E,X)·[E], which is IsEulerCopower of DGEnhancement/H0/ObjectTwistK0.lean and DGEnhancement/H0/LinearEvaluationK0.lean and the field's type on the nose. Both constructions take it as a hypothesis hV; neither depends on how, or whether, the repository proves it for a particular package.

Two constructions, one per evaluation package, and neither derived from the other: the additive EvaluationData (copowers by additive cochains over ℤ) and the scalar-linear LinearEvaluationData (copowers by k-linear cochains). The repository has no adapter between them and this file adds none. Two independent producers witness that the interface is not tailored to one construction.

What this does not say #

Nothing here says T is an autoequivalence, that E is spherical, or constructs a copower: the copower object assignment is the one the evaluation data already chose.

source

noncomputable def CategoryTheory.LinearEvaluationData.TwistConeData.toSphericalTwistData (k : Type w) [Field k] {C : Type u} [DGCategory C] [IsPretriangulated C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [Triangulated.HomFiniteBounded k (H0 C)] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) (hV : IsEulerCopower k V) :

Triangulated.SphericalTwist.SphericalTwistData k (H0 C) (have this := E; this)

The scalar-linear dg object twist is SphericalTwistData, given the Euler copower formula.

Every field but copower_class is the existing dg construction on H⁰ C: the instances of T are the proved h0CommShift and h0IsTriangulated, and ev, π, δ and distinguished are the three maps and the distinguished values of twistTriangleFunctor.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.LinearEvaluationData.TwistConeData.toSphericalTwistData_T (k : Type w) [Field k] {C : Type u} [DGCategory C] [IsPretriangulated C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [Triangulated.HomFiniteBounded k (H0 C)] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) (hV : IsEulerCopower k V) :

(toSphericalTwistData k K hV).T = K.twist.h0

The functor of the constructed data is the dg twist on H⁰, on the nose.

source

@[simp]

theorem CategoryTheory.LinearEvaluationData.TwistConeData.toSphericalTwistData_copower (k : Type w) [Field k] {C : Type u} [DGCategory C] [IsPretriangulated C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [Triangulated.HomFiniteBounded k (H0 C)] {E : C} {V : LinearEvaluationData k E} (K : TwistConeData k V) (hV : IsEulerCopower k V) :

(toSphericalTwistData k K hV).copower = V.functor.h0

The copower of the constructed data is the scalar-linear evaluation functor on H⁰.

source

noncomputable def CategoryTheory.EvaluationData.TwistConeData.toSphericalTwistData (k : Type w) [DivisionRing k] {C : Type u} [DGCategory C] [IsPretriangulated C] [Linear k (H0 C)] [Triangulated.HomFiniteBounded k (H0 C)] {E : C} {V : EvaluationData E} (K : V.TwistConeData) (hV : IsEulerCopower k V) :

Triangulated.SphericalTwist.SphericalTwistData k (H0 C) (have this := E; this)

The additive dg object twist is SphericalTwistData, given the Euler copower formula. The construction of LinearEvaluationData.TwistConeData.toSphericalTwistData for the additive evaluation package; the two are not compared.

Equations