Preservation of pretriangulated dg structure

Every dg functor preserves the representability witnesses that define shifts and cones. DGFunctor.preservesShifts and DGFunctor.preservesChosenCones supply the two dg-level capabilities automatically. For cones, the inverse to the image splitting map is built from the images of the two projections extracted from the source cone. Transport to the ordinary shift functors and cone triangles on H⁰ belongs to the dg-enhancement layer.

structure CategoryTheory.DGFunctor.PreservesShifts {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) : Type (max u v)

A dg functor preserves shifts when it sends every dg shift witness to a shift witness on the image objects, with the defining homogeneous element given by the dg functor's map.

No pretriangulated instance is required to state the capability: callers may provide individual witnesses, while H⁰ adapters add existence assumptions only when they choose shifts for every object.

• mapShift {X Y : C} {n : ℤ} (s : IsShiftBy X n Y) : IsShiftBy (F.obj X) n (F.obj Y)

  The target shift witness associated to a source shift witness.

• mapShift_hom {X Y : C} {n : ℤ} (s : IsShiftBy X n Y) : (self.mapShift s).hom = (F.map (-n)) s.hom

  The associated shift element is the image of the source element.

def CategoryTheory.DGFunctor.PreservesShifts.id (C : Type u) [DGCategory C] : (DGFunctor.id C).PreservesShifts

The identity dg functor preserves shift witnesses.

Equations

• CategoryTheory.DGFunctor.PreservesShifts.id C = { mapShift := fun {X Y : C} {n : ℤ} (s : CategoryTheory.IsShiftBy X n Y) => s, mapShift_hom := ⋯ }

def CategoryTheory.DGFunctor.PreservesShifts.comp {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F : DGFunctor C D} {G : DGFunctor D E} (hF : F.PreservesShifts) (hG : G.PreservesShifts) : (F.comp G).PreservesShifts

Shift preservation is closed under composition of dg functors.

Equations

• hF.comp hG = { mapShift := fun {X Y : C} {n : ℤ} (s : CategoryTheory.IsShiftBy X n Y) => hG.mapShift (hF.mapShift s), mapShift_hom := ⋯ }

noncomputable def CategoryTheory.DGFunctor.preservesShifts {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) : F.PreservesShifts

Every dg functor preserves shifts.

A shift element is a closed, two-sided invertible element of degree -n: IsShiftBy.inv extracts the inverse from surjectivity of right composition, and hom_inv and inv_hom are the two identities. A dg functor preserves the graded composition and the identities on the nose, so it carries an invertible element to an invertible element, and right composition with the image is bijective with right composition with the image of the inverse.

So PreservesShifts is not a hypothesis anybody has to discharge; it is supplied here for every dg functor. The structure stays because it names the capability and because mapShift is the useful accessor, but a caller that used to take a PreservesShifts argument can now call this instead.

Equations

• F.preservesShifts = { mapShift := fun {X Y : C} {n : ℤ} (s : CategoryTheory.IsShiftBy X n Y) => { hom := (F.map (-n)) s.hom, hom_closed := ⋯, bijective := ⋯ }, mapShift_hom := ⋯ }

def CategoryTheory.DGFunctor.mapHomotopySquare {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) {X₁ Y₁ X₂ Y₂ : C} {f₁ : ↑((DGCategoryStruct.dgHom X₁ Y₁).X 0)} {f₂ : ↑((DGCategoryStruct.dgHom X₂ Y₂).X 0)} {a : ↑((DGCategoryStruct.dgHom X₁ X₂).X 0)} {b : ↑((DGCategoryStruct.dgHom Y₁ Y₂).X 0)} (s : DGCategory.HomotopySquare f₁ f₂ a b) : DGCategory.HomotopySquare ((F.map 0) f₁) ((F.map 0) f₂) ((F.map 0) a) ((F.map 0) b)

Apply a dg functor to a chosen homotopy-commutative square. The homotopy itself is mapped, so this construction retains the witness needed by later cone maps rather than merely proving that the image square commutes in H⁰.

Equations

• F.mapHomotopySquare s = CategoryTheory.DGCategory.HomotopySquare.ofBoundary ⋯ ⋯ ((F.map (-1)) s.homotopy) ⋯

@[simp]

theorem CategoryTheory.DGFunctor.mapHomotopySquare_homotopy {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) {X₁ Y₁ X₂ Y₂ : C} {f₁ : ↑((DGCategoryStruct.dgHom X₁ Y₁).X 0)} {f₂ : ↑((DGCategoryStruct.dgHom X₂ Y₂).X 0)} {a : ↑((DGCategoryStruct.dgHom X₁ X₂).X 0)} {b : ↑((DGCategoryStruct.dgHom Y₁ Y₂).X 0)} (s : DGCategory.HomotopySquare f₁ f₂ a b) : (F.mapHomotopySquare s).homotopy = (F.map (-1)) s.homotopy

structure CategoryTheory.DGFunctor.PreservesChosenCones {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) : Type (max u v)

Strong dg-level preservation of cone witnesses.

For every supplied cone witness, the image object is equipped with a cone witness whose two inclusions are exactly the images of the source inclusions. This chosen, composable capability is intentionally stronger than the later H⁰ proposition that an image triangle is merely isomorphic to some cone triangle.

