Quasi-equivalences of differential graded categories

A DG functor is quasi-fully faithful when it induces a quasi-isomorphism on every Hom complex. A quasi-equivalence additionally reaches every target object up to isomorphism in the homotopy category. Full DG subcategories furnish a basic example: their inclusions are quasi-equivalences exactly when each ambient object is isomorphic in H⁰ to an object of the subcategory.

On homotopy categories, a quasi-fully faithful DG functor F induces a fully faithful functor H⁰(F), and a quasi-equivalence induces an equivalence H⁰(C) ≌ H⁰(D). The converse fails: H⁰(F) only sees the degree-zero cohomology of the Hom complexes.

Main results

• CategoryTheory.EnrichedFunctor.IsQuasiFullyFaithful.full_mapDGHomotopyCategory and CategoryTheory.EnrichedFunctor.IsQuasiFullyFaithful.faithful_mapDGHomotopyCategory: a quasi-fully faithful DG functor induces a fully faithful functor on homotopy categories.
• CategoryTheory.EnrichedFunctor.isQuasiEquivalence_iff_isQuasiFullyFaithful_and_essSurj: a quasi-equivalence is a quasi-fully faithful DG functor whose induced functor on homotopy categories is essentially surjective.
• CategoryTheory.EnrichedFunctor.IsQuasiEquivalence.isEquivalence_mapDGHomotopyCategory: a quasi-equivalence induces an equivalence of homotopy categories.
• TauCeti.DGFullSubcategory.isQuasiEquivalence_inclusion_iff: when the inclusion of a full DG subcategory is a quasi-equivalence.

References

• B. Keller, Deriving DG categories, Section 2.
• V. Drinfeld, DG quotients of DG categories, Section 2.

def CategoryTheory.EnrichedFunctor.IsQuasiFullyFaithful {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) : Prop

A DG functor is quasi-fully faithful if its map on each Hom complex is a quasi-isomorphism, in every cohomological degree.

Equations

• F.IsQuasiFullyFaithful = ∀ (X Y : C), QuasiIso (F.map X Y)

theorem CategoryTheory.EnrichedFunctor.IsQuasiFullyFaithful.isIso_homologyMap {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] {F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D} (hF : F.IsQuasiFullyFaithful) (X Y : C) (n : ℤ) : IsIso (HomologicalComplex.homologyMap (F.map X Y) n)

A quasi-fully-faithful DG functor induces an isomorphism on the cohomology of each Hom complex in every degree.

theorem CategoryTheory.EnrichedFunctor.isQuasiFullyFaithful_iff_isIso_homologyMap {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) : F.IsQuasiFullyFaithful ↔ ∀ (X Y : C) (n : ℤ), IsIso (HomologicalComplex.homologyMap (F.map X Y) n)

A DG functor is quasi-fully faithful exactly when it induces isomorphisms on all Hom cohomology groups.

@[simp]

theorem CategoryTheory.EnrichedFunctor.isQuasiFullyFaithful_id {R : Type v} [CommRing R] {C : Type u₁} [TauCeti.DGCategory R C] : (id (CochainComplex (ModuleCat R) ℤ) C).IsQuasiFullyFaithful

The identity DG functor is quasi-fully faithful.

theorem CategoryTheory.EnrichedFunctor.isQuasiFullyFaithful_of_isIso_map {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] {F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D} (hF : ∀ (X Y : C), IsIso (F.map X Y)) : F.IsQuasiFullyFaithful

A DG functor which is an isomorphism on every Hom complex is quasi-fully faithful.

theorem CategoryTheory.EnrichedFunctor.IsQuasiFullyFaithful.comp {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} {E : Type u₃} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] [TauCeti.DGCategory R E] {F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D} {G : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) D E} (hF : F.IsQuasiFullyFaithful) (hG : G.IsQuasiFullyFaithful) : (EnrichedFunctor.comp (CochainComplex (ModuleCat R) ℤ) F G).IsQuasiFullyFaithful

Composition preserves quasi-full faithfulness.

@[simp]

theorem CategoryTheory.EnrichedFunctor.isQuasiFullyFaithful_op_iff {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) : F.op.IsQuasiFullyFaithful ↔ F.IsQuasiFullyFaithful

A DG functor is quasi-fully faithful exactly when its opposite is: the Hom chain maps are the same maps with source and target reversed.

