Documentation

DerivedAlgGeo.CategoryTheory.Triangulated.DGEnhancement.H0.ConeFunctor

Functorial dg cones, read in a presented category #

H0.coneTriangleFunctor is intrinsic to the dg category and is owned by Algebra/Homology/DGCategory/Pretriangulated/H0/ConeFunctor.lean. This file is the adapter: it transports those cone triangles along the comparison equivalence of an Enhancement, which is where a chosen ordinary category first appears.

The two compatibilities are hypotheses, in two different strengths #

Transporting a triangle at all needs the comparison to commute with the shift, so coneTriangleFunctor below carries [e.equiv.functor.CommShift ℤ]. Concluding that the transported triangle is distinguished needs the comparison to be exact, so coneTriangleFunctor_obj_distinguished additionally carries [e.equiv.functor.IsTriangulated]. Neither is proved here or anywhere else for a general presentation; Cdg.enhancementExact is the one place either is discharged.

Keeping the weaker construction under the weaker hypothesis is deliberate: a consumer that only needs the triangle's vertices should not be made to supply exactness it cannot prove. Exact.coneTriangle_mem_distTriang at the end is the same conclusion read off the bundled refinement, for a consumer that holds one.

source
noncomputable def CategoryTheory.Enhancement.coneTriangleFunctor {W : Type u'} [Category.{v', u'} W] [HasShift W ℤ] (e : Enhancement W) [e.equiv.functor.CommShift ℤ] :
Functor (DGCategory.ConePresentation e.dgCat) (Pretriangulated.Triangle W)

The functorial dg cone triangles of an enhancement, read in the enhanced category through the comparison equivalence. This is the form in which an enhanced kernel category, or any other enhanced triangulated category, hands its chosen cones to ordinary triangulated consumers.

Equations
Instances For
    source
    @[simp]
    theorem CategoryTheory.Enhancement.coneTriangleFunctor_obj_obj₁ {W : Type u'} [Category.{v', u'} W] [HasShift W ℤ] (e : Enhancement W) [e.equiv.functor.CommShift ℤ] (A : DGCategory.ConePresentation e.dgCat) :
    (e.coneTriangleFunctor.obj A).obj₁ = e.equiv.functor.obj A.source
    source
    @[simp]
    theorem CategoryTheory.Enhancement.coneTriangleFunctor_obj_obj₂ {W : Type u'} [Category.{v', u'} W] [HasShift W ℤ] (e : Enhancement W) [e.equiv.functor.CommShift ℤ] (A : DGCategory.ConePresentation e.dgCat) :
    (e.coneTriangleFunctor.obj A).obj₂ = e.equiv.functor.obj A.target
    source
    @[simp]
    theorem CategoryTheory.Enhancement.coneTriangleFunctor_obj_obj₃ {W : Type u'} [Category.{v', u'} W] [HasShift W ℤ] (e : Enhancement W) [e.equiv.functor.CommShift ℤ] (A : DGCategory.ConePresentation e.dgCat) :
    (e.coneTriangleFunctor.obj A).obj₃ = e.equiv.functor.obj A.cone
    source
    theorem CategoryTheory.Enhancement.coneTriangleFunctor_obj_distinguished {W : Type u'} [Category.{v', u'} W] [HasShift W ℤ] (e : Enhancement W) [e.equiv.functor.CommShift ℤ] [Limits.HasZeroObject W] [Preadditive W] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] [e.equiv.functor.IsTriangulated] (A : DGCategory.ConePresentation e.dgCat) :
    e.coneTriangleFunctor.obj A ∈ Pretriangulated.distinguishedTriangles

    When the comparison equivalence is exact, every transported cone triangle is distinguished in the enhanced category.

    source
    theorem CategoryTheory.Enhancement.Exact.coneTriangle_mem_distTriang {W : Type u'} [Category.{v', u'} W] [Limits.HasZeroObject W] [Preadditive W] [HasShift W ℤ] [∀ (n : ℤ), (shiftFunctor W n).Additive] [Pretriangulated W] {e : Enhancement W} (h : e.Exact) (A : DGCategory.ConePresentation e.dgCat) :
    h.mapTriangle.obj ((H0.coneTriangleFunctor e.dgCat).obj A) ∈ Pretriangulated.distinguishedTriangles

    The same conclusion as coneTriangleFunctor_obj_distinguished, read off a bundled Enhancement.Exact instead of two loose instance hypotheses.

    This is the form a consumer that already holds the refinement wants: it supplies one term rather than arranging for two typeclass goals to be solved, and the CommShift used to transport the triangle is visibly the one the refinement carries rather than whichever instance happened to be in scope.