English
Let G be an object of a category C. G is a detector if and only if for every pair of objects X, Y and every morphism f: X → Y, the condition that for every morphism h: G → Y there exists a unique h': G → X with h' ∘ f = h implies that f is an isomorphism.
Русский
Пусть G — объект в категории C. G является детектором тогда и только тогда, когда для любых объектов X, Y и любого морфизма f: X → Y условие: для каждого морфизма h: G → Y существует единственный h': G → X такой, что h' ∘ f = h, влечет за собой, что f является изоморфизмом.
LaTeX
$$$\\mathrm{IsDetector}(G) \\iff \\forall X,Y\\; (f: X \\to Y),\\;\\big(\\forall h: G \\to Y, \\exists! h': G \\to X,\\; h' \\circ f = h\\big) \\to \\mathrm{IsIso}(f)$$$
Lean4
theorem isDetector_def (G : C) : IsDetector G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : G ⟶ Y, ∃! h', h' ≫ f = 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 _) _⟩
