English
Let C be a category with zero morphisms and a zero object, and let c be a complex shape with no loop. For any object X in C and any index j, the functor that sends a complex K to the morphisms X ⟶ K.X_j is corepresentable by a canonical object, namely evalCompCoyonedaCorepresentative c X j.
Русский
Пусть C — категория с нулевыми морфизмами и нулевым объектом, и пусть c — форму комплекса без петель. Для любого объекта X в C и любого индекса j функция, отправляющая комплекс K в множество морфизмов X ⟶ K.X_j, является ко-репрезентируемой объектом evalCompCoyonedaCorepresentative c X j.
LaTeX
$$$(\mathrm{eval}\,C\,c\,j) \circ \mathrm{coyoneda}(\mathrm{op}\,X) \text{ is corepresentable by } \mathrm{evalCompCoyonedaCorepresentative}\,c\,X\,j.$$$
Lean4
/-- If a complex shape `c : ComplexShape ι` has no loop,
then for any `X : C` and `j : ι`, the functor which sends `K : HomologicalComplex C c`
to `X ⟶ K.X j` is corepresentable. -/
noncomputable def evalCompCoyonedaCorepresentable (X : C) (j : ι) :
(eval C c j ⋙ coyoneda.obj (op X)).CorepresentableBy (evalCompCoyonedaCorepresentative c X j) :=
by
dsimp [evalCompCoyonedaCorepresentative]
classical
split_ifs with h
· exact evalCompCoyonedaCorepresentableByDoubleId _ (fun hj ↦ c.not_rel_of_eq hj h.choose_spec) _
· apply evalCompCoyonedaCorepresentableBySingle
obtain _ | _ := c.exists_distinct_prev_or j <;> tauto
