C^dg A is pretriangulated

The witness for dg-enhancements-e5. Nothing here is a new construction: the shift is CochainComplex.shiftFunctor, the cone is CochainComplex.mappingCone, and every clause is discharged by the Mathlib lemma written for it.

clause	supplied by
IsShiftBy.hom	Cocycle.rightShift of Cocycle.ofHom (𝟙 K)
IsShiftBy.hom_closed	Cocycle.δ_eq_zero
IsShiftBy.bijective	Cochain.rightUnshift_comp
IsConeOf.inl, .inr	mappingCone.inl, mappingCone.inr
IsConeOf.δ_inl	mappingCone.δ_inl
IsConeOf.bijective	mappingCone.id and inl_fst/inl_snd/inr_fst/inr_snd

The shift bijection is not proved by exhibiting an inverse

Cochain.rightUnshift_comp says that unshifting a composite with the canonical cochain returns the cochain you started with. So right composition is a section of Cochain.rightUnshift, and rightUnshift is itself injective by Cochain.rightShift_rightUnshift. A section of an injection is a bijection, so both round trips reduce to those two Mathlib lemmas and no sign bookkeeping.

Why the type ascriptions are written out

Cdg A is a type synonym for CochainComplex A ℤ and Cdg.of is the identity, so dgHom K L and HomComplex (of A K) (of A L) are the same term definitionally — but only after unfolding the synonym and the instance projection. Elaboration does not unfold either while it is choosing an instance, so (of A K)⟦n⟧ written at the ascribed type Cdg A looks for HasShift (Cdg A) ℤ and fails. Every shift is therefore ascribed at CochainComplex A ℤ and converted afterwards.

def CategoryTheory.Cdg.shiftObj {A : Type u} [Category.{v, u} A] [Preadditive A] (K : Cdg A) (n : ℤ) : Cdg A

The shift of an object of C^dg A, as an object of C^dg A.

Equations

• K.shiftObj n = (CategoryTheory.shiftFunctor (CochainComplex A ℤ) n).obj (CategoryTheory.Cdg.of A K)

theorem CategoryTheory.Cdg.of_shiftObj {A : Type u} [Category.{v, u} A] [Preadditive A] (K : Cdg A) (n : ℤ) : of A (K.shiftObj n) = (shiftFunctor (CochainComplex A ℤ) n).obj (of A K)

noncomputable def CategoryTheory.Cdg.shiftCocycle {A : Type u} [Category.{v, u} A] [Preadditive A] (K : Cdg A) (n : ℤ) : CochainComplex.HomComplex.Cocycle (of A K) ((shiftFunctor (CochainComplex A ℤ) n).obj (of A K)) (-n)

The identity of K, right-shifted: the canonical closed cochain of degree -n from K to K⟦n⟧. Degree -n rather than n because Homᵈ(K, L) = ∏ₚ Hom(Kᵖ, L^{p+d}) and (K⟦n⟧)^q = K^{q+n}.

Equations

• K.shiftCocycle n = (CochainComplex.HomComplex.Cocycle.ofHom (CategoryTheory.CategoryStruct.id (CategoryTheory.Cdg.of A K))).rightShift n (-n) ⋯

theorem CategoryTheory.Cdg.rightUnshift_shiftCocycle {A : Type u} [Category.{v, u} A] [Preadditive A] (K : Cdg A) (n : ℤ) : (↑(K.shiftCocycle n)).rightUnshift 0 ⋯ = CochainComplex.HomComplex.Cochain.ofHom (CategoryStruct.id (of A K))

Unshifting the canonical cochain returns the identity.

noncomputable def CategoryTheory.Cdg.isShiftBy {A : Type u} [Category.{v, u} A] [Preadditive A] (K : Cdg A) (n : ℤ) : IsShiftBy K n (K.shiftObj n)

K⟦n⟧ is a shift of K by n in C^dg A.

Equations

• K.isShiftBy n = { hom := ↑(K.shiftCocycle n), hom_closed := ⋯, bijective := ⋯ }

