mathlib3 documentation


Functors which reflect isomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

It is formalized as a Prop valued typeclass reflects_isomorphisms F.

Any fully faithful functor reflects isomorphisms.

structure category_theory.reflects_isomorphisms {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) :

Define what it means for a functor F : C ⥤ D to reflect isomorphisms: for any morphism f : A ⟶ B, if f is an isomorphism then f is as well. Note that we do not assume or require that F is faithful.

Instances of this typeclass

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