category_theory.functor.fully_faithful

@[class]

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

Type (max u₁ v₁ v₂)

preimage : Π {X Y : C}, (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
witness' : (∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (category_theory.full.preimage f) = f) . "obviously"

A functor F : C ⥤ D is full if for each X Y : C, F.map is surjective. In fact, we use a constructive definition, so the full F typeclass contains data, specifying a particular preimage of each f : F.obj X ⟶ F.obj Y.

See https://stacks.math.columbia.edu/tag/001C.

Instances of this typeclass

Instances of other typeclasses for category_theory.full

category_theory.full.has_sizeof_inst

source

@[simp]

theorem category_theory.full.witness {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C ⥤ D} [self : category_theory.full F] {X Y : C} (f : F.obj X ⟶ F.obj Y) :

F.map (category_theory.full.preimage f) = f

source

@[class]

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

Prop

map_injective' : (∀ {X Y : C}, function.injective F.map) . "obviously"

A functor F : C ⥤ D is faithful if for each X Y : C, F.map is injective.

See https://stacks.math.columbia.edu/tag/001C.

Instances of this typeclass

source

theorem category_theory.faithful.map_injective {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [self : category_theory.faithful F] {X Y : C} :

function.injective F.map

source

theorem category_theory.functor.map_injective {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {X Y : C} (F : C ⥤ D) [category_theory.faithful F] :

function.injective F.map

source

theorem category_theory.functor.map_iso_injective {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {X Y : C} (F : C ⥤ D) [category_theory.faithful F] :

function.injective F.map_iso

source

def category_theory.functor.preimage {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {X Y : C} (F : C ⥤ D) [category_theory.full F] (f : F.obj X ⟶ F.obj Y) :

X ⟶ Y

The specified preimage of a morphism under a full functor.

Equations

F.preimage f = category_theory.full.preimage f

source

@[simp]

theorem category_theory.functor.image_preimage {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) [category_theory.full F] {X Y : C} (f : F.obj X ⟶ F.obj Y) :

F.map (F.preimage f) = f

source

theorem category_theory.functor.map_surjective {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {X Y : C} (F : C ⥤ D) [category_theory.full F] :

function.surjective F.map

source

noncomputable def category_theory.functor.full_of_exists {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (h : ∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), ∃ (p : X ⟶ Y), F.map p = f) :

category_theory.full F

Deduce that F is full from the existence of preimages, using choice.

Equations

F.full_of_exists h = (λ (_x : ∀ (X Y : C) (f : F.obj X ⟶ F.obj Y), F.map ((λ (X Y : C) (f : F.obj X ⟶ F.obj Y), classical.some _) X Y f) = f), {preimage := λ (X Y : C) (f : F.obj X ⟶ F.obj Y), classical.some _, witness' := _x}) _

source

noncomputable def category_theory.functor.full_of_surjective {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C ⥤ D) (h : ∀ (X Y : C), function.surjective F.map) :

category_theory.full F

Deduce that F is full from surjectivity of F.map, using choice.

Equations

F.full_of_surjective h = F.full_of_exists h

source

@[simp]

theorem category_theory.preimage_id {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] {X : C} :

F.preimage (𝟙 (F.obj X)) = 𝟙 X

source

@[simp]

theorem category_theory.preimage_comp {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] {X Y Z : C} (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z) :

F.preimage (f ≫ g) = F.preimage f ≫ F.preimage g

source

@[simp]

theorem category_theory.preimage_map {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] {X Y : C} (f : X ⟶ Y) :

F.preimage (F.map f) = f

source

@[simp]

theorem category_theory.functor.preimage_iso_hom {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] {X Y : C} (f : F.obj X ≅ F.obj Y) :

(F.preimage_iso f).hom = F.preimage f.hom

source

def category_theory.functor.preimage_iso {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] {X Y : C} (f : F.obj X ≅ F.obj Y) :

X ≅ Y

If F : C ⥤ D is fully faithful, every isomorphism F.obj X ≅ F.obj Y has a preimage.

Equations

F.preimage_iso f = {hom := F.preimage f.hom, inv := F.preimage f.inv, hom_inv_id' := _, inv_hom_id' := _}

source

@[simp]

theorem category_theory.functor.preimage_iso_inv {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] {X Y : C} (f : F.obj X ≅ F.obj Y) :

(F.preimage_iso f).inv = F.preimage f.inv

source

@[simp]

theorem category_theory.functor.preimage_iso_map_iso {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] {X Y : C} (f : X ≅ Y) :

F.preimage_iso (F.map_iso f) = f

source

theorem category_theory.is_iso_of_fully_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] {X Y : C} (f : X ⟶ Y) [category_theory.is_iso (F.map f)] :

category_theory.is_iso f

If the image of a morphism under a fully faithful functor in an isomorphism, then the original morphisms is also an isomorphism.

source

def category_theory.equiv_of_fully_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] {X Y : C} :

(X ⟶ Y) ≃ (F.obj X ⟶ F.obj Y)

If F is fully faithful, we have an equivalence of hom-sets X ⟶ Y and F X ⟶ F Y.

Equations

category_theory.equiv_of_fully_faithful F = {to_fun := λ (f : X ⟶ Y), F.map f, inv_fun := λ (f : F.obj X ⟶ F.obj Y), F.preimage f, left_inv := _, right_inv := _}

source

@[simp]

theorem category_theory.equiv_of_fully_faithful_symm_apply {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] {X Y : C} (f : F.obj X ⟶ F.obj Y) :

⇑((category_theory.equiv_of_fully_faithful F).symm) f = F.preimage f

source

@[simp]

theorem category_theory.equiv_of_fully_faithful_apply {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] {X Y : C} (f : X ⟶ Y) :

⇑(category_theory.equiv_of_fully_faithful F) f = F.map f

source

def category_theory.iso_equiv_of_fully_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] {X Y : C} :

(X ≅ Y) ≃ (F.obj X ≅ F.obj Y)

If F is fully faithful, we have an equivalence of iso-sets X ≅ Y and F X ≅ F Y.

Equations

category_theory.iso_equiv_of_fully_faithful F = {to_fun := λ (f : X ≅ Y), F.map_iso f, inv_fun := λ (f : F.obj X ≅ F.obj Y), F.preimage_iso f, left_inv := _, right_inv := _}

source

@[simp]

theorem category_theory.iso_equiv_of_fully_faithful_symm_apply {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] {X Y : C} (f : F.obj X ≅ F.obj Y) :

⇑((category_theory.iso_equiv_of_fully_faithful F).symm) f = F.preimage_iso f

source

@[simp]

theorem category_theory.iso_equiv_of_fully_faithful_apply {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] {X Y : C} (f : X ≅ Y) :

⇑(category_theory.iso_equiv_of_fully_faithful F) f = F.map_iso f

source

@[simp]

theorem category_theory.nat_trans_of_comp_fully_faithful_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u_1} [category_theory.category E] {F G : C ⥤ D} (H : D ⥤ E) [category_theory.full H] [category_theory.faithful H] (α : F ⋙ H ⟶ G ⋙ H) (X : C) :

(category_theory.nat_trans_of_comp_fully_faithful H α).app X = ⇑((category_theory.equiv_of_fully_faithful H).symm) (α.app X)

source

def category_theory.nat_trans_of_comp_fully_faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u_1} [category_theory.category E] {F G : C ⥤ D} (H : D ⥤ E) [category_theory.full H] [category_theory.faithful H] (α : F ⋙ H ⟶ G ⋙ H) :

F ⟶ G

We can construct a natural transformation between functors by constructing a natural transformation between those functors composed with a fully faithful functor.

Equations

category_theory.nat_trans_of_comp_fully_faithful H α = {app := λ (X : C), ⇑((category_theory.equiv_of_fully_faithful H).symm) (α.app X), naturality' := _}

source

def category_theory.nat_iso_of_comp_fully_faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u_1} [category_theory.category E] {F G : C ⥤ D} (H : D ⥤ E) [category_theory.full H] [category_theory.faithful H] (i : F ⋙ H ≅ G ⋙ H) :

F ≅ G

We can construct a natural isomorphism between functors by constructing a natural isomorphism between those functors composed with a fully faithful functor.

Equations

category_theory.nat_iso_of_comp_fully_faithful H i = category_theory.nat_iso.of_components (λ (X : C), ⇑((category_theory.iso_equiv_of_fully_faithful H).symm) (i.app X)) _

source

@[simp]

theorem category_theory.nat_iso_of_comp_fully_faithful_hom_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u_1} [category_theory.category E] {F G : C ⥤ D} (H : D ⥤ E) [category_theory.full H] [category_theory.faithful H] (i : F ⋙ H ≅ G ⋙ H) (X : C) :

(category_theory.nat_iso_of_comp_fully_faithful H i).hom.app X = H.preimage (i.hom.app X)

source

@[simp]

theorem category_theory.nat_iso_of_comp_fully_faithful_inv_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u_1} [category_theory.category E] {F G : C ⥤ D} (H : D ⥤ E) [category_theory.full H] [category_theory.faithful H] (i : F ⋙ H ≅ G ⋙ H) (X : C) :

(category_theory.nat_iso_of_comp_fully_faithful H i).inv.app X = H.preimage (i.inv.app X)

source

theorem category_theory.nat_iso_of_comp_fully_faithful_hom {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u_1} [category_theory.category E] {F G : C ⥤ D} (H : D ⥤ E) [category_theory.full H] [category_theory.faithful H] (i : F ⋙ H ≅ G ⋙ H) :

(category_theory.nat_iso_of_comp_fully_faithful H i).hom = category_theory.nat_trans_of_comp_fully_faithful H i.hom

source

theorem category_theory.nat_iso_of_comp_fully_faithful_inv {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u_1} [category_theory.category E] {F G : C ⥤ D} (H : D ⥤ E) [category_theory.full H] [category_theory.faithful H] (i : F ⋙ H ≅ G ⋙ H) :

(category_theory.nat_iso_of_comp_fully_faithful H i).inv = category_theory.nat_trans_of_comp_fully_faithful H i.inv

source

def category_theory.nat_trans.equiv_of_comp_fully_faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u_1} [category_theory.category E] {F G : C ⥤ D} (H : D ⥤ E) [category_theory.full H] [category_theory.faithful H] :

