mathlib docs: category_theory.reflects

@[class]

structure category_theory.reflects_isomorphisms {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) :

Type (max u₁ v₁ v₂)

reflects : Π {A B : C} (f : A ⟶ B) [_inst_3 : 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

source

def 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] :

category_theory.is_iso f

If F reflects isos and F.map f is an iso, then f is an iso.

Equations

category_theory.is_iso_of_reflects_iso f F = category_theory.reflects_isomorphisms.reflects F f

source

@[instance]

def category_theory.category_theory.reflects_isomorphisms {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] :

category_theory.reflects_isomorphisms F

Equations

category_theory.category_theory.reflects_isomorphisms F = {reflects := λ (X Y : C) (f : X ⟶ Y) (i : category_theory.is_iso (F.map f)), {inv := F.preimage (category_theory.is_iso.inv (F.map f)), hom_inv_id' := _, inv_hom_id' := _}}