isIso_iff_bijective — Mathlib

English

If the forgetful functor reflects isomorphisms, then IsIso f iff the underlying map is bijective.

Русский

Если забывающий функтор отражает изоморфизмы, то IsIso f эквивалентно биективности базовой функции.

LaTeX

$$$\\text{IsIso}(f) \\iff \\text{Bijective}((\\mathrm{forget}\\,C).map f)$$$

Lean4

/-- If the forgetful functor of a concrete category reflects isomorphisms, being an isomorphism
is equivalent to being bijective. -/
theorem isIso_iff_bijective [(forget C).ReflectsIsomorphisms] {X Y : C} (f : X ⟶ Y) : IsIso f ↔ Function.Bijective f :=
  by
  rw [← CategoryTheory.isIso_iff_bijective]
  exact ⟨fun _ ↦ inferInstance, fun _ ↦ isIso_of_reflects_iso f (forget C)⟩

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