A forget₂ C D
forgetful functor between concrete categories C
and D
whose forgetful functors both reflect isomorphisms, itself reflects isomorphisms.
@[instance]
@[instance]
def
category_theory.forget₂.category_theory.reflects_isomorphisms
(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)] :
A forget₂ C D
forgetful functor between concrete categories C
and D
where forget C
reflects isomorphisms, itself reflects isomorphisms.