The DG Yoneda embedding of a DG category

For a small DG category C over R, the right DG modules over C are the DG functors Cᵒᵖ ⥤ C(R) into cochain complexes, and they form a DG category whose Hom complexes consist of the natural families of homogeneous morphisms (TauCeti.DGFunctor.instDGCategory). This file makes the representable modules Hom(-, X) of TauCeti.CategoryTheory.DG.Representable into a DG functor, the DG Yoneda embedding TauCeti.dgYoneda : C ⥤ Mod-C, and proves the Yoneda lemma at the level of Hom complexes.

A morphism u : X ⟶ X' of degree n acts on Hom(Y, X) by postcomposition in Keller's order, g ↦ u ∘ g = (-1) ^ (p * n) • (g ≫ u) for g of degree p (TauCeti.dgPostcomp). With this sign, postcomposition commutes with the differentials and with composition on the nose, and it commutes with the precomposition action of C up to the Koszul sign (-1) ^ (p * n) demanded of a natural family of degree n (TauCeti.dgComp_dgMap_dgPostcomp, in TauCeti.CategoryTheory.DG.Representable).

The DG Yoneda lemma identifies the Hom complex of modules Hom(Hom(-, X), F) with the complex F(X), by evaluating the component at X on the identity of X (TauCeti.dgRepresentableHomIso). The inverse sends x of degree n to the morphism whose component at Y is g ↦ (-1) ^ (p * n) • F(g)(x). On closed degree-zero morphisms this is the Yoneda bijection TauCeti.dgYonedaEquiv for DG natural transformations. For a representable target the inverse is postcomposition, so the Yoneda embedding is an isomorphism on every Hom complex, and in particular quasi-fully faithful.

Main definitions

• TauCeti.dgPostcompHom: postcomposition as a morphism of right DG modules Hom(-, X) ⟶ Hom(-, X').
• TauCeti.dgYoneda: the DG Yoneda embedding.
• TauCeti.dgRepresentableHomEquiv: the degreewise Yoneda bijection between morphisms Hom(-, X) ⟶ F of degree n and elements of F(X) of degree n.
• TauCeti.dgRepresentableHomIso: the Yoneda isomorphism of complexes Hom(Hom(-, X), F) ≅ F(X).

Main results

• TauCeti.isNatural_dgPostcomp: postcompositions form a natural family.
• TauCeti.dgYoneda_obj and TauCeti.dgYoneda_dgMap: the Yoneda embedding sends X to Hom(-, X) and acts on morphisms by postcomposition.
• TauCeti.dgRepresentableHomEquiv_dgDifferential: the Yoneda bijection commutes with the differentials.
• TauCeti.dgRepresentableHomEquiv_homEquivDGCycles: on closed degree-zero morphisms it is TauCeti.dgYonedaEquiv.
• TauCeti.isIso_map_dgYoneda: the Yoneda embedding is an isomorphism on Hom complexes.
• TauCeti.isQuasiFullyFaithful_dgYoneda: the Yoneda embedding is quasi-fully faithful.

References

• B. Keller, Deriving DG categories, Annales scientifiques de l'École Normale Supérieure 27 (1994), Sections 1 and 2.
• G. M. Kelly, Basic concepts of enriched category theory, Sections 2.4 and 2.5, for the enriched Yoneda lemma and the full faithfulness of the enriched Yoneda embedding.

Naturality of postcomposition

theorem TauCeti.isNatural_dgPostcomp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X X' : C} {n : ℤ} (u : DGHom R n X X') : DGFunctor.IsNatural fun (Y : Cᵒᵖ) => (dgPostcomp R Y n) u

Postcomposition is natural: for u : X ⟶ X' of degree n, the postcompositions with u form a natural family of degree-n morphisms Hom(-, X) ⟶ Hom(-, X') of right DG modules.

The Yoneda embedding

