instIsCorepresentableCompObjOppositeTypeCoyonedaOpObjLeftAdjointObjIsDefined

English

For each object X of F, the composite F ⋙ coyoneda.obj (op X.obj) is corepresentable; i.e., there is a canonical representability by X.

Русский

Для каждого X из F, композиция F ⋙ coyoneda.obj (op X.obj) является ядром представления; существует каноническая представимость через X.

LaTeX

$$$\text{IsCorepresentable}(F \circ \mathrm{coyoneda.obj}(\mathrm{op} X))$$$

Lean4

instance (X : F.PartialLeftAdjointSource) : IsCorepresentable (F ⋙ coyoneda.obj (op X.obj)) :=
  X.property

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