(F ⟶ G) ≃ (F ⋙ H ⟶ G ⋙ H)

Horizontal composition with a fully faithful functor induces a bijection on natural transformations.

Equations

category_theory.nat_trans.equiv_of_comp_fully_faithful H = {to_fun := λ (α : F ⟶ G), α ◫ 𝟙 H, inv_fun := category_theory.nat_trans_of_comp_fully_faithful H _inst_5, left_inv := _, right_inv := _}

source

@[simp]

theorem category_theory.nat_trans.equiv_of_comp_fully_faithful_apply {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u_1} [category_theory.category E] {F G : C ⥤ D} (H : D ⥤ E) [category_theory.full H] [category_theory.faithful H] (α : F ⟶ G) :

⇑(category_theory.nat_trans.equiv_of_comp_fully_faithful H) α = α ◫ 𝟙 H

source

@[simp]

theorem category_theory.nat_trans.equiv_of_comp_fully_faithful_symm_apply {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u_1} [category_theory.category E] {F G : C ⥤ D} (H : D ⥤ E) [category_theory.full H] [category_theory.faithful H] (α : F ⋙ H ⟶ G ⋙ H) :

⇑((category_theory.nat_trans.equiv_of_comp_fully_faithful H).symm) α = category_theory.nat_trans_of_comp_fully_faithful H α

