English
Let G be an object of a category C. G is a codetector if and only if for every X, Y and f: X → Y, the condition that for all h: X → G there exists a unique h': Y → ? such that f ≫ h' = h holds implies that f is an isomorphism.
Русский
Пусть G — объект в категории C. G является кодетектором тогда и только тогда, когда для любых X, Y и f: X → Y условие, что для каждого h: X → G существует единственный h': Y → ? такой, что f ≫ h' = h, влечет за собой, что 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 isCodetector_def (G : C) :
IsCodetector G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : X ⟶ G, ∃! h', f ≫ h' = h) → IsIso f :=
⟨fun hG X Y f hf =>
hG _ fun H hH h => by
obtain rfl := Set.mem_singleton_iff.1 hH
exact hf h,
fun hG _ _ _ hf => hG _ fun _ => hf _ (Set.mem_singleton _) _⟩
