Cocycles, coboundaries, and Z⁰ of a dg category

The degree-zero cocycles of a dg category form an ordinary category on the same objects, and the coboundaries sit inside them as an additive subgroup. H⁰ is the quotient; this file builds everything the quotient needs.

Both halves rest on the Leibniz rule, at three different pairs of degrees:

• (0, 0) — composition of cocycles is a cocycle, so Z⁰ is a category;
• (0, -1) — a cocycle composed with a coboundary is a coboundary;
• (-1, 0) — a coboundary composed with a cocycle is a coboundary.

The last two are what make composition descend to H⁰. They are the reason the Leibniz rule is an axiom of DGCategory rather than a lemma about a special case, and the Const example in DerivedAlgGeo.Algebra.Homology.DGCategory/Instances.lean — whose differential is zero — tests none of them.

The induced functor on H⁰ also carries canonical identity and composition comparisons. Their associativity and two unit laws are recorded here as the ordinary pseudofunctor coherence equations. They are exposed directly because the repository has no bundled bicategory of dg categories on which to install Mathlib's Pseudofunctor; introducing a partial replacement would duplicate that abstraction.

A wrinkle in the degrees

dgComp_leibniz states the shifted degrees as p + 1, and those are dependent arguments: simp only [zero_add] cannot normalise 0 + 1 to 1 in a goal without breaking the motive. Hypotheses are therefore restated at the shifted degree — they typecheck directly, the degrees being definitionally equal — rather than rewriting the goal.

def CategoryTheory.cocycles {C : Type u} [DGCategory C] (X Y : C) : AddSubgroup ↑((DGCategoryStruct.dgHom X Y).X 0)

The degree-zero cocycles from X to Y.

Equations

• CategoryTheory.cocycles X Y = (AddCommGrpCat.Hom.hom ((CategoryTheory.DGCategoryStruct.dgHom X Y).d 0 1)).ker

def CategoryTheory.coboundaries {C : Type u} [DGCategory C] (X Y : C) : AddSubgroup ↑((DGCategoryStruct.dgHom X Y).X 0)

The degree-zero coboundaries from X to Y.

Equations

• CategoryTheory.coboundaries X Y = (AddCommGrpCat.Hom.hom ((CategoryTheory.DGCategoryStruct.dgHom X Y).d (-1) 0)).range

theorem CategoryTheory.mem_cocycles_iff {C : Type u} [DGCategory C] {X Y : C} (f : ↑((DGCategoryStruct.dgHom X Y).X 0)) : f ∈ cocycles X Y ↔ (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X Y).d 0 1)) f = 0

theorem CategoryTheory.mem_coboundaries_iff {C : Type u} [DGCategory C] {X Y : C} (f : ↑((DGCategoryStruct.dgHom X Y).X 0)) : f ∈ coboundaries X Y ↔ ∃ (h : ↑((DGCategoryStruct.dgHom X Y).X (-1))), (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X Y).d (-1) 0)) h = f

theorem CategoryTheory.coboundaries_le_cocycles {C : Type u} [DGCategory C] (X Y : C) : coboundaries X Y ≤ cocycles X Y

Every coboundary is a cocycle: this is d ∘ d = 0.

theorem CategoryTheory.comp_coboundary_mem {C : Type u} [DGCategory C] {X Y Z : C} {f : ↑((DGCategoryStruct.dgHom X Y).X 0)} (hf : f ∈ cocycles X Y) {b : ↑((DGCategoryStruct.dgHom Y Z).X 0)} (hb : b ∈ coboundaries Y Z) : ((DGCategoryStruct.dgComp 0 0 0 ⋯) f) b ∈ coboundaries X Z

A cocycle composed with a coboundary is a coboundary. Leibniz at (0, -1): the δf term vanishes because f is closed, and the sign is +1.

theorem CategoryTheory.coboundary_comp_mem {C : Type u} [DGCategory C] {X Y Z : C} {b : ↑((DGCategoryStruct.dgHom X Y).X 0)} (hb : b ∈ coboundaries X Y) {g : ↑((DGCategoryStruct.dgHom Y Z).X 0)} (hg : g ∈ cocycles Y Z) : ((DGCategoryStruct.dgComp 0 0 0 ⋯) b) g ∈ coboundaries X Z

A coboundary composed with a cocycle is a coboundary. Leibniz at (-1, 0): the δg term vanishes because g is closed, so the sign never matters.

def CategoryTheory.Z0 (C : Type u) : Type u

Objects of Z⁰. A type synonym, so the ordinary category structure does not attach itself to C.

Equations

• CategoryTheory.Z0 C = C