source

def category_theory.nat_iso.equiv_of_comp_fully_faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u_1} [category_theory.category E] {F G : C ⥤ D} (H : D ⥤ E) [category_theory.full H] [category_theory.faithful H] :

(F ≅ G) ≃ (F ⋙ H ≅ G ⋙ H)

Horizontal composition with a fully faithful functor induces a bijection on natural isomorphisms.

Equations

category_theory.nat_iso.equiv_of_comp_fully_faithful H = {to_fun := λ (e : F ≅ G), category_theory.nat_iso.hcomp e (category_theory.iso.refl H), inv_fun := category_theory.nat_iso_of_comp_fully_faithful H _inst_5, left_inv := _, right_inv := _}

source

@[simp]

theorem category_theory.nat_iso.equiv_of_comp_fully_faithful_symm_apply {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u_1} [category_theory.category E] {F G : C ⥤ D} (H : D ⥤ E) [category_theory.full H] [category_theory.faithful H] (i : F ⋙ H ≅ G ⋙ H) :

⇑((category_theory.nat_iso.equiv_of_comp_fully_faithful H).symm) i = category_theory.nat_iso_of_comp_fully_faithful H i

source

@[simp]

theorem category_theory.nat_iso.equiv_of_comp_fully_faithful_apply {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u_1} [category_theory.category E] {F G : C ⥤ D} (H : D ⥤ E) [category_theory.full H] [category_theory.faithful H] (e : F ≅ G) :

