Representable DG modules and the Yoneda lemma

A right DG module over a DG category C is a DG functor Cᵒᵖ ⥤ C(R) into the DG category of cochain complexes of R-modules. Every object X of C gives the representable right module Hom(-, X): it sends Y to the Hom complex Hom(Y, X), and a morphism f : Z ⟶ Y of degree n acts by precomposition, the degree-n cochain g ↦ f ≫ g from Hom(Y, X) to Hom(Z, X). No sign enters: the Leibniz rule makes precomposition commute with the differentials, and the Koszul sign of composition in the opposite DG category is exactly the one of composition of cochains.

A morphism u : X ⟶ X' of degree n acts on the values Hom(Y, X) by postcomposition in Keller's order, g ↦ u ∘ g = (-1) ^ (p * n) • (g ≫ u) for g of degree p. With this sign postcomposition commutes with the differentials, identities and composition on the nose, and it commutes with precomposition up to the Koszul sign (-1) ^ (p * n); this is what makes it a morphism of right DG modules in TauCeti.CategoryTheory.DG.Yoneda.

The Yoneda lemma identifies DG natural transformations Hom(-, X) ⟶ F, that is closed degree-zero morphisms of right DG modules, with the closed degree-zero elements of F(X): a transformation η goes to η_X(1_X), and a closed element x of degree zero goes to the transformation whose component at Y sends g : Y ⟶ X of degree p to F(g)(x). For a representable target Hom(-, X') the closed degree-zero elements are the closed degree-zero morphisms X ⟶ X', and the transformation they give is postcomposition.

Main definitions

• TauCeti.dgRepresentable: the representable right DG module Hom(-, X).
• TauCeti.dgPostcomp: postcomposition with a homogeneous morphism, as a morphism of the DG category of cochain complexes between values of representable modules.
• TauCeti.dgYonedaEquiv: the Yoneda bijection between DG natural transformations out of Hom(-, X) and closed degree-zero elements of F(X).
• TauCeti.dgRepresentableNatTransEquiv: DG natural transformations between representables are the closed degree-zero morphisms between the representing objects.

Main results

• TauCeti.dgRepresentable_dgMap_v: a morphism acts on the representable module by precomposition.
• TauCeti.dgPostcomp_dgDifferential, TauCeti.dgPostcomp_dgId and TauCeti.dgPostcomp_dgComp: postcomposition commutes with the differentials, identities and composition.
• TauCeti.dgComp_dgMap_dgPostcomp: postcomposition commutes with precomposition up to the Koszul sign.
• TauCeti.dgMap_dgComp_v_apply: a right DG module carries a composite to the composite of cochains in the reversed order.
• TauCeti.dgYonedaEquiv_apply_coe and TauCeti.dgApp_dgYonedaEquiv_symm_v: the two directions of the Yoneda bijection.
• TauCeti.dgApp_dgRepresentableNatTransEquiv_symm_v: the transformation between representables given by a closed morphism is postcomposition with it.

References

• B. Keller, Deriving DG categories, Sections 1 and 2.
• G. M. Kelly, Basic concepts of enriched category theory, Section 1.9, for the Yoneda lemma on underlying sets of natural transformations.

The representable right DG module

noncomputable def TauCeti.dgPrecomp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) {Y Z : C} (n : ℤ) : DGHom R n Z Y →ₗ[R] CochainComplex.HomComplex.Cochain (dgHomComplex R Y X) (dgHomComplex R Z X) n

Precomposition with a morphism f : Z ⟶ Y of degree n, as a degree-n cochain from Hom(Y, X) to Hom(Z, X), linear in f. Its component on morphisms of degree p sends g to f ≫ g (TauCeti.dgPrecomp_v).

@[simp]

theorem TauCeti.dgPrecomp_v (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) {Y Z : C} {n : ℤ} (f : DGHom R n Z Y) (p q : ℤ) (hpq : p + n = q) (g : DGHom R p Y X) : (ModuleCat.Hom.hom (((dgPrecomp R X n) f).v p q hpq)) g = dgComp R f g ⋯

The component of precomposition with f on a morphism g is the composite f ≫ g.

@[simp]

theorem TauCeti.dgPrecomp_dgDifferential (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) {Y Z : C} {n : ℤ} (f : DGHom R n Z Y) : (dgPrecomp R X (n + 1)) ((dgDifferential R n) f) = CochainComplex.HomComplex.δ n (n + 1) ((dgPrecomp R X n) f)

Precomposition commutes with the differentials: by the Leibniz rule, precomposing with d f is the differential of precomposing with f in the Hom complex of cochains.

@[simp]

theorem TauCeti.dgPrecomp_dgId (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : C) : (dgPrecomp R X 0) (dgId R Y) = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id (dgHomComplex R Y X))

Precomposition with an identity is the identity cochain.

@[simp]

