A forget₂ C D forgetful functor between concrete categories C and D
whose forgetful functors both reflect isomorphisms, itself reflects isomorphisms.
@[instance]
Equations
- category_theory.forget.category_theory.reflects_isomorphisms = {reflects := λ (X Y : Type u) (f : X ⟶ Y) (i : category_theory.is_iso ((category_theory.forget (Type u)).map f)), i}
@[instance]
def
category_theory.forget₂.category_theory.reflects_isomorphisms
(C : Type (u+1))
[category_theory.large_category C]
[category_theory.concrete_category C]
(D : Type (u+1))
[category_theory.large_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.
Equations
- category_theory.forget₂.category_theory.reflects_isomorphisms C D = {reflects := λ (X Y : C) (f : X ⟶ Y) (i : category_theory.is_iso ((category_theory.forget₂ C D).map f)), category_theory.is_iso_of_reflects_iso f (category_theory.forget C)}