A forget₂ C D
forgetful functor between concrete categories C
and D
whose forgetful functors both reflect isomorphisms, itself reflects isomorphisms.
theorem
CategoryTheory.reflectsIsomorphisms_forget₂
(C : Type (u + 1))
[CategoryTheory.Category.{u_1, u + 1} C]
[CategoryTheory.ConcreteCategory C]
(D : Type (u + 1))
[CategoryTheory.Category.{u_2, u + 1} D]
[CategoryTheory.ConcreteCategory D]
[CategoryTheory.HasForget₂ C D]
[CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget C)]
:
A forget₂ C D
forgetful functor between concrete categories C
and D
where forget C
reflects isomorphisms, itself reflects isomorphisms.