The free rank-one right module, the differential graded Yoneda lemma and embedding #

A differential graded algebra A is a differential graded right module over itself — this is TauCeti.IsDGAlgebra.isDGRightModule, the free rank-one right module, the module represented by the unique object of the one-object differential graded category attached to A.

The Yoneda lemma identifies the cochains out of it with the module itself. A right-module map A ⟶ M is determined by the image of 1; an element x of degree p produces the map a ↦ x * a; and the two constructions are mutually inverse and linear over the ground ring. Evaluation at 1 moreover commutes with the differentials on the nose, because d 1 = 0 kills the second term of the graded commutator d_M ∘ f - (-1)^p f ∘ d_A. So the Hom complex out of the free rank-one module is the underlying cochain complex of M, and in particular a morphism of differential graded right modules A ⟶ M is the same thing as a degree-zero cycle of M.

Taking M = A, the inverse of evaluation at 1 sends a to left multiplication by a, and these maps assemble into the differential graded Yoneda embedding of the one-object differential graded category TauCeti.DGSingleObj h into the differential graded category of right modules: its unique object goes to the free rank-one module, and a morphism a goes to the right-module cochain x ↦ a * x. Left multiplication commutes with the differentials by the Leibniz rule, and it preserves composition because both categories put the same Koszul sign (-1) ^ (p * q) between Mathlib's enriched factor order and Keller's composition order. The embedding is an isomorphism on every Hom complex, so in particular it is quasi-fully faithful.

Main definitions #

TauCeti.dgYonedaCochainEquiv: evaluation at 1, as a linear equivalence between the degree-p right-module cochains out of the free rank-one module and the degree-p part of M.
TauCeti.dgYonedaHomEquiv: morphisms of differential graded right modules out of the free rank-one module are the degree-zero cycles of M.
TauCeti.dgYonedaIso: the degreewise identification as an isomorphism of cochain complexes.
TauCeti.dgYonedaEmbedding: the differential graded Yoneda embedding of the one-object differential graded category of A into differential graded right modules.
TauCeti.dgYonedaEmbeddingHomEquiv: its action on morphisms of a fixed degree, a linear equivalence.

Main results #

TauCeti.dgYonedaEmbeddingHomEquiv_apply: a morphism a acts on the free rank-one module by left multiplication.
TauCeti.isIso_map_dgYonedaEmbedding: the Yoneda embedding is an isomorphism on Hom complexes.
TauCeti.isQuasiFullyFaithful_dgYonedaEmbedding: the Yoneda embedding is quasi-fully faithful.

Implementation notes #

The Hom complex out of the free rank-one module has its terms in the universe of A →ₗ[Aᵐᵒᵖ] M, while the underlying complex of M has its terms in the universe of M; an isomorphism between them therefore needs the universe of A to be at most that of M. This is what M : Type (max uA uM) expresses in TauCeti.dgYonedaIso, and it is the widest hypothesis under which the two complexes are objects of a single category without inserting ULift. The degreewise statements carry no universe constraint at all.

References #

B. Keller, Deriving DG categories, Sections 1 and 2.
B. Keller, Introduction to A-infinity algebras and modules, Sections 3.1 and 4.1.