theorem TauCeti.dgPrecomp_dgComp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) {Y Z W : C} {p q n : ℤ} (f : DGHom R p Z Y) (g : DGHom R q W Z) (h : q + p = n) : (dgPrecomp R X n) (dgComp R g f h) = ((dgPrecomp R X p) f).comp ((dgPrecomp R X q) g) ⋯

Precomposition is contravariantly functorial: precomposing with g ≫ f is precomposing with f and then with g, with no sign.

noncomputable def TauCeti.dgRepresentable (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) Cᵒᵖ (CochainComplex (ModuleCat R) ℤ)

The representable right DG module Hom(-, X) of an object X of a DG category: the DG functor from the opposite DG category to cochain complexes sending Y to the Hom complex Hom(Y, X), on which a morphism f : Z ⟶ Y of degree n acts by precomposition.

theorem TauCeti.dgRepresentable_obj (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) (Y : Cᵒᵖ) : (dgRepresentable R X).obj Y = dgHomComplex R (Opposite.unop Y) X

The representable module Hom(-, X) sends Y to the Hom complex Hom(Y, X).

@[simp]

theorem TauCeti.dgRepresentable_dgMap (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) {Y Z : C} {n : ℤ} (f : DGHom R n Z Y) : ((dgRepresentable R X).dgMap n) f = (dgPrecomp R X n) f

A morphism acts on the representable module by precomposition with it.

Postcomposition

