isDetecting — Mathlib

English

The functor freeYoneda is detecting, meaning that if a morphism becomes an isomorphism after applying freeYoneda to all components, then the original morphism is an isomorphism.

Русский

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

LaTeX

$$$\\text{IsDetecting}(\\mathrm{freeYoneda} R)$$$

Lean4

theorem isDetecting : IsDetecting (freeYoneda R) :=
  (isSeparating R).isDetecting

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