English
If for every T ∈ C the map x ↦ f ≫ x from Y ⟶ T to X ⟶ T is bijective, then f is an isomorphism. Equivalently, f is an isomorphism iff the family of maps given by postcomposition with f is bijective on all targets.
Русский
Если для каждого T ∈ C отображение x ↦ f ≫ x: Y ⟶ T → X ⟶ T является биективным, то f является изоморфизмом. Эквивалентно: f изоморфизм тогда и только тогда, когда семейство отображений по постпроекции через f биективно на всех мишенях.
LaTeX
$$$$ \text{If } \forall T,\; (Y ⟶ T) \to (X ⟶ T) \text{ via } x \mapsto f \circ x \text{ is bijective, then } f \text{ is an isomorphism}. $$$$
Lean4
theorem isIso_of_coyoneda_map_bijective {X Y : C} (f : X ⟶ Y)
(hf : ∀ (T : C), Function.Bijective (fun (x : Y ⟶ T) => f ≫ x)) : IsIso f :=
by
obtain ⟨g, hg : f ≫ g = 𝟙 X⟩ := (hf X).2 (𝟙 X)
refine ⟨g, hg, (hf _).1 ?_⟩
simp only [Category.comp_id, ← Category.assoc, hg, Category.id_comp]
