Transporting dg-functor capabilities to H⁰

DGFunctor.PreservesShifts and DGFunctor.PreservesChosenCones are dg-level capabilities, owned by Algebra/Homology/DGCategory/Pretriangulated/Functor.lean. Every dg functor has both capabilities. This file spends them on the ordinary functor H⁰(F): h0CommShift packages the chosen shift witnesses into a CommShift, and h0IsTriangulated proves that every dg functor between pretriangulated dg categories induces a triangulated functor.

H0/Triangle.lean owns the distinguished triangles of H⁰ and the pretriangulated instance; everything here consumes them, which is why the dependency runs this way rather than the other. Both files sit under the H0 umbrella, so no consumer has to know which of the two a name comes from.

The backward.isDefEq.respectTransparency options are load-bearing

Five declarations below carry set_option backward.isDefEq.respectTransparency false. They were tried without it: commShift fails with a type mismatch whose two sides print identically, and preservesConeTriangles_of_preservesChosenCones fails to find 𝟙 under Functor.map. Both are the shift and cone witnesses being compared at instances transparency, which does not unfold H0, IsPretriangulated.shiftObj or the chosen witnesses. Removing them needs those comparisons restated through explicit show steps, not a tactic swap.

The two uses in Triangulated/FullSubcategory.lean are the same story. Note that until this file was given its own umbrella entry nothing imported it, so a green build was not evidence that these proofs still worked.

Why the cone-generator property is the right hypothesis

H⁰'s distinguished triangles are by definition those isomorphic to a dg cone triangle, so a functor is triangulated as soon as it sends cone triangles to distinguished triangles. PreservesConeTriangles is that condition and nothing more; preservesConeTriangles_of_preservesChosenCones derives it from the strong dg-level capability, and the two isTriangulated_of_… results close the loop.

noncomputable def CategoryTheory.DGFunctor.shiftCommIso {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) (hF : F.PreservesShifts) (n : ℤ) [IsPretriangulated C] [IsPretriangulated D] : (shiftFunctor (H0 C) n).comp F.h0 ≅ F.h0.comp (shiftFunctor (H0 D) n)

The shift comparison induced on H⁰ by dg-level shift preservation.

Equations

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

theorem CategoryTheory.DGFunctor.shiftCommIso_zero_hom_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) [IsPretriangulated C] [IsPretriangulated D] (hF : F.PreservesShifts) (X : H0 C) : (F.shiftCommIso hF 0).hom.app X = CategoryStruct.comp (F.h0.map ((H0.shiftFunctorZeroIso C).hom.app X)) ((H0.shiftFunctorZeroIso D).inv.app (F.h0.obj X))

theorem CategoryTheory.DGFunctor.shiftCommIso_add_hom_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) [IsPretriangulated C] [IsPretriangulated D] (hF : F.PreservesShifts) (a b : ℤ) (X : H0 C) : (F.shiftCommIso hF (a + b)).hom.app X = CategoryStruct.comp (F.h0.map ((H0.shiftFunctorAddIso C a b).hom.app X)) (CategoryStruct.comp ((F.shiftCommIso hF b).hom.app ((H0.shiftFunctor C a).obj X)) (CategoryStruct.comp ((H0.shiftFunctor D b).map ((F.shiftCommIso hF a).hom.app X)) ((H0.shiftFunctorAddIso D a b).inv.app (F.h0.obj X))))

@[reducible]

noncomputable def CategoryTheory.DGFunctor.commShift {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) [IsPretriangulated C] [IsPretriangulated D] (hF : F.PreservesShifts) : F.h0.CommShift ℤ

The dg-level shift-preservation data supplies the coherent shift structure required by the ordinary functor H⁰(F).

Equations

• F.commShift hF = { commShiftIso := fun (n : ℤ) => F.shiftCommIso hF n, commShiftIso_zero := ⋯, commShiftIso_add := ⋯ }

@[reducible]

noncomputable def CategoryTheory.DGFunctor.h0CommShift {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) [IsPretriangulated C] [IsPretriangulated D] : F.h0.CommShift ℤ

The canonical coherent shift package on H⁰(F) for an arbitrary dg functor between pretriangulated dg categories.

This is an explicit definition rather than a global instance so that callers can control which comparison is used when several naturally isomorphic functor presentations are in scope.

Equations

• F.h0CommShift = F.commShift F.preservesShifts

structure CategoryTheory.DGFunctor.PreservesConeTriangles {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) [IsPretriangulated C] [IsPretriangulated D] [F.h0.CommShift ℤ] : Prop

Preservation data for the cone generators of H⁰.

This is the reusable exactness seam for a dg functor: it asks that the image of each chosen dg cone triangle be isomorphic to a cone triangle in the target. The record itself is only the weak generator condition; the theorem below constructs it for every dg functor from the strong split-cone witness. It does not duplicate Functor.IsTriangulated as a field.

• map_cone {X Y : C} (f : ↥(cocycles X Y)) {Z : C} (hc : IsConeOf (↑f) Z) : ∃ (Z' : D) (hc' : IsConeOf ((F.map 0) ↑f) Z'), Nonempty (F.h0.mapTriangle.obj (H0.coneTriangle f hc) ≅ H0.coneTriangle ⟨(F.map 0) ↑f, ⋯⟩ hc')

  The image of a dg cone triangle is a target cone triangle up to triangle isomorphism.

theorem CategoryTheory.DGFunctor.preservesConeTriangles_of_preservesChosenCones {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) [IsPretriangulated C] [IsPretriangulated D] (hShift : F.PreservesShifts) (hCone : F.PreservesChosenCones) : F.PreservesConeTriangles

Strong dg-level preservation of chosen shifts and cones implies the weak cone-generator preservation property needed for exactness on H⁰.

The target cone is the image object itself. The comparison triangle has identity components: compatibility of the first two arrows is forced by the stored image inclusions, while compatibility of the connecting arrow is derived from uniqueness of cone projections and the canonical shift comparison.

theorem CategoryTheory.DGFunctor.isTriangulated_of_preservesConeTriangles {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) [IsPretriangulated C] [IsPretriangulated D] [F.h0.CommShift ℤ] (hF : F.PreservesConeTriangles) : F.h0.IsTriangulated

A dg functor with cone-generator preservation induces a triangulated functor on H⁰. The proof is the generator argument built into the definition of H⁰.distinguishedTriangles, followed by closure under triangle isomorphism.

theorem CategoryTheory.DGFunctor.isTriangulated_of_preservesShifts_and_coneTriangles {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) [IsPretriangulated C] [IsPretriangulated D] (hShift : F.PreservesShifts) (hCone : F.PreservesConeTriangles) : F.h0.IsTriangulated

A shift-preserving dg functor needs only cone-generator preservation in addition to its canonical shift structure to induce a triangulated functor on H⁰. The explicit instance argument keeps callers from having to reproduce the commShift construction at every use site.

theorem CategoryTheory.DGFunctor.isTriangulated_of_preservesShifts_and_chosenCones {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) [IsPretriangulated C] [IsPretriangulated D] (hShift : F.PreservesShifts) (hCone : F.PreservesChosenCones) : F.h0.IsTriangulated

The strong composable dg capabilities are sufficient to make H⁰(F) a triangulated functor. The weak cone-generator proposition is derived internally and does not have to be supplied by callers.

theorem CategoryTheory.DGFunctor.h0IsTriangulated {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) [IsPretriangulated C] [IsPretriangulated D] : F.h0.IsTriangulated

Every dg functor between pretriangulated dg categories induces a triangulated functor on H⁰.

The shift and cone packages are selected explicitly rather than installed as global instances.