The seam: H⁰(C^dg A) and the homotopy category

dg-enhancements-e4's theorem. The route is to identify this repository's cocycles and coboundaries with Mathlib's, so that the Hom-groups of H⁰(C^dg A) are CochainComplex.HomComplex.CohomologyClass _ _ 0, and then to use CohomologyClass.homAddEquiv, which Mathlib already proves.

theorem CategoryTheory.Cdg.cocycles_eq {A : Type u} [Category.{v, u} A] [Preadditive A] (K L : Cdg A) : cocycles K L = CochainComplex.HomComplex.cocycle (of A K) (of A L) 0

This repository's degree-zero cocycles are Mathlib's.

theorem CategoryTheory.Cdg.mem_coboundaries_iff' {A : Type u} [Category.{v, u} A] [Preadditive A] (K L : Cdg A) (f : ↑((DGCategoryStruct.dgHom K L).X 0)) : f ∈ coboundaries K L ↔ ∃ (β : CochainComplex.HomComplex.Cochain (of A K) (of A L) (-1)), CochainComplex.HomComplex.δ (-1) 0 β = f

This repository's degree-zero coboundaries are Mathlib's, transported along cocycles_eq. Mathlib's version is a subgroup of the cocycles and asks for a primitive in degree m with m + 1 = 0; this one is the range of δ (-1) 0. The two conditions are the same condition.

Crossing the instance boundary

Cocycle K L 0 and ↥(cocycles K L) are the same subtype of the same group, but Cocycle is a def carrying instAddCommGroupCocycle while the subgroup carries the one AddSubgroup supplies. AddSubgroup is indexed by that instance, so the two subgroup terms do not share a type for rw, and an ext proof fails on an application type mismatch rather than on content.

Building the maps explicitly avoids the question: a hand-written AddMonoidHom typechecks by defeq, where instance matching would not.

def CategoryTheory.Cdg.toCocycle {A : Type u} [Category.{v, u} A] [Preadditive A] (K L : Cdg A) : ↥(cocycles K L) →+ CochainComplex.HomComplex.Cocycle (of A K) (of A L) 0

This repository's degree-zero cocycles, as Mathlib's.

Equations

