Documentation

DerivedAlgGeo.Algebra.Homology.DGCategory.Pretriangulated.H0.ConeFunctor

Functorial dg cones in H⁰ #

The category DGCategory.ConePresentation C retains a closed dg arrow, a chosen cone, and homotopy-coherent maps between such presentations. This file sends that category functorially to the category of triangles in H⁰ C.

This is stronger than choosing a triangulated cone object-by-object: identity and composition are inherited from the explicit dg homotopies and cone maps, and every object lands in the full subcategory of distinguished triangles. The pretriangulated instance is needed only for the H⁰ side, where the chosen shift functor lives; the category of cone presentations itself needs none.

Everything here is intrinsic to the dg category: no ordinary category has been chosen, and no comparison equivalence appears. Reading these cone triangles in an enhanced category is the adapter CategoryTheory/Triangulated/DGEnhancement/H0/ConeFunctor.lean, which is where the shift and exactness compatibilities of a comparison are required.

source
noncomputable def CategoryTheory.H0.coneSourceFunctor (C : Type u) [DGCategory C] :
Functor (DGCategory.ConePresentation C) (H0 C)

The source vertex of a chosen dg cone presentation, functorially in homotopy-coherent maps of presentations.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def CategoryTheory.H0.coneTargetFunctor (C : Type u) [DGCategory C] :
    Functor (DGCategory.ConePresentation C) (H0 C)

    The target vertex of a chosen dg cone presentation.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def CategoryTheory.H0.coneObjectFunctor (C : Type u) [DGCategory C] :
      Functor (DGCategory.ConePresentation C) (H0 C)

      The chosen cone vertex, with the retained closed dg cone map on morphisms.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.H0.coneSourceFunctor_obj (C : Type u) [DGCategory C] (A : DGCategory.ConePresentation C) :
        (coneSourceFunctor C).obj A = A.source
        source
        @[simp]
        theorem CategoryTheory.H0.coneSourceFunctor_map (C : Type u) [DGCategory C] {A B : DGCategory.ConePresentation C} (m : A ⟶ B) :
        (coneSourceFunctor C).map m = homMk ⟨m.source, ⋯⟩
        source
        @[simp]
        theorem CategoryTheory.H0.coneTargetFunctor_obj (C : Type u) [DGCategory C] (A : DGCategory.ConePresentation C) :
        (coneTargetFunctor C).obj A = A.target
        source
        @[simp]
        theorem CategoryTheory.H0.coneTargetFunctor_map (C : Type u) [DGCategory C] {A B : DGCategory.ConePresentation C} (m : A ⟶ B) :
        (coneTargetFunctor C).map m = homMk ⟨m.target, ⋯⟩
        source
        @[simp]
        theorem CategoryTheory.H0.coneObjectFunctor_obj (C : Type u) [DGCategory C] (A : DGCategory.ConePresentation C) :
        (coneObjectFunctor C).obj A = A.cone
        source
        @[simp]
        theorem CategoryTheory.H0.coneObjectFunctor_map (C : Type u) [DGCategory C] {A B : DGCategory.ConePresentation C} (m : A ⟶ B) :
        (coneObjectFunctor C).map m = homMk m.coneMorphism.hom
        source
        noncomputable def CategoryTheory.H0.coneTriangleFunctor (C : Type u) [DGCategory C] [IsPretriangulated C] :
        Functor (DGCategory.ConePresentation C) (Pretriangulated.Triangle (H0 C))

        A chosen dg cone presentation determines a triangle in H⁰, and a homotopy-coherent cone morphism determines a morphism of those triangles. The construction preserves identities and composition.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.H0.coneTriangleFunctor_obj (C : Type u) [DGCategory C] [IsPretriangulated C] (A : DGCategory.ConePresentation C) :
          (coneTriangleFunctor C).obj A = coneTriangle A.arrow A.isCone
          source
          @[simp]
          theorem CategoryTheory.H0.coneTriangleFunctor_map (C : Type u) [DGCategory C] [IsPretriangulated C] {A B : DGCategory.ConePresentation C} (m : A ⟶ B) :
          (coneTriangleFunctor C).map m = IsConeOf.Morphism.toTriangleMorphism A.isCone B.isCone m.coneMorphism
          source
          theorem CategoryTheory.H0.coneTriangleFunctor_obj_distinguished (C : Type u) [DGCategory C] [IsPretriangulated C] (A : DGCategory.ConePresentation C) :
          (coneTriangleFunctor C).obj A ∈ Pretriangulated.distinguishedTriangles

          Every triangle in the functorial dg cone family is distinguished.

          source
          @[reducible, inline]
          abbrev CategoryTheory.H0.distinguishedTriangleProperty (C : Type u) [DGCategory C] [IsPretriangulated C] :
          ObjectProperty (Pretriangulated.Triangle (H0 C))

          The object property of being a distinguished triangle in H⁰ C.

          Equations
          Instances For
            source
            noncomputable def CategoryTheory.H0.distinguishedConeTriangleFunctor (C : Type u) [DGCategory C] [IsPretriangulated C] :
            Functor (DGCategory.ConePresentation C) (distinguishedTriangleProperty C).FullSubcategory

            The functorial dg cone construction with its codomain restricted to the full subcategory of distinguished triangles.

            Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.H0.distinguishedConeTriangleFunctor_obj_val (C : Type u) [DGCategory C] [IsPretriangulated C] (A : DGCategory.ConePresentation C) :
              ((distinguishedConeTriangleFunctor C).obj A).obj = coneTriangle A.arrow A.isCone