Scalar-linear Hom-complex comparison for dg shifts

The additive comparison IsShiftBy.homIso identifies the Hom-complex into a chosen shift with a shifted Hom-complex. In a k-linear dg category the same right-composition map is linear in every degree, so it gives an isomorphism of ModuleCat k-valued complexes.

This file supplies that scalar refinement. It does not define another shift, cohomology object, or quotient: the comparison is built from the existing IsShiftBy witness and DGLinear.homComplex.

noncomputable def CategoryTheory.IsShiftBy.linearHomMap {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} {n : ℤ} (h : IsShiftBy X n Y) (W : C) : DGLinear.homComplex k W X ⟶ (shiftFunctor (CochainComplex (ModuleCat k) ℤ) (-n)).obj (DGLinear.homComplex k W Y)

Right composition with the shift element as a morphism of scalar-linear Hom-complexes. It is obtained from the standard Mathlib equivalence between closed degree--n cochains and maps into the -n shift.

Equations

• h.linearHomMap W = CochainComplex.HomComplex.Cocycle.equivHomShift.symm (CategoryTheory.IsShiftBy.linearHomCocycle✝ h W)

@[simp]

theorem CategoryTheory.IsShiftBy.linearHomMap_f_apply {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} {n : ℤ} (h : IsShiftBy X n Y) (W : C) (p : ℤ) (f : ↑((DGCategoryStruct.dgHom W X).X p)) : (ModuleCat.Hom.hom ((h.linearHomMap W).f p)) f = ((DGCategoryStruct.dgComp p (-n) (p + -n) ⋯) f) h.hom

theorem CategoryTheory.IsShiftBy.bijective_linearHomMap {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} {n : ℤ} (h : IsShiftBy X n Y) (W : C) (p : ℤ) : Function.Bijective ⇑(ModuleCat.Hom.hom ((h.linearHomMap W).f p))

Every component of the scalar-linear Hom-complex comparison is bijective.

noncomputable def CategoryTheory.IsShiftBy.linearHomIso {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} {n : ℤ} (h : IsShiftBy X n Y) (W : C) : DGLinear.homComplex k W X ≅ (shiftFunctor (CochainComplex (ModuleCat k) ℤ) (-n)).obj (DGLinear.homComplex k W Y)

The scalar-linear Hom-complex isomorphism represented by a chosen dg shift.

Equations

• h.linearHomIso W = HomologicalComplex.Hom.isoOfComponents (fun (p : ℤ) => CategoryTheory.asIso ((h.linearHomMap W).f p)) ⋯

@[simp]

theorem CategoryTheory.IsShiftBy.linearHomIso_hom_f_apply {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} {n : ℤ} (h : IsShiftBy X n Y) (W : C) (p : ℤ) (f : ↑((DGCategoryStruct.dgHom W X).X p)) : (ModuleCat.Hom.hom ((h.linearHomIso W).hom.f p)) f = ((DGCategoryStruct.dgComp p (-n) (p + -n) ⋯) f) h.hom