⇑(category_theory.nat_iso.equiv_of_comp_fully_faithful H) e = category_theory.nat_iso.hcomp e (category_theory.iso.refl H)

source

@[protected, instance]

def category_theory.full.id {C : Type u₁} [category_theory.category C] :

category_theory.full (𝟭 C)

Equations

category_theory.full.id = {preimage := λ (_x _x_1 : C) (f : (𝟭 C).obj _x ⟶ (𝟭 C).obj _x_1), f, witness' := _}

source

@[protected, instance]

def category_theory.faithful.id {C : Type u₁} [category_theory.category C] :

category_theory.faithful (𝟭 C)

source

@[protected, instance]

def category_theory.faithful.comp {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.faithful F] [category_theory.faithful G] :

category_theory.faithful (F ⋙ G)

source

theorem category_theory.faithful.of_comp {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.faithful (F ⋙ G)] :

category_theory.faithful F

source

def category_theory.full.of_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : C ⥤ D} [category_theory.full F] (α : F ≅ F') :

category_theory.full F'

If F is full, and naturally isomorphic to some F', then F' is also full.

Equations

category_theory.full.of_iso α = {preimage := λ (X Y : C) (f : F'.obj X ⟶ F'.obj Y), F.preimage ((α.app X).hom ≫ f ≫ (α.app Y).inv), witness' := _}

source

theorem category_theory.faithful.of_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F F' : C ⥤ D} [category_theory.faithful F] (α : F ≅ F') :

category_theory.faithful F'

source

theorem category_theory.faithful.of_comp_iso {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} {H : C ⥤ E} [ℋ : category_theory.faithful H] (h : F ⋙ G ≅ H) :

category_theory.faithful F

source

theorem category_theory.iso.faithful_of_comp {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} {H : C ⥤ E} [ℋ : category_theory.faithful H] (h : F ⋙ G ≅ H) :

category_theory.faithful F

Alias of category_theory.faithful.of_comp_iso.

source

theorem category_theory.faithful.of_comp_eq {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} {H : C ⥤ E} [ℋ : category_theory.faithful H] (h : F ⋙ G = H) :

category_theory.faithful F

source

theorem eq.faithful_of_comp {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} {H : C ⥤ E} [ℋ : category_theory.faithful H] (h : F ⋙ G = H) :

category_theory.faithful F

Alias of category_theory.faithful.of_comp_eq.

source

@[protected]

def category_theory.faithful.div {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C ⥤ E) (G : D ⥤ E) [category_theory.faithful G] (obj : C → D) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X) (map : Π {X Y : C}, (X ⟶ Y) → (obj X ⟶ obj Y)) (h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) == F.map f) :