• K.toCocycle L = { toFun := fun (z : ↥(CategoryTheory.cocycles K L)) => ⟨↑z, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

def CategoryTheory.Cdg.ofCocycle {A : Type u} [Category.{v, u} A] [Preadditive A] (K L : Cdg A) : CochainComplex.HomComplex.Cocycle (of A K) (of A L) 0 →+ ↥(cocycles K L)

And back.

Equations

• K.ofCocycle L = { toFun := fun (z : CochainComplex.HomComplex.Cocycle (CategoryTheory.Cdg.of A K) (CategoryTheory.Cdg.of A L) 0) => ⟨↑z, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

theorem CategoryTheory.Cdg.toCocycle_val {A : Type u} [Category.{v, u} A] [Preadditive A] (K L : Cdg A) (z : ↥(cocycles K L)) : ↑((K.toCocycle L) z) = ↑z

theorem CategoryTheory.Cdg.ofCocycle_val {A : Type u} [Category.{v, u} A] [Preadditive A] (K L : Cdg A) (z : CochainComplex.HomComplex.Cocycle (of A K) (of A L) 0) : ↑((K.ofCocycle L) z) = ↑z

theorem CategoryTheory.Cdg.ofCocycle_toCocycle {A : Type u} [Category.{v, u} A] [Preadditive A] (K L : Cdg A) (z : ↥(cocycles K L)) : (K.ofCocycle L) ((K.toCocycle L) z) = z

theorem CategoryTheory.Cdg.toCocycle_ofCocycle {A : Type u} [Category.{v, u} A] [Preadditive A] (K L : Cdg A) (z : CochainComplex.HomComplex.Cocycle (of A K) (of A L) 0) : (K.toCocycle L) ((K.ofCocycle L) z) = z

def CategoryTheory.Cdg.cocycleAddEquiv {A : Type u} [Category.{v, u} A] [Preadditive A] (K L : Cdg A) : ↥(cocycles K L) ≃+ CochainComplex.HomComplex.Cocycle (of A K) (of A L) 0

The two subtypes are the same group; only their instance paths differ.

Equations

• K.cocycleAddEquiv L = { toFun := ⇑(K.toCocycle L), invFun := ⇑(K.ofCocycle L), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Lifting the identification to the quotients

theorem CategoryTheory.Cdg.coboundariesIn_le_comap {A : Type u} [Category.{v, u} A] [Preadditive A] (K L : Cdg A) : H0.coboundariesIn K L ≤ AddSubgroup.comap (K.toCocycle L) (CochainComplex.HomComplex.coboundaries (of A K) (of A L) 0)

theorem CategoryTheory.Cdg.coboundaries_le_comap {A : Type u} [Category.{v, u} A] [Preadditive A] (K L : Cdg A) : CochainComplex.HomComplex.coboundaries (of A K) (of A L) 0 ≤ AddSubgroup.comap (K.ofCocycle L) (H0.coboundariesIn K L)

def CategoryTheory.Cdg.homEquivCohomologyClass {A : Type u} [Category.{v, u} A] [Preadditive A] (K L : Cdg A) : ↥(cocycles K L) ⧸ H0.coboundariesIn K L ≃+ CochainComplex.HomComplex.CohomologyClass (of A K) (of A L) 0

The Hom-group of H⁰(C^dg A) is Mathlib's group of degree-zero cohomology classes. Both directions are QuotientAddGroup.map of the corresponding AddMonoidHom, and both round trips are rfl on representatives.

Equations

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

The Hom-level seam

def CategoryTheory.Cdg.postcompAddEquiv {D : Type u_1} [Category.{u_2, u_1} D] [Preadditive D] {X Y Y' : D} (e : Y ≅ Y') : (X ⟶ Y) ≃+ (X ⟶ Y')

Postcomposition with an isomorphism, as an isomorphism of Hom-groups. Built by hand because it is used once and the additivity is one simp.

Equations

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

noncomputable def CategoryTheory.Cdg.homSeam {A : Type u} [Category.{v, u} A] [Preadditive A] (K L : Cdg A) : ↥(cocycles K L) ⧸ H0.coboundariesIn K L ≃+ ((HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj (of A K) ⟶ (HomotopyCategory.quotient A (ComplexShape.up ℤ)).obj (of A L))

The Hom-level seam. A degree-zero cohomology class in C^dg A is a morphism of the homotopy category, and the correspondence is an isomorphism of abelian groups.

Everything to the right of homEquivCohomologyClass is Mathlib's: the middle step is CohomologyClass.homAddEquiv, and the last undoes the ⟦0⟧ its statement carries.

Equations

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

The functor H⁰(C^dg A) ⥤ K(A)

theorem CategoryTheory.Cdg.homOf_comp {A : Type u} [Category.{v, u} A] [Preadditive A] {K L M : CochainComplex A ℤ} (z : CochainComplex.HomComplex.Cocycle K L 0) (w : CochainComplex.HomComplex.Cocycle L M 0) (hzw : (↑z).comp ↑w ⋯ ∈ CochainComplex.HomComplex.cocycle K M 0) : CochainComplex.HomComplex.Cocycle.homOf ⟨(↑z).comp ↑w ⋯, hzw⟩ = CategoryStruct.comp z.homOf w.homOf

Composition of degree-zero cocycles names composition of morphisms. Both sides are z.v i i ≫ w.v i i in each degree.

theorem CategoryTheory.Cdg.quotient_map_homOf_eq {A : Type u} [Category.{v, u} A] [Preadditive A] {K L : CochainComplex A ℤ} (z w : CochainComplex.HomComplex.Cocycle K L 0) (β : CochainComplex.HomComplex.Cochain K L (-1)) (hβ : ↑z = CochainComplex.HomComplex.δ (-1) 0 β + ↑w) : (HomotopyCategory.quotient A (ComplexShape.up ℤ)).map z.homOf = (HomotopyCategory.quotient A (ComplexShape.up ℤ)).map w.homOf

Two degree-zero cocycles differing by a coboundary name homotopic morphisms, so they agree in the homotopy category.

theorem CategoryTheory.Cdg.homOf_dgComp {A : Type u} [Category.{v, u} A] [Preadditive A] {K L M : Cdg A} (z : ↥(cocycles K L)) (w : ↥(cocycles L M)) (hzw : ((DGCategoryStruct.dgComp 0 0 0 ⋯) ↑z) ↑w ∈ cocycles K M) : ((K.toCocycle M) ⟨((DGCategoryStruct.dgComp 0 0 0 ⋯) ↑z) ↑w, hzw⟩).homOf = CategoryStruct.comp ((K.toCocycle L) z).homOf ((L.toCocycle M) w).homOf

homOf_comp, restated with dgComp in place of Cochain.comp. The two are the same by dgComp_eq, but the functor's goal is built from dgComp, and rw matches syntactically.

noncomputable def CategoryTheory.Cdg.h0Functor {A : Type u} [Category.{v, u} A] [Preadditive A] : Functor (H0 (Cdg A)) (HomotopyCategory A (ComplexShape.up ℤ))

The seam functor. H⁰(C^dg A) ⥤ K(A): the identity on objects, sending a cohomology class to the morphism its representative names.

Equations

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

The seam functor is an equivalence

instance CategoryTheory.Cdg.instFaithfulH0HomotopyCategoryIntUpH0Functor {A : Type u} [Category.{v, u} A] [Preadditive A] : h0Functor.Faithful

instance CategoryTheory.Cdg.instFullH0HomotopyCategoryIntUpH0Functor {A : Type u} [Category.{v, u} A] [Preadditive A] : h0Functor.Full

instance CategoryTheory.Cdg.instEssSurjH0HomotopyCategoryIntUpH0Functor {A : Type u} [Category.{v, u} A] [Preadditive A] : h0Functor.EssSurj

instance CategoryTheory.Cdg.instIsEquivalenceH0HomotopyCategoryIntUpH0Functor {A : Type u} [Category.{v, u} A] [Preadditive A] : h0Functor.IsEquivalence

noncomputable def CategoryTheory.Cdg.seam {A : Type u} [Category.{v, u} A] [Preadditive A] : H0 (Cdg A) ≌ HomotopyCategory A (ComplexShape.up ℤ)

The seam. H⁰(C^dg A) ≌ K(A): the H⁰ of the dg category of cochain complexes is the homotopy category.

Equations

• CategoryTheory.Cdg.seam = CategoryTheory.Cdg.h0Functor.asEquivalence