reflectsIsomorphismsOp — Mathlib

English

In the opposite context, if the source of a faithful functor is a category with a subobject classifier, the functor reflects isomorphisms.

Русский

В противоположной ситуации, если источник ответственного функтор имеет классификатор подмножества, функтор отражает изоморфизмы.

LaTeX

$$$\forall X,Y: C^{op}, f: X \to Y, IsIso(F.map\,f) \Rightarrow IsIso(f)$$$

Lean4

/-- If the source of a faithful functor is the opposite category of one with a subobject classifier,
  the same holds -- the functor reflects isomorphisms.
-/
instance reflectsIsomorphismsOp (D : Type u₀) [Category.{v₀} D] (F : Cᵒᵖ ⥤ D) [Functor.Faithful F] :
    Functor.ReflectsIsomorphisms F :=
  reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms F

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