isIso_iff_yoneda_map_bijective — Mathlib

English

For f: X ⟶ Y, IsIso f iff for all T, the map (x: T ⟶ X) ↦ x ≫ f is bijective.

Русский

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

LaTeX

$$IsIso f ↔ ∀ T, Bijective (λ x : T ⟶ X, x ≫ f)$$

Lean4

theorem isIso_iff_yoneda_map_bijective {X Y : C} (f : X ⟶ Y) :
    IsIso f ↔ (∀ (T : C), Function.Bijective (fun (x : T ⟶ X) => x ≫ f)) :=
  by
  refine ⟨fun _ ↦ ?_, fun hf ↦ isIso_of_yoneda_map_bijective f hf⟩
  intro T
  rw [← isIso_iff_bijective]
  exact inferInstanceAs (IsIso ((yoneda.map f).app _))

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