def CategoryTheory.Cdg.coneCocycle {A : Type u} [Category.{v, u} A] [Preadditive A] {K L : Cdg A} (f : ↑((DGCategoryStruct.dgHom K L).X 0)) (hf : f ∈ cocycles K L) : CochainComplex.HomComplex.Cocycle (of A K) (of A L) 0

A closed degree-zero cochain of C^dg A, as one of Mathlib's cocycles. cocycles K L and HomComplex.cocycle (of A K) (of A L) 0 are the same subgroup of the same group, but of two different subgroup terms, so the crossing is written by hand exactly as in Model/Seam.lean.

Equations

• CategoryTheory.Cdg.coneCocycle f hf = ⟨f, hf⟩

noncomputable def CategoryTheory.Cdg.coneHom {A : Type u} [Category.{v, u} A] [Preadditive A] {K L : Cdg A} (f : ↑((DGCategoryStruct.dgHom K L).X 0)) (hf : f ∈ cocycles K L) : of A K ⟶ of A L

The morphism of complexes a closed degree-zero cochain presents.

Equations

• CategoryTheory.Cdg.coneHom f hf = (CategoryTheory.Cdg.coneCocycle f hf).homOf

@[simp]

theorem CategoryTheory.Cdg.cochain_ofHom_coneHom {A : Type u} [Category.{v, u} A] [Preadditive A] {K L : Cdg A} (f : ↑((DGCategoryStruct.dgHom K L).X 0)) (hf : f ∈ cocycles K L) : CochainComplex.HomComplex.Cochain.ofHom (coneHom f hf) = f

noncomputable def CategoryTheory.Cdg.coneObj {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) : Cdg A

The mapping cone of a closed degree-zero cochain, as an object of C^dg A.

Equations

• CategoryTheory.Cdg.coneObj f hf = CochainComplex.mappingCone (CategoryTheory.Cdg.coneHom f hf)

theorem CategoryTheory.Cdg.comp_fst_of_split {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] {K L W : Cdg A} (f : ↑((DGCategoryStruct.dgHom K L).X 0)) (hf : f ∈ cocycles K L) (p q : ℤ) (hq : p + 1 = q) (h1 : q + -1 = p) (a : CochainComplex.HomComplex.Cochain (of A W) (of A K) q) (b : CochainComplex.HomComplex.Cochain (of A W) (of A L) p) : (a.comp (CochainComplex.mappingCone.inl (coneHom f hf)) h1 + b.comp (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr (coneHom f hf))) ⋯).comp (↑(CochainComplex.mappingCone.fst (coneHom f hf))) hq = a

Recovering the first component of a split map into the cone: compose with fst. The inr term dies by inr_fst.

theorem CategoryTheory.Cdg.comp_snd_of_split {A : Type u} [Category.{v, u} A] [Preadditive A] [Limits.HasBinaryBiproducts A] {K L W : Cdg A} (f : ↑((DGCategoryStruct.dgHom K L).X 0)) (hf : f ∈ cocycles K L) (p q : ℤ) (h1 : q + -1 = p) (a : CochainComplex.HomComplex.Cochain (of A W) (of A K) q) (b : CochainComplex.HomComplex.Cochain (of A W) (of A L) p) : (a.comp (CochainComplex.mappingCone.inl (coneHom f hf)) h1 + b.comp (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr (coneHom f hf))) ⋯).comp (CochainComplex.mappingCone.snd (coneHom f hf)) ⋯ = b

And the second component: compose with snd, where the inl term dies by inl_snd.

noncomputable def CategoryTheory.Cdg.isConeOf {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 (coneObj f hf)

Mathlib's mapping cone is a cone in the dg sense. Every field is one of its lemmas: the splitting is mappingCone.id read forwards and inl_fst/inl_snd/inr_fst/inr_snd read backwards.

Equations

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

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

C^dg A is pretriangulated whenever A has a zero object and binary biproducts: the shift is isShiftBy, the cone is isConeOf, and the zero object is A's.