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.Functor.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.
For any
f, ifF.map fis an iso, then so wasf
Instances
@[deprecated CategoryTheory.Functor.ReflectsIsomorphisms]
def
CategoryTheory.ReflectsIsomorphisms
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Alias of CategoryTheory.Functor.ReflectsIsomorphisms.
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 For
theorem
CategoryTheory.isIso_of_reflects_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{A B : C}
(f : A ⟶ B)
(F : CategoryTheory.Functor C D)
[CategoryTheory.IsIso (F.map f)]
[F.ReflectsIsomorphisms]
:
If F reflects isos and F.map f is an iso, then f is an iso.
theorem
CategoryTheory.isIso_iff_of_reflects_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{A B : C}
(f : A ⟶ B)
(F : CategoryTheory.Functor C D)
[F.ReflectsIsomorphisms]
:
CategoryTheory.IsIso (F.map f) ↔ CategoryTheory.IsIso f
theorem
CategoryTheory.Functor.FullyFaithful.reflectsIsomorphisms
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
:
F.ReflectsIsomorphisms
@[instance 100]
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)
[F.Full]
[F.Faithful]
:
F.ReflectsIsomorphisms
instance
CategoryTheory.reflectsIsomorphisms_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)
[F.ReflectsIsomorphisms]
[G.ReflectsIsomorphisms]
:
(F.comp G).ReflectsIsomorphisms
theorem
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)
[(F.comp G).ReflectsIsomorphisms]
:
F.ReflectsIsomorphisms
@[instance 100]
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)
[F.ReflectsMonomorphisms]
[F.ReflectsEpimorphisms]
:
F.ReflectsIsomorphisms
instance
CategoryTheory.instReflectsIsomorphismsFunctorObjWhiskeringRight
{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 D E)
[F.ReflectsIsomorphisms]
:
((CategoryTheory.whiskeringRight C D E).obj F).ReflectsIsomorphisms
theorem
CategoryTheory.Functor.balanced_of_preserves
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.ReflectsIsomorphisms]
[F.PreservesEpimorphisms]
[F.PreservesMonomorphisms]
[CategoryTheory.Balanced D]
: