The seam commutes with the shift

dg-enhancements-e7. Cdg.seam : H⁰(C^dg A) ≌ K(A) is an equivalence of ordinary categories, and both sides carry a shift by ℤ: on the left the one H0Shift.lean builds out of IsPretriangulated.exists_shift, on the right Mathlib's, induced through the quotient. Nothing so far relates them. Functor.CommShift does, and #378 calls it "the real content of this epic".

The route: factor through cochain complexes

The two shifts are built by different routes out of the same shift on CochainComplex A ℤ, so the comparison is cleanest with that common source kept in the picture. The tautological functor

Cdg.toH0 : CochainComplex A ℤ ⥤ H⁰(C^dg A)

is the identity on objects, sends a chain map to the class of its own cochain, and is full; and it satisfies Cdg.toH0 ⋙ Cdg.h0Functor = HomotopyCategory.quotient on morphisms as well as objects (Cdg.h0Functor_map_toH0_map). So a CommShift structure on Cdg.toH0, together with Mathlib's on the quotient functor, assembles into one on the seam -- and that assembly is formal, which is the point of going this way round.

Where the mathematics actually is

All of it is in Cdg.toH0's two coherence identities, and both reduce to IsShiftBy.compare bookkeeping over the model lemmas of HomotopyCategory/ShiftComparison.lean. The chosen shift IsPretriangulated.shiftObj is Classical.choice, so it is never unfolded; what is used is that any two shifts of the same object by the same degree are canonically isomorphic and that those comparisons compose (IsShiftBy.compare_trans). The add coherence telescopes a four-term composite into a single compare in exactly that way.

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 no rewrite fires. 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.

def CategoryTheory.Cdg.toH0 (A : Type u) [Category.{v, u} A] [Preadditive A] : Functor (CochainComplex A ℤ) (H0 (Cdg A))

Cochain complexes into H⁰(C^dg A).

Equations

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

theorem CategoryTheory.Cdg.toH0_map {A : Type u} [Category.{v, u} A] [Preadditive A] {K L : CochainComplex A ℤ} (φ : K ⟶ L) : (toH0 A).map φ = H0.homMk ⟨CochainComplex.HomComplex.Cochain.ofHom φ, ⋯⟩

instance CategoryTheory.Cdg.toH0_additive {A : Type u} [Category.{v, u} A] [Preadditive A] : (toH0 A).Additive

The tautological functor from cochain complexes to H⁰(C^dg A) is additive.

instance CategoryTheory.Cdg.instFullCochainComplexIntH0ToH0 {A : Type u} [Category.{v, u} A] [Preadditive A] : (toH0 A).Full

theorem CategoryTheory.Cdg.h0Functor_map_toH0_map {A : Type u} [Category.{v, u} A] [Preadditive A] {K L : CochainComplex A ℤ} (φ : K ⟶ L) : h0Functor.map ((toH0 A).map φ) = (HomotopyCategory.quotient A (ComplexShape.up ℤ)).map φ

noncomputable def CategoryTheory.Cdg.toH0ShiftIso {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] (K : Cdg A) (n : ℤ) : (have this := K.shiftObj n; this) ≅ have this := IsPretriangulated.shiftObj (Cdg A) K n; this

The comparison between the model shift and the chosen shift, in H⁰.

Equations

• K.toH0ShiftIso n = CategoryTheory.H0.compareIso (K.isShiftBy n) (CategoryTheory.IsPretriangulated.shiftWitness (CategoryTheory.Cdg A) K n)

theorem CategoryTheory.Cdg.compare_isShiftBy_zero {A : Type u} [Category.{v, u} A] [Preadditive A] (K : Cdg A) : (K.isShiftBy 0).compare (IsShiftBy.self K) = CochainComplex.HomComplex.Cochain.ofHom ((shiftFunctorZero (CochainComplex A ℤ) ℤ).hom.app (of A K))

theorem CategoryTheory.Cdg.compare_isShiftBy_add {A : Type u} [Category.{v, u} A] [Preadditive A] (K : Cdg A) (a b : ℤ) : (K.isShiftBy (a + b)).compare ((K.isShiftBy a).comp' ((K.shiftObj a).isShiftBy b) (a + b) ⋯) = CochainComplex.HomComplex.Cochain.ofHom ((shiftFunctorAdd (CochainComplex A ℤ) a b).hom.app (of A K))

theorem CategoryTheory.Cdg.toH0ShiftIso_zero_hom {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] (K : Cdg A) : (K.toH0ShiftIso 0).hom = CategoryStruct.comp ((toH0 A).map ((shiftFunctorZero (CochainComplex A ℤ) ℤ).hom.app (of A K))) ((H0.shiftFunctorZeroIso (Cdg A)).inv.app K)

The zero coherence, componentwise.

theorem CategoryTheory.Cdg.toH0ShiftIso_add_hom {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] (K : Cdg A) (a b : ℤ) : (K.toH0ShiftIso (a + b)).hom = CategoryStruct.comp ((toH0 A).map ((shiftFunctorAdd (CochainComplex A ℤ) a b).hom.app (of A K))) (CategoryStruct.comp ((K.shiftObj a).toH0ShiftIso b).hom (CategoryStruct.comp ((H0.shiftFunctor (Cdg A) b).map (K.toH0ShiftIso a).hom) ((H0.shiftFunctorAddIso (Cdg A) a b).inv.app K)))

The add coherence, componentwise.

@[implicit_reducible]

noncomputable instance CategoryTheory.Cdg.toH0CommShift {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] : (toH0 A).CommShift ℤ

Equations

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

noncomputable def CategoryTheory.Cdg.seamShiftIso {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] (n : ℤ) (X : H0 (Cdg A)) : h0Functor.obj ((shiftFunctor (H0 (Cdg A)) n).obj X) ≅ (shiftFunctor (HomotopyCategory A (ComplexShape.up ℤ)) n).obj (h0Functor.obj X)

The seam's commutation isomorphism with the shift, at one object: undo the comparison of Cdg.toH0, then apply Mathlib's for the quotient functor.

Equations

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

theorem CategoryTheory.Cdg.seamShiftIso_hom {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] (n : ℤ) (X : H0 (Cdg A)) : (seamShiftIso n X).hom = CategoryStruct.comp (h0Functor.map ((Functor.commShiftIso (toH0 A) n).inv.app X)) ((Functor.commShiftIso (HomotopyCategory.quotient A (ComplexShape.up ℤ)) n).hom.app X)

noncomputable def CategoryTheory.Cdg.seamCommShiftIso {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] [Limits.HasZeroObject A] (n : ℤ) : (shiftFunctor (H0 (Cdg A)) n).comp h0Functor ≅ h0Functor.comp (shiftFunctor (HomotopyCategory A (ComplexShape.up ℤ)) n)

The seam commutes with the shift.

Equations

• CategoryTheory.Cdg.seamCommShiftIso n = CategoryTheory.NatIso.ofComponents (fun (X : CategoryTheory.H0 (CategoryTheory.Cdg A)) => CategoryTheory.Cdg.seamShiftIso n X) ⋯

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

@[implicit_reducible]

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

dg-enhancements-e7, the shift half.

Equations

• CategoryTheory.Cdg.h0FunctorCommShift = { commShiftIso := CategoryTheory.Cdg.seamCommShiftIso, commShiftIso_zero := ⋯, commShiftIso_add := ⋯ }