noncomputable def TauCeti.dgPostcompHom (R : Type v) [CommRing R] {C : Type v} [DGCategory R C] (X X' : C) (n : ℤ) : DGHom R n X X' →ₗ[R] DGHom R n { toEnrichedFunctor := dgRepresentable R X } { toEnrichedFunctor := dgRepresentable R X' }

Postcomposition with u : X ⟶ X' of degree n, as a degree-n morphism of right DG modules Hom(-, X) ⟶ Hom(-, X'): its component at Y is TauCeti.dgPostcomp. This is the action of the Yoneda embedding on morphisms (TauCeti.dgYoneda_dgMap).

@[simp]

theorem TauCeti.dgApp_dgPostcompHom (R : Type v) [CommRing R] {C : Type v} [DGCategory R C] {X X' : C} {n : ℤ} (u : DGHom R n X X') (Y : Cᵒᵖ) : (DGFunctor.dgApp R n Y) ((dgPostcompHom R X X' n) u) = (dgPostcomp R Y n) u

The component at Y of postcomposition with u, as a morphism of right DG modules, is postcomposition with u on Hom(Y, X).

@[simp]

theorem TauCeti.dgPostcompHom_dgDifferential (R : Type v) [CommRing R] {C : Type v} [DGCategory R C] {X X' : C} {n : ℤ} (u : DGHom R n X X') : (dgPostcompHom R X X' (n + 1)) ((dgDifferential R n) u) = (dgDifferential R n) ((dgPostcompHom R X X' n) u)

Postcomposition, as a morphism of right DG modules, commutes with the differentials.

@[simp]

theorem TauCeti.dgPostcompHom_dgId (R : Type v) [CommRing R] {C : Type v} [DGCategory R C] (X : C) : (dgPostcompHom R X X 0) (dgId R X) = dgId R { toEnrichedFunctor := dgRepresentable R X }

Postcomposition with an identity is the identity morphism of right DG modules.

@[simp]

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

Postcomposition, as a morphism of right DG modules, is functorial.

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

The DG Yoneda embedding of a DG category C into the DG category of right DG modules over C, the DG functors Cᵒᵖ ⥤ C(R): an object X goes to the representable module Hom(-, X), and a morphism u : X ⟶ X' of degree n goes to the degree-n morphism of modules Hom(-, X) ⟶ Hom(-, X') given by postcomposition with u, g ↦ u ∘ g (TauCeti.dgYoneda_dgMap).

@[simp]

theorem TauCeti.dgYoneda_obj (R : Type v) [CommRing R] {C : Type v} [DGCategory R C] (X : C) : (dgYoneda R).obj X = { toEnrichedFunctor := dgRepresentable R X }

The Yoneda embedding sends an object X to the representable module Hom(-, X).

@[simp]

theorem TauCeti.dgYoneda_dgMap (R : Type v) [CommRing R] {C : Type v} [DGCategory R C] {X X' : C} {n : ℤ} (u : DGHom R n X X') : ((dgYoneda R).dgMap n) u = (dgPostcompHom R X X' n) u

The Yoneda embedding acts on morphisms by postcomposition.

The Yoneda lemma

noncomputable def TauCeti.dgRepresentableHomEquiv (R : Type v) [CommRing R] {C : Type v} [DGCategory R C] (X : C) (F : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) Cᵒᵖ (CochainComplex (ModuleCat R) ℤ)) (n : ℤ) : DGHom R n { toEnrichedFunctor := dgRepresentable R X } { toEnrichedFunctor := F } ≃ₗ[R] ↑((F.obj (Opposite.op X)).X n)

The DG Yoneda lemma, degreewise: morphisms of degree n of right DG modules Hom(-, X) ⟶ F are the elements of F(X) of degree n. A morphism η goes to η_X(1_X) (TauCeti.dgRepresentableHomEquiv_apply), and an element x goes to the morphism whose component at Y sends g : Y ⟶ X of degree p to (-1) ^ (p * n) • F(g)(x) (TauCeti.dgApp_dgRepresentableHomEquiv_symm_v).

@[simp]

theorem TauCeti.dgRepresentableHomEquiv_apply (R : Type v) [CommRing R] {C : Type v} [DGCategory R C] (X : C) (F : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) Cᵒᵖ (CochainComplex (ModuleCat R) ℤ)) {n : ℤ} (η : DGHom R n { toEnrichedFunctor := dgRepresentable R X } { toEnrichedFunctor := F }) : (dgRepresentableHomEquiv R X F n) η = (ModuleCat.Hom.hom (CochainComplex.HomComplex.Cochain.v ((DGFunctor.dgApp R n (Opposite.op X)) η) 0 n ⋯)) (dgId R X)

The Yoneda bijection sends a morphism η : Hom(-, X) ⟶ F to η_X(1_X).

@[simp]

