English
Given a chain complex X and an object Y, this constructs a cochain complex of modules of maps X.X_i → Y.
Русский
Пусть X — цепной комплекс и Y — объект; строится коцепный комплекс модулей из морфизмов X_i → Y.
LaTeX
$$$\\text{linearYonedaObj}(X,Y) := \\text{cochain complex with } (X_i \\to Y)\\text{ as morphisms}$$$
Lean4
/-- Given a chain complex `X` and an object `Y`, this is the cochain complex
which in degree `i` consists of the module of morphisms `X.X i ⟶ Y`. -/
@[simps! X d]
def linearYonedaObj {α : Type*} [AddRightCancelSemigroup α] [One α] (X : ChainComplex C α) (A : Type*) [Ring A]
[Linear A C] (Y : C) : CochainComplex (ModuleCat A) α :=
((((linearYoneda A C).obj Y).rightOp.mapHomologicalComplex _).obj X).unop