C ⥤ D

“Divide” a functor by a faithful functor.

Equations

category_theory.faithful.div F G obj h_obj map h_map = {obj := obj, map := map, map_id' := _, map_comp' := _}

source

theorem category_theory.faithful.div_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C ⥤ E) [category_theory.faithful F] (G : D ⥤ E) [category_theory.faithful G] (obj : C → D) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X) (map : Π {X Y : C}, (X ⟶ Y) → (obj X ⟶ obj Y)) (h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) == F.map f) :

category_theory.faithful.div F G obj h_obj map h_map ⋙ G = F

source

theorem category_theory.faithful.div_faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C ⥤ E) [category_theory.faithful F] (G : D ⥤ E) [category_theory.faithful G] (obj : C → D) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X) (map : Π {X Y : C}, (X ⟶ Y) → (obj X ⟶ obj Y)) (h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) == F.map f) :

category_theory.faithful (category_theory.faithful.div F G obj h_obj map h_map)

source

@[protected, instance]

def category_theory.full.comp {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.full F] [category_theory.full G] :

category_theory.full (F ⋙ G)

Equations

category_theory.full.comp F G = {preimage := λ (_x _x_1 : C) (f : (F ⋙ G).obj _x ⟶ (F ⋙ G).obj _x_1), F.preimage (G.preimage f), witness' := _}

source

def category_theory.full.of_comp_faithful {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.full (F ⋙ G)] [category_theory.faithful G] :

category_theory.full F

If F ⋙ G is full and G is faithful, then F is full.

Equations

category_theory.full.of_comp_faithful F G = {preimage := λ (X Y : C) (f : F.obj X ⟶ F.obj Y), (F ⋙ G).preimage (G.map f), witness' := _}

source

def category_theory.full.of_comp_faithful_iso {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} {H : C ⥤ E} [category_theory.full H] [category_theory.faithful G] (h : F ⋙ G ≅ H) :

category_theory.full F

If F ⋙ G is full and G is faithful, then F is full.

Equations

category_theory.full.of_comp_faithful_iso h = category_theory.full.of_comp_faithful F G

source

def category_theory.fully_faithful_cancel_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F G : C ⥤ D} (H : D ⥤ E) [category_theory.full H] [category_theory.faithful H] (comp_iso : F ⋙ H ≅ G ⋙ H) :

F ≅ G

Given a natural isomorphism between F ⋙ H and G ⋙ H for a fully faithful functor H, we can 'cancel' it to give a natural iso between F and G.

Equations

category_theory.fully_faithful_cancel_right H comp_iso = category_theory.nat_iso.of_components (λ (X : C), H.preimage_iso (comp_iso.app X)) _

source

@[simp]

theorem category_theory.fully_faithful_cancel_right_hom_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F G : C ⥤ D} {H : D ⥤ E} [category_theory.full H] [category_theory.faithful H] (comp_iso : F ⋙ H ≅ G ⋙ H) (X : C) :

(category_theory.fully_faithful_cancel_right H comp_iso).hom.app X = H.preimage (comp_iso.hom.app X)

source

@[simp]

theorem category_theory.fully_faithful_cancel_right_inv_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F G : C ⥤ D} {H : D ⥤ E} [category_theory.full H] [category_theory.faithful H] (comp_iso : F ⋙ H ≅ G ⋙ H) (X : C) :

(category_theory.fully_faithful_cancel_right H comp_iso).inv.app X = H.preimage (comp_iso.inv.app X)

mathlib3 documentation

Full and faithful functors #

Main definitions and results #