isIso_of_yoneda_map_bijective — Mathlib

English

Let X,Y be objects of C and f: X ⟶ Y. If for every T ∈ C, the function (x: T ⟶ X) ↦ x ≫ f is bijective, then f is an isomorphism.

Русский

Пусть X,Y — объекты C и f: X ⟶ Y. Если для каждого T в C отображение (x: T ⟶ X) ↦ x ≫ f является биективным, то f является изоморфизмом.

LaTeX

$$$\forall T:\, C,\; \mathrm{Bijective}\left(\lambda x:X(T)\;\mapsto\; x\,\cdot f\right) \Rightarrow IsIso f$$$

Lean4

theorem isIso_of_yoneda_map_bijective {X Y : C} (f : X ⟶ Y)
    (hf : ∀ (T : C), Function.Bijective (fun (x : T ⟶ X) => x ≫ f)) : IsIso f :=
  by
  obtain ⟨g, hg : g ≫ f = 𝟙 Y⟩ := (hf Y).2 (𝟙 Y)
  exact ⟨g, (hf _).1 (by cat_disch), hg⟩

Похожие утверждения