Functors which reflect isomorphisms #
A functor F reflects isomorphisms if whenever F.map f is an isomorphism, f was too.
It is formalized as a Prop valued typeclass ReflectsIsomorphisms F.
Any fully faithful functor reflects isomorphisms.
class
CategoryTheory.ReflectsIsomorphisms
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
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.
- reflects : ∀ {A B : C} (f : A ⟶ B) [inst : CategoryTheory.IsIso (F.map f)], CategoryTheory.IsIso f
For any
f, ifF.map fis an iso, then so wasf
Instances
theorem
CategoryTheory.isIso_of_reflects_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{A : C}
{B : C}
(f : A ⟶ B)
(F : CategoryTheory.Functor C D)
[CategoryTheory.IsIso (F.map f)]
[CategoryTheory.ReflectsIsomorphisms F]
:
If F reflects isos and F.map f is an iso, then f is an iso.
instance
CategoryTheory.reflectsIsomorphisms_of_full_and_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Full F]
[CategoryTheory.Faithful F]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.reflectsIsomorphisms_of_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.ReflectsIsomorphisms F]
[CategoryTheory.ReflectsIsomorphisms G]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Balanced C]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.ReflectsMonomorphisms F]
[CategoryTheory.Functor.ReflectsEpimorphisms F]
:
Equations
- ⋯ = ⋯