The scalar-linear Hom dg functor

For a fixed object E of a k-linear dg category, right composition assembles the linear Hom-complexes Hom(E, X) into a k-linear dg functor to the standard dg category of module-valued cochain complexes.

This is the right-adjoint-shaped half of the tensor--Hom interface. The adjunction itself belongs in LinearCopowerAdjunction, where scalar-linear copowers are available. No pretriangulated, cone, or finiteness assumptions are needed here.

def CategoryTheory.DGLinear.homFunctor (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] (E : C) : DGFunctor C (Cdg (ModuleCat k))

For fixed E, the scalar-linear Hom-complex Hom(E, -) is a dg functor to the standard dg category of k-module complexes.

Equations

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

@[simp]

theorem CategoryTheory.DGLinear.homFunctor_obj (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] (E X : C) : (homFunctor k E).obj X = homComplex k E X

Normalize object projections to the fixed-source Hom-complex. This is a simp lemma because objects have a canonical normal form; the map projection below remains explicit so rewriting does not unfold abstract functor maps.

theorem CategoryTheory.DGLinear.homFunctor_map (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] (E : C) {X Y : C} (p : ℤ) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) : ((homFunctor k E).map p) f = (postcompCochain k E p) f

The Hom dg functor acts on a homogeneous morphism by right composition. Kept out of the simp set to preserve the abstract functor-map normal form.

instance CategoryTheory.DGLinear.homFunctor_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] (E : C) : DGFunctor.Linear k (homFunctor k E)

The Hom dg functor preserves the scalar action.