A quasi-equivalence induces an equivalence on H⁰

DGFunctor.IsQuasiEquivalence asks that every Hom-complex map be a quasi-isomorphism and that H⁰ F be essentially surjective. This file proves that such an F induces an equivalence H⁰ C ≌ H⁰ D.

This is dg-enhancements-e10, and it is what turns the recorded TwistCotwistEquivalenceConditions from data into a conclusion: those conditions are quasi-equivalences, and until now nothing in the repository consumed a quasi-equivalence at all.

The seam, and how it is crossed

A morphism of H⁰ is a degree-zero cocycle modulo coboundaries, while QuasiIso speaks about Mathlib's homology object. Identifying the two is the seam LinearH0.lean flagged as missing.

It is crossed without ever comparing the two descriptions of homology. Mathlib's ShortComplex.LeftHomologyMapData.quasiIso_iff says a morphism of short complexes is a quasi-isomorphism exactly when the φH of any left homology map datum is an isomorphism, and ShortComplex.abLeftHomologyData presents the homology of a short complex of abelian groups as the concrete quotient. So building one left homology map datum by hand, with φH the map F induces on cocycles modulo coboundaries, converts the hypothesis directly into that map being bijective. No naturality statement about abHomologyIso is needed, and Mathlib has none.

What the two halves give

Bijectivity of that map is full faithfulness of H⁰ F: injectivity is faithfulness, surjectivity is fullness. With the essential surjectivity that IsQuasiEquivalence already carries, Functor.IsEquivalence follows, since that class is exactly the three conditions.

What this does not say

Nothing about the converse, and nothing about dg functors that are only quasi-equivalences up to homotopy. It also says nothing about triangulated structure: the equivalence produced here is an equivalence of ordinary categories, and DGFunctor.h0Equivalence_functor says its functor is H⁰ F. Exactness of H⁰ F is proved separately, for every dg functor between pretriangulated dg categories, as DGFunctor.h0IsTriangulated; the two meet in DGFunctor.isTriangulated_h0Equivalence, the induced equivalence being triangulated in Mathlib's sense Equivalence.IsTriangulated.

@[reducible, inline]

abbrev CategoryTheory.homSc {C : Type u} [DGCategory C] (X Y : C) : ShortComplex AddCommGrpCat

The degree-zero short complex of a Hom complex: Hom⁻¹ ⟶ Hom⁰ ⟶ Hom¹.

Equations

• CategoryTheory.homSc X Y = HomologicalComplex.sc' (CategoryTheory.DGCategoryStruct.dgHom X Y) (-1) 0 1

theorem CategoryTheory.range_abToCycles {C : Type u} [DGCategory C] (X Y : C) : (homSc X Y).abToCycles.range = H0.coboundariesIn X Y

The cocycles of H⁰ are the kernel appearing in abLeftHomologyData, and the coboundaries are the range of abToCycles. The first is definitional; this is the second.

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

The map of degree-zero short complexes a dg functor induces.

Equations

• F.mapHomSc X Y = (HomologicalComplex.shortComplexFunctor' AddCommGrpCat (ComplexShape.up ℤ) (-1) 0 1).map (F.mapComplex X Y)

def CategoryTheory.DGFunctor.mapCocycles {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) (X Y : C) : ↥(cocycles X Y) →+ ↥(cocycles (F.obj X) (F.obj Y))

The action of F on degree-zero cocycles.

Equations

• F.mapCocycles X Y = ((F.map 0).comp (CategoryTheory.cocycles X Y).subtype).codRestrict (CategoryTheory.cocycles (F.obj X) (F.obj Y)) ⋯

def CategoryTheory.DGFunctor.mapH0Hom {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) (X Y : C) : ↥(cocycles X Y) ⧸ H0.coboundariesIn X Y →+ ↥(cocycles (F.obj X) (F.obj Y)) ⧸ H0.coboundariesIn (F.obj X) (F.obj Y)

The action of F on H⁰ Hom-groups, as a map of quotients.

Equations

• F.mapH0Hom X Y = QuotientAddGroup.map (CategoryTheory.H0.coboundariesIn X Y) (CategoryTheory.H0.coboundariesIn (F.obj X) (F.obj Y)) (F.mapCocycles X Y) ⋯

noncomputable def CategoryTheory.DGFunctor.mapHomScData {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) (X Y : C) : ShortComplex.LeftHomologyMapData (F.mapHomSc X Y) (homSc X Y).abLeftHomologyData (homSc (F.obj X) (F.obj Y)).abLeftHomologyData

The left homology map datum whose φH is the map on H⁰ Hom-groups.

abLeftHomologyData presents the homology of each short complex as cocycles modulo coboundaries, and this datum's φH is exactly what F does there. LeftHomologyMapData.quasiIso_iff then converts the quasi-isomorphism hypothesis into bijectivity of that map.

Equations

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

theorem CategoryTheory.DGFunctor.h0_map_eq_mapH0Hom {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) (X Y : H0 C) : F.h0.map = ⇑(F.mapH0Hom (H0.of C X) (H0.of C Y))

H⁰ F acts on Hom-groups by mapH0Hom: both are the quotient map induced by F.map 0.

noncomputable def CategoryTheory.DGFunctor.homologyQuotientEquiv {C : Type u} [DGCategory C] (X Y : C) : ↑(homSc X Y).abLeftHomologyData.H ≃+ ↥(cocycles X Y) ⧸ H0.coboundariesIn X Y

The comparison between the two quotients: abLeftHomologyData divides by the range of abToCycles, and H⁰ divides by the coboundaries.

Equations

• CategoryTheory.DGFunctor.homologyQuotientEquiv X Y = QuotientAddGroup.quotientAddEquivOfEq ⋯

theorem CategoryTheory.DGFunctor.mapH0Hom_comp_homologyQuotientEquiv {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) (X Y : C) (z : ↑(homSc X Y).abLeftHomologyData.H) : (homologyQuotientEquiv (F.obj X) (F.obj Y)) ((AddCommGrpCat.Hom.hom (F.mapHomScData X Y).φH) z) = (F.mapH0Hom X Y) ((homologyQuotientEquiv X Y) z)

theorem CategoryTheory.DGFunctor.bijective_mapH0Hom {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) (hF : F.IsQuasiEquivalence) (X Y : C) : Function.Bijective ⇑(F.mapH0Hom X Y)

The quasi-isomorphism hypothesis, read on H⁰ Hom-groups.

LeftHomologyMapData.quasiIso_iff turns the hypothesis into IsIso of the datum's φH, isIso_iff_bijective turns that into bijectivity, and the comparison above carries it to the map H⁰ F induces.

theorem CategoryTheory.DGFunctor.faithful_h0 {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) (hF : F.IsQuasiEquivalence) : F.h0.Faithful

H⁰ of a quasi-equivalence is faithful.

theorem CategoryTheory.DGFunctor.full_h0 {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) (hF : F.IsQuasiEquivalence) : F.h0.Full

H⁰ of a quasi-equivalence is full.

theorem CategoryTheory.DGFunctor.isEquivalence_h0 {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) (hF : F.IsQuasiEquivalence) : F.h0.IsEquivalence

A quasi-equivalence induces an equivalence on H⁰.

This is dg-enhancements-e10. Faithfulness and fullness come from the Hom-complex quasi-isomorphisms; essential surjectivity is the other field of IsQuasiEquivalence.

noncomputable def CategoryTheory.DGFunctor.h0Equivalence {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) (hF : F.IsQuasiEquivalence) : H0 C ≌ H0 D

The equivalence H⁰ C ≌ H⁰ D a quasi-equivalence induces.

Equations

• F.h0Equivalence hF = F.h0.asEquivalence

@[simp]

theorem CategoryTheory.DGFunctor.h0Equivalence_functor {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) (hF : F.IsQuasiEquivalence) : (F.h0Equivalence hF).functor = F.h0

The forward functor of the induced equivalence is H⁰ F itself, so the equivalence adds no second construction: everything proved of F.h0 (its linearity, its shift and triangulated structure) is a statement about it.