Linearity of H⁰

A k-linear dg category has a canonically k-linear homotopy category. The construction uses Mathlib's ordinary CategoryTheory.Linear root: degree-zero cocycles form a submodule, coboundaries form a submodule of the cocycles, and the Hom-modules of H⁰ are the resulting quotient modules.

A scalar-preserving dg functor therefore induces a Mathlib-linear functor on H⁰. No separate ordinary category structure is introduced.

This leaf packages linearity only. Exactness of H⁰ F is a separate capability: DGFunctor.PreservesShifts and DGFunctor.PreservesChosenCones are constructed for every dg functor, by DGFunctor.preservesShifts and DGFunctor.preservesChosenCones (DGCategory/Pretriangulated/Functor.lean), and, between pretriangulated dg categories, DGFunctor.h0IsTriangulated (DGCategory/Pretriangulated/H0/Functor.lean) spends them on H⁰ F.

The other seam this file used to flag, identifying a general H⁰-Hom quotient with Mathlib's chosen homology object, is crossed in DGCategory/QuasiEquivalence.lean: not by comparing the two descriptions of homology, but by building one ShortComplex.LeftHomologyMapData whose φH is the map on cocycles modulo coboundaries. IsQuasiEquivalence now does supply full faithfulness on H⁰.

def CategoryTheory.H0.cocyclesSubmodule {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] (X Y : C) : Submodule k ↑((DGCategoryStruct.dgHom X Y).X 0)

Degree-zero cocycles as a k-submodule of the degree-zero part of the Hom-complex.

Equations

• CategoryTheory.H0.cocyclesSubmodule X Y = { carrier := ↑(CategoryTheory.cocycles X Y), add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[implicit_reducible]

instance CategoryTheory.H0.cocyclesModule {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] (X Y : C) : Module k ↥(cocycles X Y)

The cocycles inherit their module structure from the ambient degree-zero piece of the Hom-complex.

Equations

• CategoryTheory.H0.cocyclesModule X Y = id inferInstance

def CategoryTheory.H0.coboundariesSubmodule {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] (X Y : C) : Submodule k ↥(cocycles X Y)

Degree-zero coboundaries as a k-submodule of the cocycles.

Equations

• CategoryTheory.H0.coboundariesSubmodule X Y = { carrier := ↑(CategoryTheory.H0.coboundariesIn X Y), add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[implicit_reducible]

instance CategoryTheory.H0.homModule {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] (X Y : H0 C) : Module k (X ⟶ Y)

Each Hom-group of H⁰ C is the quotient module of degree-zero cocycles by degree-zero coboundaries.

Equations

• X.homModule Y = id inferInstance

@[implicit_reducible]

instance CategoryTheory.H0.linear {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] : Linear k (H0 C)

The canonical Mathlib k-linear structure on H⁰ of a k-linear dg category.

Equations

• CategoryTheory.H0.linear = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }

instance CategoryTheory.DGFunctor.h0Linear {k : Type w} [CommRing k] {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [(X Y : D) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [DGLinear k D] (F : DGFunctor C D) [Linear k F] : Functor.Linear k F.h0

H⁰ of a scalar-preserving dg functor is a Mathlib-linear functor.