English
Let G be an object. G is a codetector iff for all X,Y and f: X ⟶ Y, the property that every map from X to G factors uniquely through f (i.e., for all h: X ⟶ G there exists a unique h': Y ⟶ X with f ≫ h' = h) implies f is an isomorphism.
Русский
Пусть G — объект. G является кодетектором тогда и только тогда, когда для любых X, Y и f: X ⟶ Y свойство, что каждый отображение из X в G факторизуется через f уникальным образом, влечет за собой, что f есть изоморфизм.
LaTeX
$$$\\mathrm{IsCodetector}(G) \\iff \\forall X,Y\\; (f: X \\to Y),\\; (\\forall h: X \\to G, \\exists! h': Y \\to X,\\; f \\circ h' = h) \\to \\mathrm{IsIso}(f)$$$
Lean4
theorem «def» {G : C} : IsCodetector G → ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : X ⟶ G, ∃! h', f ≫ h' = h) → IsIso f :=
(isCodetector_def _).1
