English
Let 𝒢 be a set of objects in the opposite category C^op. The collection 𝒢 unop in C detects isomorphisms if and only if 𝒢 is codetecting in C^op. Equivalently, detection after applying the unop operation corresponds to codetection in the original opposite category.
Русский
Пусть 𝒢 — множество объектов в противоположной категории C^op. Тогда 𝒢 вверх оболочкой в C распознаёт изоморфизмы тогда и только если 𝒢 является кододетектирующим в C^op. Иными словами, обнаружение после применения операции unop эквивалентно кододетектированию в исходной противоположной категории.
LaTeX
$$$IsDetecting\big(\mathcal{G}^{\mathrm{unop}}\big) \;\Longleftrightarrow\; IsCodetecting(\mathcal{G})$$$
Lean4
theorem isDetecting_unop_iff (𝒢 : Set Cᵒᵖ) : IsDetecting 𝒢.unop ↔ IsCodetecting 𝒢 := by
rw [← isCodetecting_op_iff, Set.unop_op]