• mapCone {X Y Z : C} {f : ↑((DGCategoryStruct.dgHom X Y).X 0)} (hc : IsConeOf f Z) : IsConeOf ((F.map 0) f) (F.obj Z)

  The target cone witness carried by the image object.

• mapCone_inr {X Y Z : C} {f : ↑((DGCategoryStruct.dgHom X Y).X 0)} (hc : IsConeOf f Z) : (self.mapCone hc).inr = (F.map 0) hc.inr

  The target cone inclusion is the image of the source cone inclusion.

• mapCone_inl {X Y Z : C} {f : ↑((DGCategoryStruct.dgHom X Y).X 0)} (hc : IsConeOf f Z) : (self.mapCone hc).inl = (F.map (-1)) hc.inl

  The shifted source inclusion is the image of the source cone inclusion.

def CategoryTheory.DGFunctor.PreservesChosenCones.id (C : Type u) [DGCategory C] : (DGFunctor.id C).PreservesChosenCones

The identity dg functor preserves chosen cone witnesses.

Equations

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

def CategoryTheory.DGFunctor.PreservesChosenCones.comp {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {F : DGFunctor C D} {G : DGFunctor D E} (hF : F.PreservesChosenCones) (hG : G.PreservesChosenCones) : (F.comp G).PreservesChosenCones

Strong cone preservation is closed under composition of dg functors.

Equations

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

def CategoryTheory.DGFunctor.PreservesChosenCones.ofIso {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} (hF : F.PreservesChosenCones) (e : (have this := F; this) ≅ have this := G; this) : G.PreservesChosenCones

Strong preservation of the chosen cone witnesses is invariant under an isomorphism of dg functors in the closed degree-zero category.

Equations

• hF.ofIso e = CategoryTheory.DGFunctor.PreservesChosenCones.ofIsoAux✝ hF e

theorem CategoryTheory.DGFunctor.PreservesChosenCones.mapCone_fst {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F : DGFunctor C D} (hF : F.PreservesChosenCones) {X Y Z : C} {f : ↑((DGCategoryStruct.dgHom X Y).X 0)} (hc : IsConeOf f Z) : (hF.mapCone hc).fst = (F.map 1) hc.fst

The projection from an image cone to its source is the image of the source cone projection. This is forced by uniqueness of the cone splitting; it is not an additional field of PreservesChosenCones.

theorem CategoryTheory.DGFunctor.PreservesChosenCones.mapCone_snd {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F : DGFunctor C D} (hF : F.PreservesChosenCones) {X Y Z : C} {f : ↑((DGCategoryStruct.dgHom X Y).X 0)} (hc : IsConeOf f Z) : (hF.mapCone hc).snd = (F.map 0) hc.snd

The projection from an image cone to its target is the image of the source cone projection, again derived from uniqueness of the cone splitting.

theorem CategoryTheory.DGFunctor.PreservesChosenCones.mapCone_toShift {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F : DGFunctor C D} (hCone : F.PreservesChosenCones) (hShift : F.PreservesShifts) {X Y Z X' : C} {f : ↑((DGCategoryStruct.dgHom X Y).X 0)} (hc : IsConeOf f Z) (s : IsShiftBy X 1 X') : (F.map 0) (hc.toShift s) = (hCone.mapCone hc).toShift (hShift.mapShift s)

A cone-preserving, shift-preserving dg functor carries the connecting map of a supplied cone to the connecting map built from the corresponding image witnesses.

noncomputable def CategoryTheory.DGFunctor.preservesChosenCones {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) : F.PreservesChosenCones

Every dg functor preserves the chosen cone witnesses.

The cone universal property is a split representability statement. A source cone supplies projections fst and snd satisfying the usual five matrix identities with inl and inr. After applying a dg functor, those identities still hold. For an arbitrary target object W, they exhibit

c ↦ (c ≫ F(fst), c ≫ F(snd))

as the inverse to the image cone's splitting map. Thus neither fullness nor a pretriangulated existence assumption is needed. The structure remains useful as a named package consumed by the H⁰ exactness adapters.

Equations

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

theorem CategoryTheory.DGFunctor.mapShift_inv_eq {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F : DGFunctor C D} (hF : F.PreservesShifts) {X Y : C} {n : ℤ} (s : IsShiftBy X n Y) : (hF.mapShift s).inv = (F.map n) s.inv

The inverse of the image shift witness is forced by the image of the source inverse. This removes the Classical.choice hidden in IsShiftBy.inv from every later transport calculation.

theorem CategoryTheory.DGFunctor.map_mapShift {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F : DGFunctor C D} (hF : F.PreservesShifts) {X X' Y Y' : C} {n : ℤ} (s : IsShiftBy X n Y) (s' : IsShiftBy X' n Y') (f : ↑((DGCategoryStruct.dgHom X X').X 0)) : (F.map 0) (s.mapShift s' f) = (hF.mapShift s).mapShift (hF.mapShift s') ((F.map 0) f)

F commutes with the dg action on morphisms induced by a shift witness.

theorem CategoryTheory.DGFunctor.map_compare {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F : DGFunctor C D} (hF : F.PreservesShifts) {X Y Y' : C} {n : ℤ} (s : IsShiftBy X n Y) (t : IsShiftBy X n Y') : (F.map 0) (s.compare t) = (hF.mapShift s).compare (hF.mapShift t)

F commutes with comparisons between two shifts of the same object.