noncomputable def TauCeti.dgPostcomp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (Y : Cᵒᵖ) {X X' : C} (n : ℤ) : DGHom R n X X' →ₗ[R] DGHom R n ((dgRepresentable R X).obj Y) ((dgRepresentable R X').obj Y)

Postcomposition with a morphism u : X ⟶ X' of degree n, as a degree-n morphism Hom(Y, X) ⟶ Hom(Y, X') of the DG category of cochain complexes between the values at Y of the representable modules of X and X', linear in u. It is precomposition with u in the opposite DG category, so its component on morphisms of degree p sends g to the Keller-ordered composite u ∘ g = (-1) ^ (p * n) • (g ≫ u) (TauCeti.dgPostcomp_v).

@[simp]

theorem TauCeti.dgPostcomp_v (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (Y : C) {X X' : C} {n : ℤ} (u : DGHom R n X X') (p q : ℤ) (hpq : p + n = q) (g : DGHom R p Y X) : (ModuleCat.Hom.hom (CochainComplex.HomComplex.Cochain.v ((dgPostcomp R (Opposite.op Y) n) u) p q hpq)) g = (p * n).negOnePow • dgComp R g u hpq

The component of postcomposition with u on a morphism g of degree p is the Keller-ordered composite (-1) ^ (p * n) • (g ≫ u).

@[simp]

theorem TauCeti.dgPostcomp_dgDifferential (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (Y : Cᵒᵖ) {X X' : C} {n : ℤ} (u : DGHom R n X X') : (dgPostcomp R Y (n + 1)) ((dgDifferential R n) u) = (dgDifferential R n) ((dgPostcomp R Y n) u)

Postcomposition commutes with the differentials: postcomposing with d u is the differential of postcomposing with u, by the Leibniz rule in Keller's order.

@[simp]

theorem TauCeti.dgPostcomp_dgId (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (Y : Cᵒᵖ) (X : C) : (dgPostcomp R Y 0) (dgId R X) = dgId R ((dgRepresentable R X).obj Y)

Postcomposition with an identity is the identity.

@[simp]

theorem TauCeti.dgPostcomp_dgComp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (Y : Cᵒᵖ) {X X' X'' : C} {p q n : ℤ} (u : DGHom R p X X') (v : DGHom R q X' X'') (h : p + q = n) : (dgPostcomp R Y n) (dgComp R u v h) = dgComp R ((dgPostcomp R Y p) u) ((dgPostcomp R Y q) v) h

Postcomposition is functorial: postcomposing with u ≫ v is postcomposing with u and then with v.

theorem TauCeti.dgComp_dgMap_dgPostcomp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X X' : C} {Y Z : Cᵒᵖ} {p n m : ℤ} (f : DGHom R p Y Z) (u : DGHom R n X X') (h : p + n = m) (h' : n + p = m) : dgComp R (((dgRepresentable R X).dgMap p) f) ((dgPostcomp R Z n) u) h = (p * n).negOnePow • dgComp R ((dgPostcomp R Y n) u) (((dgRepresentable R X').dgMap p) f) h'

Postcomposition commutes with the module action up to the Koszul sign (-1) ^ (p * n) of the degrees: acting on Hom(-, X) by f : Y ⟶ Z of degree p in Cᵒᵖ and then postcomposing with u : X ⟶ X' of degree n is (-1) ^ (p * n) times postcomposing first and acting by f on Hom(-, X') afterwards.

The Yoneda lemma

theorem TauCeti.dgMap_dgComp_v_apply {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (X : C) (F : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) Cᵒᵖ (CochainComplex (ModuleCat R) ℤ)) {Y Z : C} {q r s : ℤ} (f : DGHom R q Z Y) (g : DGHom R r Y X) (h : q + r = s) {n : ℤ} (x : ↑((F.obj (Opposite.op X)).X n)) (k t : ℤ) (hk : n + r = k) (ht : n + s = t) : (ModuleCat.Hom.hom (CochainComplex.HomComplex.Cochain.v ((F.dgMap s) (dgComp R f g h)) n t ht)) x = (ModuleCat.Hom.hom (CochainComplex.HomComplex.Cochain.v ((F.dgMap q) f) k t ⋯)) ((ModuleCat.Hom.hom (CochainComplex.HomComplex.Cochain.v ((F.dgMap r) g) n k hk)) x)

A DG functor out of the opposite category carries a composite f ≫ g to the composite of cochains in the reversed order: evaluated on an element x of degree n, it is F(f)(F(g)(x)).

noncomputable def TauCeti.dgYonedaEquiv {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (X : C) (F : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) Cᵒᵖ (CochainComplex (ModuleCat R) ℤ)) : DGNatTrans (dgRepresentable R X) F ≃ ↥(ModuleCat.Hom.hom ((F.obj (Opposite.op X)).d 0 1)).ker

The Yoneda lemma for right DG modules: DG natural transformations Hom(-, X) ⟶ F are the closed degree-zero elements of F(X). A transformation goes to the image of the identity of X under its component at X (TauCeti.dgYonedaEquiv_apply_coe), and a closed element x goes to the transformation sending g : Y ⟶ X to F(g)(x) (TauCeti.dgApp_dgYonedaEquiv_symm_v).

@[simp]

theorem TauCeti.dgYonedaEquiv_apply_coe {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (X : C) (F : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) Cᵒᵖ (CochainComplex (ModuleCat R) ℤ)) (α : DGNatTrans (dgRepresentable R X) F) : ↑((dgYonedaEquiv X F) α) = (ModuleCat.Hom.hom (CochainComplex.HomComplex.Cochain.v (α.dgApp (Opposite.op X)) 0 0 ⋯)) (dgId R X)

The Yoneda bijection sends a transformation to the image of the identity of X under its component at X.

@[simp]

theorem TauCeti.dgApp_dgYonedaEquiv_symm_v {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (X : C) (F : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) Cᵒᵖ (CochainComplex (ModuleCat R) ℤ)) (x : ↥(ModuleCat.Hom.hom ((F.obj (Opposite.op X)).d 0 1)).ker) {Y : C} {p : ℤ} (g : DGHom R p Y X) : (ModuleCat.Hom.hom (CochainComplex.HomComplex.Cochain.v (((dgYonedaEquiv X F).symm x).dgApp (Opposite.op Y)) p p ⋯)) g = (ModuleCat.Hom.hom (CochainComplex.HomComplex.Cochain.v ((F.dgMap p) g) 0 p ⋯)) ↑x

The transformation given by a closed element x of degree zero sends g : Y ⟶ X of degree p to F(g)(x).

Transformations between representable modules

noncomputable def TauCeti.dgRepresentableNatTransEquiv (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X X' : C) : DGNatTrans (dgRepresentable R X) (dgRepresentable R X') ≃ ↥(dgCycles R X X')

DG natural transformations between representable modules Hom(-, X) ⟶ Hom(-, X') are the closed degree-zero morphisms X ⟶ X': a transformation goes to the image of the identity of X, and a closed morphism u goes to postcomposition with u (TauCeti.dgApp_dgRepresentableNatTransEquiv_symm_v).

@[simp]

theorem TauCeti.dgRepresentableNatTransEquiv_apply_coe {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (X X' : C) (α : DGNatTrans (dgRepresentable R X) (dgRepresentable R X')) : ↑((dgRepresentableNatTransEquiv R X X') α) = (ModuleCat.Hom.hom (CochainComplex.HomComplex.Cochain.v (α.dgApp (Opposite.op X)) 0 0 ⋯)) (dgId R X)

The closed morphism of a transformation between representable modules is the image of the identity under its component at the source.

@[simp]

theorem TauCeti.dgApp_dgRepresentableNatTransEquiv_symm_v {R : Type v} [CommRing R] {C : Type u} [DGCategory R C] (X X' : C) (u : ↥(dgCycles R X X')) {Y : C} {p : ℤ} (g : DGHom R p Y X) : (ModuleCat.Hom.hom (CochainComplex.HomComplex.Cochain.v (((dgRepresentableNatTransEquiv R X X').symm u).dgApp (Opposite.op Y)) p p ⋯)) g = dgComp R g ↑u ⋯

The transformation between representable modules given by a closed morphism u : X ⟶ X' is postcomposition with u.