coyonedaFunctor_reflectsLimits — Mathlib

English

The coyoneda functor reflects limits: a natural transformation is an isomorphism iff its image under coyoneda is an isomorphism.

Русский

Функтор койонеда отражает пределы: естественное преобразование является изоморфизмом тогда и только тогда, когда его образ под койонедой также изоморфен.

LaTeX

$$$\\mathrm{ReflectsLimits}(\\mathrm{coyoneda})$$$

Lean4

noncomputable instance coyonedaFunctor_reflectsLimits : ReflectsLimitsOfSize.{t, w} (@coyoneda C _) :=
  inferInstance

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