mathlib documentation

category_theory.reflects_isomorphisms

Functors which reflect isomorphisms #

A functor F reflects isomorphisms if whenever F.map f is an isomorphism, f was too.

It is formalized as a Prop valued typeclass reflects_isomorphisms F.

Any fully faithful functor reflects isomorphisms.

If F reflects isos and F.map f is an iso, then f is an iso.