def CategoryTheory.Z0.of (C : Type u) (X : Z0 C) : C

The underlying object of C.

Equations

• CategoryTheory.Z0.of C X = X

theorem CategoryTheory.Z0.comp_mem {C : Type u} [DGCategory C] {X Y Z : C} {f : ↑((DGCategoryStruct.dgHom X Y).X 0)} (hf : f ∈ cocycles X Y) {g : ↑((DGCategoryStruct.dgHom Y Z).X 0)} (hg : g ∈ cocycles Y Z) : ((DGCategoryStruct.dgComp 0 0 0 ⋯) f) g ∈ cocycles X Z

Composition of cocycles is a cocycle: Leibniz at (0, 0), with both differential terms vanishing.

@[implicit_reducible]

instance CategoryTheory.Z0.category {C : Type u} [DGCategory C] : Category.{v, u} (Z0 C)

Equations

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

The two computation rules below are stated through Subtype.val on the ascribed subgroup type: X ⟶ Y in Z0 C is cocycles _ _, but only definitionally, so the anonymous coercion does not fire on the ⟶ form.

@[simp]

theorem CategoryTheory.Z0.id_val {C : Type u} [DGCategory C] (X : Z0 C) : ↑(CategoryStruct.id X) = DGCategoryStruct.dgId (of C X)

@[simp]

theorem CategoryTheory.Z0.comp_val {C : Type u} [DGCategory C] {X Y Z : Z0 C} (f : X ⟶ Y) (g : Y ⟶ Z) : ↑(CategoryStruct.comp f g) = ((DGCategoryStruct.dgComp 0 0 0 ⋯) ↑f) ↑g

theorem CategoryTheory.comp_sub_mem {C : Type u} [DGCategory C] {X Y Z : C} {f₁ f₂ : ↑((DGCategoryStruct.dgHom X Y).X 0)} {g₁ g₂ : ↑((DGCategoryStruct.dgHom Y Z).X 0)} (hf₂ : f₂ ∈ cocycles X Y) (hg₁ : g₁ ∈ cocycles Y Z) (hf : f₁ - f₂ ∈ coboundaries X Y) (hg : g₁ - g₂ ∈ coboundaries Y Z) : ((DGCategoryStruct.dgComp 0 0 0 ⋯) f₁) g₁ - ((DGCategoryStruct.dgComp 0 0 0 ⋯) f₂) g₂ ∈ coboundaries X Z

Composition respects cohomology classes. Writing f₁ ∘ g₁ - f₂ ∘ g₂ = (f₁ - f₂) ∘ g₁ + f₂ ∘ (g₁ - g₂) reduces this to the two descent lemmas, one for each summand.

Only f₂ and g₁ are required to be closed — the split above touches the other two only through the differences, which are already assumed to be coboundaries.

def CategoryTheory.H0 (C : Type u) : Type u

Objects of H⁰.

Equations

• CategoryTheory.H0 C = C

def CategoryTheory.H0.of (C : Type u) (X : H0 C) : C

The underlying object of C.

Equations

• CategoryTheory.H0.of C X = X

theorem CategoryTheory.H0.of_self {C : Type u} (X : H0 C) : of C X = X

of is the identity. Not a simp lemma: making it one changes how the quotient's membership goals normalise and breaks the descent proofs above. Pass it explicitly where objects need to be unfolded.

def CategoryTheory.H0.coboundariesIn {C : Type u} [DGCategory C] (X Y : C) : AddSubgroup ↥(cocycles X Y)

The coboundaries, viewed inside the cocycles.

Equations

• CategoryTheory.H0.coboundariesIn X Y = (CategoryTheory.coboundaries X Y).addSubgroupOf (CategoryTheory.cocycles X Y)

@[implicit_reducible]

instance CategoryTheory.H0.category {C : Type u} [DGCategory C] : Category.{v, u} (H0 C)

Equations

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

@[implicit_reducible]

instance CategoryTheory.H0.preadditive {C : Type u} [DGCategory C] : Preadditive (H0 C)

H⁰ is preadditive: its Hom-sets are quotients of abelian groups, and composition is biadditive because dgComp is.

Equations

• CategoryTheory.H0.preadditive = { homGroup := fun (X Y : CategoryTheory.H0 C) => id inferInstance, add_comp := ⋯, comp_add := ⋯ }

def CategoryTheory.H0.homMk {C : Type u} [DGCategory C] {X Y : C} (f : ↥(cocycles X Y)) : (have this := X; this) ⟶ have this := Y; this

The morphism of H⁰ a cocycle represents. Every construction that descends a dg morphism to H⁰ goes through this constructor, and the three computation rules below are what downstream files rewrite with.

