isIso_iff_coyoneda_map_bijective — Mathlib

English

For a morphism f : X ⟶ Y, IsIso f holds iff for every object T the map (Y ⟶ T) → (X ⟶ T) given by precomposition with f is bijective.

Русский

Для морфизма f: X ⟶ Y изоморфизм эквивалентен тому, что для каждого T отображение (Y ⟶ T) → (X ⟶ T) заданное предоположением по f является биективным.

LaTeX

$$$$ \text{IsIso}(f) \iff \forall T,\; \text{Bijective}(\lambda x: Y \to T,\; f \circ x) $$$$

Lean4

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

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