The transported triangulated structure is Mathlib's

dg-enhancements-e7. H⁰(C^dg A) carries the pretriangulated structure H0Triangle.lean builds out of dg cones, and K(A) = HomotopyCategory A carries Mathlib's, built out of mapping cones. Cdg.seam identifies the two categories and Model/CommShift.lean identifies their shifts. This file proves that the two structures agree.

What "agree" means, and why it is a set equality

Pretriangulated.distinguishedTriangles is a field of the class, so the two structures agree exactly when the two sets of triangles correspond. No notion of "isomorphism of triangulated structures" exists at the pin, and none is invented here: the theorem is

Cdg.seam_distinguishedTriangles_eq :
  {T | Cdg.seam.inverse.mapTriangle.obj T ∈ H0.distinguishedTriangles (Cdg A)}
    = HomotopyCategory.Pretriangulated.distinguishedTriangles A

an equality of two terms of Set (Triangle (HomotopyCategory A (ComplexShape.up ℤ))). Cdg.distinguishedTriangles_eq is the same statement read on H⁰, and Cdg.mem_distTriang_iff is the pointwise form both come from.

Transporting a triangle needs the shift comparison, which is why Functor.mapTriangle -- and hence this file -- rests on Cdg.h0FunctorCommShift. Nothing here assumes the comparison; it is the CommShift instance built in HomotopyCategory/CommShift.lean.

The sign

The dg connecting morphism IsConeOf.toShift is fst followed by the shift with no sign; Mathlib's CochainComplex.mappingCone.triangle uses -mappingCone.fst. Cdg.triangle_mor₃_eq records that discrepancy, and H0.coneTriangle carries the sign that removes it. Without it the two structures would genuinely differ: diagonal isomorphisms of triangles realise exactly the sign patterns whose product over the three vertices is +1, and negating the third map alone is not one of them, so the disagreement could not be absorbed by an isomorphism.

The octahedral half

The pin supplies IsTriangulated (HomotopyCategory A (ComplexShape.up ℤ)) (Mathlib/Algebra/Homology/HomotopyCategory/Triangulated.lean), so the octahedral axiom transfers back along the fully faithful triangulated seam: IsTriangulated (H0 (Cdg A)) is an instance below. It is stated only for this model. For a general pretriangulated dg category C this file proves nothing about IsTriangulated (H0 C), and nothing at the pin does either -- the octahedron there would have to be built from the dg cone directly, which is not dg-enhancements-e7's scope.

backward.isDefEq.respectTransparency

H0 C is a type synonym for C, so goals about H0 (Cdg A) are routinely ill-typed at instances transparency and rewriting stalls. Mathlib's own set_option backward.isDefEq.respectTransparency false is the sanctioned way through, and it is used here for exactly the declarations that need it.

theorem CategoryTheory.Cdg.isConeOf_fst {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] {K L : Cdg A} (f : ↑((DGCategoryStruct.dgHom K L).X 0)) (hf : f ∈ cocycles K L) : (isConeOf f hf).fst = ↑(CochainComplex.mappingCone.fst (coneHom f hf))

The dg cone's degree-one projection is Mathlib's mappingCone.fst.

theorem CategoryTheory.Cdg.toShift_isShiftBy {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] {K L : Cdg A} (f : ↑((DGCategoryStruct.dgHom K L).X 0)) (hf : f ∈ cocycles K L) : (isConeOf f hf).toShift (K.isShiftBy 1) = (↑(CochainComplex.mappingCone.fst (coneHom f hf))).rightShift 1 0 ⋯

The dg connecting morphism, at the model shift, is Mathlib's fst right-shifted.

theorem CategoryTheory.Cdg.triangle_mor₃_eq {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] {K L : Cdg A} (f : ↑((DGCategoryStruct.dgHom K L).X 0)) (hf : f ∈ cocycles K L) : (CochainComplex.mappingCone.triangle (coneHom f hf)).mor₃ = (-((coneObj f hf).toCocycle (K.shiftObj 1)) ⟨(isConeOf f hf).toShift (K.isShiftBy 1), ⋯⟩).homOf