Equations

• CategoryTheory.H0.homMk f = ↑f

theorem CategoryTheory.H0.homMk_eq_homMk {C : Type u} [DGCategory C] {X Y : C} {a b : ↥(cocycles X Y)} (h : ↑a - ↑b ∈ coboundaries X Y) : homMk a = homMk b

Two cocycles represent the same morphism of H⁰ when they differ by a coboundary. The quotient's own eq_iff_sub_mem says so; this restates it on the underlying elements, which is the form every homotopy produces.

theorem CategoryTheory.H0.homMk_neg {C : Type u} [DGCategory C] {X Y : C} (a : ↥(cocycles X Y)) : homMk (-a) = -homMk a

Negation of an H⁰ morphism is negation of a representative.

theorem CategoryTheory.H0.homMk_comp {C : Type u} [DGCategory C] {X Y Z : C} (a : ↥(cocycles X Y)) (b : ↥(cocycles Y Z)) : CategoryStruct.comp (homMk a) (homMk b) = homMk ⟨((DGCategoryStruct.dgComp 0 0 0 ⋯) ↑a) ↑b, ⋯⟩

Composition of H⁰ morphisms is dgComp of representatives.

theorem CategoryTheory.H0.homMk_id {C : Type u} [DGCategory C] (X : C) : homMk ⟨DGCategoryStruct.dgId X, ⋯⟩ = CategoryStruct.id (have this := X; this)

The identity of H⁰ is represented by the dg identity.

theorem CategoryTheory.DGFunctor.map_mem_cocycles {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) {X Y : C} {f : ↑((DGCategoryStruct.dgHom X Y).X 0)} (hf : f ∈ cocycles X Y) : (F.map 0) f ∈ cocycles (F.obj X) (F.obj Y)

A dg functor sends cocycles to cocycles: it commutes with the differential, and an additive map sends 0 to 0.

theorem CategoryTheory.DGFunctor.map_mem_coboundaries {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) {X Y : C} {f : ↑((DGCategoryStruct.dgHom X Y).X 0)} (hf : f ∈ coboundaries X Y) : (F.map 0) f ∈ coboundaries (F.obj X) (F.obj Y)

A dg functor sends coboundaries to coboundaries, for the same reason and with no closedness hypothesis: map_d already exhibits the primitive.

def CategoryTheory.DGFunctor.h0 {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) : Functor (H0 C) (H0 D)

The functor H⁰(F) induced by a dg functor.

Equations

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

instance CategoryTheory.DGFunctor.h0_additive {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) : F.h0.Additive

The functor on H⁰ induced by a dg functor is additive.

def CategoryTheory.DGFunctor.mapComplex {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) (X Y : C) : DGCategoryStruct.dgHom X Y ⟶ DGCategoryStruct.dgHom (F.obj X) (F.obj Y)

A dg functor's action on a single Hom-complex, packaged as a morphism of cochain complexes. map_d is exactly the commutation square.

Equations

