instIsCorepresentableCompEvalObjOppositeFunctorTypeCoyonedaOp

English

For every X in C and every index j, the functor (eval C c j) composed with coyoneda.obj (op X) is corepresentable; equivalently there exists a corepresenting object evalCompCoyonedaCorepresentative c X j.

Русский

Для каждого X в C и каждого индекса j композиция (eval C c j) сCoyoneda.obj (op X) ко‑репрезентируется; то есть существует ко‑репрезентируемый объект evalCompCoyonedaCorepresentative c X j.

LaTeX

$$$\big((\mathrm{eval}\,C\,c\,j) \circ (\mathrm{coyoneda}\, (\mathrm{op}\,X))\big) \text{ is corepresentable by } evalCompCoyonedaCorepresentative c X j.$$$

Lean4

instance (X : C) (j : ι) : (eval C c j ⋙ coyoneda.obj (op X)).IsCorepresentable where
  has_corepresentation := ⟨_, ⟨evalCompCoyonedaCorepresentable c X j⟩⟩

Похожие утверждения