The sign. Mathlib's standard triangle uses -mappingCone.fst; the dg toShift is +fst. This is why H0.coneTriangle carries a sign.

theorem CategoryTheory.Cdg.h0Functor_commShiftIso_hom_app {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] (n : ℤ) (X : H0 (Cdg A)) : (Functor.commShiftIso h0Functor n).hom.app X = (seamShiftIso n X).hom

noncomputable def CategoryTheory.Cdg.mapTriangleConeTriangleIso {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] {K L : Cdg A} (f : ↥(cocycles K L)) : h0Functor.mapTriangle.obj (H0.coneTriangle f (isConeOf ↑f ⋯)) ≅ CochainComplex.mappingCone.triangleh (coneHom ↑f ⋯)

The image of a model cone triangle is Mathlib's standard triangle.

Equations

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

instance CategoryTheory.Cdg.h0FunctorIsTriangulated {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] : h0Functor.IsTriangulated

The seam is a triangulated functor.

theorem CategoryTheory.Cdg.mem_distTriang_iff {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] (T : Pretriangulated.Triangle (H0 (Cdg A))) : h0Functor.mapTriangle.obj T ∈ Pretriangulated.distinguishedTriangles ↔ T ∈ Pretriangulated.distinguishedTriangles

The agreement theorem, as an equivalence.

theorem CategoryTheory.Cdg.distinguishedTriangles_eq {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] : H0.distinguishedTriangles (Cdg A) = h0Functor.mapTriangle.obj ⁻¹' HomotopyCategory.Pretriangulated.distinguishedTriangles A

The agreement theorem, as an equality of sets of triangles.

instance CategoryTheory.Cdg.instIsTriangulatedH0 {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] : IsTriangulated (H0 (Cdg A))

The octahedral axiom for H⁰(C^dg A).

The same statements, read on the seam

@[implicit_reducible]

noncomputable instance CategoryTheory.Cdg.seamFunctorCommShift {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] : seam.functor.CommShift ℤ

Equations

• CategoryTheory.Cdg.seamFunctorCommShift = { commShiftIso := CategoryTheory.Cdg.seamFunctorCommShift._aux_1, commShiftIso_zero := ⋯, commShiftIso_add := ⋯ }

@[implicit_reducible]

noncomputable instance CategoryTheory.Cdg.seamInverseCommShift {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] : seam.inverse.CommShift ℤ

Equations

• CategoryTheory.Cdg.seamInverseCommShift = CategoryTheory.Cdg.seam.commShiftInverse ℤ

instance CategoryTheory.Cdg.seamCommShift {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] : seam.CommShift ℤ

instance CategoryTheory.Cdg.seamFunctorIsTriangulated {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] : seam.functor.IsTriangulated

instance CategoryTheory.Cdg.seamIsTriangulated {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] : seam.IsTriangulated

theorem CategoryTheory.Cdg.seam_distinguishedTriangles_eq {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] : {T : Pretriangulated.Triangle (HomotopyCategory A (ComplexShape.up ℤ)) | seam.inverse.mapTriangle.obj T ∈ H0.distinguishedTriangles (Cdg A)} = HomotopyCategory.Pretriangulated.distinguishedTriangles A

The agreement theorem, transported onto the homotopy category.

noncomputable def CategoryTheory.Cdg.enhancementExact {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] : (enhancement A).Exact

C^dg A is an exact enhancement of the homotopy category, not merely an H⁰ presentation of it.

Enhancement.Exact is supplied data everywhere else in the library; this is the one place it is discharged, and both fields come from theorems rather than from a hypothesis. commShift is Cdg.h0FunctorCommShift, built in HomotopyCategory/CommShift.lean from the seam's shift comparison; isTriangulated is Cdg.h0FunctorIsTriangulated above, which is the agreement theorem seam_distinguishedTriangles_eq in functor form.

Neither this nor anything downstream says that an exact enhancement of HomotopyCategory A is unique. dg-enhancements-e15 remains open, and the statement it will need quantifies over this structure rather than over Enhancement.

Equations

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