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.map f is an isomorphism, f was too.
It is formalized as a Prop valued typeclass reflects_isomorphisms F.
Any fully faithful functor reflects isomorphisms.
@[class]
structure
category_theory.reflects_isomorphisms
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
Prop
- reflects : ∀ {A B : C} (f : A ⟶ B) [_inst_4 : category_theory.is_iso (F.map f)], category_theory.is_iso f
Define what it means for a functor F : C ⥤ D to reflect isomorphisms: for any
morphism f : A ⟶ B, if F.map 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
- category_theory.of_full_and_faithful
- category_theory.reflects_isomorphisms_of_reflects_monomorphisms_of_reflects_epimorphisms
- category_theory.functor.comp.reflects_isomorphisms
- category_theory.limits.cones.reflects_cone_isomorphism
- category_theory.limits.cocones.reflects_cocone_isomorphism
- category_theory.structured_arrow.proj_reflects_iso
- category_theory.costructured_arrow.proj_reflects_iso
- category_theory.over.forget_reflects_iso
- category_theory.under.forget_reflects_iso
- Mon.forget_reflects_isos
- AddMon.forget_reflects_isos
- CommMon.forget_reflects_isos
- AddCommMon.forget_reflects_isos
- Group.forget_reflects_isos
- AddGroup.forget_reflects_isos
- CommGroup.forget_reflects_isos
- AddCommGroup.forget_reflects_isos
- category_theory.forget.reflects_isomorphisms
- Ring.forget_reflects_isos
- CommRing.forget_reflects_isos
- Algebra.forget_reflects_isos
theorem
category_theory.is_iso_of_reflects_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{A B : C}
(f : A ⟶ B)
(F : C ⥤ D)
[category_theory.is_iso (F.map f)]
[category_theory.reflects_isomorphisms F] :
If F reflects isos and F.map f is an iso, then f is an iso.
@[protected, instance]
def
category_theory.of_full_and_faithful
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.full F]
[category_theory.faithful F] :
@[protected, instance]
def
category_theory.functor.comp.reflects_isomorphisms
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[category_theory.reflects_isomorphisms F]
[category_theory.reflects_isomorphisms G] :
@[protected, instance]
def
category_theory.reflects_isomorphisms_of_reflects_monomorphisms_of_reflects_epimorphisms
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.balanced C]
(F : C ⥤ D)
[F.reflects_monomorphisms]
[F.reflects_epimorphisms] :