The category of chosen dg cones

A cone in a dg category is useful functorially only when morphisms retain the degree-minus-one homotopy witnessing commutativity of the underlying square. DGCategory.ConePresentation bundles a closed dg arrow with a chosen cone, and its morphisms are the homotopy squares and closed cone maps constructed in Pretriangulated.Lift.

The resulting category is the reusable dg-level owner of functorial cones. Its composition uses the explicit composite homotopy and cone map, and both cone squares are stated on the cone projections, so no shift witness and no pretriangulated instance are needed. Passage to ordinary distinguished triangles belongs to the DGEnhancement/H0 layer.

structure CategoryTheory.DGCategory.ConePresentation (C : Type u) [DGCategory C] : Type (max u v)

A closed degree-zero dg arrow together with a chosen cone object and cone witness.

• source : C

  Source of the presented arrow.

• target : C

  Target of the presented arrow.

• arrow : ↥(cocycles self.source self.target)

  The closed arrow whose cone is presented.

• cone : C

  The chosen cone object.

• isCone : IsConeOf (↑self.arrow) self.cone

  The chosen representability witness for the cone.

structure CategoryTheory.DGCategory.ConePresentation.Hom {C : Type u} [DGCategory C] (A B : ConePresentation C) : Type v

A morphism of chosen cone presentations. The maps on source and target are dg morphisms, and coneMorphism retains both the chosen homotopy and the closed map on cones.

• source : ↑((DGCategoryStruct.dgHom A.source B.source).X 0)

  Map between source objects.

• target : ↑((DGCategoryStruct.dgHom A.target B.target).X 0)

  Map between target objects.

• coneMorphism : A.isCone.Morphism B.isCone self.source self.target

  The homotopy-coherent induced map between the chosen cones.

theorem CategoryTheory.DGCategory.ConePresentation.Hom.ext {C : Type u} [DGCategory C] {A B : ConePresentation C} {m n : A.Hom B} (hsource : m.source = n.source) (htarget : m.target = n.target) (hhomotopy : m.coneMorphism.homotopy = n.coneMorphism.homotopy) (hcone : ↑m.coneMorphism.hom = ↑n.coneMorphism.hom) : m = n

A morphism of cone presentations is determined by its two boundary maps, chosen homotopy, and map on cones.

theorem CategoryTheory.DGCategory.ConePresentation.Hom.ext_iff {C : Type u} [DGCategory C] {A B : ConePresentation C} {m n : A.Hom B} : m = n ↔ m.source = n.source ∧ m.target = n.target ∧ m.coneMorphism.homotopy = n.coneMorphism.homotopy ∧ ↑m.coneMorphism.hom = ↑n.coneMorphism.hom

def CategoryTheory.DGCategory.ConePresentation.Hom.id {C : Type u} [DGCategory C] (A : ConePresentation C) : A.Hom A

Identity morphism of a chosen cone presentation.

Equations

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

def CategoryTheory.DGCategory.ConePresentation.Hom.comp {C : Type u} [DGCategory C] {A B D : ConePresentation C} (m : A.Hom B) (n : B.Hom D) : A.Hom D

Composition of morphisms of chosen cone presentations.

Equations

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

@[implicit_reducible]

instance CategoryTheory.DGCategory.ConePresentation.instCategory {C : Type u} [DGCategory C] : Category.{v, max u v} (ConePresentation C)

Chosen dg cones and their homotopy-coherent cone morphisms form a category.

Equations

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

@[simp]

theorem CategoryTheory.DGCategory.ConePresentation.id_source {C : Type u} [DGCategory C] (A : ConePresentation C) : (CategoryStruct.id A).source = DGCategoryStruct.dgId A.source

@[simp]

theorem CategoryTheory.DGCategory.ConePresentation.id_target {C : Type u} [DGCategory C] (A : ConePresentation C) : (CategoryStruct.id A).target = DGCategoryStruct.dgId A.target

@[simp]

theorem CategoryTheory.DGCategory.ConePresentation.comp_source {C : Type u} [DGCategory C] {A B D : ConePresentation C} (m : A ⟶ B) (n : B ⟶ D) : (CategoryStruct.comp m n).source = ((DGCategoryStruct.dgComp 0 0 0 ⋯) m.source) n.source

@[simp]

theorem CategoryTheory.DGCategory.ConePresentation.comp_target {C : Type u} [DGCategory C] {A B D : ConePresentation C} (m : A ⟶ B) (n : B ⟶ D) : (CategoryStruct.comp m n).target = ((DGCategoryStruct.dgComp 0 0 0 ⋯) m.target) n.target