• F.mapComplex X Y = { f := fun (p : ℤ) => AddCommGrpCat.ofHom (F.map p), comm' := ⋯ }

structure CategoryTheory.DGFunctor.IsQuasiEquivalence {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) : Prop

A quasi-equivalence of dg categories: the action on every Hom-complex is a quasi-isomorphism, and H⁰ of it is essentially surjective.

That a quasi-equivalence induces an equivalence H⁰ C ≌ H⁰ D is DGFunctor.isEquivalence_h0 and DGFunctor.h0Equivalence (DGCategory/QuasiEquivalence.lean), and that this equivalence is triangulated between pretriangulated dg categories is DGFunctor.isTriangulated_h0Equivalence (DGCategory/Pretriangulated/H0/FunctorTransport.lean).

• quasiIso (X Y : C) : QuasiIso (F.mapComplex X Y)

  Every Hom-complex map is a quasi-isomorphism.

• essSurj : F.h0.EssSurj

  H⁰ F hits every object up to isomorphism.

def CategoryTheory.Z0.toH0 (C : Type u) [DGCategory C] : Functor (Z0 C) (H0 C)

The quotient functor from cocycles to cohomology classes.

Equations

• CategoryTheory.Z0.toH0 C = { obj := fun (X : CategoryTheory.Z0 C) => X, map := fun {X Y : CategoryTheory.Z0 C} (f : X ⟶ Y) => ↑f, map_id := ⋯, map_comp := ⋯ }

instance CategoryTheory.Z0.toH0_full (C : Type u) [DGCategory C] : (toH0 C).Full

Every morphism in H⁰ C has a degree-zero cocycle representative.

@[simp]

theorem CategoryTheory.DGFunctor.h0_obj {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) (X : H0 C) : F.h0.obj X = F.obj (H0.of C X)

The object part of H⁰ F. A simp lemma because otherwise the objects in a naturality square stay in the h0.obj form and Category.comp_id — whose statement mentions the codomain — cannot match.

@[simp]

theorem CategoryTheory.DGFunctor.h0_map_mk {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) {X Y : H0 C} (f : ↥(cocycles (H0.of C X) (H0.of C Y))) : F.h0.map ↑f = ↑⟨(F.map 0) ↑f, ⋯⟩

How H⁰ F acts on a class: this is the computation rule simp needs before any naturality square involving h0 will close.

def CategoryTheory.DGFunctor.h0IdIso {C : Type u} [DGCategory C] : (id C).h0 ≅ Functor.id (H0 C)

H⁰ of the identity dg functor is the identity.

Equations

• CategoryTheory.DGFunctor.h0IdIso = CategoryTheory.NatIso.ofComponents (fun (x : CategoryTheory.H0 C) => CategoryTheory.Iso.refl ((CategoryTheory.DGFunctor.id C).h0.obj x)) ⋯

The identity comparison has literal identity components in both directions.

@[simp]

theorem CategoryTheory.DGFunctor.h0IdIso_hom_app {C : Type u} [DGCategory C] (X : H0 C) : h0IdIso.hom.app X = CategoryStruct.id ((id C).h0.obj X)

The forward component of h0IdIso is the identity. This exposes the computation without requiring consumers to unfold NatIso.ofComponents.

@[simp]

theorem CategoryTheory.DGFunctor.h0IdIso_inv_app {C : Type u} [DGCategory C] (X : H0 C) : h0IdIso.inv.app X = CategoryStruct.id ((Functor.id (H0 C)).obj X)

The inverse component of h0IdIso is the identity. This exposes the computation without requiring consumers to unfold NatIso.ofComponents.

def CategoryTheory.DGFunctor.h0CompIso {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] (F : DGFunctor C D) (G : DGFunctor D E) : (F.comp G).h0 ≅ F.h0.comp G.h0

H⁰ takes composition of dg functors to composition of functors.

Equations

• F.h0CompIso G = CategoryTheory.NatIso.ofComponents (fun (x : CategoryTheory.H0 C) => CategoryTheory.Iso.refl ((F.comp G).h0.obj x)) ⋯

@[simp]

theorem CategoryTheory.DGFunctor.h0CompIso_hom_app {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] (F : DGFunctor C D) (G : DGFunctor D E) (X : H0 C) : (F.h0CompIso G).hom.app X = CategoryStruct.id ((F.comp G).h0.obj X)

The forward component of h0CompIso is the identity. This is the component computation used when descending dg whiskering to H⁰.

@[simp]

theorem CategoryTheory.DGFunctor.h0CompIso_inv_app {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] (F : DGFunctor C D) (G : DGFunctor D E) (X : H0 C) : (F.h0CompIso G).inv.app X = CategoryStruct.id ((F.h0.comp G.h0).obj X)

The inverse component of h0CompIso is the identity. This is the component computation used when descending dg whiskering to H⁰.

theorem CategoryTheory.DGFunctor.h0CompIso_assoc {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] {B : Type u'''} [DGCategory B] (F : DGFunctor C D) (G : DGFunctor D E) (H : DGFunctor E B) : (F.comp G).h0CompIso H ≪≫ Functor.isoWhiskerRight (F.h0CompIso G) H.h0 ≪≫ F.h0.associator G.h0 H.h0 = F.h0CompIso (G.comp H) ≪≫ F.h0.isoWhiskerLeft (G.h0CompIso H)

The H⁰ composition comparison satisfies the pseudofunctor associativity law. The ordinary functor associator is retained explicitly even though dg-functor composition is strict.

theorem CategoryTheory.DGFunctor.h0CompIso_comp_id {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) : F.h0CompIso (id D) ≪≫ F.h0.isoWhiskerLeft h0IdIso ≪≫ F.h0.rightUnitor = Iso.refl F.h0

The H⁰ composition comparison is coherent with right composition by the identity dg functor and the ordinary right unitor.

theorem CategoryTheory.DGFunctor.h0CompIso_id_comp {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) : (id C).h0CompIso F ≪≫ Functor.isoWhiskerRight h0IdIso F.h0 ≪≫ F.h0.leftUnitor = Iso.refl F.h0

The H⁰ composition comparison is coherent with left composition by the identity dg functor and the ordinary left unitor.