theorem TauCeti.dgApp_dgRepresentableHomEquiv_symm_v (R : Type v) [CommRing R] {C : Type v} [DGCategory R C] (X : C) (F : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) Cᵒᵖ (CochainComplex (ModuleCat R) ℤ)) {n : ℤ} (x : ↑((F.obj (Opposite.op X)).X n)) {Y : C} {p q : ℤ} (hpq : p + n = q) (g : DGHom R p Y X) : (ModuleCat.Hom.hom (CochainComplex.HomComplex.Cochain.v ((DGFunctor.dgApp R n (Opposite.op Y)) ((dgRepresentableHomEquiv R X F n).symm x)) p q hpq)) g = (p * n).negOnePow • (ModuleCat.Hom.hom (CochainComplex.HomComplex.Cochain.v ((F.dgMap p) g) n q ⋯)) x

The morphism Hom(-, X) ⟶ F given by an element x of F(X) of degree n sends g : Y ⟶ X of degree p to (-1) ^ (p * n) • F(g)(x).

theorem TauCeti.dgRepresentableHomEquiv_dgDifferential (R : Type v) [CommRing R] {C : Type v} [DGCategory R C] (X : C) (F : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) Cᵒᵖ (CochainComplex (ModuleCat R) ℤ)) {n : ℤ} (η : DGHom R n { toEnrichedFunctor := dgRepresentable R X } { toEnrichedFunctor := F }) : (dgRepresentableHomEquiv R X F (n + 1)) ((dgDifferential R n) η) = (ModuleCat.Hom.hom ((F.obj (Opposite.op X)).d n (n + 1))) ((dgRepresentableHomEquiv R X F n) η)

The Yoneda bijection commutes with the differentials: the value at the identity of the differential of η is the differential of the value of η at the identity.

noncomputable def TauCeti.dgRepresentableHomIso (R : Type v) [CommRing R] {C : Type v} [DGCategory R C] (X : C) (F : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) Cᵒᵖ (CochainComplex (ModuleCat R) ℤ)) : dgHomComplex R { toEnrichedFunctor := dgRepresentable R X } { toEnrichedFunctor := F } ≅ F.obj (Opposite.op X)

The DG Yoneda lemma: evaluation at the identity of X is an isomorphism from the Hom complex of right DG modules Hom(Hom(-, X), F) to the complex F(X).

@[simp]

theorem TauCeti.dgRepresentableHomIso_hom_f_apply (R : Type v) [CommRing R] {C : Type v} [DGCategory R C] (X : C) (F : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) Cᵒᵖ (CochainComplex (ModuleCat R) ℤ)) {n : ℤ} (η : DGHom R n { toEnrichedFunctor := dgRepresentable R X } { toEnrichedFunctor := F }) : (ModuleCat.Hom.hom ((dgRepresentableHomIso R X F).hom.f n)) η = (dgRepresentableHomEquiv R X F n) η

The degree-n component of the Yoneda isomorphism is the Yoneda bijection.

theorem TauCeti.dgRepresentableHomEquiv_homEquivDGCycles (R : Type v) [CommRing R] {C : Type v} [DGCategory R C] (X : C) (F : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) Cᵒᵖ (CochainComplex (ModuleCat R) ℤ)) (α : { toEnrichedFunctor := dgRepresentable R X } ⟶ { toEnrichedFunctor := F }) : (dgRepresentableHomEquiv R X F 0) ↑((DGFunctor.homEquivDGCycles R { toEnrichedFunctor := dgRepresentable R X } { toEnrichedFunctor := F }) α) = ↑((dgYonedaEquiv X F) α)

On closed degree-zero morphisms the Yoneda bijection is the Yoneda bijection TauCeti.dgYonedaEquiv for DG natural transformations.

Full faithfulness of the Yoneda embedding

theorem TauCeti.dgRepresentableHomEquiv_dgPostcompHom (R : Type v) [CommRing R] {C : Type v} [DGCategory R C] {X X' : C} {n : ℤ} (u : DGHom R n X X') : (dgRepresentableHomEquiv R X (dgRepresentable R X') n) ((dgPostcompHom R X X' n) u) = u

The value at the identity of postcomposition with u is u.

theorem TauCeti.isIso_map_dgYoneda (R : Type v) [CommRing R] {C : Type v} [DGCategory R C] (X X' : C) : CategoryTheory.IsIso ((dgYoneda R).map X X')

The DG Yoneda embedding is fully faithful: it is an isomorphism on every Hom complex.

theorem TauCeti.isQuasiFullyFaithful_dgYoneda (R : Type v) [CommRing R] {C : Type v} [DGCategory R C] : (dgYoneda R).IsQuasiFullyFaithful

The DG Yoneda embedding is quasi-fully faithful.