Mathlib.CategoryTheory.Functor.ReflectsIso.Basic

CategoryTheory.Functor.ReflectsIsomorphisms structure

(F : C ⥤ D)

Full source

/-- 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.
-/
class Functor.ReflectsIsomorphisms (F : C ⥤ D) : Prop where
 /-- For any `f`, if `F.map f` is an iso, then so was `f`. -/
  reflects : ∀ {A B : C} (f : A ⟶ B) [IsIso (F.map f)], IsIso f

Functor that reflects isomorphisms

Informal description

A functor $ F : C \to D $ reflects isomorphisms if for any morphism $ f : A \to B $ in $ C $, whenever $ F(f) $ is an isomorphism in $ D $, then $ f $ is also an isomorphism in $ C $. This property does not require $ F $ to be faithful.

CategoryTheory.isIso_of_reflects_iso theorem

{A B : C} (f : A ⟶ B) (F : C ⥤ D) [IsIso (F.map f)] [F.ReflectsIsomorphisms] : IsIso f

Full source

/-- If `F` reflects isos and `F.map f` is an iso, then `f` is an iso. -/
theorem isIso_of_reflects_iso {A B : C} (f : A ⟶ B) (F : C ⥤ D) [IsIso (F.map f)]
    [F.ReflectsIsomorphisms] : IsIso f :=
  ReflectsIsomorphisms.reflects F f

Reflection of Isomorphisms by a Functor

Informal description

Let $F \colon C \to D$ be a functor that reflects isomorphisms, and let $f \colon A \to B$ be a morphism in $C$. If $F(f)$ is an isomorphism in $D$, then $f$ is an isomorphism in $C$.

CategoryTheory.isIso_iff_of_reflects_iso theorem

{A B : C} (f : A ⟶ B) (F : C ⥤ D) [F.ReflectsIsomorphisms] : IsIso (F.map f) ↔ IsIso f

Full source

lemma isIso_iff_of_reflects_iso {A B : C} (f : A ⟶ B) (F : C ⥤ D) [F.ReflectsIsomorphisms] :
    IsIsoIsIso (F.map f) ↔ IsIso f :=
  ⟨fun _ => isIso_of_reflects_iso f F, fun _ => inferInstance⟩

Isomorphism Reflection Criterion for Functors

Informal description

Let $F \colon C \to D$ be a functor that reflects isomorphisms, and let $f \colon A \to B$ be a morphism in $C$. Then $F(f)$ is an isomorphism in $D$ if and only if $f$ is an isomorphism in $C$.

CategoryTheory.Functor.FullyFaithful.reflectsIsomorphisms theorem

{F : C ⥤ D} (hF : F.FullyFaithful) : F.ReflectsIsomorphisms

Full source

lemma Functor.FullyFaithful.reflectsIsomorphisms {F : C ⥤ D} (hF : F.FullyFaithful) :
    F.ReflectsIsomorphisms where
  reflects _ _ := hF.isIso_of_isIso_map _

Fully Faithful Functors Reflect Isomorphisms

Informal description

Let $F \colon C \to D$ be a fully faithful functor between categories. Then $F$ reflects isomorphisms, i.e., for any morphism $f$ in $C$, if $F(f)$ is an isomorphism in $D$, then $f$ is an isomorphism in $C$.

CategoryTheory.reflectsIsomorphisms_of_full_and_faithful instance

(F : C ⥤ D) [F.Full] [F.Faithful] : F.ReflectsIsomorphisms

Full source

instance (priority := 100) reflectsIsomorphisms_of_full_and_faithful
    (F : C ⥤ D) [F.Full] [F.Faithful] :
    F.ReflectsIsomorphisms :=
  (Functor.FullyFaithful.ofFullyFaithful F).reflectsIsomorphisms

Full and Faithful Functors Reflect Isomorphisms

Informal description

For any functor $F \colon C \to D$ between categories that is both full and faithful, $F$ reflects isomorphisms. That is, if $F(f)$ is an isomorphism in $D$ for some morphism $f$ in $C$, then $f$ is an isomorphism in $C$.

CategoryTheory.reflectsIsomorphisms_comp instance

(F : C ⥤ D) (G : D ⥤ E) [F.ReflectsIsomorphisms] [G.ReflectsIsomorphisms] : (F ⋙ G).ReflectsIsomorphisms

Full source

instance reflectsIsomorphisms_comp (F : C ⥤ D) (G : D ⥤ E)
    [F.ReflectsIsomorphisms] [G.ReflectsIsomorphisms] :
    (F ⋙ G).ReflectsIsomorphisms :=
  ⟨fun f (hf : IsIso (G.map _)) => by
    haveI := isIso_of_reflects_iso (F.map f) G
    exact isIso_of_reflects_iso f F⟩

Composition of Isomorphism-Reflecting Functors Reflects Isomorphisms

Informal description

For any functors $F \colon C \to D$ and $G \colon D \to E$ that both reflect isomorphisms, their composition $F \circ G$ also reflects isomorphisms.

CategoryTheory.reflectsIsomorphisms_of_comp theorem

(F : C ⥤ D) (G : D ⥤ E) [(F ⋙ G).ReflectsIsomorphisms] : F.ReflectsIsomorphisms

Full source

lemma reflectsIsomorphisms_of_comp (F : C ⥤ D) (G : D ⥤ E)
    [(F ⋙ G).ReflectsIsomorphisms] : F.ReflectsIsomorphisms where
  reflects f _ := by
    rw [← isIso_iff_of_reflects_iso _ (F ⋙ G)]
    dsimp
    infer_instance

Reflection of Isomorphisms by Component Functor in Composition

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors between categories. If the composition $F \circ G$ reflects isomorphisms, then $F$ also reflects isomorphisms.

CategoryTheory.instReflectsIsomorphismsFunctorObjWhiskeringRight instance

(F : D ⥤ E) [F.ReflectsIsomorphisms] : ((whiskeringRight C D E).obj F).ReflectsIsomorphisms

Full source

instance (F : D ⥤ E) [F.ReflectsIsomorphisms] :
    ((whiskeringRight C D E).obj F).ReflectsIsomorphisms where
  reflects {X Y} f _ := by
    rw [NatTrans.isIso_iff_isIso_app]
    intro Z
    rw [← isIso_iff_of_reflects_iso _ F]
    change IsIso ((((whiskeringRight C D E).obj F).map f).app Z)
    infer_instance

Right Whiskering Preserves Isomorphism Reflection

Informal description

For any functor $F \colon D \to E$ that reflects isomorphisms, the right whiskering functor $(C \to D) \to (C \to E)$ obtained by post-composing with $F$ also reflects isomorphisms.