def CategoryTheory.EnrichedFunctor.IsQuasiEquivalence {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) : Prop

A DG functor is a quasi-equivalence when it is a quasi-isomorphism on all Hom complexes and every target object is isomorphic in H⁰ to an object in its image.

Equations

• F.IsQuasiEquivalence = (F.IsQuasiFullyFaithful ∧ ∀ (Y : D), ∃ (X : C), Nonempty (TauCeti.DGHomotopyCategory.of R (F.obj X) ≅ TauCeti.DGHomotopyCategory.of R Y))

theorem CategoryTheory.EnrichedFunctor.IsQuasiEquivalence.isQuasiFullyFaithful {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] {F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D} (hF : F.IsQuasiEquivalence) : F.IsQuasiFullyFaithful

A quasi-equivalence is quasi-fully faithful.

theorem CategoryTheory.EnrichedFunctor.IsQuasiEquivalence.essentiallySurjective {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] {F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D} (hF : F.IsQuasiEquivalence) (Y : D) : ∃ (X : C), Nonempty (TauCeti.DGHomotopyCategory.of R (F.obj X) ≅ TauCeti.DGHomotopyCategory.of R Y)

A quasi-equivalence reaches every target object up to isomorphism in H⁰.

@[simp]

theorem CategoryTheory.EnrichedFunctor.isQuasiEquivalence_id {R : Type v} [CommRing R] {C : Type u₁} [TauCeti.DGCategory R C] : (id (CochainComplex (ModuleCat R) ℤ) C).IsQuasiEquivalence

The identity DG functor is a quasi-equivalence.

The induced functor on homotopy categories

theorem CategoryTheory.EnrichedFunctor.IsQuasiFullyFaithful.mapDGHomotopyCategory_map_bijective {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] {F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D} (hF : F.IsQuasiFullyFaithful) (X Y : TauCeti.DGHomotopyCategory R C) : Function.Bijective F.mapDGHomotopyCategory.map

A quasi-fully faithful DG functor induces a bijection on every Hom of homotopy categories.

theorem CategoryTheory.EnrichedFunctor.IsQuasiFullyFaithful.full_mapDGHomotopyCategory {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] {F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D} (hF : F.IsQuasiFullyFaithful) : F.mapDGHomotopyCategory.Full

A quasi-fully faithful DG functor induces a full functor on homotopy categories.

theorem CategoryTheory.EnrichedFunctor.IsQuasiFullyFaithful.faithful_mapDGHomotopyCategory {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] {F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D} (hF : F.IsQuasiFullyFaithful) : F.mapDGHomotopyCategory.Faithful

A quasi-fully faithful DG functor induces a faithful functor on homotopy categories.

theorem CategoryTheory.EnrichedFunctor.isQuasiEquivalence_iff_isQuasiFullyFaithful_and_essSurj {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) : F.IsQuasiEquivalence ↔ F.IsQuasiFullyFaithful ∧ F.mapDGHomotopyCategory.EssSurj

A DG functor is a quasi-equivalence exactly when it is quasi-fully faithful and the functor it induces on homotopy categories is essentially surjective.

theorem CategoryTheory.EnrichedFunctor.IsQuasiEquivalence.isEquivalence_mapDGHomotopyCategory {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] {F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D} (hF : F.IsQuasiEquivalence) : F.mapDGHomotopyCategory.IsEquivalence

A quasi-equivalence of DG categories induces an equivalence of homotopy categories.

@[simp]

theorem TauCeti.DGFullSubcategory.isQuasiFullyFaithful_inclusion {R : Type v} [CommRing R] {C : Type u₁} [DGCategory R C] {P : C → Prop} : (inclusion R).IsQuasiFullyFaithful

The inclusion of a full DG subcategory is quasi-fully faithful: its maps on Hom complexes are identity maps.

@[simp]

theorem TauCeti.DGFullSubcategory.isQuasiEquivalence_inclusion_iff {R : Type v} [CommRing R] {C : Type u₁} [DGCategory R C] {P : C → Prop} : (inclusion R).IsQuasiEquivalence ↔ ∀ (Y : C), ∃ (X : C), P X ∧ Nonempty (DGHomotopyCategory.of R X ≅ DGHomotopyCategory.of R Y)

Inclusion of a full DG subcategory is a quasi-equivalence precisely when every ambient object is isomorphic in H⁰ to an object satisfying its predicate.