reflectsIsomorphisms — Mathlib

English

If the source of a faithful functor has a subobject classifier, the functor reflects isomorphisms. This holds in particular for balanced categories.

Русский

Если область определения точного функторы имеет классификатор подмножества, функтор отражает изоморфизмы. Это верно и для сбалансированных категорий.

LaTeX

$$$\forall X,Y: C, f: X \to Y,\; IsIso(F.map\,f) \Rightarrow IsIso(f)$$$

Lean4

/-- If the source of a faithful functor has a subobject classifier, the functor reflects
  isomorphisms. This holds for any balanced category.
-/
instance reflectsIsomorphisms (D : Type u₀) [Category.{v₀} D] (F : C ⥤ D) [Functor.Faithful F] :
    Functor.ReflectsIsomorphisms F :=
  reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms F

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