The scalar-linear copower--Hom dg adjunction

In a k-linear dg category with scalar-linear copowers, the selected copower functor - ⊗ E is left dg adjoint to the linear Hom-complex functor Hom(E, -). The unit is the universal chain map of the selected copower and the counit is exactly the existing scalar-linear evaluation transformation.

Both triangle identities hold strictly in the dg categories. This file does not use pretriangulatedness, cones, finiteness, or a model of Perf(k), and it makes no sphericality or equivalence claim.

theorem CategoryTheory.LinearEvaluationData.ofHasLinearCopowers_functor_eq (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] [HasLinearCopowers k C] (E : C) : (ofHasLinearCopowers k E).functor = (DGLinear.homFunctor k E).comp (linearCopowerFunctor k E)

The selected scalar-linear evaluation functor is the composite of the linear Hom-complex functor with the selected copower functor.

noncomputable def CategoryTheory.linearCopowerAdjunction (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] [HasLinearCopowers k C] (E : C) : DGAdjunction (linearCopowerFunctor k E) (DGLinear.homFunctor k E)

The selected scalar-linear copower functor is left dg adjoint to the linear Hom-complex functor.

Equations

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

theorem CategoryTheory.linearCopowerAdjunction_unit_app (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] [HasLinearCopowers k C] (E : C) (K : Cdg (ModuleCat k)) : DGFunctor.HomogeneousNatTrans.app (linearCopowerAdjunction k E).unit K = CochainComplex.HomComplex.Cochain.ofHom (linearCopowerIsLinearCopower (Cdg.of (ModuleCat k) K) E).univ

The unit component of the scalar-linear copower--Hom dg adjunction is the universal chain map of the selected copower.

theorem CategoryTheory.linearCopowerAdjunction_counit (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] [HasLinearCopowers k C] (E : C) : (linearCopowerAdjunction k E).counit = (LinearEvaluationData.ofHasLinearCopowers k E).evaluation

The counit of the scalar-linear copower--Hom dg adjunction is exactly the selected scalar-linear evaluation transformation.

theorem CategoryTheory.linearCopowerAdjunction_counit_app (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] [HasLinearCopowers k C] (E Y : C) : DGFunctor.HomogeneousNatTrans.app (linearCopowerAdjunction k E).counit Y = (LinearEvaluationData.ofHasLinearCopowers k E).evalHom Y

Because the adjunction reuses the existing evaluation transformation, its counit component reduces definitionally to the selected representing lift of the identity cochain.