category_theory.concrete_category.reflects_isomorphisms

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

A forget₂ C D forgetful functor between concrete categories C and D whose forgetful functors both reflect isomorphisms, itself reflects isomorphisms.

source

@[protected, instance]

def category_theory.forget.reflects_isomorphisms :

category_theory.reflects_isomorphisms (category_theory.forget (Type u))

source

theorem category_theory.reflects_isomorphisms_forget₂ (C : Type (u+1)) [category_theory.category C] [category_theory.concrete_category C] (D : Type (u+1)) [category_theory.category D] [category_theory.concrete_category D] [category_theory.has_forget₂ C D] [category_theory.reflects_isomorphisms (category_theory.forget C)] :

category_theory.reflects_isomorphisms (category_theory.forget₂ C D)

A forget₂ C D forgetful functor between concrete categories C and D where forget C reflects isomorphisms, itself reflects isomorphisms.